Safe Haskell  None 

Language  Haskell98 
 newtype Var = Var Int
 data Symbolic a where
 newtype Concrete a where
 newtype Environment = Environment {}
 data EnvironmentError
 emptyEnvironment :: Environment
 insertConcrete :: Symbolic a > Concrete a > Environment > Environment
 reifyDynamic :: forall a. Typeable a => Dynamic > Either EnvironmentError (Concrete a)
 reifyEnvironment :: Environment > forall a. Symbolic a > Either EnvironmentError (Concrete a)
 reify :: HTraversable t => Environment > t Symbolic > Either EnvironmentError (t Concrete)
 data Command n m state = (HTraversable input, Show (input Symbolic), Typeable output) => Command {
 commandGen :: state Symbolic > Maybe (Gen n (input Symbolic))
 commandExecute :: input Concrete > Test m output
 commandCallbacks :: [Callback input output m state]
 data Callback input output m state
 commandGenOK :: Command n m state > state Symbolic > Bool
 data Action m state = (HTraversable input, Show (input Symbolic)) => Action {
 actionInput :: input Symbolic
 actionOutput :: Symbolic output
 actionExecute :: input Concrete > Test m output
 actionRequire :: state Symbolic > input Symbolic > Bool
 actionUpdate :: forall v. Ord1 v => state v > input v > v output > state v
 actionEnsure :: state Concrete > input Concrete > output > Test m ()
 takeVariables :: forall t. HTraversable t => t Symbolic > Map Var TypeRep
 variablesOK :: HTraversable t => t Symbolic > Map Var TypeRep > Bool
 dropInvalid :: (forall v. state v) > [Action m state] > [Action m state]
 action :: (Monad n, Monad m) => [Command n m state] > Gen (StateT (state Symbolic, Var) n) (Action m state)
 actions :: (Monad n, Monad m) => Range Int > (forall v. state v) > [Command n m state] > Gen n [Action m state]
 execute :: (HasCallStack, Monad m) => (state Concrete, Environment) > Action m state > Test m (state Concrete, Environment)
 executeSequential :: forall m state. (HasCallStack, MonadCatch m) => (forall v. state v) > [Action m state] > Test m ()
Variables
Symbolic variable names.
Environment
newtype Environment Source #
A mapping of symbolic values to concrete values.
data EnvironmentError Source #
Environment errors.
emptyEnvironment :: Environment Source #
Create an empty environment.
insertConcrete :: Symbolic a > Concrete a > Environment > Environment Source #
Insert a symbolic / concrete pairing in to the environment.
reifyDynamic :: forall a. Typeable a => Dynamic > Either EnvironmentError (Concrete a) Source #
Cast a Dynamic
in to a concrete value.
reifyEnvironment :: Environment > forall a. Symbolic a > Either EnvironmentError (Concrete a) Source #
Turns an environment in to a function for looking up a concrete value from a symbolic one.
reify :: HTraversable t => Environment > t Symbolic > Either EnvironmentError (t Concrete) Source #
Convert a symbolic structure to a concrete one, using the provided environment.
Commands
data Command n m state Source #
The specification for the expected behaviour of an Action
.
(HTraversable input, Show (input Symbolic), Typeable output) => Command  

data Callback input output m state Source #
Optional command configuration.
Require (state Symbolic > input Symbolic > Bool)  A precondition for a command that must be verified before the command can be executed. This is mainly used during shrinking to ensure that it is still OK to run a command despite the fact that some previously executed commands may have been removed from the sequence. 
Update (forall v. Ord1 v => state v > input v > v output > state v)  Updates the model state, given the input and output of the command. Note
that this function is polymorphic in the type of values. This is because
it must work over 
Ensure (state Concrete > input Concrete > output > Test m ())  A postcondition for a command that must be verified for the command to be considered a success. 
commandGenOK :: Command n m state > state Symbolic > Bool Source #
Checks that input for a command can be executed in the given state.
Actions
An instantiation of a Command
which can be executed, and its effect
evaluated.
(HTraversable input, Show (input Symbolic)) => Action  

takeVariables :: forall t. HTraversable t => t Symbolic > Map Var TypeRep Source #
Collects all the symbolic values in a data structure and produces a set of all the variables they refer to.
variablesOK :: HTraversable t => t Symbolic > Map Var TypeRep > Bool Source #
Checks that the symbolic values in the data structure refer only to the variables in the provided set, and that they are of the correct type.
dropInvalid :: (forall v. state v) > [Action m state] > [Action m state] Source #
Drops invalid actions from the sequence.
action :: (Monad n, Monad m) => [Command n m state] > Gen (StateT (state Symbolic, Var) n) (Action m state) Source #
Generates a single action from a set of possible commands.
actions :: (Monad n, Monad m) => Range Int > (forall v. state v) > [Command n m state] > Gen n [Action m state] Source #
Generates a sequence of actions from an initial model state and set of commands.
execute :: (HasCallStack, Monad m) => (state Concrete, Environment) > Action m state > Test m (state Concrete, Environment) Source #
Executes a single action in the given evironment.
executeSequential :: forall m state. (HasCallStack, MonadCatch m) => (forall v. state v) > [Action m state] > Test m () Source #
Executes a list of actions sequentially, verifying that all postconditions are met and no exceptions are thrown.
To generate a sequence of actions to execute, see the
actions
combinator in the Hedgehog.Gen module.