{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}

-- | Type-indexed runtime-checked properties.
module Data.Checked
  ( Checked
  , trustMe
  , trustThat
  , trustMap
  , checked
  , Property(..)
  , maybeHolds
  , check
  ) where

import Data.Typeable (Typeable)
import Control.DeepSeq (NFData(..))

-- | Wrapper-evidence for property /p/.
newtype Checked p v = Checked v deriving Typeable

instance NFData v ⇒ NFData (Checked p v) where
  rnf :: Checked p v -> ()
rnf (Checked v
v) = v -> ()
forall a. NFData a => a -> ()
rnf v
v

-- | Use when the property can be deduced without a runtime check.
trustMe ∷ v → Checked p v
trustMe :: forall v p. v -> Checked p v
trustMe = v -> Checked p v
forall p v. v -> Checked p v
Checked
{-# INLINE trustMe #-}

-- | Use when the property can be deduced without a runtime check.
trustThat ∷ p → v → Checked p v
trustThat :: forall p v. p -> v -> Checked p v
trustThat p
_ = v -> Checked p v
forall p v. v -> Checked p v
Checked
{-# INLINE trustThat #-}

-- | Apply a fuction that preserves the property to the checked value.
trustMap ∷ (v → v) → Checked p v → Checked p v
trustMap :: forall v p. (v -> v) -> Checked p v -> Checked p v
trustMap v -> v
f (Checked v
v) = v -> Checked p v
forall p v. v -> Checked p v
Checked (v -> v
f v
v)
{-# INLINE trustMap #-}

-- | Unwrap the checked value.
checked ∷ Checked p v → v
checked :: forall p v. Checked p v -> v
checked (Checked v
v) = v
v
{-# INLINE checked #-}

class Property p v where
  -- | Test if the property holds for the given value.
  --   The first argument is supposed to be ignored.
  holds ∷ p → v → Bool

-- | Return 'Just' /v/ if /p/ holds and 'Nothing' overwise.
maybeHolds ∷ Property p v ⇒ p → v → Maybe v
maybeHolds :: forall p v. Property p v => p -> v -> Maybe v
maybeHolds p
p v
v | p -> v -> Bool
forall p v. Property p v => p -> v -> Bool
holds p
p v
v = v -> Maybe v
forall a. a -> Maybe a
Just v
v
               | Bool
otherwise = Maybe v
forall a. Maybe a
Nothing
{-# INLINABLE maybeHolds #-}

-- | Wrap the value if the property holds.
check ∷ ∀ p v . Property p v ⇒ v → Maybe (Checked p v)
check :: forall p v. Property p v => v -> Maybe (Checked p v)
check v
v | p -> v -> Bool
forall p v. Property p v => p -> v -> Bool
holds (p
forall a. HasCallStack => a
undefined ∷ p) v
v = Checked p v -> Maybe (Checked p v)
forall a. a -> Maybe a
Just (v -> Checked p v
forall p v. v -> Checked p v
Checked v
v)
        | Bool
otherwise               = Maybe (Checked p v)
forall a. Maybe a
Nothing
{-# INLINABLE check #-}