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

-- | A version of 'DC.Checked' that requires client code to provide
--   a non-bottom value of the property index type to use @trust*@
--   functions.
module Data.Checked.Strict
  ( Checked
  , trustThat
  , trustMap
  , checked
  , Property(..)
  , maybeHolds
  , check
  , relax
  ) where

import Data.Typeable (Typeable)
import Control.DeepSeq (NFData(..))
import Data.Checked (Property(..), maybeHolds)
import qualified Data.Checked as DC

-- | 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.
--   Note that /p/ is evaluated to WHNF, so you can't use 'undefined'.
trustThat ∷ p → v → Checked p v
trustThat :: p -> v -> Checked p v
trustThat p
p v
v = p
p p -> Checked p v -> Checked p v
`seq` v -> Checked p v
forall p v. v -> Checked p v
Checked v
v
{-# INLINE trustThat #-}

-- | Apply a fuction that preserves the property to the checked value.
--   Note that /p/ is evaluated to WHNF, so you can't use 'undefined'.
trustMap ∷ p → (v → v) → Checked p v → Checked p v
trustMap :: p -> (v -> v) -> Checked p v -> Checked p v
trustMap p
p v -> v
f (Checked v
v) = p
p p -> Checked p v -> Checked p v
`seq` 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 :: Checked p v -> v
checked (Checked v
v) = v
v
{-# INLINE checked #-}

-- | Wrap the value if the property holds.
check ∷ ∀ p v . Property p v ⇒ v → Maybe (Checked p v)
check :: 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 #-}

-- | Rewrap a value into the less strict 'DC.Checked' type.
relax ∷ Checked p v → DC.Checked p v
relax :: Checked p v -> Checked p v
relax (Checked v
v) = v -> Checked p v
forall v p. v -> Checked p v
DC.trustMe v
v
{-# INLINE relax #-}