{-# 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 (
  -- * Variables
    Var(..)
  , concrete
  , opaque

  , Concrete(..)
  , Symbolic(..)
  , Name(..)

  -- * Environment
  , Environment(..)
  , EnvironmentError(..)
  , emptyEnvironment
  , insertConcrete
  , reifyDynamic
  , reifyEnvironment
  , reify

  -- * Commands
  , Command(..)
  , Callback(..)
  , commandGenOK

  -- * Actions
  , 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)


-- | Symbolic variable names.
--
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

-- | Symbolic values: Because hedgehog generates actions in a separate phase
--   before execution, you will sometimes need to refer to the result of a
--   previous action in a generator without knowing the value of the result
--   (e.g., to get the ID of a previously-created user).
--
--   Symbolic variables provide a token to stand in for the actual variables at
--   generation time (and in 'Require'/'Update' callbacks). At execution time,
--   real values are available, so your execute actions work on 'Concrete'
--   variables.
--
--   See also: 'Command', 'Var'
--
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

-- | Concrete values: At test-execution time, 'Symbolic' values from generation
--   are replaced with 'Concrete' values from performing actions. This type
--   gives us something of the same kind as 'Symbolic' to pass as a type
--   argument to 'Var'.
--
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

------------------------------------------------------------------------

-- | Variables are the potential or actual result of executing an action. They
--   are parameterised by either `Symbolic` or `Concrete` depending on the
--   phase of the test.
--
--   `Symbolic` variables are the potential results of actions. These are used
--   when generating the sequence of actions to execute. They allow actions
--   which occur later in the sequence to make use of the result of an action
--   which came earlier in the sequence.
--
--   `Concrete` variables are the actual results of actions. These are used
--   during test execution. They provide access to the actual runtime value of
--   a variable.
--
--   The state update `Callback` for a command needs to be polymorphic in the
--   type of variable because it is used in both the generation and the
--   execution phase.
--
--   The order of arguments makes 'Var' 'HTraverable', which is how 'Symbolic'
--   values are turned into 'Concrete' ones.
--
newtype Var a v =
  Var (v a)

-- | Take the value from a concrete variable.
--
concrete :: Var a Concrete -> a
concrete :: Var a Concrete -> a
concrete (Var (Concrete a
x)) =
  a
x

-- | Take the value from an opaque concrete variable.
--
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)

------------------------------------------------------------------------
-- Symbolic Environment

-- | A mapping of symbolic values to concrete values.
--
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)

-- | Environment errors.
--
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)

-- | Create an empty environment.
--
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

-- | Insert a symbolic / concrete pairing in to the environment.
--
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

-- | Cast a 'Dynamic' in to a concrete value.
--
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

-- | Turns an environment in to a function for looking up a concrete value from
--   a symbolic one.
--
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

-- | Convert a symbolic structure to a concrete one, using the provided environment.
--
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)

------------------------------------------------------------------------
-- Callbacks

-- | Optional command configuration.
--
data Callback input output state =
  -- | 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.
  --
    Require (state Symbolic -> input Symbolic -> Bool)

  -- | 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 'Symbolic' values when we are generating actions, and
  --   'Concrete' values when we are executing them.
  --
  | Update (forall v. Ord1 v => state v -> input v -> Var output v -> state v)

  -- | A post-condition for a command that must be verified for the command to
  --   be considered a success.
  --
  --   This callback receives the state prior to execution as the first
  --   argument, and the state after execution as the second argument.
  --
  | 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

------------------------------------------------------------------------

-- | The specification for the expected behaviour of an
-- 'Action'. These are used to generate sequences of actions to test.
--
-- This is the main type you will use when writing state machine
-- tests. @gen@ is usually an instance of 'MonadGen', and @m@ is usually
-- an instance of 'MonadTest'. These constraints appear when you pass
-- your 'Command' list to 'sequential' or 'parallel'.
--
data Command gen m (state :: (Type -> Type) -> Type) =
  forall input output.
  (TraversableB input, Show (input Symbolic), Show output, Typeable output) =>
  Command {
    -- | A generator which provides random arguments for a command. If the
    --   command cannot be executed in the current state, it should return
    --   'Nothing'.
    --
      ()
commandGen ::
        state Symbolic -> Maybe (gen (input Symbolic))

    -- | Executes a command using the arguments generated by 'commandGen'.
    --
    , ()
commandExecute ::
        input Concrete -> m output

    -- | A set of callbacks which provide optional command configuration such
    --   as pre-condtions, post-conditions and state updates.
    --
    , ()
commandCallbacks ::
        [Callback input output state]
    }

-- | Checks that input for a command can be executed in the given 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)

-- | An instantiation of a 'Command' which can be executed, and its effect
--   evaluated.
--
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

-- | Extract the variable name and the type from a symbolic value.
--
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))

-- | Insert a symbolic variable in to a map of variables to types.
--
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

-- | Collects all the symbolic values in a data structure and produces a set of
--   all the variables they refer to.
--
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

-- | 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.
--
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

-- | Drops invalid actions from the sequence.
--
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

-- | Generates a single action from a set of possible commands.
--
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

    -- If we shrink the input, we still want to use the same output. Otherwise
    -- any actions using this output as part of their input will be dropped. But
    -- the existing output is still in the context, so `contextNewVar` will
    -- create a new one. To avoid that, we generate the output before the input.
    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

    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
      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

-- | A sequence of actions to execute.
--
newtype Sequential m state =
  Sequential {
      -- | The sequence of actions.
      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

-- FIXME we should not abuse Show to get nice output for actions
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

-- | Generates a sequence of actions from an initial model state and set of commands.
--
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)

-- | A sequential prefix of actions to execute, with two branches to execute in parallel.
--
data Parallel m state =
  Parallel {
      -- | The sequential prefix.
      Parallel m state -> [Action m state]
parallelPrefix :: [Action m state]

      -- | The first branch.
    , Parallel m state -> [Action m state]
parallelBranch1 :: [Action m state]

      -- | The second branch.
    , Parallel m state -> [Action m state]
parallelBranch2 :: [Action m state]
    }

-- FIXME we should not abuse Show to get nice output for actions
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
    ]


-- | Given the initial model state and set of commands, generates prefix
--   actions to be run sequentially, followed by two branches to be run in
--   parallel.
--
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)

-- | Executes a single action in the given evironment.
--
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)

-- | 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
--   'Hedgehog.Gen.sequential' combinator in the "Hedgehog.Gen" module.
--
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"


-- | Executes the prefix actions sequentially, then executes the two branches
--   in parallel, verifying that no exceptions are thrown and that there is at
--   least one sequential interleaving where all the post-conditions are met.
--
--   To generate parallel actions to execute, see the 'Hedgehog.Gen.parallel'
--   combinator in the "Hedgehog.Gen" module.
--
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