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 pre-condition 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 post-condition 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 post-conditions are met and no exceptions are thrown.
To generate a sequence of actions to execute, see the
actions
combinator in the Hedgehog.Gen module.