{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Test.QuickCheck.StateModel (
module Test.QuickCheck.StateModel.Variables,
StateModel (..),
RunModel (..),
PostconditionM (..),
WithUsedVars (..),
Annotated (..),
Step (..),
Polarity (..),
ActionWithPolarity (..),
LookUp,
Actions (..),
pattern Actions,
EnvEntry (..),
pattern (:=?),
Env,
Realized,
Generic,
monitorPost,
counterexamplePost,
stateAfter,
runActions,
lookUpVar,
lookUpVarMaybe,
initialAnnotatedState,
computeNextState,
computePrecondition,
computeArbitraryAction,
computeShrinkAction,
failureResult,
) where
import Control.Monad
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer (Endo (..), WriterT, runWriterT, tell)
import Data.Data
import Data.Kind
import Data.List
import Data.Set qualified as Set
import GHC.Generics
import GHC.Stack
import Test.QuickCheck as QC
import Test.QuickCheck.DynamicLogic.SmartShrinking
import Test.QuickCheck.Monadic
import Test.QuickCheck.StateModel.Variables
class
( forall a. Show (Action state a)
, forall a. HasVariables (Action state a)
, Show state
, HasVariables state
) =>
StateModel state
where
data Action state a
actionName :: Action state a -> String
actionName = forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
arbitraryAction :: VarContext -> state -> Gen (Any (Action state))
shrinkAction :: Typeable a => VarContext -> state -> Action state a -> [Any (Action state)]
shrinkAction VarContext
_ state
_ Action state a
_ = []
initialState :: state
nextState :: Typeable a => state -> Action state a -> Var a -> state
nextState state
s Action state a
_ Var a
_ = state
s
failureNextState :: Typeable a => state -> Action state a -> state
failureNextState state
s Action state a
_ = state
s
precondition :: state -> Action state a -> Bool
precondition state
_ Action state a
_ = Bool
True
validFailingAction :: state -> Action state a -> Bool
validFailingAction state
_ Action state a
_ = Bool
False
deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))
type family Realized (m :: Type -> Type) a :: Type
type instance Realized IO a = a
type instance Realized (StateT s m) a = Realized m a
type instance Realized (ReaderT r m) a = Realized m a
type instance Realized (WriterT w m) a = Realized m a
type instance Realized Identity a = a
newtype PostconditionM m a = PostconditionM {forall (m :: * -> *) a.
PostconditionM m a -> WriterT (Endo Property, Endo Property) m a
runPost :: WriterT (Endo Property, Endo Property) m a}
deriving (forall a b. a -> PostconditionM m b -> PostconditionM m a
forall a b. (a -> b) -> PostconditionM m a -> PostconditionM m b
forall (m :: * -> *) a b.
Functor m =>
a -> PostconditionM m b -> PostconditionM m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PostconditionM m a -> PostconditionM m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> PostconditionM m b -> PostconditionM m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> PostconditionM m b -> PostconditionM m a
fmap :: forall a b. (a -> b) -> PostconditionM m a -> PostconditionM m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PostconditionM m a -> PostconditionM m b
Functor, forall a. a -> PostconditionM m a
forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m a
forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
forall a b.
PostconditionM m (a -> b)
-> PostconditionM m a -> PostconditionM m b
forall a b c.
(a -> b -> c)
-> PostconditionM m a -> PostconditionM m b -> PostconditionM m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall {m :: * -> *}. Applicative m => Functor (PostconditionM m)
forall (m :: * -> *) a. Applicative m => a -> PostconditionM m a
forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m a
forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m (a -> b)
-> PostconditionM m a -> PostconditionM m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> PostconditionM m a -> PostconditionM m b -> PostconditionM m c
<* :: forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m a
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m a
*> :: forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
liftA2 :: forall a b c.
(a -> b -> c)
-> PostconditionM m a -> PostconditionM m b -> PostconditionM m c
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> PostconditionM m a -> PostconditionM m b -> PostconditionM m c
<*> :: forall a b.
PostconditionM m (a -> b)
-> PostconditionM m a -> PostconditionM m b
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m (a -> b)
-> PostconditionM m a -> PostconditionM m b
pure :: forall a. a -> PostconditionM m a
$cpure :: forall (m :: * -> *) a. Applicative m => a -> PostconditionM m a
Applicative, forall a. a -> PostconditionM m a
forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
forall a b.
PostconditionM m a
-> (a -> PostconditionM m b) -> PostconditionM m b
forall {m :: * -> *}. Monad m => Applicative (PostconditionM m)
forall (m :: * -> *) a. Monad m => a -> PostconditionM m a
forall (m :: * -> *) a b.
Monad m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
forall (m :: * -> *) a b.
Monad m =>
PostconditionM m a
-> (a -> PostconditionM m b) -> PostconditionM m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> PostconditionM m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> PostconditionM m a
>> :: forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
>>= :: forall a b.
PostconditionM m a
-> (a -> PostconditionM m b) -> PostconditionM m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
PostconditionM m a
-> (a -> PostconditionM m b) -> PostconditionM m b
Monad, forall (m :: * -> *) a. Monad m => m a -> PostconditionM m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
lift :: forall (m :: * -> *) a. Monad m => m a -> PostconditionM m a
$clift :: forall (m :: * -> *) a. Monad m => m a -> PostconditionM m a
MonadTrans)
monitorPost :: Monad m => (Property -> Property) -> PostconditionM m ()
monitorPost :: forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PostconditionM m ()
monitorPost Property -> Property
m = forall (m :: * -> *) a.
WriterT (Endo Property, Endo Property) m a -> PostconditionM m a
PostconditionM forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (forall a. (a -> a) -> Endo a
Endo Property -> Property
m, forall a. Monoid a => a
mempty)
counterexamplePost :: Monad m => String -> PostconditionM m ()
counterexamplePost :: forall (m :: * -> *). Monad m => String -> PostconditionM m ()
counterexamplePost String
c = forall (m :: * -> *) a.
WriterT (Endo Property, Endo Property) m a -> PostconditionM m a
PostconditionM forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (forall a. Monoid a => a
mempty, forall a. (a -> a) -> Endo a
Endo forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample String
c)
class Monad m => RunModel state m where
perform :: forall a. Typeable a => state -> Action state a -> LookUp m -> m (Realized m a)
postcondition :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool
postcondition (state, state)
_ Action state a
_ LookUp m
_ Realized m a
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
postconditionOnFailure :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool
postconditionOnFailure (state, state)
_ Action state a
_ LookUp m
_ Realized m a
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
monitoring :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property
monitoring (state, state)
_ Action state a
_ LookUp m
_ Realized m a
_ Property
prop = Property
prop
failureResult :: HasCallStack => a
failureResult :: forall a. HasCallStack => a
failureResult = forall a. HasCallStack => String -> a
error String
"A result of a failing action has been erronesouly inspected"
computePostcondition :: forall m state a. RunModel state m => (state, state) -> ActionWithPolarity state a -> LookUp m -> Realized m a -> PostconditionM m Bool
computePostcondition :: forall (m :: * -> *) state a.
RunModel state m =>
(state, state)
-> ActionWithPolarity state a
-> LookUp m
-> Realized m a
-> PostconditionM m Bool
computePostcondition (state, state)
ss (ActionWithPolarity Action state a
a Polarity
p) LookUp m
l Realized m a
r
| Polarity
p forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity = forall state (m :: * -> *) a.
RunModel state m =>
(state, state)
-> Action state a
-> LookUp m
-> Realized m a
-> PostconditionM m Bool
postcondition (state, state)
ss Action state a
a LookUp m
l Realized m a
r
| Bool
otherwise = forall state (m :: * -> *) a.
RunModel state m =>
(state, state)
-> Action state a
-> LookUp m
-> Realized m a
-> PostconditionM m Bool
postconditionOnFailure (state, state)
ss Action state a
a LookUp m
l Realized m a
r
type LookUp m = forall a. Typeable a => Var a -> Realized m a
type Env m = [EnvEntry m]
data EnvEntry m where
(:==) :: Typeable a => Var a -> Realized m a -> EnvEntry m
infix 5 :==
pattern (:=?) :: forall a m. Typeable a => Var a -> Realized m a -> EnvEntry m
pattern v $m:=? :: forall {r} {a} {m :: * -> *}.
Typeable a =>
EnvEntry m -> (Var a -> Realized m a -> r) -> ((# #) -> r) -> r
:=? val <- (viewAtType -> Just (v, val))
viewAtType :: forall a m. Typeable a => EnvEntry m -> Maybe (Var a, Realized m a)
viewAtType :: forall a (m :: * -> *).
Typeable a =>
EnvEntry m -> Maybe (Var a, Realized m a)
viewAtType ((Var a
v :: Var b) :== Realized m a
val)
| Just a :~: a
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @b = forall a. a -> Maybe a
Just (Var a
v, Realized m a
val)
| Bool
otherwise = forall a. Maybe a
Nothing
lookUpVarMaybe :: forall a m. Typeable a => Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe :: forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe [] Var a
_ = forall a. Maybe a
Nothing
lookUpVarMaybe (((Var a
v' :: Var b) :== Realized m a
a) : [EnvEntry m]
env) Var a
v =
case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @b of
Just a :~: a
Refl | Var a
v forall a. Eq a => a -> a -> Bool
== Var a
v' -> forall a. a -> Maybe a
Just Realized m a
a
Maybe (a :~: a)
_ -> forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe [EnvEntry m]
env Var a
v
lookUpVar :: Typeable a => Env m -> Var a -> Realized m a
lookUpVar :: forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env Var a
v = case forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe Env m
env Var a
v of
Maybe (Realized m a)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var a
v forall a. [a] -> [a] -> [a]
++ String
" is not bound!"
Just Realized m a
a -> Realized m a
a
data WithUsedVars a = WithUsedVars VarContext a
data Polarity
= PosPolarity
| NegPolarity
deriving (Eq Polarity
Polarity -> Polarity -> Bool
Polarity -> Polarity -> Ordering
Polarity -> Polarity -> Polarity
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Polarity -> Polarity -> Polarity
$cmin :: Polarity -> Polarity -> Polarity
max :: Polarity -> Polarity -> Polarity
$cmax :: Polarity -> Polarity -> Polarity
>= :: Polarity -> Polarity -> Bool
$c>= :: Polarity -> Polarity -> Bool
> :: Polarity -> Polarity -> Bool
$c> :: Polarity -> Polarity -> Bool
<= :: Polarity -> Polarity -> Bool
$c<= :: Polarity -> Polarity -> Bool
< :: Polarity -> Polarity -> Bool
$c< :: Polarity -> Polarity -> Bool
compare :: Polarity -> Polarity -> Ordering
$ccompare :: Polarity -> Polarity -> Ordering
Ord, Polarity -> Polarity -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Polarity -> Polarity -> Bool
$c/= :: Polarity -> Polarity -> Bool
== :: Polarity -> Polarity -> Bool
$c== :: Polarity -> Polarity -> Bool
Eq)
instance Show Polarity where
show :: Polarity -> String
show Polarity
PosPolarity = String
"+"
show Polarity
NegPolarity = String
"-"
data ActionWithPolarity state a = Eq (Action state a) =>
ActionWithPolarity
{ forall state a. ActionWithPolarity state a -> Action state a
polarAction :: Action state a
, forall state a. ActionWithPolarity state a -> Polarity
polarity :: Polarity
}
instance HasVariables (Action state a) => HasVariables (ActionWithPolarity state a) where
getAllVariables :: ActionWithPolarity state a -> Set (Any Var)
getAllVariables = forall a. HasVariables a => a -> Set (Any Var)
getAllVariables forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall state a. ActionWithPolarity state a -> Action state a
polarAction
deriving instance Eq (Action state a) => Eq (ActionWithPolarity state a)
data Step state where
(:=)
:: (Typeable a, Eq (Action state a), Show (Action state a))
=> Var a
-> ActionWithPolarity state a
-> Step state
infix 5 :=
instance (forall a. HasVariables (Action state a)) => HasVariables (Step state) where
getAllVariables :: Step state -> Set (Any Var)
getAllVariables (Var a
var := ActionWithPolarity state a
act) = forall a. Ord a => a -> Set a -> Set a
Set.insert (forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Var a
var) forall a b. (a -> b) -> a -> b
$ forall a. HasVariables a => a -> Set (Any Var)
getAllVariables (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act)
funName :: Polarity -> String
funName :: Polarity -> String
funName Polarity
PosPolarity = String
"action"
funName Polarity
_ = String
"failingAction"
instance Show (Step state) where
show :: Step state -> String
show (Var a
var := ActionWithPolarity state a
act) = forall a. Show a => a -> String
show Var a
var forall a. [a] -> [a] -> [a]
++ String
" <- " forall a. [a] -> [a] -> [a]
++ Polarity -> String
funName (forall state a. ActionWithPolarity state a -> Polarity
polarity ActionWithPolarity state a
act) forall a. [a] -> [a] -> [a]
++ String
" $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act)
instance Show (WithUsedVars (Step state)) where
show :: WithUsedVars (Step state) -> String
show (WithUsedVars VarContext
ctx (Var a
var := ActionWithPolarity state a
act)) =
if forall a. Typeable a => Var a -> VarContext -> Bool
isWellTyped Var a
var VarContext
ctx
then forall a. Show a => a -> String
show Var a
var forall a. [a] -> [a] -> [a]
++ String
" <- " forall a. [a] -> [a] -> [a]
++ Polarity -> String
funName (forall state a. ActionWithPolarity state a -> Polarity
polarity ActionWithPolarity state a
act) forall a. [a] -> [a] -> [a]
++ String
" $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act)
else Polarity -> String
funName (forall state a. ActionWithPolarity state a -> Polarity
polarity ActionWithPolarity state a
act) forall a. [a] -> [a] -> [a]
++ String
" $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act)
instance Eq (Step state) where
(Var a
v := ActionWithPolarity state a
act) == :: Step state -> Step state -> Bool
== (Var a
v' := ActionWithPolarity state a
act') =
forall a b. Var a -> Var b
unsafeCoerceVar Var a
v forall a. Eq a => a -> a -> Bool
== Var a
v' Bool -> Bool -> Bool
&& forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity state a
act forall a. Eq a => a -> a -> Bool
== forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity state a
act'
data Actions state = Actions_ [String] (Smart [Step state])
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall state x. Rep (Actions state) x -> Actions state
forall state x. Actions state -> Rep (Actions state) x
$cto :: forall state x. Rep (Actions state) x -> Actions state
$cfrom :: forall state x. Actions state -> Rep (Actions state) x
Generic)
pattern Actions :: [Step state] -> Actions state
pattern $bActions :: forall state. [Step state] -> Actions state
$mActions :: forall {r} {state}.
Actions state -> ([Step state] -> r) -> ((# #) -> r) -> r
Actions as <-
Actions_ _ (Smart _ as)
where
Actions [Step state]
as = forall state. [String] -> Smart [Step state] -> Actions state
Actions_ [] (forall a. Int -> a -> Smart a
Smart Int
0 [Step state]
as)
{-# COMPLETE Actions #-}
instance Semigroup (Actions state) where
Actions_ [String]
rs (Smart Int
k [Step state]
as) <> :: Actions state -> Actions state -> Actions state
<> Actions_ [String]
rs' (Smart Int
_ [Step state]
as') = forall state. [String] -> Smart [Step state] -> Actions state
Actions_ ([String]
rs forall a. [a] -> [a] -> [a]
++ [String]
rs') (forall a. Int -> a -> Smart a
Smart Int
k ([Step state]
as forall a. Semigroup a => a -> a -> a
<> [Step state]
as'))
instance Eq (Actions state) where
Actions [Step state]
as == :: Actions state -> Actions state -> Bool
== Actions [Step state]
as' = [Step state]
as forall a. Eq a => a -> a -> Bool
== [Step state]
as'
instance StateModel state => Show (Actions state) where
show :: Actions state -> String
show (Actions [Step state]
as) =
let as' :: [WithUsedVars (Step state)]
as' = forall a. VarContext -> a -> WithUsedVars a
WithUsedVars (forall state. StateModel state => Actions state -> VarContext
usedVariables (forall state. [Step state] -> Actions state
Actions [Step state]
as)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Step state]
as
in forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. [a] -> [a] -> [a]
(++) (String
"do " forall a. a -> [a] -> [a]
: forall a. a -> [a]
repeat String
" ") (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [WithUsedVars (Step state)]
as' forall a. [a] -> [a] -> [a]
++ [String
"pure ()"])
usedVariables :: forall state. StateModel state => Actions state -> VarContext
usedVariables :: forall state. StateModel state => Actions state -> VarContext
usedVariables (Actions [Step state]
as) = Annotated state -> [Step state] -> VarContext
go forall state. StateModel state => Annotated state
initialAnnotatedState [Step state]
as
where
go :: Annotated state -> [Step state] -> VarContext
go :: Annotated state -> [Step state] -> VarContext
go Annotated state
aState [] = forall a. HasVariables a => a -> VarContext
allVariables (forall state. Annotated state -> state
underlyingState Annotated state
aState)
go Annotated state
aState ((Var a
var := ActionWithPolarity state a
act) : [Step state]
steps) =
forall a. HasVariables a => a -> VarContext
allVariables (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act)
forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> VarContext
allVariables (forall state. Annotated state -> state
underlyingState Annotated state
aState)
forall a. Semigroup a => a -> a -> a
<> Annotated state -> [Step state] -> VarContext
go (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated state
aState ActionWithPolarity state a
act Var a
var) [Step state]
steps
instance forall state. StateModel state => Arbitrary (Actions state) where
arbitrary :: Gen (Actions state)
arbitrary = do
([Step state]
as, [String]
rejected) <- Annotated state -> Int -> Gen ([Step state], [String])
arbActions forall state. StateModel state => Annotated state
initialAnnotatedState Int
1
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall state. [String] -> Smart [Step state] -> Actions state
Actions_ [String]
rejected (forall a. Int -> a -> Smart a
Smart Int
0 [Step state]
as)
where
arbActions :: Annotated state -> Int -> Gen ([Step state], [String])
arbActions :: Annotated state -> Int -> Gen ([Step state], [String])
arbActions Annotated state
s Int
step = forall a. (Int -> Gen a) -> Gen a
sized forall a b. (a -> b) -> a -> b
$ \Int
n ->
let w :: Int
w = Int
n forall a. Integral a => a -> a -> a
`div` Int
2 forall a. Num a => a -> a -> a
+ Int
1
in forall a. [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, forall (m :: * -> *) a. Monad m => a -> m a
return ([], []))
,
( Int
w
, do
(Maybe (Any (ActionWithPolarity state))
mact, [String]
rej) <- Gen (Maybe (Any (ActionWithPolarity state)), [String])
satisfyPrecondition
case Maybe (Any (ActionWithPolarity state))
mact of
Just (Some act :: ActionWithPolarity state a
act@ActionWithPolarity{}) -> do
let var :: Var a
var = forall a. Int -> Var a
mkVar Int
step
([Step state]
as, [String]
rejected) <- Annotated state -> Int -> Gen ([Step state], [String])
arbActions (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated state
s ActionWithPolarity state a
act Var a
var) (Int
step forall a. Num a => a -> a -> a
+ Int
1)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Var a
var forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity state a
act) forall a. a -> [a] -> [a]
: [Step state]
as, [String]
rej forall a. [a] -> [a] -> [a]
++ [String]
rejected)
Maybe (Any (ActionWithPolarity state))
Nothing ->
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
)
]
where
satisfyPrecondition :: Gen (Maybe (Any (ActionWithPolarity state)), [String])
satisfyPrecondition = forall a. (Int -> Gen a) -> Gen a
sized forall a b. (a -> b) -> a -> b
$ \Int
n -> Int
-> Int
-> [String]
-> Gen (Maybe (Any (ActionWithPolarity state)), [String])
go Int
n (Int
2 forall a. Num a => a -> a -> a
* Int
n) []
go :: Int
-> Int
-> [String]
-> Gen (Maybe (Any (ActionWithPolarity state)), [String])
go Int
m Int
n [String]
rej
| Int
m forall a. Ord a => a -> a -> Bool
> Int
n = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [String]
rej)
| Bool
otherwise = do
Any (ActionWithPolarity state)
a <- forall a. Int -> Gen a -> Gen a
resize Int
m forall a b. (a -> b) -> a -> b
$ forall state.
StateModel state =>
Annotated state -> Gen (Any (ActionWithPolarity state))
computeArbitraryAction Annotated state
s
case Any (ActionWithPolarity state)
a of
Some ActionWithPolarity state a
act ->
if forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated state
s ActionWithPolarity state a
act
then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity state a
act), [String]
rej)
else Int
-> Int
-> [String]
-> Gen (Maybe (Any (ActionWithPolarity state)), [String])
go (Int
m forall a. Num a => a -> a -> a
+ Int
1) Int
n (forall state a. StateModel state => Action state a -> String
actionName (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act) forall a. a -> [a] -> [a]
: [String]
rej)
shrink :: Actions state -> [Actions state]
shrink (Actions_ [String]
rs Smart [Step state]
as) =
forall a b. (a -> b) -> [a] -> [b]
map (forall state. [String] -> Smart [Step state] -> Actions state
Actions_ [String]
rs) (forall a. (a -> [a]) -> Smart a -> [Smart a]
shrinkSmart (forall a b. (a -> b) -> [a] -> [b]
map (forall state. StateModel state => [Step state] -> [Step state]
prune forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
customActionsShrinker forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (Step state, Annotated state) -> [(Step state, Annotated state)]
shrinker forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall state.
StateModel state =>
[Step state] -> [(Step state, Annotated state)]
withStates) Smart [Step state]
as)
where
shrinker :: (Step state, Annotated state) -> [(Step state, Annotated state)]
shrinker :: (Step state, Annotated state) -> [(Step state, Annotated state)]
shrinker (Var a
v := ActionWithPolarity state a
act, Annotated state
s) = [(forall a b. Var a -> Var b
unsafeCoerceVar Var a
v forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity state a
act', Annotated state
s) | Some act' :: ActionWithPolarity state a
act'@ActionWithPolarity{} <- forall state a.
(Typeable a, StateModel state) =>
Annotated state
-> ActionWithPolarity state a -> [Any (ActionWithPolarity state)]
computeShrinkAction Annotated state
s ActionWithPolarity state a
act]
customActionsShrinker :: [(Step state, Annotated state)] -> [[(Step state, Annotated state)]]
customActionsShrinker :: [(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
customActionsShrinker [(Step state, Annotated state)]
acts =
let usedVars :: Set (Any Var)
usedVars = forall a. Monoid a => [a] -> a
mconcat [forall a. HasVariables a => a -> Set (Any Var)
getAllVariables ActionWithPolarity state a
a forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set (Any Var)
getAllVariables (forall state. Annotated state -> state
underlyingState Annotated state
s) | (Var a
_ := ActionWithPolarity state a
a, Annotated state
s) <- [(Step state, Annotated state)]
acts]
binding :: (Step state, Annotated state) -> Bool
binding (Var a
v := ActionWithPolarity state a
_, Annotated state
_) = forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Var a
v forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Any Var)
usedVars
go :: [(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
go [] = [[]]
go ((Step state, Annotated state)
p : [(Step state, Annotated state)]
ps)
| (Step state, Annotated state) -> Bool
binding (Step state, Annotated state)
p = forall a b. (a -> b) -> [a] -> [b]
map ((Step state, Annotated state)
p forall a. a -> [a] -> [a]
:) ([(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
go [(Step state, Annotated state)]
ps)
| Bool
otherwise = [(Step state, Annotated state)]
ps forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ((Step state, Annotated state)
p forall a. a -> [a] -> [a]
:) ([(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
go [(Step state, Annotated state)]
ps)
in [(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
go [(Step state, Annotated state)]
acts
data Annotated state = Metadata
{ forall state. Annotated state -> VarContext
vars :: VarContext
, forall state. Annotated state -> state
underlyingState :: state
}
instance Show state => Show (Annotated state) where
show :: Annotated state -> String
show (Metadata VarContext
ctx state
s) = forall a. Show a => a -> String
show VarContext
ctx forall a. [a] -> [a] -> [a]
++ String
" |- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show state
s
initialAnnotatedState :: StateModel state => Annotated state
initialAnnotatedState :: forall state. StateModel state => Annotated state
initialAnnotatedState = forall state. VarContext -> state -> Annotated state
Metadata forall a. Monoid a => a
mempty forall state. StateModel state => state
initialState
actionWithPolarity :: (StateModel state, Eq (Action state a)) => Annotated state -> Action state a -> ActionWithPolarity state a
actionWithPolarity :: forall state a.
(StateModel state, Eq (Action state a)) =>
Annotated state -> Action state a -> ActionWithPolarity state a
actionWithPolarity Annotated state
s Action state a
a =
let p :: Polarity
p
| forall state a. StateModel state => state -> Action state a -> Bool
precondition (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a = Polarity
PosPolarity
| forall state a. StateModel state => state -> Action state a -> Bool
validFailingAction (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a = Polarity
NegPolarity
| Bool
otherwise = Polarity
PosPolarity
in forall state a.
Eq (Action state a) =>
Action state a -> Polarity -> ActionWithPolarity state a
ActionWithPolarity Action state a
a Polarity
p
computePrecondition :: StateModel state => Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition :: forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated state
s (ActionWithPolarity Action state a
a Polarity
p) =
let polarPrecondition :: Bool
polarPrecondition
| Polarity
p forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity = forall state a. StateModel state => state -> Action state a -> Bool
precondition (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a
| Bool
otherwise = forall state a. StateModel state => state -> Action state a -> Bool
validFailingAction (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a Bool -> Bool -> Bool
&& Bool -> Bool
not (forall state a. StateModel state => state -> Action state a -> Bool
precondition (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a)
in forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Some Var a
v) -> Var a
v forall a. Typeable a => Var a -> VarContext -> Bool
`isWellTyped` forall state. Annotated state -> VarContext
vars Annotated state
s) (forall a. HasVariables a => a -> Set (Any Var)
getAllVariables Action state a
a)
Bool -> Bool -> Bool
&& Bool
polarPrecondition
computeNextState
:: (StateModel state, Typeable a)
=> Annotated state
-> ActionWithPolarity state a
-> Var a
-> Annotated state
computeNextState :: forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated state
s ActionWithPolarity state a
a Var a
v
| forall state a. ActionWithPolarity state a -> Polarity
polarity ActionWithPolarity state a
a forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity = forall state. VarContext -> state -> Annotated state
Metadata (forall a. Typeable a => VarContext -> Var a -> VarContext
extendContext (forall state. Annotated state -> VarContext
vars Annotated state
s) Var a
v) (forall state a.
(StateModel state, Typeable a) =>
state -> Action state a -> Var a -> state
nextState (forall state. Annotated state -> state
underlyingState Annotated state
s) (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
a) Var a
v)
| Bool
otherwise = forall state. VarContext -> state -> Annotated state
Metadata (forall state. Annotated state -> VarContext
vars Annotated state
s) (forall state a.
(StateModel state, Typeable a) =>
state -> Action state a -> state
failureNextState (forall state. Annotated state -> state
underlyingState Annotated state
s) (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
a))
computeArbitraryAction
:: StateModel state
=> Annotated state
-> Gen (Any (ActionWithPolarity state))
computeArbitraryAction :: forall state.
StateModel state =>
Annotated state -> Gen (Any (ActionWithPolarity state))
computeArbitraryAction Annotated state
s = do
Some Action state a
a <- forall state.
StateModel state =>
VarContext -> state -> Gen (Any (Action state))
arbitraryAction (forall state. Annotated state -> VarContext
vars Annotated state
s) (forall state. Annotated state -> state
underlyingState Annotated state
s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some forall a b. (a -> b) -> a -> b
$ forall state a.
(StateModel state, Eq (Action state a)) =>
Annotated state -> Action state a -> ActionWithPolarity state a
actionWithPolarity Annotated state
s Action state a
a
computeShrinkAction
:: forall state a
. (Typeable a, StateModel state)
=> Annotated state
-> ActionWithPolarity state a
-> [Any (ActionWithPolarity state)]
computeShrinkAction :: forall state a.
(Typeable a, StateModel state) =>
Annotated state
-> ActionWithPolarity state a -> [Any (ActionWithPolarity state)]
computeShrinkAction Annotated state
s (ActionWithPolarity Action state a
a Polarity
_) =
[forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (forall state a.
(StateModel state, Eq (Action state a)) =>
Annotated state -> Action state a -> ActionWithPolarity state a
actionWithPolarity Annotated state
s Action state a
a') | Some Action state a
a' <- forall state a.
(StateModel state, Typeable a) =>
VarContext -> state -> Action state a -> [Any (Action state)]
shrinkAction (forall state. Annotated state -> VarContext
vars Annotated state
s) (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a]
prune :: forall state. StateModel state => [Step state] -> [Step state]
prune :: forall state. StateModel state => [Step state] -> [Step state]
prune = Annotated state -> [Step state] -> [Step state]
loop forall state. StateModel state => Annotated state
initialAnnotatedState
where
loop :: Annotated state -> [Step state] -> [Step state]
loop Annotated state
_s [] = []
loop Annotated state
s ((Var a
var := ActionWithPolarity state a
act) : [Step state]
as)
| forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition @state Annotated state
s ActionWithPolarity state a
act =
(Var a
var forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity state a
act) forall a. a -> [a] -> [a]
: Annotated state -> [Step state] -> [Step state]
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated state
s ActionWithPolarity state a
act Var a
var) [Step state]
as
| Bool
otherwise =
Annotated state -> [Step state] -> [Step state]
loop Annotated state
s [Step state]
as
withStates :: forall state. StateModel state => [Step state] -> [(Step state, Annotated state)]
withStates :: forall state.
StateModel state =>
[Step state] -> [(Step state, Annotated state)]
withStates = Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop forall state. StateModel state => Annotated state
initialAnnotatedState
where
loop :: Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop Annotated state
_s [] = []
loop Annotated state
s ((Var a
var := ActionWithPolarity state a
act) : [Step state]
as) =
(Var a
var forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity state a
act, Annotated state
s) forall a. a -> [a] -> [a]
: Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState @state Annotated state
s ActionWithPolarity state a
act Var a
var) [Step state]
as
stateAfter :: forall state. StateModel state => Actions state -> Annotated state
stateAfter :: forall state. StateModel state => Actions state -> Annotated state
stateAfter (Actions [Step state]
actions) = Annotated state -> [Step state] -> Annotated state
loop forall state. StateModel state => Annotated state
initialAnnotatedState [Step state]
actions
where
loop :: Annotated state -> [Step state] -> Annotated state
loop Annotated state
s [] = Annotated state
s
loop Annotated state
s ((Var a
var := ActionWithPolarity state a
act) : [Step state]
as) = Annotated state -> [Step state] -> Annotated state
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState @state Annotated state
s ActionWithPolarity state a
act Var a
var) [Step state]
as
runActions
:: forall state m
. (StateModel state, RunModel state m)
=> Actions state
-> PropertyM m (Annotated state, Env m)
runActions :: forall state (m :: * -> *).
(StateModel state, RunModel state m) =>
Actions state -> PropertyM m (Annotated state, Env m)
runActions (Actions_ [String]
rejected (Smart Int
_ [Step state]
actions)) = Annotated state
-> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop forall state. StateModel state => Annotated state
initialAnnotatedState [] [Step state]
actions
where
loop :: Annotated state -> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop :: Annotated state
-> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop Annotated state
_s Env m
env [] = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
rejected) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor forall a b. (a -> b) -> a -> b
$
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Actions rejected by precondition" [String]
rejected
forall (m :: * -> *) a. Monad m => a -> m a
return (Annotated state
_s, forall a. [a] -> [a]
reverse Env m
env)
loop Annotated state
s Env m
env ((Var a
v := ActionWithPolarity state a
act) : [Step state]
as) = do
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
pre forall a b. (a -> b) -> a -> b
$ forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated state
s ActionWithPolarity state a
act
Realized m a
ret <- forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run forall a b. (a -> b) -> a -> b
$ forall state (m :: * -> *) a.
(RunModel state m, Typeable a) =>
state -> Action state a -> LookUp m -> m (Realized m a)
perform (forall state. Annotated state -> state
underlyingState Annotated state
s) (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act) (forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env)
let name :: String
name = forall a. Show a => a -> String
show (forall state a. ActionWithPolarity state a -> Polarity
polarity ActionWithPolarity state a
act) forall a. [a] -> [a] -> [a]
++ forall state a. StateModel state => Action state a -> String
actionName (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act)
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor forall a b. (a -> b) -> a -> b
$ forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Actions" [String
name]
let var :: Var a
var = forall a b. Var a -> Var b
unsafeCoerceVar Var a
v
s' :: Annotated state
s' = forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated state
s ActionWithPolarity state a
act Var a
var
env' :: Env m
env' = (Var a
var forall a (m :: * -> *).
Typeable a =>
Var a -> Realized m a -> EnvEntry m
:== Realized m a
ret) forall a. a -> [a] -> [a]
: Env m
env
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor forall a b. (a -> b) -> a -> b
$ forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Action polarity" [forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall state a. ActionWithPolarity state a -> Polarity
polarity ActionWithPolarity state a
act]
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor forall a b. (a -> b) -> a -> b
$ forall state (m :: * -> *) a.
RunModel state m =>
(state, state)
-> Action state a
-> LookUp m
-> Realized m a
-> Property
-> Property
monitoring @state @m (forall state. Annotated state -> state
underlyingState Annotated state
s, forall state. Annotated state -> state
underlyingState Annotated state
s') (forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act) (forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env') Realized m a
ret
(Bool
b, (Endo Property -> Property
mon, Endo Property -> Property
onFail)) <-
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
PostconditionM m a -> WriterT (Endo Property, Endo Property) m a
runPost
forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) state a.
RunModel state m =>
(state, state)
-> ActionWithPolarity state a
-> LookUp m
-> Realized m a
-> PostconditionM m Bool
computePostcondition @m
(forall state. Annotated state -> state
underlyingState Annotated state
s, forall state. Annotated state -> state
underlyingState Annotated state
s')
ActionWithPolarity state a
act
(forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env)
Realized m a
ret
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor Property -> Property
mon
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor Property -> Property
onFail
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert Bool
b
Annotated state
-> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop Annotated state
s' Env m
env' [Step state]
as