    {-# 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.Exception.Safe (MonadCatch)
    import           Control.Monad (foldM, foldM_)
    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
    $c== :: Name -> Name -> Bool
    == :: Name -> Name -> Bool
    $c/= :: Name -> Name -> Bool
    /= :: 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
    $ccompare :: Name -> Name -> Ordering
    compare :: Name -> Name -> Ordering
    $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
    >= :: Name -> Name -> Bool
    $cmax :: Name -> Name -> Name
    max :: Name -> Name -> Name
    $cmin :: Name -> Name -> Name
    min :: Name -> Name -> 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
    $c+ :: Name -> Name -> Name
    + :: Name -> Name -> Name
    $c- :: Name -> Name -> Name
    - :: Name -> Name -> Name
    $c* :: Name -> Name -> Name
    * :: Name -> Name -> Name
    $cnegate :: Name -> Name
    negate :: Name -> Name
    $cabs :: Name -> Name
    abs :: Name -> Name
    $csignum :: Name -> Name
    signum :: Name -> Name
    $cfromInteger :: Integer -> Name
    fromInteger :: Integer -> 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 :: forall a.
    (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 :: forall a b. (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 :: forall a b.
    (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
    $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
    /= :: 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
    $ccompare :: forall a. Ord a => Concrete a -> Concrete a -> Ordering
    compare :: Concrete a -> Concrete a -> Ordering
    $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
    >= :: Concrete a -> Concrete a -> Bool
    $cmax :: forall a. Ord a => Concrete a -> Concrete a -> Concrete a
    max :: Concrete a -> Concrete a -> Concrete a
    $cmin :: forall a. Ord a => Concrete a -> Concrete a -> Concrete a
    min :: Concrete a -> Concrete a -> Concrete a
    Ord, (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
    $cfmap :: forall a b. (a -> b) -> Concrete a -> Concrete b
    fmap :: forall a b. (a -> b) -> Concrete a -> Concrete b
    $c<$ :: forall a b. a -> Concrete b -> Concrete a
    <$ :: forall a b. a -> Concrete b -> Concrete a
    Functor, (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
    $cfold :: forall m. Monoid m => Concrete m -> m
    fold :: forall m. Monoid m => Concrete m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Concrete a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Concrete a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Concrete a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Concrete a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Concrete a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Concrete a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Concrete a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Concrete a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Concrete a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Concrete a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Concrete a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Concrete a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Concrete a -> a
    foldr1 :: forall a. (a -> a -> a) -> Concrete a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Concrete a -> a
    foldl1 :: forall a. (a -> a -> a) -> Concrete a -> a
    $ctoList :: forall a. Concrete a -> [a]
    toList :: forall a. Concrete a -> [a]
    $cnull :: forall a. Concrete a -> Bool
    null :: forall a. Concrete a -> Bool
    $clength :: forall a. Concrete a -> Int
    length :: forall a. Concrete a -> Int
    $celem :: forall a. Eq a => a -> Concrete a -> Bool
    elem :: forall a. Eq a => a -> Concrete a -> Bool
    $cmaximum :: forall a. Ord a => Concrete a -> a
    maximum :: forall a. Ord a => Concrete a -> a
    $cminimum :: forall a. Ord a => Concrete a -> a
    minimum :: forall a. Ord a => Concrete a -> a
    $csum :: forall a. Num a => Concrete a -> a
    sum :: forall a. Num a => Concrete a -> a
    $cproduct :: forall a. Num a => Concrete a -> a
    product :: forall a. Num a => Concrete a -> a
    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
    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)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Concrete a -> f (Concrete b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Concrete a -> f (Concrete b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Concrete (f a) -> f (Concrete a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Concrete (f a) -> f (Concrete a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Concrete a -> m (Concrete b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Concrete a -> m (Concrete b)
    $csequence :: forall (m :: * -> *) a. Monad m => Concrete (m a) -> m (Concrete a)
    sequence :: forall (m :: * -> *) a. Monad m => Concrete (m a) -> m (Concrete a)
    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 :: forall a.
    (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 :: forall a b. (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 :: forall a b.
    (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' 'FunctorB' and 'TraversableB', 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 :: forall a. 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 :: forall a. 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 (f :: * -> *) (g :: * -> *).
    (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 (e :: * -> *) (f :: * -> *) (g :: * -> *).
    Applicative e =>
    (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 a b. (a -> b) -> e a -> e b
    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
    $cshowsPrec :: Int -> Environment -> ShowS
    showsPrec :: Int -> Environment -> ShowS
    $cshow :: Environment -> String
    show :: Environment -> String
    $cshowList :: [Environment] -> ShowS
    showList :: [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
    $c== :: EnvironmentError -> EnvironmentError -> Bool
    == :: EnvironmentError -> EnvironmentError -> Bool
    $c/= :: EnvironmentError -> EnvironmentError -> Bool
    /= :: 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
    $ccompare :: EnvironmentError -> EnvironmentError -> Ordering
    compare :: EnvironmentError -> EnvironmentError -> Ordering
    $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
    >= :: EnvironmentError -> EnvironmentError -> Bool
    $cmax :: EnvironmentError -> EnvironmentError -> EnvironmentError
    max :: EnvironmentError -> EnvironmentError -> EnvironmentError
    $cmin :: EnvironmentError -> EnvironmentError -> EnvironmentError
    min :: EnvironmentError -> EnvironmentError -> 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
    $cshowsPrec :: Int -> EnvironmentError -> ShowS
    showsPrec :: Int -> EnvironmentError -> ShowS
    $cshow :: EnvironmentError -> String
    show :: EnvironmentError -> String
    $cshowList :: [EnvironmentError] -> ShowS
    showList :: [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 a b. (a -> b) -> [a] -> [b]
    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 :: forall a. 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 :: forall a.
    Typeable a =>
    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 :: forall (t :: (* -> *) -> *).
    TraversableB t =>
    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)
    forall (e :: * -> *) (f :: * -> *) (g :: * -> *).
    Applicative e =>
    (forall a. f a -> e (g a)) -> t f -> e (t 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 :: forall (state :: (* -> *) -> *) (input :: (* -> *) -> *) output.
    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 :: 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 = \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 :: 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 = \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 :: forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
    [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 :: 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 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 b a. (b -> a -> b) -> b -> [a] -> b
    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 :: forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
    [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 :: forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
    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 :: forall a. 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 :: forall a. 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 :: forall (t :: (* -> *) -> *).
    TraversableB t =>
    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 a. a -> m 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)
    forall (e :: * -> *) (f :: * -> *) (g :: * -> *).
    Applicative e =>
    (forall a. f a -> e (g a)) -> t f -> e (t g)
    btraverse Symbolic a -> StateT (Map Name TypeRep) Identity (Symbolic a)
    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 :: forall (t :: (* -> *) -> *).
    TraversableB t =>
    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 {
          forall (state :: (* -> *) -> *). Context state -> state Symbolic
    contextState :: state Symbolic
        , forall (state :: (* -> *) -> *). Context state -> Map Name TypeRep
    _contextVars :: Map Name TypeRep
        }

    mkContext :: state Symbolic -> Context state
    mkContext :: forall (state :: (* -> *) -> *). 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 :: forall (state :: (* -> *) -> *) (m :: * -> *).
    MonadState (Context state) m =>
    state Symbolic -> m ()
    contextUpdate state Symbolic
    state = do
      Context _ vars <- m (Context state)
    forall s (m :: * -> *). MonadState s m => m s
    get
      put $ Context state vars

    contextNewVar :: (MonadState (Context state) m, Typeable a) => m (Symbolic a)
    contextNewVar :: forall (state :: (* -> *) -> *) (m :: * -> *) a.
    (MonadState (Context state) m, Typeable a) =>
    m (Symbolic a)
    contextNewVar = do
      Context state vars <- m (Context state)
    forall s (m :: * -> *). MonadState s m => m s
    get

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

      put $ Context state (insertSymbolic var vars)
      pure var

    -- | Drops invalid actions from the sequence.
    --
    dropInvalid :: [Action m state] -> State (Context state) [Action m state]
    dropInvalid :: forall (m :: * -> *) (state :: (* -> *) -> *).
    [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 state0 vars0 <- m (Context state)
    forall s (m :: * -> *). MonadState s m => m s
    get

          if require state0 input && variablesOK input vars0 then do
            let
              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 =
                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

            put $ Context state vars
            pure $ Just step
          else
            pure Nothing
      in
        ([Maybe (Action m state)] -> [Action m state])
    -> StateT (Context state) Identity [Maybe (Action m state)]
    -> StateT (Context state) Identity [Action m state]
    forall a b.
    (a -> b)
    -> StateT (Context state) Identity a
    -> StateT (Context state) Identity b
    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)]
     -> StateT (Context state) Identity [Action m state])
    -> ([Action m state]
        -> StateT (Context state) Identity [Maybe (Action m state)])
    -> [Action m state]
    -> StateT (Context state) Identity [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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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 :: 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 =
      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 state0 _ <- GenT (StateT (Context state) (GenBase gen)) (Context state)
    forall s (m :: * -> *). MonadState s m => m s
    get

        Command mgenInput exec callbacks <-
          Gen.element_ $ 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) 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.
        output <- contextNewVar

        input <-
          case mgenInput 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
    forall (m :: * -> *) (n :: * -> *) b.
    Monad m =>
    (forall a. m a -> n a) -> GenT m b -> GenT n b
    hoist GenBase gen a -> StateT (Context state) (GenBase gen) a
    forall a. GenBase gen a -> StateT (Context state) (GenBase gen) a
    forall (m :: * -> *) a.
    Monad m =>
    m a -> StateT (Context state) m 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 a. gen a -> GenT (GenBase gen) a
    forall (m :: * -> *) a. MonadGen m => m a -> GenT (GenBase m) a
    Gen.toGenT gen (input Symbolic)
    gen

        if not $ callbackRequire callbacks state0 input then
          pure Nothing

        else do
          contextUpdate $
            callbackUpdate callbacks state0 input (Var output)

          pure . Just $
            Action input output exec
              (callbackRequire callbacks)
              (callbackUpdate callbacks)
              (callbackEnsure callbacks)

    genActions ::
         (MonadGen gen, MonadTest m)
      => Range Int
      -> [Command gen m state]
      -> Context state
      -> gen ([Action m state], Context state)
    genActions :: 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 Context state
    ctx = do
      xs <- GenT (GenBase gen) [Action m state] -> gen [Action m state]
    forall a. GenT (GenBase gen) a -> gen a
    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
    forall (f :: (* -> *) -> * -> *) (m :: * -> *) a.
    Transformer f GenT m =>
    GenT (f m) a -> f (GenT 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)
      pure $
        dropInvalid xs `runState` ctx

    -- | A sequence of actions to execute.
    --
    newtype Sequential m state =
      Sequential {
          -- | The sequence of actions.
          forall (m :: * -> *) (state :: (* -> *) -> *).
    Sequential m state -> [Action m state]
    sequentialActions :: [Action m state]
        }

    renderAction :: Action m state -> [String]
    renderAction :: forall (m :: * -> *) (state :: (* -> *) -> *).
    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 a. [a] -> 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 a b. (a -> b) -> [a] -> [b]
    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 :: forall (m :: * -> *) (state :: (* -> *) -> *).
    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 a. [a] -> 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
    -> 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 a b. (a -> b) -> [a] -> [b]
    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 :: forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
    (MonadGen gen, MonadTest m) =>
    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 a b. (a -> b) -> gen a -> gen b
    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.
          forall (m :: * -> *) (state :: (* -> *) -> *).
    Parallel m state -> [Action m state]
    parallelPrefix :: [Action m state]

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

          -- | The second branch.
        , forall (m :: * -> *) (state :: (* -> *) -> *).
    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 :: forall (m :: * -> *) (state :: (* -> *) -> *).
    (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 :: forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
    (MonadGen gen, MonadTest m) =>
    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
      (prefix, 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)
      (branch1, ctx1) <- genActions parallelN commands ctx0
      (branch2, _ctx2) <- genActions parallelN commands ctx1 { contextState = contextState ctx0 }

      pure $ Parallel prefix branch1 branch2

    data ActionCheck state =
      ActionCheck {
          forall (state :: (* -> *) -> *).
    ActionCheck state -> state Concrete -> state Concrete
    checkUpdate :: state Concrete -> state Concrete
        , forall (state :: (* -> *) -> *).
    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 :: forall (m :: * -> *) (state :: (* -> *) -> *).
    (MonadTest m, HasCallStack) =>
    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
        env0 <- StateT Environment m Environment
    forall s (m :: * -> *). MonadState s m => m s
    get
        input <- evalEither $ reify env0 sinput
        output <- lift $ exec input

        let
          coutput =
            output -> Concrete output
    forall a. a -> Concrete a
    Concrete output
    output

          env =
            Symbolic output -> Concrete output -> Environment -> Environment
    forall a. Symbolic a -> Concrete a -> Environment -> Environment
    insertConcrete Symbolic output
    soutput Concrete output
    coutput Environment
    env0

        put env

        pure $
          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 :: forall (m :: * -> *) (state :: (* -> *) -> *).
    (MonadTest m, HasCallStack) =>
    (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 <- 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 <- exec input

        let
          coutput =
            output -> Concrete output
    forall a. a -> Concrete a
    Concrete output
    output

          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 =
            Symbolic output -> Concrete output -> Environment -> Environment
    forall a. Symbolic a -> Concrete a -> Environment -> Environment
    insertConcrete Symbolic output
    soutput Concrete output
    coutput Environment
    env0

        liftTest $ ensure state0 state input output

        pure (state, 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 (m :: * -> *) (state :: (* -> *) -> *).
    (MonadTest m, MonadCatch m, HasCallStack) =>
    (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 :: forall a. [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 :: forall (state :: (* -> *) -> *).
    state Concrete -> [ActionCheck state] -> Test ()
    checkActions state Concrete
    s0 = \case
      [] ->
        () -> Test ()
    forall a. a -> TestT Identity a
    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 :: forall (m :: * -> *) (state :: (* -> *) -> *).
    MonadTest m =>
    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 a b. (a -> b) -> [a] -> [b]
    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 a. a -> m a
    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 (m :: * -> *) (state :: (* -> *) -> *).
    (MonadTest m, MonadCatch m, MonadBaseControl IO m, HasCallStack) =>
    (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
        (s0, 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

        ((xs, env1), (ys, env2)) <-
          Async.concurrently
            (runStateT (traverse execute branch1) env0)
            (runStateT (traverse execute branch2) env0)

        let
          env = [Environment] -> Environment
    unionsEnvironment [Environment
    env0, Environment
    env1, Environment
    env2]

        annotate $ renderParallel (renderActionResult env) p
        linearize s0 xs ys