Merge pull request #33 from well-typed/jdral/tweak-variable-context-helpers

Tweak variable context helpers

Author: jorisdral

CHANGELOG.md

@@ -2,6 +2,15 @@
 
 ## ?.?.? -- ????-??-??
 
+* BREAKING: Rename `lookupGVar` to `realLookupVar`, and add a `RealLookup`
+  convenience alias that is used in the type of `RealLookupVar`. The type of
+  `realLookupVar` is slightly different than the type of `lookupGVar`, but only
+  in the positions of universal quantification over types.
+* NON-BREAKING: improved error messages for `realLookupVar` and `lookupVar`,
+  which might throw an error when variables are ill-defined or unevaluable.
+* PATCH: some documentation is moved from convenience aliases like
+  `ModelFindVariables` to the functions have these aliases in their type, like
+  `findVars`.
 * BREAKING: Enable verbose counterexamples by default in the 'postcondition'
   function using 'postconditionWith'.
 * NON-BREAKING: Add a new 'postconditionWith' function that can be configured to

src/Test/QuickCheck/StateModel/Lockstep.hs

@@ -22,16 +22,17 @@ module Test.QuickCheck.StateModel.Lockstep (
   , ModelLookUp
   , ModelShrinkVar
   , ModelVar
+  , RealLookUp
     -- * Variable context
   , ModelVarContext
   , lookupVar
   , findVars
   , shrinkVar
+  , realLookupVar
     -- * Variables
   , GVar -- opaque
   , AnyGVar(..)
   , unsafeMkGVar
-  , lookUpGVar
   , mapGVar
     -- ** Operations
   , Operation(..)

src/Test/QuickCheck/StateModel/Lockstep/API.hs

@@ -16,19 +16,21 @@ module Test.QuickCheck.StateModel.Lockstep.API (
   , ModelLookUp
   , ModelVar
   , ModelShrinkVar
+  , RealLookUp
     -- * Variable context
   , ModelVarContext
   , findVars
   , lookupVar
   , shrinkVar
+  , realLookupVar
   ) where
 
 import Data.Constraint (Dict(..))
 import Data.Kind
 import Data.Typeable
 
 import Test.QuickCheck (Gen)
-import Test.QuickCheck.StateModel (StateModel, Any, RunModel, Realized, Action)
+import Test.QuickCheck.StateModel (StateModel, Any, RunModel, Realized, Action, LookUp)
 
 import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)
 import Test.QuickCheck.StateModel.Lockstep.GVar (GVar, AnyGVar(..), fromVar)
@@ -181,21 +183,19 @@ class ( InLockstep state
 -- | An action in the lock-step model
 type LockstepAction state = Action (Lockstep state)
 
--- | Look up a variable for model execution
---
--- The type of the variable is the type in the /real/ system.
+-- | See 'lookupVar'.
 type ModelLookUp state = forall a. ModelVar state a -> ModelValue state a
 
--- | Find variables of the appropriate type
---
--- The type you pass must be the result type of (previously executed) actions.
--- If you want to change the type of the variable, see 'EnvF.mapGVar'.
+-- | See 'findVars'.
 type ModelFindVariables state = forall a.
           Typeable a
        => Proxy a -> [GVar (ModelOp state) a]
 
--- | Shrink variables to /earlier/ variables of the same type.
-type ModelShrinkVar state a = ModelVar state a -> [ModelVar state a]
+-- | See 'shrinkVar'.
+type ModelShrinkVar state = forall a. ModelVar state a -> [ModelVar state a]
+
+-- | See 'realLookupVar'.
+type RealLookUp m op = forall a. Proxy m -> LookUp m -> GVar op a -> Realized m a
 
 -- | Variables with a "functor-esque" instance
 type ModelVar state = GVar (ModelOp state)
@@ -207,24 +207,45 @@ type ModelVar state = GVar (ModelOp state)
 -- | The environment of known variables and their (model) values.
 --
 -- This environment can be queried for information about known variables through
--- 'findVars' and 'lookupVar'. This environment is updated automically by the
--- lockstep framework.
+-- 'findVars', 'lookupVar', and 'shrinkVar'. This environment is updated
+-- automically by the lockstep framework.
 type ModelVarContext state = EnvF (ModelValue state)
 
--- | See 'ModelFindVariables'.
+-- | Find variables of the appropriate type
+--
+-- The type you pass must be the result type of (previously executed) actions.
+-- If you want to change the type of the variable, see 'EnvF.mapGVar'.
 findVars ::
      InLockstep state
   => ModelVarContext state -> ModelFindVariables state
 findVars env _ = map fromVar $ EnvF.keysOfType env
 
--- | See 'ModelLookUp'.
+-- | Look up a variable for execution of the model.
+--
+-- The type of the variable is the type in the /real/ system.
 lookupVar ::
      InLockstep state
   => ModelVarContext state -> ModelLookUp state
-lookupVar env = EnvF.lookUpEnvF env
+lookupVar env gvar = case EnvF.lookUpEnvF env gvar of
+    Just x -> x
+    Nothing -> error
+      "lookupVar: the variable (ModelVar) must be well-defined and evaluable, \
+      \but this requirement was violated. Normally, this is guaranteed by the \
+      \default test 'precondition'."
 
--- | See 'ModelShrinkVar'.
+-- | Shrink variables to /earlier/ variables of the same type.
 shrinkVar ::
      (Typeable state, InterpretOp (ModelOp state) (ModelValue state))
-  => ModelVarContext state -> ModelShrinkVar state a
-shrinkVar env var = EnvF.shrinkGVar env var
+  => ModelVarContext state -> ModelShrinkVar state
+shrinkVar env var = EnvF.shrinkGVar env var
+
+-- | Look up a variable for execution of the real system.
+--
+-- The type of the variable is the type in the /real/ system.
+realLookupVar :: InterpretOp op (WrapRealized m) => RealLookUp m op
+realLookupVar p lookUp gvar = case EnvF.lookUpGVar p lookUp gvar of
+    Just x -> x
+    Nothing -> error
+      "realLookupVar: the variable (GVar) must be well-defined and evaluable, \
+      \but this requirement was violated. Normally, this is guaranteed by the \
+      \default test 'precondition'."

src/Test/QuickCheck/StateModel/Lockstep/GVar.hs

@@ -23,7 +23,7 @@ module Test.QuickCheck.StateModel.Lockstep.GVar (
 
 import Prelude hiding (map)
 
-import Data.Maybe (isJust, fromJust)
+import Data.Maybe (isJust)
 import Data.Typeable
 
 import GHC.Show
@@ -96,30 +96,29 @@ lookUpWrapped _ m v = WrapRealized (m v)
 
 -- | Lookup 'GVar' given a lookup function for 'Var'
 --
--- The variable must be in the environment and evaluation must succeed.
--- This is normally guaranteed by the default test 'precondition'.
+-- The result is 'Just' if the variable is in the environment and evaluation
+-- succeeds. This is normally guaranteed by the default test 'precondition'.
 lookUpGVar ::
      InterpretOp op (WrapRealized m)
-  => Proxy m -> LookUp m -> GVar op a -> Realized m a
+  => Proxy m -> LookUp m -> GVar op a -> Maybe (Realized m a)
 lookUpGVar p lookUp (GVar var op) =
-    unwrapRealized $ fromJust $ intOp op (lookUpWrapped p lookUp var)
+    unwrapRealized <$> intOp op (lookUpWrapped p lookUp var)
 
 {-------------------------------------------------------------------------------
   Interop with EnvF
 -------------------------------------------------------------------------------}
 
 -- | Lookup 'GVar'
 --
--- The variable must be in the environment and evaluation must succeed.
--- This is normally guaranteed by the default test 'precondition'.
-lookUpEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> f a
-lookUpEnvF env (GVar var op) = fromJust $
+-- The result is 'Just' if the variable is in the environment and evaluation
+-- succeeds. This is normally guaranteed by the default test 'precondition'.
+lookUpEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> Maybe (f a)
+lookUpEnvF env (GVar var op) =
     EnvF.lookup var env >>= intOp op
 
 -- | Check if the variable is well-defined and evaluation will succeed.
 definedInEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> Bool
-definedInEnvF env (GVar var op) = isJust $
-    EnvF.lookup var env >>= intOp op
+definedInEnvF env gvar = isJust (lookUpEnvF env gvar)
 
 -- | Shrink a 'GVar' to earlier 'GVar's of the same type. It is guaranteed that
 -- the shrunk variables are in the environment and that evaluation will succeed.

test/Test/IORef/Full.hs

@@ -208,11 +208,11 @@ runIO action lookUp = ReaderT $ \(buggy, brokenRef) ->
       Read  v   -> readIORef (lookUpRef v)
   where
     lookUpRef :: ModelVar M (IORef Int) -> IORef Int
-    lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp
+    lookUpRef = realLookupVar (Proxy @RealMonad) lookUp
 
     lookUpInt :: Either Int (ModelVar M Int) -> Int
     lookUpInt (Left  x) = x
-    lookUpInt (Right v) = lookUpGVar (Proxy @RealMonad) lookUp v
+    lookUpInt (Right v) = realLookupVar (Proxy @RealMonad) lookUp v
 
 -- | The second write to the same variable will be broken
 brokenWrite :: Buggy -> IORef BrokenRef -> IORef Int -> Int -> IO Int

test/Test/IORef/Simple.hs

@@ -155,7 +155,7 @@ runIO action lookUp =
       Read  v   -> readIORef (lookUpRef v)
   where
     lookUpRef :: ModelVar M (IORef Int) -> IORef Int
-    lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp
+    lookUpRef = realLookupVar (Proxy @RealMonad) lookUp
 
 runModel ::
      Action (Lockstep M) a

test/Test/MockFS.hs

@@ -351,7 +351,7 @@ runIO action lookUp = ReaderT $ \root -> aux root action
             _                     -> pure s
       where
         lookUp' :: FsVar x -> x
-        lookUp' = lookUpGVar (Proxy @RealMonad) lookUp
+        lookUp' = realLookupVar (Proxy @RealMonad) lookUp
 
 catchErr :: forall a. IO a -> IO (Either Err a)
 catchErr act = catch (Right <$> act) handler