packages feed

quickcheck-lockstep (empty) → 0.1.0

raw patch · 16 files changed

+1625/−0 lines, 16 filesdep +QuickCheckdep +basedep +containers

Dependencies added: QuickCheck, base, containers, directory, filepath, mtl, quickcheck-dynamic, quickcheck-lockstep, tasty, tasty-hunit, tasty-quickcheck, temporary

Files

+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for quickcheck-lockstep++## 0.1.0 -- 2022-10-11++* First release
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2022, Edsko de Vries++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Edsko de Vries nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ quickcheck-lockstep.cabal view
@@ -0,0 +1,97 @@+cabal-version:      2.4+name:               quickcheck-lockstep+version:            0.1.0+license:            BSD-3-Clause+license-file:       LICENSE+author:             Edsko de Vries+maintainer:         edsko@well-typed.com+extra-source-files: CHANGELOG.md+category:           Testing+synopsis:           Library for lockstep-style testing with 'quickcheck-dynamic'+description:        Lockstep-style testing is a particular approach for blackbox+                    testing of stateful APIs: we generate a random sequence of+                    APIs calls, then execute them both against the system under+                    test and against a model, and compare responses up to some+                    notion of observability.++source-repository head+  type:     git+  location: https://github.com/well-typed/quickcheck-lockstep++common lang+  default-language:+      Haskell2010+  default-extensions:+      FlexibleContexts+      FlexibleInstances+      GADTs+      ImportQualifiedPost+      LambdaCase+      MultiParamTypeClasses+      QuantifiedConstraints+      RankNTypes+      ScopedTypeVariables+      StandaloneDeriving+      TypeApplications+      TypeFamilies+  other-extensions:+      UndecidableInstances+  ghc-options:+      -Wall+      -Wprepositive-qualified-module+      -Wredundant-constraints++library+  import:+      lang+  exposed-modules:+      Test.QuickCheck.StateModel.Lockstep+      Test.QuickCheck.StateModel.Lockstep.Defaults+      Test.QuickCheck.StateModel.Lockstep.Op.Identity+      Test.QuickCheck.StateModel.Lockstep.Op.SumProd+      Test.QuickCheck.StateModel.Lockstep.Run+  other-modules:+      Test.QuickCheck.StateModel.Lockstep.API+      Test.QuickCheck.StateModel.Lockstep.EnvF+      Test.QuickCheck.StateModel.Lockstep.GVar+      Test.QuickCheck.StateModel.Lockstep.Op+  build-depends:+      -- quickcheck-dynamic requires ghc 8.10 minimum+      base               >= 4.14 && < 4.15+    , mtl                >= 2.2  && < 2.3+    , containers         >= 0.6  && < 0.7+    , QuickCheck         >= 2.14 && < 2.15+    , quickcheck-dynamic >= 2.0  && < 2.1+  hs-source-dirs:+      src++test-suite test-quickcheck-lockstep+  import:+      lang+  type:+      exitcode-stdio-1.0+  hs-source-dirs:+      test+  main-is:+      Main.hs+  other-modules:+      Test.MockFS+      Test.MockFS.Mock+      Test.IORef+  default-extensions:+      DeriveGeneric+      EmptyCase+  build-depends:+      -- Version bounds determined by main lib+      base+    , containers+    , directory+    , filepath+    , mtl+    , QuickCheck+    , quickcheck-dynamic+    , quickcheck-lockstep+    , tasty+    , tasty-hunit+    , tasty-quickcheck+    , temporary
+ src/Test/QuickCheck/StateModel/Lockstep.hs view
@@ -0,0 +1,37 @@+-- | Lockstep-style testing using @quickcheck-dynamic@+--+-- See <https://well-typed.com/blog/2022/09/lockstep-with-quickcheck-dynamic/>+-- for a tutorial.+--+-- This module is intended for unqualified import alongside imports of+-- "Test.QuickCheck.StateModel".+--+-- > import Test.QuickCheck.StateModel+-- > import Test.QuickCheck.StateModel.Lockstep+-- > import Test.QuickCheck.StateModel.Lockstep.Run      qualified as Lockstep+-- > import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep+module Test.QuickCheck.StateModel.Lockstep (+    -- * Main abstraction+    Lockstep -- opaque+  , InLockstep(..)+  , RunLockstep(..)+    -- ** Convenience aliases+  , LockstepAction+  , ModelFindVariables+  , ModelLookUp+  , ModelVar+    -- * Variables+  , GVar -- opaque+  , AnyGVar(..)+  , lookUpGVar+  , mapGVar+    -- ** Operations+  , Operation(..)+  , InterpretOp(..)+  ) where++import Prelude hiding (init)++import Test.QuickCheck.StateModel.Lockstep.API+import Test.QuickCheck.StateModel.Lockstep.Op+import Test.QuickCheck.StateModel.Lockstep.GVar
+ src/Test/QuickCheck/StateModel/Lockstep/API.hs view
@@ -0,0 +1,174 @@+-- | Public API+--+-- This is re-exported through "Test.QuickCheck.StateModel.Lockstep".+module Test.QuickCheck.StateModel.Lockstep.API (+    -- * State+    Lockstep(..)+    -- * Main abstraction+  , InLockstep(..)+  , RunLockstep(..)+    -- * Convenience aliases+  , LockstepAction+  , ModelFindVariables+  , ModelLookUp+  , ModelVar+  ) where++import Data.Kind+import Data.Typeable++import Test.QuickCheck (Gen)+import Test.QuickCheck.StateModel (StateModel, Any, RunModel, Realized, Action)++import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)+import Test.QuickCheck.StateModel.Lockstep.GVar (GVar, AnyGVar(..))+import Test.QuickCheck.StateModel.Lockstep.Op+import Test.QuickCheck.StateModel.Lockstep.Op.Identity qualified as Identity++{-------------------------------------------------------------------------------+  Lockstep state++  @quickcheck-dynamic@ takes care of keeping track of the responses of the+  system under test, but not the model. We do that here.++  Implementation note: the 'RunModel' class in @quickcheck-dynamic@ uses a type+  family 'Realized': for an @Action state a@, the response from the real system+  is expected to be of type @Realized m a@. This allows the same tests to be run+  against different "test execution backends"; for example, we could run the+  tests in the real IO monad, or using an IO monad simulator.++  This is an orthogonal generalization to what Lockstep provides: no matter the+  test execution backend, the /model/ will always be the same. We could perhaps+  piggy-back on the same abstraction if we introduced a separate monad parameter+  @n@ for the model, and then use @Realized n a@ instead of @ModelValue a@. This+  might work, but it's less clear how to then also that for 'Observable'.+  Overall, it seems cleaner to reserve 'Realized' exclusively for the+  parameterization over test execution backends.+-------------------------------------------------------------------------------}++data Lockstep state = Lockstep {+      lockstepModel :: state+    , lockstepEnv   :: EnvF (ModelValue state)+    }++-- | The 'Show' instance does not show the internal environment+instance Show state => Show (Lockstep state) where+  show = show . lockstepModel++{-------------------------------------------------------------------------------+  Main lockstep abstraction+-------------------------------------------------------------------------------}++class+     ( StateModel (Lockstep state)+     , Typeable state+     , InterpretOp (ModelOp state) (ModelValue state)+     , forall a. Show (ModelValue state a)+     , forall a. Eq   (Observable state a)+     , forall a. Show (Observable state a)+     )+  => InLockstep state where+  -- | Values in the mock environment+  --+  -- 'ModelValue' witnesses the relation between values returned by the real+  -- system and values returned by the model.+  --+  -- In most cases, we expect the real system and the model to return the+  -- /same/ value. However, for some things we must allow them to diverge:+  -- consider file handles for example.+  data ModelValue state a++  -- | Observable responses+  --+  -- The real system returns values of type @a@, and the model returns values+  -- of type @MockValue a@. @Observable a@ defines the parts of those results+  -- that expect to be the /same/ for both.+  data Observable state a++  -- | Type of operations required on the results of actions+  --+  -- Whenever an action has a result of type @a@, but we later need a variable+  -- of type @b@, we need a constructor+  --+  -- > GetB :: ModelOp state a b+  --+  -- in the 'ModelOp' type. For many tests, the standard 'Op' type will+  -- suffice, but not always.+  type ModelOp state :: Type -> Type -> Type+  type ModelOp state = Identity.Op++  -- | Extract the observable part of a response from the model+  observeModel :: ModelValue state a-> Observable state a++  -- | All variables required by a command+  usedVars :: LockstepAction state a -> [AnyGVar (ModelOp state)]++  -- | Step the model+  --+  -- The order of the arguments mimicks 'perform'.+  modelNextState ::+       LockstepAction state a+    -> ModelLookUp state+    -> state+    -> (ModelValue state a, state)++  -- | Generate an arbitrary action, given a way to find variables+  arbitraryWithVars ::+       ModelFindVariables state+    -> state+    -> Gen (Any (LockstepAction state))++  -- | Shrink an action, given a way to find variables+  --+  -- This is optional; without an implementation of 'shrinkWithVars', lists of+  -- actions will still be pruned, but /individual/ actions will not be shrunk.+  shrinkWithVars ::+       ModelFindVariables state+    -> state+    -> LockstepAction state a+    -> [Any (LockstepAction state)]+  shrinkWithVars _ _ _ = []++  -- | Tag actions+  --+  -- Tagging is optional, but can help understand your test input data as+  -- well as your shrinker (see 'tagActions').+  tagStep ::+       (state, state)+    -> LockstepAction state a+    -> ModelValue state a+    -> [String]+  tagStep _ _ _ = []++class ( InLockstep state+      , RunModel (Lockstep state) m+      ) => RunLockstep state m where+  -- See also 'Observable'+  observeReal ::+       Proxy m+    -> LockstepAction state a -> Realized m a -> Observable state a++{-------------------------------------------------------------------------------+  Convenience aliases+-------------------------------------------------------------------------------}++-- | 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.+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+-- 'StateModel.Lockstep.GVar.map'.+type ModelFindVariables state = forall a.+          Typeable a+       => Proxy a -> [GVar (ModelOp state) a]++-- | Variables with a "functor-esque" instance+type ModelVar state = GVar (ModelOp state)+
+ src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs view
@@ -0,0 +1,155 @@+-- | Default implementations for the @quickcheck-dynamic@ class methods+--+-- Intended for qualified import.+--+-- > import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep+module Test.QuickCheck.StateModel.Lockstep.Defaults (+    -- * Default implementations for methods of 'StateModel'+    initialState+  , nextState+  , precondition+  , arbitraryAction+  , shrinkAction+    -- * Default implementations for methods of 'RunModel'+  , postcondition+  , monitoring+  ) where++import Prelude hiding (init)++import Data.Maybe (isNothing)+import Data.Typeable++import Test.QuickCheck (Gen, Property)+import Test.QuickCheck qualified as QC+import Test.QuickCheck.StateModel (Var, Any(..), LookUp, Realized)++import Test.QuickCheck.StateModel.Lockstep.API+import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)+import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF+import Test.QuickCheck.StateModel.Lockstep.GVar++{-------------------------------------------------------------------------------+  Default implementations for members of 'StateModel'+-------------------------------------------------------------------------------}++-- | Default implementation for 'Test.QuickCheck.StateModel.initialState'+initialState :: state -> Lockstep state+initialState state = Lockstep {+      lockstepModel = state+    , lockstepEnv   = EnvF.empty+    }++-- | Default implementation for 'Test.QuickCheck.StateModel.nextState'+nextState :: forall state a.+     (InLockstep state, Typeable a)+  => Lockstep state+  -> LockstepAction state a+  -> Var a+  -> Lockstep state+nextState (Lockstep state env) action var =+    Lockstep state' $ EnvF.insert var modelResp env+  where+    modelResp :: ModelValue state a+    state'    :: state+    (modelResp, state') = modelNextState action (lookUpEnvF env) state++-- | Default implementation for 'Test.QuickCheck.StateModel.precondition'+--+-- The default precondition only checks that all variables have a value+-- and that the operations on them are defined.+precondition ::+     InLockstep state+  => Lockstep state -> LockstepAction state a -> Bool+precondition (Lockstep _ env) =+    all (\(SomeGVar var) -> definedInEnvF env var) . usedVars++-- | Default implementation for 'Test.QuickCheck.StateModel.arbitraryAction'+arbitraryAction ::+     InLockstep state+  => Lockstep state -> Gen (Any (LockstepAction state))+arbitraryAction (Lockstep state env) =+    arbitraryWithVars (varsOfType env) state++-- | Default implementation for 'Test.QuickCheck.StateModel.shrinkAction'+shrinkAction ::+     InLockstep state+  => Lockstep state+  -> LockstepAction state a -> [Any (LockstepAction state)]+shrinkAction (Lockstep state env) =+    shrinkWithVars (varsOfType env) state++{-------------------------------------------------------------------------------+  Default implementations for methods of 'RunModel'+-------------------------------------------------------------------------------}++-- | Default implementation for 'Test.QuickCheck.StateModel.postcondition'+--+-- The default postcondition verifies that the real system and the model+-- return the same results, up to " observability ".+postcondition :: forall m state a.+     RunLockstep state m+  => (Lockstep state, Lockstep state)+  -> LockstepAction state a+  -> LookUp m+  -> Realized m a+  -> m Bool+postcondition (before, _after) action _lookUp a =+    pure $ isNothing $ checkResponse (Proxy @m) before action a++monitoring :: forall m state a.+     RunLockstep state m+  => Proxy m+  -> (Lockstep state, Lockstep state)+  -> LockstepAction state a+  -> LookUp m+  -> Realized m a+  -> Property -> Property+monitoring p (before, after) action _lookUp realResp =+      QC.counterexample ("State: " ++ show after)+    . maybe id QC.counterexample (checkResponse p before action realResp)+    . QC.tabulate "Tags" tags+  where+    tags :: [String]+    tags = tagStep (lockstepModel before, lockstepModel after) action modelResp++    modelResp :: ModelValue state a+    modelResp = fst $ modelNextState+                        action+                        (lookUpEnvF $ lockstepEnv before)+                        (lockstepModel before)++{-------------------------------------------------------------------------------+  Internal auxiliary+-------------------------------------------------------------------------------}++varsOfType ::+     InLockstep state+  => EnvF (ModelValue state) -> ModelFindVariables state+varsOfType env _ = map fromVar $ EnvF.keysOfType env++-- | Check the response of the system under test against the model+--+-- This is used in 'postcondition', where we can however only return a 'Bool',+-- and in 'monitoring', to give the user more detailed feedback.+checkResponse :: forall m state a.+     RunLockstep state m+  => Proxy m+  -> Lockstep state -> LockstepAction state a -> Realized m a -> Maybe String+checkResponse p (Lockstep state env) action a =+    compareEquality (observeReal p action a) (observeModel modelResp)+  where+    modelResp :: ModelValue state a+    modelResp = fst $ modelNextState action (lookUpEnvF env) state++    compareEquality ::  Observable state a -> Observable state a -> Maybe String+    compareEquality real mock+      | real == mock = Nothing+      | otherwise    = Just $ concat [+            "System under test returned: "+          , show real+          , "\nbut model returned:         "+          , show mock+          ]++
+ src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs view
@@ -0,0 +1,59 @@+-- | Environment parameterised by functor @f@+--+-- Intended for qualified import:+--+-- > import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)+-- > import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF+module Test.QuickCheck.StateModel.Lockstep.EnvF (+    EnvF -- opaque+    -- * Construction+  , empty+  , insert+    -- * Query+  , lookup+  , keysOfType+  ) where++import Prelude hiding (lookup)++import Control.Monad+import Data.Foldable (asum)+import Data.Maybe (mapMaybe)+import Data.Typeable++import Test.QuickCheck.StateModel (Var(..))++{-------------------------------------------------------------------------------+  Types+-------------------------------------------------------------------------------}++data EnvEntry f where+  EnvEntry :: Typeable a => Var a -> f a -> EnvEntry f++newtype EnvF f = EnvF [EnvEntry f]++{-------------------------------------------------------------------------------+  Construction+-------------------------------------------------------------------------------}++empty :: EnvF f+empty = EnvF []++insert :: Typeable a => Var a -> f a -> EnvF f -> EnvF f+insert x fa (EnvF env) = EnvF (EnvEntry x fa : env)++{-------------------------------------------------------------------------------+  Query+-------------------------------------------------------------------------------}++lookup :: forall f a. (Typeable f, Typeable a) => Var a -> EnvF f -> Maybe (f a)+lookup = \var (EnvF env) ->+    asum $ map (\(EnvEntry var' fa') -> aux var var' fa') env+  where+    aux :: Typeable a' => Var a -> Var a' -> f a' -> Maybe (f a)+    aux (Var x) (Var y) fa' = do+        guard (x == y)+        cast fa'++keysOfType :: Typeable a => EnvF f -> [Var a]+keysOfType (EnvF env) = mapMaybe (\(EnvEntry var _) -> cast var) env
+ src/Test/QuickCheck/StateModel/Lockstep/GVar.hs view
@@ -0,0 +1,99 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Generalized variables+--+-- Intended for unqualified import.+module Test.QuickCheck.StateModel.Lockstep.GVar (+    GVar -- opaque+  , AnyGVar(..)+    -- * Construction+  , fromVar+  , mapGVar+    -- * Interop with 'Env'+  , lookUpGVar+    -- * Interop with 'EnvF'+  , lookUpEnvF+  , definedInEnvF+  ) where++import Prelude hiding (map)++import Data.Maybe (isJust, fromJust)+import Data.Typeable++import Test.QuickCheck.StateModel (Var(..), LookUp, Realized)++import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)+import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF+import Test.QuickCheck.StateModel.Lockstep.Op++{-------------------------------------------------------------------------------+  Main type+-------------------------------------------------------------------------------}++-- | Generalized variables+--+-- The key difference between 'GVar' and the standard 'Var' type is that+-- 'GVar' have a functor-esque structure: see 'map'.+data GVar op f where+  GVar :: Typeable x => Var x -> op x y -> GVar op y++data AnyGVar op where+  SomeGVar :: GVar op y -> AnyGVar op++deriving instance (forall x. Show (op x a)) => Show (GVar op a)++instance (forall x. Eq (op x a)) => Eq (GVar op a) where+  (==) = \(GVar x op) (GVar x' op') -> aux x x' op op'+    where+      aux :: forall x x'.+           (Typeable x, Typeable x')+        => Var x -> Var x' -> op x a -> op x' a -> Bool+      aux x x' op op' =+          case eqT @x @x' of+            Nothing   -> False+            Just Refl -> (x, op) == (x', op')++{-------------------------------------------------------------------------------+  Construction+-------------------------------------------------------------------------------}++fromVar :: (Operation op, Typeable a) => Var a -> GVar op a+fromVar var = GVar var opIdentity++mapGVar :: (forall x. op x a -> op x b) -> GVar op a -> GVar op b+mapGVar f (GVar var op) = GVar var (f op)++{-------------------------------------------------------------------------------+  Interop with 'Env'+-------------------------------------------------------------------------------}++lookUpWrapped :: Typeable a => Proxy m -> LookUp m -> Var a -> WrapRealized m a+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'.+lookUpGVar ::+     InterpretOp op (WrapRealized m)+  => Proxy m -> LookUp m -> GVar op a -> Realized m a+lookUpGVar p lookUp (GVar var op) =+    unwrapRealized $ fromJust $ 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 $+    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
+ src/Test/QuickCheck/StateModel/Lockstep/Op.hs view
@@ -0,0 +1,46 @@+module Test.QuickCheck.StateModel.Lockstep.Op (+    Operation(..)+  , InterpretOp(..)+  , WrapRealized(..)+  , intOpRealizedId+  ) where++import Test.QuickCheck.StateModel (Realized)+import Data.Coerce++{-------------------------------------------------------------------------------+  Operations++  This is basically reified functions. We reify them for two reasons:++  1. It means we can define proper Show/Eq instances for 'GVar'+  2. It allows us to give separate interpretations of 'Op' for mock values+     and for real values.+-------------------------------------------------------------------------------}++class Operation op where+  opIdentity :: op a a++class Operation op => InterpretOp op f where+  intOp :: op a b -> f a -> Maybe (f b)++{-------------------------------------------------------------------------------+  Interop with 'Realized'++  We want to execute operations against 'Realized' values, but since that is+  a newtype, we need to wrap and unwrap in order to be able to give the+  appropriate 'InterpretOp' instances.+-------------------------------------------------------------------------------}++newtype WrapRealized m a = WrapRealized {+      unwrapRealized :: Realized m a+    }++-- | Convenience function for defining 'InterpretOp' instances+--+-- This can be used for monads like @IO@ where @Realized m a@ is just @a@.+intOpRealizedId ::+     (Realized m a ~ a, Realized m b ~ b)+  => (op a b -> a -> Maybe b)+  -> op a b -> WrapRealized m a -> Maybe (WrapRealized m b)+intOpRealizedId = coerce
+ src/Test/QuickCheck/StateModel/Lockstep/Op/Identity.hs view
@@ -0,0 +1,18 @@+module Test.QuickCheck.StateModel.Lockstep.Op.Identity (Op(..)) where++import Test.QuickCheck.StateModel.Lockstep.Op++-- | Very simple operation type that supports identity only+--+-- This can be used by tests that don't need to map over variables. That is,+-- where variables always refer to the /exact/ result of previously executed+-- commands. Such tests will not need to define any 'InterpretOp' instances.+data Op a b where+  OpId :: Op a a++deriving instance Show (Op a b)+deriving instance Eq   (Op a b)++instance Operation   Op   where opIdentity = OpId+instance InterpretOp Op f where intOp OpId = Just+
+ src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs view
@@ -0,0 +1,96 @@+{-# LANGUAGE TypeOperators #-}+module Test.QuickCheck.StateModel.Lockstep.Op.SumProd (Op(..)) where++import Control.Monad.Reader (ReaderT)+import Control.Monad.State+import GHC.Show (appPrec)++import Test.QuickCheck.StateModel.Lockstep.Op++{-------------------------------------------------------------------------------+  Example (but very useful) 'Operation' example++  Because this is designed for testing where we want everything to be 'Show'able+  and 'Typeable', matching on 'Op' might reveal some additonal constrants.+  This is useful in 'OpComp' where we have an existential variable (@b@), but+  it's also useful for example in 'OpRight': the caller might have a constraint+  @Show (Either a b)@, but that doesn't give them a way to obtain a constraint+  @Show a@; the implication only goes one way.++  (These are the same constraints that 'Any' imposes.)+-------------------------------------------------------------------------------}++-- | Operations with support for products (pairs) and sums ('Either')+data Op a b where+  OpId    :: Op a a+  OpFst   :: Op (a, b) a+  OpSnd   :: Op (b, a) a+  OpLeft  :: Op (Either a b) a+  OpRight :: Op (Either b a) a+  OpComp  :: Op b c -> Op a b -> Op a c++intOpId :: Op a b -> a -> Maybe b+intOpId OpId         = Just+intOpId OpFst        = Just . fst+intOpId OpSnd        = Just . snd+intOpId OpLeft       = either Just (const Nothing)+intOpId OpRight      = either (const Nothing) Just+intOpId (OpComp g f) = intOpId g <=< intOpId f++{-------------------------------------------------------------------------------+  'InterpretOp' instances+-------------------------------------------------------------------------------}++instance Operation Op where+  opIdentity = OpId++instance InterpretOp Op (WrapRealized IO) where+  intOp = intOpRealizedId intOpId++instance InterpretOp Op (WrapRealized (ReaderT r IO)) where+  intOp = intOpRealizedId intOpId++instance InterpretOp Op (WrapRealized (StateT s IO)) where+  intOp = intOpRealizedId intOpId++{-------------------------------------------------------------------------------+  'Show' and 'Eq' instances+-------------------------------------------------------------------------------}++sameOp :: Op a b -> Op c d -> Bool+sameOp = go+  where+    go :: Op a b -> Op c d -> Bool+    go OpId         OpId           = True+    go OpFst        OpFst          = True+    go OpSnd        OpSnd          = True+    go OpLeft       OpLeft         = True+    go OpRight      OpRight        = True+    go (OpComp g f) (OpComp g' f') = go g g' && go f f'+    go _            _              = False++    _coveredAllCases :: Op a b -> ()+    _coveredAllCases = \case+        OpId    -> ()+        OpFst   -> ()+        OpSnd   -> ()+        OpLeft  -> ()+        OpRight -> ()+        OpComp{} -> ()++instance Eq (Op a b)  where+  (==) = sameOp++instance Show (Op a b) where+  showsPrec p = \op -> case op of+      OpComp{} -> showParen (p > appPrec) (go op)+      _        -> go op+    where+      go :: Op x y -> String -> String+      go OpId         = showString "id"+      go OpFst        = showString "fst"+      go OpSnd        = showString "snd"+      go OpLeft       = showString "fromLeft"+      go OpRight      = showString "fromRight"+      go (OpComp g f) = go g . showString " . " . go f+
+ src/Test/QuickCheck/StateModel/Lockstep/Run.hs view
@@ -0,0 +1,135 @@+-- | Run lockstep tests+--+-- Intended for qualified import.+--+-- > import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep+module Test.QuickCheck.StateModel.Lockstep.Run (+    -- * Finding labelled examples+    tagActions+    -- * Run tests+  , runActions+  , runActionsBracket+  ) where++import Prelude hiding (init)++import Control.Exception+import Control.Monad.Reader+import Data.Set (Set)+import Data.Set qualified as Set+import Data.Typeable+import Test.QuickCheck.Monadic++import Test.QuickCheck (Property, Testable)+import Test.QuickCheck qualified as QC+import Test.QuickCheck.StateModel hiding (runActions)+import Test.QuickCheck.StateModel qualified as StateModel++import Test.QuickCheck.StateModel.Lockstep.API+import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF+import Test.QuickCheck.StateModel.Lockstep.GVar++{-------------------------------------------------------------------------------+  Finding labelled examples++  Implementation note: the 'monitoring' hook from 'StateModel' cannot be used+  for finding labelled examples. This hook is called many times during test+  execution (once per action); this means that we cannot call 'label' inside+  'monitoring', but must instead use 'tabulate'. However, 'tabulate' is not+  supported by 'labelledExamples'. In 'tagActions' we therefore run over all+  actions, collecting tags as we go, and then do a /single/ call to 'label'+  at the end.+-------------------------------------------------------------------------------}++-- | Tag a list of actions+--+-- This can be used together with QuickCheck's 'labelledExamples' to test your+-- tagging code as well as your shrinker (QuickCheck will try to produce+-- /minimal/ labelled examples).+--+-- Unlike 'runActions', this does not require a 'RunModel' instance; this is+-- executed against the model /only/.+tagActions :: forall state.+     InLockstep state+  => Proxy state+  -> Actions (Lockstep state)+  -> Property+tagActions _p (Actions steps) =+    go Set.empty Test.QuickCheck.StateModel.initialState steps+  where+    go :: Set String -> Lockstep state -> [Step (Lockstep state)] -> Property+    go tags _st []            = QC.label ("Tags: " ++ show (Set.toList tags)) True+    go tags  st ((v:=a) : ss) = go' tags st v a ss++    go' :: forall a.+         Typeable a+      => Set String                 -- accumulated set of tags+      -> Lockstep state             -- current state+      -> Var a                      -- variable for the result of this action+      -> Action (Lockstep state) a  -- action to execute+      -> [Step (Lockstep state)]    -- remaining steps to execute+      -> Property+    go' tags (Lockstep before env) var action ss =+        go (Set.union (Set.fromList tags') tags) st' ss+      where+        st' :: Lockstep state+        st' = Lockstep after (EnvF.insert var modelResp env)++        modelResp :: ModelValue state a+        after     :: state+        (modelResp, after) = modelNextState action (lookUpEnvF env) before++        tags' :: [String]+        tags' = tagStep (before, after) action modelResp++{-------------------------------------------------------------------------------+  Run tests+-------------------------------------------------------------------------------}++runActions ::+     RunLockstep state IO+  => Proxy state+  -> Actions (Lockstep state) -> Property+runActions _ actions = monadicIO $ void $ StateModel.runActions actions++-- | Convenience runner with support for state initialization+--+-- This is less general than 'Test.QuickCheck.StateModel.runActions', but+-- will be useful in many scenarios.+runActionsBracket ::+     RunLockstep state (ReaderT st IO)+  => Proxy state+  -> IO st         -- ^ Initialisation+  -> (st -> IO ()) -- ^ Cleanup+  -> Actions (Lockstep state) -> Property+runActionsBracket _ init cleanup actions =+    monadicBracketIO init cleanup $+      void $ StateModel.runActions actions++{-------------------------------------------------------------------------------+  Internal auxiliary+-------------------------------------------------------------------------------}++ioPropertyBracket ::+     Testable a+  => IO st+  -> (st -> IO ())+  -> ReaderT st IO a+  -> Property+ioPropertyBracket init cleanup (ReaderT prop) = do+    QC.ioProperty $ mask $ \restore -> do+      st <- init+      a  <- restore (prop st) `onException` cleanup st+      cleanup st+      return a++-- | Variation on 'monadicIO' that allows for state initialisation/cleanup+monadicBracketIO :: forall st a.+     Testable a+  => IO st+  -> (st -> IO ())+  -> (PropertyM (ReaderT st IO) a)+  -> Property+monadicBracketIO init cleanup =+    monadic (ioPropertyBracket init cleanup)+
+ test/Main.hs view
@@ -0,0 +1,12 @@+module Main (main) where++import Test.Tasty++import Test.IORef qualified+import Test.MockFS qualified++main :: IO ()+main = defaultMain $ testGroup "quickcheck-lockstep" [+      Test.IORef.tests+    , Test.MockFS.tests+    ]
+ test/Test/IORef.hs view
@@ -0,0 +1,162 @@+{-# OPTIONS_GHC -Wno-orphans #-}++module Test.IORef (tests) where++import Data.Bifunctor+import Data.IORef+import Data.Map (Map)+import Data.Map qualified as Map+import Data.Proxy+import Test.QuickCheck+import Test.Tasty+import Test.Tasty.QuickCheck (testProperty)++import Test.QuickCheck.StateModel+import Test.QuickCheck.StateModel.Lockstep+import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep+import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep++{-------------------------------------------------------------------------------+  Model "M"+-------------------------------------------------------------------------------}++type MRef = Int+type M    = Map MRef Int++initModel :: M+initModel = Map.empty++modelNew :: M -> (MRef, M)+modelNew m = (mockRef, Map.insert mockRef 0 m)+  where+    mockRef :: MRef+    mockRef = Map.size m++modelWrite :: MRef -> Int -> M -> ((), M)+modelWrite v x m = ((), Map.insert v x m)++modelRead :: MRef -> M -> (Int, M)+modelRead v m = (m Map.! v, m)++{-------------------------------------------------------------------------------+  Instances+-------------------------------------------------------------------------------}++instance StateModel (Lockstep M) where+  data Action (Lockstep M) a where+    -- | Create new IORef+    New :: Action (Lockstep M) (IORef Int)++    -- | Write value to IORef+    Write ::+         ModelVar M (IORef Int)+      -> Int+      -> Action (Lockstep M) ()++    -- | Read IORef+    Read ::+         ModelVar M (IORef Int)+      -> Action (Lockstep M) Int++  initialState    = Lockstep.initialState initModel+  nextState       = Lockstep.nextState+  precondition    = Lockstep.precondition+  arbitraryAction = Lockstep.arbitraryAction+  shrinkAction    = Lockstep.shrinkAction++instance RunModel (Lockstep M) IO where+  perform       = \_state -> runIO+  postcondition = Lockstep.postcondition+  monitoring    = Lockstep.monitoring (Proxy @IO)++instance InLockstep M where+  data ModelValue M a where+    MRef  :: MRef -> ModelValue M (IORef Int)+    MUnit :: ()   -> ModelValue M ()+    MInt  :: Int  -> ModelValue M Int++  data Observable M a where+    ORef :: Observable M (IORef Int)+    OId  :: (Show a, Eq a) => a -> Observable M a++  observeModel (MRef  _) = ORef+  observeModel (MUnit x) = OId x+  observeModel (MInt  x) = OId x++  usedVars New         = []+  usedVars (Write v _) = [SomeGVar v]+  usedVars (Read  v)   = [SomeGVar v]++  modelNextState = runModel++  arbitraryWithVars findVars _mock = oneof $ concat [+        withoutVars+      , case findVars (Proxy @(IORef Int)) of+          []   -> []+          vars -> withVars (elements vars)+      ]+    where+      withoutVars :: [Gen (Any (LockstepAction M))]+      withoutVars = [return $ Some New]++      withVars ::+           Gen (ModelVar M (IORef Int))+        -> [Gen (Any (LockstepAction M))]+      withVars genVar = [+            fmap Some $ Write <$> genVar <*> arbitrary+          , fmap Some $ Read  <$> genVar+          ]++instance RunLockstep M IO where+  observeReal _ action result =+      case (action, result) of+        (New     , _) -> ORef+        (Write{} , x) -> OId x+        (Read{}  , x) -> OId x++deriving instance Show (Action (Lockstep M) a)+deriving instance Show (Observable M a)+deriving instance Show (ModelValue M a)++deriving instance Eq (Action (Lockstep M) a)+deriving instance Eq (Observable M a)+deriving instance Eq (ModelValue M a)++{-------------------------------------------------------------------------------+  Interpreters against the real system and against the model+-------------------------------------------------------------------------------}++runIO :: Action (Lockstep M) a -> LookUp IO -> IO a+runIO action lookUp =+    case action of+      New       -> newIORef 0+      Write v x -> writeIORef (lookUpRef v) x+      Read  v   -> readIORef  (lookUpRef v)+  where+    lookUpRef :: ModelVar M (IORef Int) -> IORef Int+    lookUpRef = lookUpGVar (Proxy @IO) lookUp++runModel ::+     Action (Lockstep M) a+  -> ModelLookUp M+  -> M -> (ModelValue M a, M)+runModel action lookUp =+    case action of+      New       -> first MRef  . modelNew+      Write v x -> first MUnit . modelWrite (lookUpRef v) x+      Read  v   -> first MInt  . modelRead  (lookUpRef v)+  where+    lookUpRef :: ModelVar M (IORef Int) -> MRef+    lookUpRef var = case lookUp var of MRef r -> r++{-------------------------------------------------------------------------------+  Top-level tests+-------------------------------------------------------------------------------}++propIORef :: Actions (Lockstep M) -> Property+propIORef = Lockstep.runActions (Proxy @M)++tests :: TestTree+tests = testGroup "Test.IORef" [+      testProperty "runActions" propIORef+    ]
+ test/Test/MockFS.hs view
@@ -0,0 +1,376 @@+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE ImportQualifiedPost   #-}+{-# LANGUAGE InstanceSigs          #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE TupleSections         #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE TypeFamilies          #-}++module Test.MockFS (tests) where++import Prelude hiding (init)++import Control.Exception (catch, throwIO)+import Control.Monad+import Control.Monad.Reader+import Data.Bifunctor+import Data.Set (Set)+import Data.Set qualified as Set+import Data.Typeable+import System.Directory (removeDirectoryRecursive)+import System.Directory qualified as IO+import System.IO qualified as IO+import System.IO.Temp (createTempDirectory)+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit+import Test.Tasty.QuickCheck (testProperty)++import Test.QuickCheck (Gen)+import Test.QuickCheck qualified as QC+import Test.QuickCheck.StateModel++import Test.QuickCheck.StateModel.Lockstep+import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep+import Test.QuickCheck.StateModel.Lockstep.Op.SumProd+import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep++import Test.MockFS.Mock (Mock, Dir(..), File(..), Err)+import Test.MockFS.Mock qualified as Mock++{-------------------------------------------------------------------------------+  Model state+-------------------------------------------------------------------------------}++data FsState = FsState {+      fsStateMock  :: Mock+    , fsStateStats :: Stats+    }+  deriving (Show)++initState :: FsState+initState = FsState {+      fsStateMock  = Mock.emptyMock+    , fsStateStats = initStats+    }++{-------------------------------------------------------------------------------+  StateModel and 'RunModel' instances+-------------------------------------------------------------------------------}++type RealMonad = ReaderT FilePath IO++type FsVar a = ModelVar FsState a+type FsAct a = Action (Lockstep FsState) (Either Err a)++instance StateModel (Lockstep FsState) where+  data Action (Lockstep FsState) a where+    MkDir :: Dir                        -> FsAct ()+    Open  :: File                       -> FsAct (IO.Handle, File)+    Write :: FsVar IO.Handle  -> String -> FsAct ()+    Close :: FsVar IO.Handle            -> FsAct ()+    Read  :: Either (FsVar File) File   -> FsAct String++  initialState    = Lockstep.initialState initState+  nextState       = Lockstep.nextState+  precondition    = Lockstep.precondition+  arbitraryAction = Lockstep.arbitraryAction+  shrinkAction    = Lockstep.shrinkAction++instance RunModel (Lockstep FsState) RealMonad where+  perform       = \_st -> runIO+  postcondition = Lockstep.postcondition+  monitoring    = Lockstep.monitoring (Proxy @RealMonad)++deriving instance Show (Action (Lockstep FsState) a)+deriving instance Eq   (Action (Lockstep FsState) a)++{-------------------------------------------------------------------------------+  InLockstep instance+-------------------------------------------------------------------------------}++type FsVal a = ModelValue FsState a+type FsObs a = Observable FsState a++instance InLockstep FsState where++  --+  -- Model values+  --+  -- For model values, we must be sure that if we have a value of type+  --+  -- > FsVal IO.Handle+  --+  -- that it is a in fact mock handle. This means that here we cannot define+  --+  -- > ModelId :: a -> FsVal a+  --+  -- unlike in 'FsObs'.++  data ModelValue FsState a where+    MHandle :: Mock.MHandle -> FsVal IO.Handle++    -- Rest is regular:++    MErr    :: Err    -> FsVal Err+    MFile   :: File   -> FsVal File+    MString :: String -> FsVal String+    MUnit   :: ()     -> FsVal ()++    MEither :: Either (FsVal a) (FsVal b) -> FsVal (Either a b)+    MPair   :: (FsVal a, FsVal b)         -> FsVal (a, b)++  --+  -- Observable results+  --++  data Observable FsState a where+    OHandle :: FsObs IO.Handle+    OId     :: (Show a, Typeable a, Eq a) => a -> FsObs a+    OEither :: Either (FsObs a) (FsObs b) -> FsObs (Either a b)+    OPair   :: (FsObs a, FsObs b) -> FsObs (a, b)++  observeModel :: FsVal a -> FsObs a+  observeModel = \case+      MEither x -> OEither $ bimap observeModel observeModel x+      MPair   x -> OPair   $ bimap observeModel observeModel x+      MErr    x -> OId x+      MString x -> OId x+      MUnit   x -> OId x+      MFile   x -> OId x+      MHandle _ -> OHandle++  --+  -- Semantics+  --++  modelNextState :: forall a.+       LockstepAction FsState a+    -> ModelLookUp FsState+    -> FsState -> (FsVal a, FsState)+  modelNextState action lookUp (FsState mock stats) =+      auxStats $ runMock lookUp action mock+    where+      auxStats :: (FsVal a, Mock) -> (FsVal a, FsState)+      auxStats (result, state') =+          (result, FsState state' $ updateStats action result stats)++  --+  -- Variables+  --++  type ModelOp FsState = Op++  usedVars :: LockstepAction FsState a -> [AnyGVar (ModelOp FsState)]+  usedVars = \case+      MkDir{}        -> []+      Open{}         -> []+      Write h _      -> [SomeGVar h]+      Close h        -> [SomeGVar h]+      Read (Left h)  -> [SomeGVar h]+      Read (Right _) -> []++  --+  -- Generation, shrinking and labelling+  --++  arbitraryWithVars findVars _mock = arbitraryFsAction findVars+  shrinkWithVars    findVars _mock = shrinkFsAction    findVars++  tagStep (_, FsState _ after) act = map show . tagFsAction after act++deriving instance Show (Observable FsState a)+deriving instance Eq   (Observable FsState a)++deriving instance Show (FsVal a)++{-------------------------------------------------------------------------------+  RunLockstep instance+-------------------------------------------------------------------------------}++instance RunLockstep FsState RealMonad where+  observeReal ::+       Proxy RealMonad+    -> LockstepAction FsState a -> Realized RealMonad a -> FsObs a+  observeReal _ = \case+      MkDir{} -> OEither . bimap OId OId+      Open{}  -> OEither . bimap OId (OPair . bimap (const OHandle) OId)+      Write{} -> OEither . bimap OId OId+      Close{} -> OEither . bimap OId OId+      Read{}  -> OEither . bimap OId OId++{-------------------------------------------------------------------------------+  Interpreter against the model+-------------------------------------------------------------------------------}++runMock ::+     ModelLookUp FsState+  -> Action (Lockstep FsState) a+  -> Mock -> (FsVal a, Mock)+runMock lookUp = \case+    MkDir d   -> wrap MUnit     . Mock.mMkDir d+    Open f    -> wrap (mOpen f) . Mock.mOpen f+    Write h s -> wrap MUnit     . Mock.mWrite (getHandle $ lookUp h) s+    Close h   -> wrap MUnit     . Mock.mClose (getHandle $ lookUp h)+    Read f    -> wrap MString   . Mock.mRead (either (getFile . lookUp) id f)+  where+    wrap :: (a -> FsVal b) -> (Either Err a, Mock) -> (FsVal (Either Err b), Mock)+    wrap f = first (MEither . bimap MErr f)++    mOpen :: File -> Mock.MHandle -> FsVal (IO.Handle, File)+    mOpen f h = MPair (MHandle h, MFile f)++    getHandle :: ModelValue FsState IO.Handle -> Mock.MHandle+    getFile   :: ModelValue FsState File      -> File++    getHandle (MHandle h) = h+    getFile   (MFile   f) = f++{-------------------------------------------------------------------------------+  Generator and shrinking+-------------------------------------------------------------------------------}++arbitraryFsAction ::+     ModelFindVariables FsState+  -> Gen (Any (LockstepAction FsState))+arbitraryFsAction findVars = QC.oneof $ concat [+      withoutVars+    , case findVars (Proxy @((Either Err (IO.Handle, File)))) of+        []   -> []+        vars -> withVars (QC.elements vars)+    ]+  where+    withoutVars :: [Gen (Any (LockstepAction FsState))]+    withoutVars = [+          fmap Some $ MkDir <$> genDir+        , fmap Some $ Open  <$> genFile+        , fmap Some $ Read  <$> (Right <$> genFile)+        ]++    withVars ::+         Gen (FsVar (Either Err (IO.Handle, File)))+      -> [Gen (Any (LockstepAction FsState))]+    withVars genVar = [+          fmap Some $ Write <$> (handle <$> genVar) <*> genString+        , fmap Some $ Close <$> (handle <$> genVar)+        ]+      where+        handle :: GVar Op (Either Err (IO.Handle, File)) -> GVar Op IO.Handle+        handle = mapGVar (\op -> OpFst `OpComp` OpRight `OpComp` op)++    genDir :: Gen Dir+    genDir = do+        n <- QC.choose (0, 3)+        Dir <$> replicateM n (QC.elements ["x", "y", "z"])++    genFile :: Gen File+    genFile = File <$> genDir <*> QC.elements ["a", "b", "c"]++    genString :: Gen String+    genString = QC.sized $ \n -> replicateM n (QC.elements "ABC")++shrinkFsAction ::+     ModelFindVariables FsState+  -> Action (Lockstep FsState) a -> [Any (LockstepAction FsState)]+shrinkFsAction findVars = \case+    Open (File (Dir []) ('t' : n)) ->+      [openTemp n' | n' <- QC.shrink (read n)]+    Open _ ->+      [openTemp 100]+    Read (Right _) ->+      [ Some $ Read (Left $ mapGVar (\op -> OpSnd `OpComp` OpRight `OpComp` op) v)+      | v <- findVars (Proxy @((Either Err (IO.Handle, File))))+      ]+    _otherwise ->+      []+  where+    openTemp :: Int -> Any (LockstepAction FsState)+    openTemp n = Some $ Open (File (Dir []) ('t' : show n))++{-------------------------------------------------------------------------------+  Interpret 'Op' against 'ModelValue'+-------------------------------------------------------------------------------}++instance InterpretOp Op (ModelValue FsState) where+  intOp OpId         = Just+  intOp OpFst        = \case MPair   x -> Just (fst x)+  intOp OpSnd        = \case MPair   x -> Just (snd x)+  intOp OpLeft       = \case MEither x -> either Just (const Nothing) x+  intOp OpRight      = \case MEither x -> either (const Nothing) Just x+  intOp (OpComp g f) = intOp g <=< intOp f++{-------------------------------------------------------------------------------+  Interpreter for IO+-------------------------------------------------------------------------------}++runIO :: LockstepAction FsState a -> LookUp RealMonad -> RealMonad (Realized RealMonad a)+runIO action lookUp = ReaderT $ \root -> aux root action+  where+    aux :: FilePath -> LockstepAction FsState a -> IO a+    aux root = \case+        MkDir d -> catchErr $+          IO.createDirectory (Mock.dirFP root d)+        Open f -> catchErr $+          (,f) <$> IO.openFile (Mock.fileFP root f) IO.AppendMode+        Write h s -> catchErr $+          IO.hPutStr (lookUp' h) s+        Close h -> catchErr $+          IO.hClose (lookUp' h)+        Read f -> catchErr $+          IO.readFile (Mock.fileFP root $ either lookUp' id f)+      where+        lookUp' :: FsVar x -> x+        lookUp' = lookUpGVar (Proxy @RealMonad) lookUp++catchErr :: forall a. IO a -> IO (Either Err a)+catchErr act = catch (Right <$> act) handler+  where+    handler :: IOError -> IO (Either Err h)+    handler e = maybe (throwIO e) (return . Left) (Mock.fromIOError e)++{-------------------------------------------------------------------------------+  Statistics and tagging+-------------------------------------------------------------------------------}++-- The only statistics we need to track for this example is the files we opened+type Stats = Set File++initStats :: Stats+initStats = Set.empty++updateStats :: LockstepAction FsState a -> FsVal a -> Stats -> Stats+updateStats action result  =+   case (action, result) of+     (Open f, MEither (Right _)) -> Set.insert f+     _otherwise                  -> id++data Tag = OpenTwo | SuccessfulRead+  deriving (Show)++tagFsAction :: Stats -> LockstepAction FsState a -> FsVal a -> [Tag]+tagFsAction openedFiles = \case+    Read _ -> \v -> [SuccessfulRead | MEither (Right _) <- [v]]+    Open _ -> \_ -> [OpenTwo        | Set.size openedFiles >= 2]+    _      -> \_ -> []++{-------------------------------------------------------------------------------+  Top-level test+-------------------------------------------------------------------------------}++tests :: TestTree+tests = testGroup "Test.MockFS" [+      testCase "labelledExamples" $+        QC.labelledExamples $ Lockstep.tagActions (Proxy @FsState)+    , testProperty "propLockstep" $+        Lockstep.runActionsBracket (Proxy @FsState)+          (createTempDirectory tmpDir "QSM")+          removeDirectoryRecursive+    ]+  where+    -- TODO: tmpDir should really be a parameter to the test suite+    tmpDir :: FilePath+    tmpDir = "./tmp"
+ test/Test/MockFS/Mock.hs view
@@ -0,0 +1,124 @@+module Test.MockFS.Mock (+    -- * Paths+    Dir(..)+  , File(..)+  , dirFP+  , fileFP+    -- * Errors+  , Err(..)+  , fromIOError+    -- * Mock file system+  , MHandle+  , Mock(..)+  , emptyMock+  , mMkDir+  , mOpen+  , mWrite+  , mClose+  , mRead+  ) where++import Data.List qualified as List+import Data.Map (Map)+import Data.Map qualified as Map+import Data.Set (Set)+import Data.Set qualified as Set+import GHC.Generics (Generic)+import GHC.IO.Exception qualified as GHC+import System.FilePath ((</>))+import System.IO.Error++{-------------------------------------------------------------------------------+  Paths+-------------------------------------------------------------------------------}++data Dir = Dir [String]+  deriving (Show, Eq, Ord, Generic)++parent :: Dir -> Dir+parent (Dir fp) = Dir (init fp)++data File = File {dir :: Dir, name :: String}+  deriving (Show, Eq, Ord, Generic)++dirFP :: FilePath -> Dir -> FilePath+dirFP root (Dir d) = List.foldl' (</>) root d++fileFP :: FilePath -> File -> FilePath+fileFP root (File d f) = dirFP root d </> f++{-------------------------------------------------------------------------------+  Errors+-------------------------------------------------------------------------------}++data Err =+    AlreadyExists+  | DoesNotExist+  | HandleClosed+  | Busy+  deriving (Show, Eq)+++fromIOError :: IOError -> Maybe Err+fromIOError e =+    case ioeGetErrorType e of+      GHC.AlreadyExists    -> Just AlreadyExists+      GHC.NoSuchThing      -> Just DoesNotExist+      GHC.ResourceBusy     -> Just Busy+      GHC.IllegalOperation -> Just HandleClosed+      _otherwise           -> Nothing++{-------------------------------------------------------------------------------+  Mock implementation+-------------------------------------------------------------------------------}++type MHandle = Int++data Mock = M {+    dirs  :: Set Dir+  , files :: Map File String+  , open  :: Map MHandle File+  , next  :: MHandle+  }+  deriving (Show, Generic)++emptyMock :: Mock+emptyMock = M (Set.singleton (Dir [])) Map.empty Map.empty 0++type MockOp a = Mock -> (Either Err a, Mock)++mMkDir :: Dir -> MockOp ()+mMkDir d m@(M ds fs hs n)+  | d        `Set.member`    ds = (Left AlreadyExists, m)+  | parent d `Set.notMember` ds = (Left DoesNotExist, m)+  | otherwise                   = (Right (), M (Set.insert d ds) fs hs n)++mOpen :: File -> MockOp MHandle+mOpen f m@(M ds fs hs n)+  | alreadyOpen   = (Left Busy, m)+  | not dirExists = (Left DoesNotExist, m)+  | fileExists    = (Right n, M ds fs hs' n')+  | otherwise     = (Right n, M ds (Map.insert f "" fs) hs' n')+  where+    hs' = Map.insert n f hs+    n'  = succ n++    fileExists  =     f `Map.member` fs+    dirExists   = dir f `Set.member` ds+    alreadyOpen = f `List.elem` Map.elems hs++mWrite :: MHandle -> String -> MockOp ()+mWrite h s m@(M ds fs hs n)+  | Just f <- Map.lookup h hs = (Right (), M ds (Map.adjust (++ s) f fs) hs n)+  | otherwise                 = (Left HandleClosed, m)++mClose :: MHandle -> MockOp ()+mClose h (M ds fs hs n) = (Right (), M ds fs (Map.delete h hs) n)++mRead :: File -> MockOp String+mRead f m@(M _ fs hs _)+  | alreadyOpen               = (Left Busy         , m)+  | Just s <- Map.lookup f fs = (Right s           , m)+  | otherwise                 = (Left DoesNotExist , m)+  where+    alreadyOpen = f `List.elem` Map.elems hs