{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
module Hedgehog.Internal.State (
Var(..)
, concrete
, opaque
, Concrete(..)
, Symbolic(..)
, Name(..)
, Environment(..)
, EnvironmentError(..)
, emptyEnvironment
, insertConcrete
, reifyDynamic
, reifyEnvironment
, reify
, Command(..)
, Callback(..)
, commandGenOK
, Action(..)
, Sequential(..)
, Parallel(..)
, takeVariables
, variablesOK
, dropInvalid
, action
, sequential
, parallel
, executeSequential
, executeParallel
) where
import qualified Control.Concurrent.Async.Lifted as Async
import Control.Monad (foldM, foldM_)
import Control.Monad.Catch (MonadCatch)
import Control.Monad.State.Class (MonadState, get, put, modify)
import Control.Monad.Morph (MFunctor(..))
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Control (MonadBaseControl)
import Control.Monad.Trans.State (State, runState, execState)
import Control.Monad.Trans.State (StateT(..), evalStateT, runStateT)
import Data.Dynamic (Dynamic, toDyn, fromDynamic, dynTypeRep)
import Data.Foldable (traverse_)
import Data.Functor.Classes (Eq1(..), Ord1(..), Show1(..))
import Data.Functor.Classes (eq1, compare1, showsPrec1)
import Data.Kind (Type)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Maybe as Maybe
import Data.Typeable (Typeable, TypeRep, Proxy(..), typeRep)
import Hedgehog.Internal.Barbie (FunctorB(..), TraversableB(..))
import Hedgehog.Internal.Distributive (distributeT)
import Hedgehog.Internal.Gen (MonadGen, GenT, GenBase)
import qualified Hedgehog.Internal.Gen as Gen
import Hedgehog.Internal.Opaque (Opaque(..))
import Hedgehog.Internal.Property (MonadTest(..), Test, evalEither, evalM, success, runTest, failWith, annotate)
import Hedgehog.Internal.Range (Range)
import Hedgehog.Internal.Show (showPretty)
import Hedgehog.Internal.Source (HasCallStack, withFrozenCallStack)
newtype Name =
Name Int
deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq, Eq Name
Eq Name
-> (Name -> Name -> Ordering)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> Ord Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
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 :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmax :: Name -> Name -> Name
>= :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c< :: Name -> Name -> Bool
compare :: Name -> Name -> Ordering
$ccompare :: Name -> Name -> Ordering
$cp1Ord :: Eq Name
Ord, Integer -> Name
Name -> Name
Name -> Name -> Name
(Name -> Name -> Name)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> (Name -> Name)
-> (Name -> Name)
-> (Name -> Name)
-> (Integer -> Name)
-> Num Name
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Name
$cfromInteger :: Integer -> Name
signum :: Name -> Name
$csignum :: Name -> Name
abs :: Name -> Name
$cabs :: Name -> Name
negate :: Name -> Name
$cnegate :: Name -> Name
* :: Name -> Name -> Name
$c* :: Name -> Name -> Name
- :: Name -> Name -> Name
$c- :: Name -> Name -> Name
+ :: Name -> Name -> Name
$c+ :: Name -> Name -> Name
Num)
instance Show Name where
showsPrec :: Int -> Name -> ShowS
showsPrec Int
p (Name Int
x) =
Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Int
x
data Symbolic a where
Symbolic :: Typeable a => Name -> Symbolic a
deriving instance Eq (Symbolic a)
deriving instance Ord (Symbolic a)
instance Show (Symbolic a) where
showsPrec :: Int -> Symbolic a -> ShowS
showsPrec Int
p (Symbolic Name
x) =
Int -> Name -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Name
x
instance Show1 Symbolic where
liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Symbolic a -> ShowS
liftShowsPrec Int -> a -> ShowS
_ [a] -> ShowS
_ Int
p (Symbolic Name
x) =
Int -> Name -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Name
x
instance Eq1 Symbolic where
liftEq :: (a -> b -> Bool) -> Symbolic a -> Symbolic b -> Bool
liftEq a -> b -> Bool
_ (Symbolic Name
x) (Symbolic Name
y) =
Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
instance Ord1 Symbolic where
liftCompare :: (a -> b -> Ordering) -> Symbolic a -> Symbolic b -> Ordering
liftCompare a -> b -> Ordering
_ (Symbolic Name
x) (Symbolic Name
y) =
Name -> Name -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Name
x Name
y
newtype Concrete a where
Concrete :: a -> Concrete a
deriving (Concrete a -> Concrete a -> Bool
(Concrete a -> Concrete a -> Bool)
-> (Concrete a -> Concrete a -> Bool) -> Eq (Concrete a)
forall a. Eq a => Concrete a -> Concrete a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Concrete a -> Concrete a -> Bool
$c/= :: forall a. Eq a => Concrete a -> Concrete a -> Bool
== :: Concrete a -> Concrete a -> Bool
$c== :: forall a. Eq a => Concrete a -> Concrete a -> Bool
Eq, Eq (Concrete a)
Eq (Concrete a)
-> (Concrete a -> Concrete a -> Ordering)
-> (Concrete a -> Concrete a -> Bool)
-> (Concrete a -> Concrete a -> Bool)
-> (Concrete a -> Concrete a -> Bool)
-> (Concrete a -> Concrete a -> Bool)
-> (Concrete a -> Concrete a -> Concrete a)
-> (Concrete a -> Concrete a -> Concrete a)
-> Ord (Concrete a)
Concrete a -> Concrete a -> Bool
Concrete a -> Concrete a -> Ordering
Concrete a -> Concrete a -> Concrete a
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
forall a. Ord a => Eq (Concrete a)
forall a. Ord a => Concrete a -> Concrete a -> Bool
forall a. Ord a => Concrete a -> Concrete a -> Ordering
forall a. Ord a => Concrete a -> Concrete a -> Concrete a
min :: Concrete a -> Concrete a -> Concrete a
$cmin :: forall a. Ord a => Concrete a -> Concrete a -> Concrete a
max :: Concrete a -> Concrete a -> Concrete a
$cmax :: forall a. Ord a => Concrete a -> Concrete a -> Concrete a
>= :: Concrete a -> Concrete a -> Bool
$c>= :: forall a. Ord a => Concrete a -> Concrete a -> Bool
> :: Concrete a -> Concrete a -> Bool
$c> :: forall a. Ord a => Concrete a -> Concrete a -> Bool
<= :: Concrete a -> Concrete a -> Bool
$c<= :: forall a. Ord a => Concrete a -> Concrete a -> Bool
< :: Concrete a -> Concrete a -> Bool
$c< :: forall a. Ord a => Concrete a -> Concrete a -> Bool
compare :: Concrete a -> Concrete a -> Ordering
$ccompare :: forall a. Ord a => Concrete a -> Concrete a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Concrete a)
Ord, a -> Concrete b -> Concrete a
(a -> b) -> Concrete a -> Concrete b
(forall a b. (a -> b) -> Concrete a -> Concrete b)
-> (forall a b. a -> Concrete b -> Concrete a) -> Functor Concrete
forall a b. a -> Concrete b -> Concrete a
forall a b. (a -> b) -> Concrete a -> Concrete b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Concrete b -> Concrete a
$c<$ :: forall a b. a -> Concrete b -> Concrete a
fmap :: (a -> b) -> Concrete a -> Concrete b
$cfmap :: forall a b. (a -> b) -> Concrete a -> Concrete b
Functor, Concrete a -> Bool
(a -> m) -> Concrete a -> m
(a -> b -> b) -> b -> Concrete a -> b
(forall m. Monoid m => Concrete m -> m)
-> (forall m a. Monoid m => (a -> m) -> Concrete a -> m)
-> (forall m a. Monoid m => (a -> m) -> Concrete a -> m)
-> (forall a b. (a -> b -> b) -> b -> Concrete a -> b)
-> (forall a b. (a -> b -> b) -> b -> Concrete a -> b)
-> (forall b a. (b -> a -> b) -> b -> Concrete a -> b)
-> (forall b a. (b -> a -> b) -> b -> Concrete a -> b)
-> (forall a. (a -> a -> a) -> Concrete a -> a)
-> (forall a. (a -> a -> a) -> Concrete a -> a)
-> (forall a. Concrete a -> [a])
-> (forall a. Concrete a -> Bool)
-> (forall a. Concrete a -> Int)
-> (forall a. Eq a => a -> Concrete a -> Bool)
-> (forall a. Ord a => Concrete a -> a)
-> (forall a. Ord a => Concrete a -> a)
-> (forall a. Num a => Concrete a -> a)
-> (forall a. Num a => Concrete a -> a)
-> Foldable Concrete
forall a. Eq a => a -> Concrete a -> Bool
forall a. Num a => Concrete a -> a
forall a. Ord a => Concrete a -> a
forall m. Monoid m => Concrete m -> m
forall a. Concrete a -> Bool
forall a. Concrete a -> Int
forall a. Concrete a -> [a]
forall a. (a -> a -> a) -> Concrete a -> a
forall m a. Monoid m => (a -> m) -> Concrete a -> m
forall b a. (b -> a -> b) -> b -> Concrete a -> b
forall a b. (a -> b -> b) -> b -> Concrete a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Concrete a -> a
$cproduct :: forall a. Num a => Concrete a -> a
sum :: Concrete a -> a
$csum :: forall a. Num a => Concrete a -> a
minimum :: Concrete a -> a
$cminimum :: forall a. Ord a => Concrete a -> a
maximum :: Concrete a -> a
$cmaximum :: forall a. Ord a => Concrete a -> a
elem :: a -> Concrete a -> Bool
$celem :: forall a. Eq a => a -> Concrete a -> Bool
length :: Concrete a -> Int
$clength :: forall a. Concrete a -> Int
null :: Concrete a -> Bool
$cnull :: forall a. Concrete a -> Bool
toList :: Concrete a -> [a]
$ctoList :: forall a. Concrete a -> [a]
foldl1 :: (a -> a -> a) -> Concrete a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Concrete a -> a
foldr1 :: (a -> a -> a) -> Concrete a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Concrete a -> a
foldl' :: (b -> a -> b) -> b -> Concrete a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Concrete a -> b
foldl :: (b -> a -> b) -> b -> Concrete a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Concrete a -> b
foldr' :: (a -> b -> b) -> b -> Concrete a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Concrete a -> b
foldr :: (a -> b -> b) -> b -> Concrete a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Concrete a -> b
foldMap' :: (a -> m) -> Concrete a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Concrete a -> m
foldMap :: (a -> m) -> Concrete a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Concrete a -> m
fold :: Concrete m -> m
$cfold :: forall m. Monoid m => Concrete m -> m
Foldable, Functor Concrete
Foldable Concrete
Functor Concrete
-> Foldable Concrete
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Concrete a -> f (Concrete b))
-> (forall (f :: * -> *) a.
Applicative f =>
Concrete (f a) -> f (Concrete a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Concrete a -> m (Concrete b))
-> (forall (m :: * -> *) a.
Monad m =>
Concrete (m a) -> m (Concrete a))
-> Traversable Concrete
(a -> f b) -> Concrete a -> f (Concrete b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Concrete (m a) -> m (Concrete a)
forall (f :: * -> *) a.
Applicative f =>
Concrete (f a) -> f (Concrete a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Concrete a -> m (Concrete b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Concrete a -> f (Concrete b)
sequence :: Concrete (m a) -> m (Concrete a)
$csequence :: forall (m :: * -> *) a. Monad m => Concrete (m a) -> m (Concrete a)
mapM :: (a -> m b) -> Concrete a -> m (Concrete b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Concrete a -> m (Concrete b)
sequenceA :: Concrete (f a) -> f (Concrete a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Concrete (f a) -> f (Concrete a)
traverse :: (a -> f b) -> Concrete a -> f (Concrete b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Concrete a -> f (Concrete b)
$cp2Traversable :: Foldable Concrete
$cp1Traversable :: Functor Concrete
Traversable)
instance Show a => Show (Concrete a) where
showsPrec :: Int -> Concrete a -> ShowS
showsPrec =
Int -> Concrete a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1
instance Show1 Concrete where
liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Concrete a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
_ Int
p (Concrete a
x) =
Int -> a -> ShowS
sp Int
p a
x
instance Eq1 Concrete where
liftEq :: (a -> b -> Bool) -> Concrete a -> Concrete b -> Bool
liftEq a -> b -> Bool
eq (Concrete a
x) (Concrete b
y) =
a -> b -> Bool
eq a
x b
y
instance Ord1 Concrete where
liftCompare :: (a -> b -> Ordering) -> Concrete a -> Concrete b -> Ordering
liftCompare a -> b -> Ordering
comp (Concrete a
x) (Concrete b
y) =
a -> b -> Ordering
comp a
x b
y
newtype Var a v =
Var (v a)
concrete :: Var a Concrete -> a
concrete :: Var a Concrete -> a
concrete (Var (Concrete a
x)) =
a
x
opaque :: Var (Opaque a) Concrete -> a
opaque :: Var (Opaque a) Concrete -> a
opaque (Var (Concrete (Opaque a
x))) =
a
x
instance (Eq a, Eq1 v) => Eq (Var a v) where
== :: Var a v -> Var a v -> Bool
(==) (Var v a
x) (Var v a
y) =
v a -> v a -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1 v a
x v a
y
instance (Ord a, Ord1 v) => Ord (Var a v) where
compare :: Var a v -> Var a v -> Ordering
compare (Var v a
x) (Var v a
y) =
v a -> v a -> Ordering
forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1 v a
x v a
y
instance (Show a, Show1 v) => Show (Var a v) where
showsPrec :: Int -> Var a v -> ShowS
showsPrec Int
p (Var v a
x) =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"Var " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> v a -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1 Int
11 v a
x
instance FunctorB (Var a) where
bmap :: (forall a. f a -> g a) -> Var a f -> Var a g
bmap forall a. f a -> g a
f (Var f a
v) =
g a -> Var a g
forall a (v :: * -> *). v a -> Var a v
Var (f a -> g a
forall a. f a -> g a
f f a
v)
instance TraversableB (Var a) where
btraverse :: (forall a. f a -> e (g a)) -> Var a f -> e (Var a g)
btraverse forall a. f a -> e (g a)
f (Var f a
v) =
(g a -> Var a g) -> e (g a) -> e (Var a g)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g a -> Var a g
forall a (v :: * -> *). v a -> Var a v
Var (f a -> e (g a)
forall a. f a -> e (g a)
f f a
v)
newtype Environment =
Environment {
Environment -> Map Name Dynamic
unEnvironment :: Map Name Dynamic
} deriving (Int -> Environment -> ShowS
[Environment] -> ShowS
Environment -> String
(Int -> Environment -> ShowS)
-> (Environment -> String)
-> ([Environment] -> ShowS)
-> Show Environment
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Environment] -> ShowS
$cshowList :: [Environment] -> ShowS
show :: Environment -> String
$cshow :: Environment -> String
showsPrec :: Int -> Environment -> ShowS
$cshowsPrec :: Int -> Environment -> ShowS
Show)
data EnvironmentError =
EnvironmentValueNotFound !Name
| EnvironmentTypeError !TypeRep !TypeRep
deriving (EnvironmentError -> EnvironmentError -> Bool
(EnvironmentError -> EnvironmentError -> Bool)
-> (EnvironmentError -> EnvironmentError -> Bool)
-> Eq EnvironmentError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EnvironmentError -> EnvironmentError -> Bool
$c/= :: EnvironmentError -> EnvironmentError -> Bool
== :: EnvironmentError -> EnvironmentError -> Bool
$c== :: EnvironmentError -> EnvironmentError -> Bool
Eq, Eq EnvironmentError
Eq EnvironmentError
-> (EnvironmentError -> EnvironmentError -> Ordering)
-> (EnvironmentError -> EnvironmentError -> Bool)
-> (EnvironmentError -> EnvironmentError -> Bool)
-> (EnvironmentError -> EnvironmentError -> Bool)
-> (EnvironmentError -> EnvironmentError -> Bool)
-> (EnvironmentError -> EnvironmentError -> EnvironmentError)
-> (EnvironmentError -> EnvironmentError -> EnvironmentError)
-> Ord EnvironmentError
EnvironmentError -> EnvironmentError -> Bool
EnvironmentError -> EnvironmentError -> Ordering
EnvironmentError -> EnvironmentError -> EnvironmentError
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 :: EnvironmentError -> EnvironmentError -> EnvironmentError
$cmin :: EnvironmentError -> EnvironmentError -> EnvironmentError
max :: EnvironmentError -> EnvironmentError -> EnvironmentError
$cmax :: EnvironmentError -> EnvironmentError -> EnvironmentError
>= :: EnvironmentError -> EnvironmentError -> Bool
$c>= :: EnvironmentError -> EnvironmentError -> Bool
> :: EnvironmentError -> EnvironmentError -> Bool
$c> :: EnvironmentError -> EnvironmentError -> Bool
<= :: EnvironmentError -> EnvironmentError -> Bool
$c<= :: EnvironmentError -> EnvironmentError -> Bool
< :: EnvironmentError -> EnvironmentError -> Bool
$c< :: EnvironmentError -> EnvironmentError -> Bool
compare :: EnvironmentError -> EnvironmentError -> Ordering
$ccompare :: EnvironmentError -> EnvironmentError -> Ordering
$cp1Ord :: Eq EnvironmentError
Ord, Int -> EnvironmentError -> ShowS
[EnvironmentError] -> ShowS
EnvironmentError -> String
(Int -> EnvironmentError -> ShowS)
-> (EnvironmentError -> String)
-> ([EnvironmentError] -> ShowS)
-> Show EnvironmentError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EnvironmentError] -> ShowS
$cshowList :: [EnvironmentError] -> ShowS
show :: EnvironmentError -> String
$cshow :: EnvironmentError -> String
showsPrec :: Int -> EnvironmentError -> ShowS
$cshowsPrec :: Int -> EnvironmentError -> ShowS
Show)
emptyEnvironment :: Environment
emptyEnvironment :: Environment
emptyEnvironment =
Map Name Dynamic -> Environment
Environment Map Name Dynamic
forall k a. Map k a
Map.empty
unionsEnvironment :: [Environment] -> Environment
unionsEnvironment :: [Environment] -> Environment
unionsEnvironment =
Map Name Dynamic -> Environment
Environment (Map Name Dynamic -> Environment)
-> ([Environment] -> Map Name Dynamic)
-> [Environment]
-> Environment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Map Name Dynamic] -> Map Name Dynamic
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ([Map Name Dynamic] -> Map Name Dynamic)
-> ([Environment] -> [Map Name Dynamic])
-> [Environment]
-> Map Name Dynamic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Environment -> Map Name Dynamic)
-> [Environment] -> [Map Name Dynamic]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Environment -> Map Name Dynamic
unEnvironment
insertConcrete :: Symbolic a -> Concrete a -> Environment -> Environment
insertConcrete :: Symbolic a -> Concrete a -> Environment -> Environment
insertConcrete (Symbolic Name
k) (Concrete a
v) =
Map Name Dynamic -> Environment
Environment (Map Name Dynamic -> Environment)
-> (Environment -> Map Name Dynamic) -> Environment -> Environment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Dynamic -> Map Name Dynamic -> Map Name Dynamic
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
k (a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a
v) (Map Name Dynamic -> Map Name Dynamic)
-> (Environment -> Map Name Dynamic)
-> Environment
-> Map Name Dynamic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Environment -> Map Name Dynamic
unEnvironment
reifyDynamic :: forall a. Typeable a => Dynamic -> Either EnvironmentError (Concrete a)
reifyDynamic :: Dynamic -> Either EnvironmentError (Concrete a)
reifyDynamic Dynamic
dyn =
case Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn of
Maybe a
Nothing ->
EnvironmentError -> Either EnvironmentError (Concrete a)
forall a b. a -> Either a b
Left (EnvironmentError -> Either EnvironmentError (Concrete a))
-> EnvironmentError -> Either EnvironmentError (Concrete a)
forall a b. (a -> b) -> a -> b
$ TypeRep -> TypeRep -> EnvironmentError
EnvironmentTypeError (Proxy a -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) (Dynamic -> TypeRep
dynTypeRep Dynamic
dyn)
Just a
x ->
Concrete a -> Either EnvironmentError (Concrete a)
forall a b. b -> Either a b
Right (Concrete a -> Either EnvironmentError (Concrete a))
-> Concrete a -> Either EnvironmentError (Concrete a)
forall a b. (a -> b) -> a -> b
$ a -> Concrete a
forall a. a -> Concrete a
Concrete a
x
reifyEnvironment :: Environment -> (forall a. Symbolic a -> Either EnvironmentError (Concrete a))
reifyEnvironment :: Environment
-> forall a. Symbolic a -> Either EnvironmentError (Concrete a)
reifyEnvironment (Environment Map Name Dynamic
vars) (Symbolic Name
n) =
case Name -> Map Name Dynamic -> Maybe Dynamic
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name Dynamic
vars of
Maybe Dynamic
Nothing ->
EnvironmentError -> Either EnvironmentError (Concrete a)
forall a b. a -> Either a b
Left (EnvironmentError -> Either EnvironmentError (Concrete a))
-> EnvironmentError -> Either EnvironmentError (Concrete a)
forall a b. (a -> b) -> a -> b
$ Name -> EnvironmentError
EnvironmentValueNotFound Name
n
Just Dynamic
dyn ->
Dynamic -> Either EnvironmentError (Concrete a)
forall a.
Typeable a =>
Dynamic -> Either EnvironmentError (Concrete a)
reifyDynamic Dynamic
dyn
reify :: TraversableB t => Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify :: Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify Environment
vars =
(forall a. Symbolic a -> Either EnvironmentError (Concrete a))
-> t Symbolic -> Either EnvironmentError (t Concrete)
forall k (b :: (k -> *) -> *) (e :: * -> *) (f :: k -> *)
(g :: k -> *).
(TraversableB b, Applicative e) =>
(forall (a :: k). f a -> e (g a)) -> b f -> e (b g)
btraverse (Environment
-> forall a. Symbolic a -> Either EnvironmentError (Concrete a)
reifyEnvironment Environment
vars)
data Callback input output state =
Require (state Symbolic -> input Symbolic -> Bool)
| Update (forall v. Ord1 v => state v -> input v -> Var output v -> state v)
| Ensure (state Concrete -> state Concrete -> input Concrete -> output -> Test ())
callbackRequire1 ::
state Symbolic
-> input Symbolic
-> Callback input output state
-> Bool
callbackRequire1 :: state Symbolic
-> input Symbolic -> Callback input output state -> Bool
callbackRequire1 state Symbolic
s input Symbolic
i = \case
Require state Symbolic -> input Symbolic -> Bool
f ->
state Symbolic -> input Symbolic -> Bool
f state Symbolic
s input Symbolic
i
Update forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
_ ->
Bool
True
Ensure state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_ ->
Bool
True
callbackUpdate1 ::
Ord1 v
=> state v
-> input v
-> Var output v
-> Callback input output state
-> state v
callbackUpdate1 :: state v
-> input v
-> Var output v
-> Callback input output state
-> state v
callbackUpdate1 state v
s input v
i Var output v
o = \case
Require state Symbolic -> input Symbolic -> Bool
_ ->
state v
s
Update forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
f ->
state v -> input v -> Var output v -> state v
forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
f state v
s input v
i Var output v
o
Ensure state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_ ->
state v
s
callbackEnsure1 ::
state Concrete
-> state Concrete
-> input Concrete
-> output
-> Callback input output state
-> Test ()
callbackEnsure1 :: state Concrete
-> state Concrete
-> input Concrete
-> output
-> Callback input output state
-> Test ()
callbackEnsure1 state Concrete
s0 state Concrete
s input Concrete
i output
o = \case
Require state Symbolic -> input Symbolic -> Bool
_ ->
Test ()
forall (m :: * -> *). MonadTest m => m ()
success
Update forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
_ ->
Test ()
forall (m :: * -> *). MonadTest m => m ()
success
Ensure state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
f ->
state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
f state Concrete
s0 state Concrete
s input Concrete
i output
o
callbackRequire ::
[Callback input output state]
-> state Symbolic
-> input Symbolic
-> Bool
callbackRequire :: [Callback input output state]
-> state Symbolic -> input Symbolic -> Bool
callbackRequire [Callback input output state]
callbacks state Symbolic
s input Symbolic
i =
(Callback input output state -> Bool)
-> [Callback input output state] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (state Symbolic
-> input Symbolic -> Callback input output state -> Bool
forall (state :: (* -> *) -> *) (input :: (* -> *) -> *) output.
state Symbolic
-> input Symbolic -> Callback input output state -> Bool
callbackRequire1 state Symbolic
s input Symbolic
i) [Callback input output state]
callbacks
callbackUpdate ::
Ord1 v
=> [Callback input output state]
-> state v
-> input v
-> Var output v
-> state v
callbackUpdate :: [Callback input output state]
-> state v -> input v -> Var output v -> state v
callbackUpdate [Callback input output state]
callbacks state v
s0 input v
i Var output v
o =
(state v -> Callback input output state -> state v)
-> state v -> [Callback input output state] -> state v
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\state v
s -> state v
-> input v
-> Var output v
-> Callback input output state
-> state v
forall (v :: * -> *) (state :: (* -> *) -> *)
(input :: (* -> *) -> *) output.
Ord1 v =>
state v
-> input v
-> Var output v
-> Callback input output state
-> state v
callbackUpdate1 state v
s input v
i Var output v
o) state v
s0 [Callback input output state]
callbacks
callbackEnsure ::
[Callback input output state]
-> state Concrete
-> state Concrete
-> input Concrete
-> output
-> Test ()
callbackEnsure :: [Callback input output state]
-> state Concrete
-> state Concrete
-> input Concrete
-> output
-> Test ()
callbackEnsure [Callback input output state]
callbacks state Concrete
s0 state Concrete
s input Concrete
i output
o =
(Callback input output state -> Test ())
-> [Callback input output state] -> Test ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (state Concrete
-> state Concrete
-> input Concrete
-> output
-> Callback input output state
-> Test ()
forall (state :: (* -> *) -> *) (input :: (* -> *) -> *) output.
state Concrete
-> state Concrete
-> input Concrete
-> output
-> Callback input output state
-> Test ()
callbackEnsure1 state Concrete
s0 state Concrete
s input Concrete
i output
o) [Callback input output state]
callbacks
data Command gen m (state :: (Type -> Type) -> Type) =
forall input output.
(TraversableB input, Show (input Symbolic), Show output, Typeable output) =>
Command {
()
commandGen ::
state Symbolic -> Maybe (gen (input Symbolic))
, ()
commandExecute ::
input Concrete -> m output
, ()
commandCallbacks ::
[Callback input output state]
}
commandGenOK :: Command gen m state -> state Symbolic -> Bool
commandGenOK :: Command gen m state -> state Symbolic -> Bool
commandGenOK (Command state Symbolic -> Maybe (gen (input Symbolic))
inputGen input Concrete -> m output
_ [Callback input output state]
_) state Symbolic
state =
Maybe (gen (input Symbolic)) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (state Symbolic -> Maybe (gen (input Symbolic))
inputGen state Symbolic
state)
data Action m (state :: (Type -> Type) -> Type) =
forall input output.
(TraversableB input, Show (input Symbolic), Show output) =>
Action {
()
actionInput ::
input Symbolic
, ()
actionOutput ::
Symbolic output
, ()
actionExecute ::
input Concrete -> m output
, ()
actionRequire ::
state Symbolic -> input Symbolic -> Bool
, ()
actionUpdate ::
forall v. Ord1 v => state v -> input v -> Var output v -> state v
, ()
actionEnsure ::
state Concrete -> state Concrete -> input Concrete -> output -> Test ()
}
instance Show (Action m state) where
showsPrec :: Int -> Action m state -> ShowS
showsPrec Int
p (Action input Symbolic
input (Symbolic (Name Int
output)) input Concrete -> m output
_ state Symbolic -> input Symbolic -> Bool
_ forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
_ state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_) =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"Var " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Int
output ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" :<- " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> input Symbolic -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 input Symbolic
input
takeSymbolic :: forall a. Symbolic a -> (Name, TypeRep)
takeSymbolic :: Symbolic a -> (Name, TypeRep)
takeSymbolic (Symbolic Name
name) =
(Name
name, Proxy a -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a))
insertSymbolic :: Symbolic a -> Map Name TypeRep -> Map Name TypeRep
insertSymbolic :: Symbolic a -> Map Name TypeRep -> Map Name TypeRep
insertSymbolic Symbolic a
s =
let
(Name
name, TypeRep
typ) =
Symbolic a -> (Name, TypeRep)
forall a. Symbolic a -> (Name, TypeRep)
takeSymbolic Symbolic a
s
in
Name -> TypeRep -> Map Name TypeRep -> Map Name TypeRep
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
name TypeRep
typ
takeVariables :: forall t. TraversableB t => t Symbolic -> Map Name TypeRep
takeVariables :: t Symbolic -> Map Name TypeRep
takeVariables t Symbolic
xs =
let
go :: Symbolic a -> m (Symbolic a)
go Symbolic a
x = do
(Map Name TypeRep -> Map Name TypeRep) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Symbolic a -> Map Name TypeRep -> Map Name TypeRep
forall a. Symbolic a -> Map Name TypeRep -> Map Name TypeRep
insertSymbolic Symbolic a
x)
Symbolic a -> m (Symbolic a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Symbolic a
x
in
(State (Map Name TypeRep) (t Symbolic)
-> Map Name TypeRep -> Map Name TypeRep)
-> Map Name TypeRep
-> State (Map Name TypeRep) (t Symbolic)
-> Map Name TypeRep
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (Map Name TypeRep) (t Symbolic)
-> Map Name TypeRep -> Map Name TypeRep
forall s a. State s a -> s -> s
execState Map Name TypeRep
forall k a. Map k a
Map.empty (State (Map Name TypeRep) (t Symbolic) -> Map Name TypeRep)
-> State (Map Name TypeRep) (t Symbolic) -> Map Name TypeRep
forall a b. (a -> b) -> a -> b
$ (forall a.
Symbolic a -> StateT (Map Name TypeRep) Identity (Symbolic a))
-> t Symbolic -> State (Map Name TypeRep) (t Symbolic)
forall k (b :: (k -> *) -> *) (e :: * -> *) (f :: k -> *)
(g :: k -> *).
(TraversableB b, Applicative e) =>
(forall (a :: k). f a -> e (g a)) -> b f -> e (b g)
btraverse forall a.
Symbolic a -> StateT (Map Name TypeRep) Identity (Symbolic a)
forall (m :: * -> *) a.
MonadState (Map Name TypeRep) m =>
Symbolic a -> m (Symbolic a)
go t Symbolic
xs
variablesOK :: TraversableB t => t Symbolic -> Map Name TypeRep -> Bool
variablesOK :: t Symbolic -> Map Name TypeRep -> Bool
variablesOK t Symbolic
xs Map Name TypeRep
allowed =
let
vars :: Map Name TypeRep
vars =
t Symbolic -> Map Name TypeRep
forall (t :: (* -> *) -> *).
TraversableB t =>
t Symbolic -> Map Name TypeRep
takeVariables t Symbolic
xs
in
Map Name TypeRep -> Bool
forall k a. Map k a -> Bool
Map.null (Map Name TypeRep
vars Map Name TypeRep -> Map Name TypeRep -> Map Name TypeRep
forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map Name TypeRep
allowed) Bool -> Bool -> Bool
&&
Map Name Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((TypeRep -> TypeRep -> Bool)
-> Map Name TypeRep -> Map Name TypeRep -> Map Name Bool
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
(==) Map Name TypeRep
vars Map Name TypeRep
allowed)
data Context state =
Context {
Context state -> state Symbolic
contextState :: state Symbolic
, Context state -> Map Name TypeRep
_contextVars :: Map Name TypeRep
}
mkContext :: state Symbolic -> Context state
mkContext :: state Symbolic -> Context state
mkContext state Symbolic
initial =
state Symbolic -> Map Name TypeRep -> Context state
forall (state :: (* -> *) -> *).
state Symbolic -> Map Name TypeRep -> Context state
Context state Symbolic
initial Map Name TypeRep
forall k a. Map k a
Map.empty
contextUpdate :: MonadState (Context state) m => state Symbolic -> m ()
contextUpdate :: state Symbolic -> m ()
contextUpdate state Symbolic
state = do
Context state Symbolic
_ Map Name TypeRep
vars <- m (Context state)
forall s (m :: * -> *). MonadState s m => m s
get
Context state -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Context state -> m ()) -> Context state -> m ()
forall a b. (a -> b) -> a -> b
$ state Symbolic -> Map Name TypeRep -> Context state
forall (state :: (* -> *) -> *).
state Symbolic -> Map Name TypeRep -> Context state
Context state Symbolic
state Map Name TypeRep
vars
contextNewVar :: (MonadState (Context state) m, Typeable a) => m (Symbolic a)
contextNewVar :: m (Symbolic a)
contextNewVar = do
Context state Symbolic
state Map Name TypeRep
vars <- m (Context state)
forall s (m :: * -> *). MonadState s m => m s
get
let
var :: Symbolic a
var =
case Map Name TypeRep -> Maybe ((Name, TypeRep), Map Name TypeRep)
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey Map Name TypeRep
vars of
Maybe ((Name, TypeRep), Map Name TypeRep)
Nothing ->
Name -> Symbolic a
forall a. Typeable a => Name -> Symbolic a
Symbolic Name
0
Just ((Name
name, TypeRep
_), Map Name TypeRep
_) ->
Name -> Symbolic a
forall a. Typeable a => Name -> Symbolic a
Symbolic (Name
name Name -> Name -> Name
forall a. Num a => a -> a -> a
+ Name
1)
Context state -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Context state -> m ()) -> Context state -> m ()
forall a b. (a -> b) -> a -> b
$ state Symbolic -> Map Name TypeRep -> Context state
forall (state :: (* -> *) -> *).
state Symbolic -> Map Name TypeRep -> Context state
Context state Symbolic
state (Symbolic a -> Map Name TypeRep -> Map Name TypeRep
forall a. Symbolic a -> Map Name TypeRep -> Map Name TypeRep
insertSymbolic Symbolic a
var Map Name TypeRep
vars)
Symbolic a -> m (Symbolic a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Symbolic a
var
dropInvalid :: [Action m state] -> State (Context state) [Action m state]
dropInvalid :: [Action m state] -> State (Context state) [Action m state]
dropInvalid =
let
loop :: Action m state -> m (Maybe (Action m state))
loop step :: Action m state
step@(Action input Symbolic
input Symbolic output
output input Concrete -> m output
_execute state Symbolic -> input Symbolic -> Bool
require forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_ensure) = do
Context state Symbolic
state0 Map Name TypeRep
vars0 <- m (Context state)
forall s (m :: * -> *). MonadState s m => m s
get
if state Symbolic -> input Symbolic -> Bool
require state Symbolic
state0 input Symbolic
input Bool -> Bool -> Bool
&& input Symbolic -> Map Name TypeRep -> Bool
forall (t :: (* -> *) -> *).
TraversableB t =>
t Symbolic -> Map Name TypeRep -> Bool
variablesOK input Symbolic
input Map Name TypeRep
vars0 then do
let
state :: state Symbolic
state =
state Symbolic
-> input Symbolic -> Var output Symbolic -> state Symbolic
forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Symbolic
state0 input Symbolic
input (Symbolic output -> Var output Symbolic
forall a (v :: * -> *). v a -> Var a v
Var Symbolic output
output)
vars :: Map Name TypeRep
vars =
Symbolic output -> Map Name TypeRep -> Map Name TypeRep
forall a. Symbolic a -> Map Name TypeRep -> Map Name TypeRep
insertSymbolic Symbolic output
output Map Name TypeRep
vars0
Context state -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Context state -> m ()) -> Context state -> m ()
forall a b. (a -> b) -> a -> b
$ state Symbolic -> Map Name TypeRep -> Context state
forall (state :: (* -> *) -> *).
state Symbolic -> Map Name TypeRep -> Context state
Context state Symbolic
state Map Name TypeRep
vars
Maybe (Action m state) -> m (Maybe (Action m state))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Action m state) -> m (Maybe (Action m state)))
-> Maybe (Action m state) -> m (Maybe (Action m state))
forall a b. (a -> b) -> a -> b
$ Action m state -> Maybe (Action m state)
forall a. a -> Maybe a
Just Action m state
step
else
Maybe (Action m state) -> m (Maybe (Action m state))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Action m state)
forall a. Maybe a
Nothing
in
([Maybe (Action m state)] -> [Action m state])
-> StateT (Context state) Identity [Maybe (Action m state)]
-> State (Context state) [Action m state]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe (Action m state)] -> [Action m state]
forall a. [Maybe a] -> [a]
Maybe.catMaybes (StateT (Context state) Identity [Maybe (Action m state)]
-> State (Context state) [Action m state])
-> ([Action m state]
-> StateT (Context state) Identity [Maybe (Action m state)])
-> [Action m state]
-> State (Context state) [Action m state]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Action m state
-> StateT (Context state) Identity (Maybe (Action m state)))
-> [Action m state]
-> StateT (Context state) Identity [Maybe (Action m state)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Action m state
-> StateT (Context state) Identity (Maybe (Action m state))
forall (m :: * -> *) (state :: (* -> *) -> *) (m :: * -> *).
MonadState (Context state) m =>
Action m state -> m (Maybe (Action m state))
loop
action ::
(MonadGen gen, MonadTest m)
=> [Command gen m state]
-> GenT (StateT (Context state) (GenBase gen)) (Action m state)
action :: [Command gen m state]
-> GenT (StateT (Context state) (GenBase gen)) (Action m state)
action [Command gen m state]
commands =
GenT
(StateT (Context state) (GenBase gen)) (Maybe (Action m state))
-> GenT (StateT (Context state) (GenBase gen)) (Action m state)
forall (m :: * -> *) a. MonadGen m => m (Maybe a) -> m a
Gen.justT (GenT
(StateT (Context state) (GenBase gen)) (Maybe (Action m state))
-> GenT (StateT (Context state) (GenBase gen)) (Action m state))
-> GenT
(StateT (Context state) (GenBase gen)) (Maybe (Action m state))
-> GenT (StateT (Context state) (GenBase gen)) (Action m state)
forall a b. (a -> b) -> a -> b
$ do
Context state Symbolic
state0 Map Name TypeRep
_ <- GenT (StateT (Context state) (GenBase gen)) (Context state)
forall s (m :: * -> *). MonadState s m => m s
get
Command state Symbolic -> Maybe (gen (input Symbolic))
mgenInput input Concrete -> m output
exec [Callback input output state]
callbacks <-
[Command gen m state]
-> GenT
(StateT (Context state) (GenBase gen)) (Command gen m state)
forall (m :: * -> *) a. MonadGen m => [a] -> m a
Gen.element_ ([Command gen m state]
-> GenT
(StateT (Context state) (GenBase gen)) (Command gen m state))
-> [Command gen m state]
-> GenT
(StateT (Context state) (GenBase gen)) (Command gen m state)
forall a b. (a -> b) -> a -> b
$ (Command gen m state -> Bool)
-> [Command gen m state] -> [Command gen m state]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Command gen m state
c -> Command gen m state -> state Symbolic -> Bool
forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
Command gen m state -> state Symbolic -> Bool
commandGenOK Command gen m state
c state Symbolic
state0) [Command gen m state]
commands
input Symbolic
input <-
case state Symbolic -> Maybe (gen (input Symbolic))
mgenInput state Symbolic
state0 of
Maybe (gen (input Symbolic))
Nothing ->
String
-> GenT (StateT (Context state) (GenBase gen)) (input Symbolic)
forall a. HasCallStack => String -> a
error String
"genCommand: internal error, tried to use generator with invalid state."
Just gen (input Symbolic)
gen ->
(forall a. GenBase gen a -> StateT (Context state) (GenBase gen) a)
-> GenT (GenBase gen) (input Symbolic)
-> GenT (StateT (Context state) (GenBase gen)) (input Symbolic)
forall k (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
(b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall a. GenBase gen a -> StateT (Context state) (GenBase gen) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (GenT (GenBase gen) (input Symbolic)
-> GenT (StateT (Context state) (GenBase gen)) (input Symbolic))
-> GenT (GenBase gen) (input Symbolic)
-> GenT (StateT (Context state) (GenBase gen)) (input Symbolic)
forall a b. (a -> b) -> a -> b
$ gen (input Symbolic) -> GenT (GenBase gen) (input Symbolic)
forall (m :: * -> *) a. MonadGen m => m a -> GenT (GenBase m) a
Gen.toGenT gen (input Symbolic)
gen
if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Callback input output state]
-> state Symbolic -> input Symbolic -> Bool
forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
[Callback input output state]
-> state Symbolic -> input Symbolic -> Bool
callbackRequire [Callback input output state]
callbacks state Symbolic
state0 input Symbolic
input then
Maybe (Action m state)
-> GenT
(StateT (Context state) (GenBase gen)) (Maybe (Action m state))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Action m state)
forall a. Maybe a
Nothing
else do
Symbolic output
output <- GenT (StateT (Context state) (GenBase gen)) (Symbolic output)
forall (state :: (* -> *) -> *) (m :: * -> *) a.
(MonadState (Context state) m, Typeable a) =>
m (Symbolic a)
contextNewVar
state Symbolic -> GenT (StateT (Context state) (GenBase gen)) ()
forall (state :: (* -> *) -> *) (m :: * -> *).
MonadState (Context state) m =>
state Symbolic -> m ()
contextUpdate (state Symbolic -> GenT (StateT (Context state) (GenBase gen)) ())
-> state Symbolic -> GenT (StateT (Context state) (GenBase gen)) ()
forall a b. (a -> b) -> a -> b
$
[Callback input output state]
-> state Symbolic
-> input Symbolic
-> Var output Symbolic
-> state Symbolic
forall (v :: * -> *) (input :: (* -> *) -> *) output
(state :: (* -> *) -> *).
Ord1 v =>
[Callback input output state]
-> state v -> input v -> Var output v -> state v
callbackUpdate [Callback input output state]
callbacks state Symbolic
state0 input Symbolic
input (Symbolic output -> Var output Symbolic
forall a (v :: * -> *). v a -> Var a v
Var Symbolic output
output)
Maybe (Action m state)
-> GenT
(StateT (Context state) (GenBase gen)) (Maybe (Action m state))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Action m state)
-> GenT
(StateT (Context state) (GenBase gen)) (Maybe (Action m state)))
-> (Action m state -> Maybe (Action m state))
-> Action m state
-> GenT
(StateT (Context state) (GenBase gen)) (Maybe (Action m state))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action m state -> Maybe (Action m state)
forall a. a -> Maybe a
Just (Action m state
-> GenT
(StateT (Context state) (GenBase gen)) (Maybe (Action m state)))
-> Action m state
-> GenT
(StateT (Context state) (GenBase gen)) (Maybe (Action m state))
forall a b. (a -> b) -> a -> b
$
input Symbolic
-> Symbolic output
-> (input Concrete -> m output)
-> (state Symbolic -> input Symbolic -> Bool)
-> (forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v)
-> (state Concrete
-> state Concrete -> input Concrete -> output -> Test ())
-> Action m state
forall (m :: * -> *) (state :: (* -> *) -> *)
(input :: (* -> *) -> *) output.
(TraversableB input, Show (input Symbolic), Show output) =>
input Symbolic
-> Symbolic output
-> (input Concrete -> m output)
-> (state Symbolic -> input Symbolic -> Bool)
-> (forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v)
-> (state Concrete
-> state Concrete -> input Concrete -> output -> Test ())
-> Action m state
Action input Symbolic
input Symbolic output
output input Concrete -> m output
exec
([Callback input output state]
-> state Symbolic -> input Symbolic -> Bool
forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
[Callback input output state]
-> state Symbolic -> input Symbolic -> Bool
callbackRequire [Callback input output state]
callbacks)
([Callback input output state]
-> state v -> input v -> Var output v -> state v
forall (v :: * -> *) (input :: (* -> *) -> *) output
(state :: (* -> *) -> *).
Ord1 v =>
[Callback input output state]
-> state v -> input v -> Var output v -> state v
callbackUpdate [Callback input output state]
callbacks)
([Callback input output state]
-> state Concrete
-> state Concrete
-> input Concrete
-> output
-> Test ()
forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
[Callback input output state]
-> state Concrete
-> state Concrete
-> input Concrete
-> output
-> Test ()
callbackEnsure [Callback input output state]
callbacks)
genActions ::
(MonadGen gen, MonadTest m)
=> Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions :: Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions Range Int
range [Command gen m state]
commands Context state
ctx = do
[Action m state]
xs <- GenT (GenBase gen) [Action m state] -> gen [Action m state]
forall (m :: * -> *) a. MonadGen m => GenT (GenBase m) a -> m a
Gen.fromGenT (GenT (GenBase gen) [Action m state] -> gen [Action m state])
-> (GenT (StateT (Context state) (GenBase gen)) [Action m state]
-> GenT (GenBase gen) [Action m state])
-> GenT (StateT (Context state) (GenBase gen)) [Action m state]
-> gen [Action m state]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT (Context state) (GenT (GenBase gen)) [Action m state]
-> Context state -> GenT (GenBase gen) [Action m state]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
`evalStateT` Context state
ctx) (StateT (Context state) (GenT (GenBase gen)) [Action m state]
-> GenT (GenBase gen) [Action m state])
-> (GenT (StateT (Context state) (GenBase gen)) [Action m state]
-> StateT (Context state) (GenT (GenBase gen)) [Action m state])
-> GenT (StateT (Context state) (GenBase gen)) [Action m state]
-> GenT (GenBase gen) [Action m state]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenT (StateT (Context state) (GenBase gen)) [Action m state]
-> StateT (Context state) (GenT (GenBase gen)) [Action m state]
forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *)
(m :: * -> *) a.
(MonadTransDistributive g, Transformer f g m) =>
g (f m) a -> f (g m) a
distributeT (GenT (StateT (Context state) (GenBase gen)) [Action m state]
-> gen [Action m state])
-> GenT (StateT (Context state) (GenBase gen)) [Action m state]
-> gen [Action m state]
forall a b. (a -> b) -> a -> b
$ Range Int
-> GenT (StateT (Context state) (GenBase gen)) (Action m state)
-> GenT (StateT (Context state) (GenBase gen)) [Action m state]
forall (m :: * -> *) a. MonadGen m => Range Int -> m a -> m [a]
Gen.list Range Int
range ([Command gen m state]
-> GenT (StateT (Context state) (GenBase gen)) (Action m state)
forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
[Command gen m state]
-> GenT (StateT (Context state) (GenBase gen)) (Action m state)
action [Command gen m state]
commands)
([Action m state], Context state)
-> gen ([Action m state], Context state)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([Action m state], Context state)
-> gen ([Action m state], Context state))
-> ([Action m state], Context state)
-> gen ([Action m state], Context state)
forall a b. (a -> b) -> a -> b
$
[Action m state] -> State (Context state) [Action m state]
forall (m :: * -> *) (state :: (* -> *) -> *).
[Action m state] -> State (Context state) [Action m state]
dropInvalid [Action m state]
xs State (Context state) [Action m state]
-> Context state -> ([Action m state], Context state)
forall s a. State s a -> s -> (a, s)
`runState` Context state
ctx
newtype Sequential m state =
Sequential {
Sequential m state -> [Action m state]
sequentialActions :: [Action m state]
}
renderAction :: Action m state -> [String]
renderAction :: Action m state -> [String]
renderAction (Action input Symbolic
input (Symbolic (Name Int
output)) input Concrete -> m output
_ state Symbolic -> input Symbolic -> Bool
_ forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
_ state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_) =
let
prefix0 :: String
prefix0 =
String
"Var " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
output String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = "
prefix :: String
prefix =
Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
prefix0) Char
' '
in
case String -> [String]
lines (input Symbolic -> String
forall a. Show a => a -> String
showPretty input Symbolic
input) of
[] ->
[String
prefix0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"?"]
String
x : [String]
xs ->
(String
prefix0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x) String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
ShowS -> [String] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
prefix String -> ShowS
forall a. [a] -> [a] -> [a]
++) [String]
xs
renderActionResult :: Environment -> Action m state -> [String]
renderActionResult :: Environment -> Action m state -> [String]
renderActionResult Environment
env (Action input Symbolic
_ output :: Symbolic output
output@(Symbolic (Name Int
name)) input Concrete -> m output
_ state Symbolic -> input Symbolic -> Bool
_ forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
_ state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_) =
let
prefix0 :: String
prefix0 =
String
"Var " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = "
prefix :: String
prefix =
Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
prefix0) Char
' '
unfound :: EnvironmentError -> String
unfound = \case
EnvironmentValueNotFound Name
_
-> String
"<<not found in environment>>"
EnvironmentTypeError TypeRep
_ TypeRep
_
-> String
"<<type representation in environment unexpected>>"
actual :: String
actual =
(EnvironmentError -> String)
-> (Concrete output -> String)
-> Either EnvironmentError (Concrete output)
-> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either EnvironmentError -> String
unfound Concrete output -> String
forall a. Show a => a -> String
showPretty
(Either EnvironmentError (Concrete output) -> String)
-> Either EnvironmentError (Concrete output) -> String
forall a b. (a -> b) -> a -> b
$ Environment
-> Symbolic output -> Either EnvironmentError (Concrete output)
Environment
-> forall a. Symbolic a -> Either EnvironmentError (Concrete a)
reifyEnvironment Environment
env Symbolic output
output
in
case String -> [String]
lines String
actual of
[] ->
[String
prefix0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"?"]
String
x : [String]
xs ->
(String
prefix0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x) String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
ShowS -> [String] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
prefix String -> ShowS
forall a. [a] -> [a] -> [a]
++) [String]
xs
instance Show (Sequential m state) where
show :: Sequential m state -> String
show (Sequential [Action m state]
xs) =
[String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Action m state -> [String]) -> [Action m state] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Action m state -> [String]
forall (m :: * -> *) (state :: (* -> *) -> *).
Action m state -> [String]
renderAction [Action m state]
xs
sequential ::
(MonadGen gen, MonadTest m)
=> Range Int
-> (forall v. state v)
-> [Command gen m state]
-> gen (Sequential m state)
sequential :: Range Int
-> (forall (v :: * -> *). state v)
-> [Command gen m state]
-> gen (Sequential m state)
sequential Range Int
range forall (v :: * -> *). state v
initial [Command gen m state]
commands =
(([Action m state], Context state) -> Sequential m state)
-> gen ([Action m state], Context state)
-> gen (Sequential m state)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Action m state] -> Sequential m state
forall (m :: * -> *) (state :: (* -> *) -> *).
[Action m state] -> Sequential m state
Sequential ([Action m state] -> Sequential m state)
-> (([Action m state], Context state) -> [Action m state])
-> ([Action m state], Context state)
-> Sequential m state
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Action m state], Context state) -> [Action m state]
forall a b. (a, b) -> a
fst) (gen ([Action m state], Context state) -> gen (Sequential m state))
-> gen ([Action m state], Context state)
-> gen (Sequential m state)
forall a b. (a -> b) -> a -> b
$
Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions Range Int
range [Command gen m state]
commands (state Symbolic -> Context state
forall (state :: (* -> *) -> *). state Symbolic -> Context state
mkContext state Symbolic
forall (v :: * -> *). state v
initial)
data Parallel m state =
Parallel {
Parallel m state -> [Action m state]
parallelPrefix :: [Action m state]
, Parallel m state -> [Action m state]
parallelBranch1 :: [Action m state]
, Parallel m state -> [Action m state]
parallelBranch2 :: [Action m state]
}
instance Show (Parallel m state) where
show :: Parallel m state -> String
show =
(Action m state -> [String]) -> Parallel m state -> String
forall (m :: * -> *) (state :: (* -> *) -> *).
(Action m state -> [String]) -> Parallel m state -> String
renderParallel Action m state -> [String]
forall (m :: * -> *) (state :: (* -> *) -> *).
Action m state -> [String]
renderAction
renderParallel :: (Action m state -> [String]) -> Parallel m state -> String
renderParallel :: (Action m state -> [String]) -> Parallel m state -> String
renderParallel Action m state -> [String]
render (Parallel [Action m state]
pre [Action m state]
xs [Action m state]
ys) =
[String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
[String
"━━━ Prefix ━━━"]
, (Action m state -> [String]) -> [Action m state] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Action m state -> [String]
render [Action m state]
pre
, [String
"", String
"━━━ Branch 1 ━━━"]
, (Action m state -> [String]) -> [Action m state] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Action m state -> [String]
render [Action m state]
xs
, [String
"", String
"━━━ Branch 2 ━━━"]
, (Action m state -> [String]) -> [Action m state] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Action m state -> [String]
render [Action m state]
ys
]
parallel ::
(MonadGen gen, MonadTest m)
=> Range Int
-> Range Int
-> (forall v. state v)
-> [Command gen m state]
-> gen (Parallel m state)
parallel :: Range Int
-> Range Int
-> (forall (v :: * -> *). state v)
-> [Command gen m state]
-> gen (Parallel m state)
parallel Range Int
prefixN Range Int
parallelN forall (v :: * -> *). state v
initial [Command gen m state]
commands = do
([Action m state]
prefix, Context state
ctx0) <- Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions Range Int
prefixN [Command gen m state]
commands (state Symbolic -> Context state
forall (state :: (* -> *) -> *). state Symbolic -> Context state
mkContext state Symbolic
forall (v :: * -> *). state v
initial)
([Action m state]
branch1, Context state
ctx1) <- Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions Range Int
parallelN [Command gen m state]
commands Context state
ctx0
([Action m state]
branch2, Context state
_ctx2) <- Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions Range Int
parallelN [Command gen m state]
commands Context state
ctx1 { contextState :: state Symbolic
contextState = Context state -> state Symbolic
forall (state :: (* -> *) -> *). Context state -> state Symbolic
contextState Context state
ctx0 }
Parallel m state -> gen (Parallel m state)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Parallel m state -> gen (Parallel m state))
-> Parallel m state -> gen (Parallel m state)
forall a b. (a -> b) -> a -> b
$ [Action m state]
-> [Action m state] -> [Action m state] -> Parallel m state
forall (m :: * -> *) (state :: (* -> *) -> *).
[Action m state]
-> [Action m state] -> [Action m state] -> Parallel m state
Parallel [Action m state]
prefix [Action m state]
branch1 [Action m state]
branch2
data ActionCheck state =
ActionCheck {
ActionCheck state -> state Concrete -> state Concrete
checkUpdate :: state Concrete -> state Concrete
, ActionCheck state -> state Concrete -> state Concrete -> Test ()
checkEnsure :: state Concrete -> state Concrete -> Test ()
}
execute :: (MonadTest m, HasCallStack) => Action m state -> StateT Environment m (ActionCheck state)
execute :: Action m state -> StateT Environment m (ActionCheck state)
execute (Action input Symbolic
sinput Symbolic output
soutput input Concrete -> m output
exec state Symbolic -> input Symbolic -> Bool
_require forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
ensure) =
(HasCallStack => StateT Environment m (ActionCheck state))
-> StateT Environment m (ActionCheck state)
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => StateT Environment m (ActionCheck state))
-> StateT Environment m (ActionCheck state))
-> (HasCallStack => StateT Environment m (ActionCheck state))
-> StateT Environment m (ActionCheck state)
forall a b. (a -> b) -> a -> b
$ do
Environment
env0 <- StateT Environment m Environment
forall s (m :: * -> *). MonadState s m => m s
get
input Concrete
input <- Either EnvironmentError (input Concrete)
-> StateT Environment m (input Concrete)
forall (m :: * -> *) x a.
(MonadTest m, Show x, HasCallStack) =>
Either x a -> m a
evalEither (Either EnvironmentError (input Concrete)
-> StateT Environment m (input Concrete))
-> Either EnvironmentError (input Concrete)
-> StateT Environment m (input Concrete)
forall a b. (a -> b) -> a -> b
$ Environment
-> input Symbolic -> Either EnvironmentError (input Concrete)
forall (t :: (* -> *) -> *).
TraversableB t =>
Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify Environment
env0 input Symbolic
sinput
output
output <- m output -> StateT Environment m output
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m output -> StateT Environment m output)
-> m output -> StateT Environment m output
forall a b. (a -> b) -> a -> b
$ input Concrete -> m output
exec input Concrete
input
let
coutput :: Concrete output
coutput =
output -> Concrete output
forall a. a -> Concrete a
Concrete output
output
env :: Environment
env =
Symbolic output -> Concrete output -> Environment -> Environment
forall a. Symbolic a -> Concrete a -> Environment -> Environment
insertConcrete Symbolic output
soutput Concrete output
coutput Environment
env0
Environment -> StateT Environment m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Environment
env
ActionCheck state -> StateT Environment m (ActionCheck state)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ActionCheck state -> StateT Environment m (ActionCheck state))
-> ActionCheck state -> StateT Environment m (ActionCheck state)
forall a b. (a -> b) -> a -> b
$
(state Concrete -> state Concrete)
-> (state Concrete -> state Concrete -> Test ())
-> ActionCheck state
forall (state :: (* -> *) -> *).
(state Concrete -> state Concrete)
-> (state Concrete -> state Concrete -> Test ())
-> ActionCheck state
ActionCheck
(\state Concrete
s0 -> state Concrete
-> input Concrete -> Var output Concrete -> state Concrete
forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Concrete
s0 input Concrete
input (Concrete output -> Var output Concrete
forall a (v :: * -> *). v a -> Var a v
Var Concrete output
coutput))
(\state Concrete
s0 state Concrete
s -> state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
ensure state Concrete
s0 state Concrete
s input Concrete
input output
output)
executeUpdateEnsure ::
(MonadTest m, HasCallStack)
=> (state Concrete, Environment)
-> Action m state
-> m (state Concrete, Environment)
executeUpdateEnsure :: (state Concrete, Environment)
-> Action m state -> m (state Concrete, Environment)
executeUpdateEnsure (state Concrete
state0, Environment
env0) (Action input Symbolic
sinput Symbolic output
soutput input Concrete -> m output
exec state Symbolic -> input Symbolic -> Bool
_require forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
ensure) =
(HasCallStack => m (state Concrete, Environment))
-> m (state Concrete, Environment)
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => m (state Concrete, Environment))
-> m (state Concrete, Environment))
-> (HasCallStack => m (state Concrete, Environment))
-> m (state Concrete, Environment)
forall a b. (a -> b) -> a -> b
$ do
input Concrete
input <- Either EnvironmentError (input Concrete) -> m (input Concrete)
forall (m :: * -> *) x a.
(MonadTest m, Show x, HasCallStack) =>
Either x a -> m a
evalEither (Either EnvironmentError (input Concrete) -> m (input Concrete))
-> Either EnvironmentError (input Concrete) -> m (input Concrete)
forall a b. (a -> b) -> a -> b
$ Environment
-> input Symbolic -> Either EnvironmentError (input Concrete)
forall (t :: (* -> *) -> *).
TraversableB t =>
Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify Environment
env0 input Symbolic
sinput
output
output <- input Concrete -> m output
exec input Concrete
input
let
coutput :: Concrete output
coutput =
output -> Concrete output
forall a. a -> Concrete a
Concrete output
output
state :: state Concrete
state =
state Concrete
-> input Concrete -> Var output Concrete -> state Concrete
forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Concrete
state0 input Concrete
input (Concrete output -> Var output Concrete
forall a (v :: * -> *). v a -> Var a v
Var Concrete output
coutput)
env :: Environment
env =
Symbolic output -> Concrete output -> Environment -> Environment
forall a. Symbolic a -> Concrete a -> Environment -> Environment
insertConcrete Symbolic output
soutput Concrete output
coutput Environment
env0
Test () -> m ()
forall (m :: * -> *) a. MonadTest m => Test a -> m a
liftTest (Test () -> m ()) -> Test () -> m ()
forall a b. (a -> b) -> a -> b
$ state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
ensure state Concrete
state0 state Concrete
state input Concrete
input output
output
(state Concrete, Environment) -> m (state Concrete, Environment)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (state Concrete
state, Environment
env)
executeSequential ::
(MonadTest m, MonadCatch m, HasCallStack)
=> (forall v. state v)
-> Sequential m state
-> m ()
executeSequential :: (forall (v :: * -> *). state v) -> Sequential m state -> m ()
executeSequential forall (v :: * -> *). state v
initial (Sequential [Action m state]
xs) =
(HasCallStack => m ()) -> m ()
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => m ()) -> m ()) -> (HasCallStack => m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ m () -> m ()
forall (m :: * -> *) a.
(MonadTest m, MonadCatch m, HasCallStack) =>
m a -> m a
evalM (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
((state Concrete, Environment)
-> Action m state -> m (state Concrete, Environment))
-> (state Concrete, Environment) -> [Action m state] -> m ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ (state Concrete, Environment)
-> Action m state -> m (state Concrete, Environment)
forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, HasCallStack) =>
(state Concrete, Environment)
-> Action m state -> m (state Concrete, Environment)
executeUpdateEnsure (state Concrete
forall (v :: * -> *). state v
initial, Environment
emptyEnvironment) [Action m state]
xs
successful :: Test () -> Bool
successful :: Test () -> Bool
successful Test ()
x =
case Test () -> (Either Failure (), Journal)
forall a. Test a -> (Either Failure a, Journal)
runTest Test ()
x of
(Left Failure
_, Journal
_) ->
Bool
False
(Right ()
_, Journal
_) ->
Bool
True
interleave :: [a] -> [a] -> [[a]]
interleave :: [a] -> [a] -> [[a]]
interleave [a]
xs00 [a]
ys00 =
case ([a]
xs00, [a]
ys00) of
([], []) ->
[]
([a]
xs, []) ->
[[a]
xs]
([], [a]
ys) ->
[[a]
ys]
(xs0 :: [a]
xs0@(a
x:[a]
xs), ys0 :: [a]
ys0@(a
y:[a]
ys)) ->
[ a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
zs | [a]
zs <- [a] -> [a] -> [[a]]
forall a. [a] -> [a] -> [[a]]
interleave [a]
xs [a]
ys0 ] [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++
[ a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
zs | [a]
zs <- [a] -> [a] -> [[a]]
forall a. [a] -> [a] -> [[a]]
interleave [a]
xs0 [a]
ys ]
checkActions :: state Concrete -> [ActionCheck state] -> Test ()
checkActions :: state Concrete -> [ActionCheck state] -> Test ()
checkActions state Concrete
s0 = \case
[] ->
() -> Test ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
ActionCheck state
x : [ActionCheck state]
xs -> do
let
s :: state Concrete
s =
ActionCheck state -> state Concrete -> state Concrete
forall (state :: (* -> *) -> *).
ActionCheck state -> state Concrete -> state Concrete
checkUpdate ActionCheck state
x state Concrete
s0
ActionCheck state -> state Concrete -> state Concrete -> Test ()
forall (state :: (* -> *) -> *).
ActionCheck state -> state Concrete -> state Concrete -> Test ()
checkEnsure ActionCheck state
x state Concrete
s0 state Concrete
s
state Concrete -> [ActionCheck state] -> Test ()
forall (state :: (* -> *) -> *).
state Concrete -> [ActionCheck state] -> Test ()
checkActions state Concrete
s [ActionCheck state]
xs
linearize :: MonadTest m => state Concrete -> [ActionCheck state] -> [ActionCheck state] -> m ()
linearize :: state Concrete
-> [ActionCheck state] -> [ActionCheck state] -> m ()
linearize state Concrete
initial [ActionCheck state]
branch1 [ActionCheck state]
branch2 =
(HasCallStack => m ()) -> m ()
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => m ()) -> m ()) -> (HasCallStack => m ()) -> m ()
forall a b. (a -> b) -> a -> b
$
let
ok :: Bool
ok =
(Test () -> Bool) -> [Test ()] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Test () -> Bool
successful ([Test ()] -> Bool)
-> ([[ActionCheck state]] -> [Test ()])
-> [[ActionCheck state]]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
([ActionCheck state] -> Test ())
-> [[ActionCheck state]] -> [Test ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (state Concrete -> [ActionCheck state] -> Test ()
forall (state :: (* -> *) -> *).
state Concrete -> [ActionCheck state] -> Test ()
checkActions state Concrete
initial) ([[ActionCheck state]] -> Bool) -> [[ActionCheck state]] -> Bool
forall a b. (a -> b) -> a -> b
$
[ActionCheck state] -> [ActionCheck state] -> [[ActionCheck state]]
forall a. [a] -> [a] -> [[a]]
interleave [ActionCheck state]
branch1 [ActionCheck state]
branch2
in
if Bool
ok then
() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
else
Maybe Diff -> String -> m ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack) =>
Maybe Diff -> String -> m a
failWith Maybe Diff
forall a. Maybe a
Nothing String
"no valid interleaving"
executeParallel ::
(MonadTest m, MonadCatch m, MonadBaseControl IO m, HasCallStack)
=> (forall v. state v)
-> Parallel m state
-> m ()
executeParallel :: (forall (v :: * -> *). state v) -> Parallel m state -> m ()
executeParallel forall (v :: * -> *). state v
initial p :: Parallel m state
p@(Parallel [Action m state]
prefix [Action m state]
branch1 [Action m state]
branch2) =
(HasCallStack => m ()) -> m ()
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => m ()) -> m ()) -> (HasCallStack => m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ m () -> m ()
forall (m :: * -> *) a.
(MonadTest m, MonadCatch m, HasCallStack) =>
m a -> m a
evalM (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
(state Concrete
s0, Environment
env0) <- ((state Concrete, Environment)
-> Action m state -> m (state Concrete, Environment))
-> (state Concrete, Environment)
-> [Action m state]
-> m (state Concrete, Environment)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (state Concrete, Environment)
-> Action m state -> m (state Concrete, Environment)
forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, HasCallStack) =>
(state Concrete, Environment)
-> Action m state -> m (state Concrete, Environment)
executeUpdateEnsure (state Concrete
forall (v :: * -> *). state v
initial, Environment
emptyEnvironment) [Action m state]
prefix
(([ActionCheck state]
xs, Environment
env1), ([ActionCheck state]
ys, Environment
env2)) <-
m ([ActionCheck state], Environment)
-> m ([ActionCheck state], Environment)
-> m (([ActionCheck state], Environment),
([ActionCheck state], Environment))
forall (m :: * -> *) a b.
MonadBaseControl IO m =>
m a -> m b -> m (a, b)
Async.concurrently
(StateT Environment m [ActionCheck state]
-> Environment -> m ([ActionCheck state], Environment)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ((Action m state -> StateT Environment m (ActionCheck state))
-> [Action m state] -> StateT Environment m [ActionCheck state]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Action m state -> StateT Environment m (ActionCheck state)
forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, HasCallStack) =>
Action m state -> StateT Environment m (ActionCheck state)
execute [Action m state]
branch1) Environment
env0)
(StateT Environment m [ActionCheck state]
-> Environment -> m ([ActionCheck state], Environment)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ((Action m state -> StateT Environment m (ActionCheck state))
-> [Action m state] -> StateT Environment m [ActionCheck state]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Action m state -> StateT Environment m (ActionCheck state)
forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, HasCallStack) =>
Action m state -> StateT Environment m (ActionCheck state)
execute [Action m state]
branch2) Environment
env0)
let
env :: Environment
env = [Environment] -> Environment
unionsEnvironment [Environment
env0, Environment
env1, Environment
env2]
String -> m ()
forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ (Action m state -> [String]) -> Parallel m state -> String
forall (m :: * -> *) (state :: (* -> *) -> *).
(Action m state -> [String]) -> Parallel m state -> String
renderParallel (Environment -> Action m state -> [String]
forall (m :: * -> *) (state :: (* -> *) -> *).
Environment -> Action m state -> [String]
renderActionResult Environment
env) Parallel m state
p
state Concrete
-> [ActionCheck state] -> [ActionCheck state] -> m ()
forall (m :: * -> *) (state :: (* -> *) -> *).
MonadTest m =>
state Concrete
-> [ActionCheck state] -> [ActionCheck state] -> m ()
linearize state Concrete
s0 [ActionCheck state]
xs [ActionCheck state]
ys