{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE ExistentialQuantification  #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs               #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE RecordWildCards            #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE UndecidableInstances       #-}

module Test.StateMachine.Lockstep.NAry (
    -- * Test type-level parameters
    MockState
  , Cmd
  , Resp
  , RealHandles
  , MockHandle
  , Test
  , Tag
    -- * Test term-level parameters
  , StateMachineTest(..)
  , Event(..)
  , hoistStateMachineTest
    -- * Handle instantiation
  , At(..)
  , (:@)
    -- * Model state
  , Model(..)
  , Refs(..)
  , Refss(..)
  , FlipRef(..)
    -- * Running the tests
  , prop_sequential
  , prop_parallel
    -- * Examples
  , showLabelledExamples'
  , showLabelledExamples
  -- * Translate to state machine model
  , toStateMachine
  ) where

import           Data.Functor.Classes
import           Data.Kind
                   (Type)
import           Data.Maybe
                   (fromJust)
import           Data.Semigroup                       hiding
                   (All)
import           Data.SOP
import           Data.Typeable
import           GHC.Generics
                   (Generic)
import           Prelude
import           Test.QuickCheck
import           Test.QuickCheck.Monadic
import           Test.StateMachine                    hiding
                   (showLabelledExamples, showLabelledExamples')

import qualified Data.Monoid                          as M
import qualified Test.StateMachine.Labelling          as Label
import qualified Test.StateMachine.Sequential         as Seq
import qualified Test.StateMachine.Types              as QSM
import qualified Test.StateMachine.Types.Rank2        as Rank2

import           Test.StateMachine.Lockstep.Auxiliary
import qualified Test.StateMachine.TreeDiff           as TD

{-------------------------------------------------------------------------------
  Test type-level parameters
-------------------------------------------------------------------------------}

-- | Mock state
--
-- The @t@ argument (here and elsewhere) is a type-level tag that combines all
-- aspects of the test; it does not need any term-level constructors
--
-- > data MyTest
-- > type instance MockState MyTest = ..
type family MockState t :: Type

-- | Type-level list of the types of the handles in the system under test
--
-- NOTE: If your system under test only requires a single real handle, you
-- might consider using "Test.StateMachine.Lockstep.Simple" instead.
type family RealHandles t :: [Type]

-- | Mock handles
--
-- For each real handle @a@, @MockHandle t a@ is the corresponding mock handle.
data family MockHandle t a :: Type

-- | Commands
--
-- In @Cmd t f hs@, @hs@ is the list of real handle types, and @f@ is some
-- functor applied to each of them. Two typical instantiations are
--
-- > Cmd t I              (RealHandles t)   -- for the system under test
-- > Cmd t (MockHandle t) (RealHandles t)   -- for the mock
data family Cmd t :: (Type -> Type) -> [Type] -> Type

-- | Responses
--
-- The type arguments are similar to those of @Cmd@. Two typical instances:
--
-- > Resp t I              (RealHandles t)  -- for the system under test
-- > Resp t (MockHandle t) (RealHandles t)  -- for the mock
data family Resp t :: (Type -> Type) -> [Type] -> Type

-- | Tags
--
-- Tags are used when labelling execution runs in 'prop_sequential', as well as
-- when looking for minimal examples with a given label
-- ('showLabelledExamples').
type family Tag t :: Type

{-------------------------------------------------------------------------------
  Reference environments
-------------------------------------------------------------------------------}

-- | Relation between real and mock references for single handle type @a@
newtype Refs t r a = Refs { forall t (r :: * -> *) a.
Refs t r a -> [(Reference a r, MockHandle t a)]
unRefs :: [(Reference a r, MockHandle t a)] }
  deriving newtype (NonEmpty (Refs t r a) -> Refs t r a
Refs t r a -> Refs t r a -> Refs t r a
forall b. Integral b => b -> Refs t r a -> Refs t r a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall t (r :: * -> *) a. NonEmpty (Refs t r a) -> Refs t r a
forall t (r :: * -> *) a. Refs t r a -> Refs t r a -> Refs t r a
forall t (r :: * -> *) a b.
Integral b =>
b -> Refs t r a -> Refs t r a
stimes :: forall b. Integral b => b -> Refs t r a -> Refs t r a
$cstimes :: forall t (r :: * -> *) a b.
Integral b =>
b -> Refs t r a -> Refs t r a
sconcat :: NonEmpty (Refs t r a) -> Refs t r a
$csconcat :: forall t (r :: * -> *) a. NonEmpty (Refs t r a) -> Refs t r a
<> :: Refs t r a -> Refs t r a -> Refs t r a
$c<> :: forall t (r :: * -> *) a. Refs t r a -> Refs t r a -> Refs t r a
Semigroup, Refs t r a
[Refs t r a] -> Refs t r a
Refs t r a -> Refs t r a -> Refs t r a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall t (r :: * -> *) a. Semigroup (Refs t r a)
forall t (r :: * -> *) a. Refs t r a
forall t (r :: * -> *) a. [Refs t r a] -> Refs t r a
forall t (r :: * -> *) a. Refs t r a -> Refs t r a -> Refs t r a
mconcat :: [Refs t r a] -> Refs t r a
$cmconcat :: forall t (r :: * -> *) a. [Refs t r a] -> Refs t r a
mappend :: Refs t r a -> Refs t r a -> Refs t r a
$cmappend :: forall t (r :: * -> *) a. Refs t r a -> Refs t r a -> Refs t r a
mempty :: Refs t r a
$cmempty :: forall t (r :: * -> *) a. Refs t r a
Monoid, forall x. Rep (Refs t r a) x -> Refs t r a
forall x. Refs t r a -> Rep (Refs t r a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t (r :: * -> *) a x. Rep (Refs t r a) x -> Refs t r a
forall t (r :: * -> *) a x. Refs t r a -> Rep (Refs t r a) x
to :: forall x. Rep (Refs t r a) x -> Refs t r a
$cto :: forall t (r :: * -> *) a x. Rep (Refs t r a) x -> Refs t r a
from :: forall x. Refs t r a -> Rep (Refs t r a) x
$cfrom :: forall t (r :: * -> *) a x. Refs t r a -> Rep (Refs t r a) x
Generic)

deriving
  stock
  instance (Show1 r, Show a, Show (MockHandle t a)) => Show (Refs t r a)

deriving
  newtype
  instance (ToExpr a, ToExpr (MockHandle t a)) => ToExpr (Refs t Concrete a)

-- | Relation between real and mock references for /all/ handle types
newtype Refss t r = Refss { forall t (r :: * -> *). Refss t r -> NP (Refs t r) (RealHandles t)
unRefss :: NP (Refs t r) (RealHandles t) }

instance ( Show1 r
         , All (And Show (Compose Show (MockHandle t))) (RealHandles t)
         ) => Show (Refss t r) where
  show :: Refss t r -> String
show = [String] -> String
unlines
       forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
       forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap (forall {k} (t :: k). Proxy t
Proxy @(And Show (Compose Show (MockHandle t)))) forall a.
(Show a, Show (MockHandle t a)) =>
Refs t r a -> K String a
showOne
       forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (r :: * -> *). Refss t r -> NP (Refs t r) (RealHandles t)
unRefss
    where
      showOne :: (Show a, Show (MockHandle t a))
              => Refs t r a -> K String a
      showOne :: forall a.
(Show a, Show (MockHandle t a)) =>
Refs t r a -> K String a
showOne = forall k a (b :: k). a -> K a b
K forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

instance All (And ToExpr (Compose ToExpr (MockHandle t))) (RealHandles t)
      => ToExpr (Refss t Concrete) where
  toExpr :: Refss t Concrete -> Expr
toExpr = [Expr] -> Expr
TD.Lst
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap (forall {k} (t :: k). Proxy t
Proxy @(And ToExpr (Compose ToExpr (MockHandle t)))) forall a.
(ToExpr a, ToExpr (MockHandle t a)) =>
Refs t Concrete a -> K Expr a
toExprOne
         forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (r :: * -> *). Refss t r -> NP (Refs t r) (RealHandles t)
unRefss
    where
      toExprOne :: (ToExpr a, ToExpr (MockHandle t a))
                => Refs t Concrete a -> K TD.Expr a
      toExprOne :: forall a.
(ToExpr a, ToExpr (MockHandle t a)) =>
Refs t Concrete a -> K Expr a
toExprOne = forall k a (b :: k). a -> K a b
K forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToExpr a => a -> Expr
toExpr

instance SListI (RealHandles t) => Semigroup (Refss t r) where
  Refss NP (Refs t r) (RealHandles t)
rss <> :: Refss t r -> Refss t r -> Refss t r
<> Refss NP (Refs t r) (RealHandles t)
rss' = forall t (r :: * -> *). NP (Refs t r) (RealHandles t) -> Refss t r
Refss forall a b. (a -> b) -> a -> b
$ forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith forall a. Semigroup a => a -> a -> a
(<>) NP (Refs t r) (RealHandles t)
rss NP (Refs t r) (RealHandles t)
rss'

instance SListI (RealHandles t) => Monoid (Refss t r) where
  mempty :: Refss t r
mempty = forall t (r :: * -> *). NP (Refs t r) (RealHandles t) -> Refss t r
Refss forall a b. (a -> b) -> a -> b
$ forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure (forall t (r :: * -> *) a.
[(Reference a r, MockHandle t a)] -> Refs t r a
Refs forall a. Monoid a => a
mempty)

{-------------------------------------------------------------------------------
  Default instantiation to handles
-------------------------------------------------------------------------------}

type family Test (f :: (Type -> Type) -> [Type] -> Type) :: Type where
  Test (Cmd  t) = t
  Test (Resp t) = t

newtype FlipRef r h = FlipRef { forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef :: Reference h r }
  deriving stock (Int -> FlipRef r h -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (r :: * -> *) h.
(Show1 r, Show h) =>
Int -> FlipRef r h -> ShowS
forall (r :: * -> *) h. (Show1 r, Show h) => [FlipRef r h] -> ShowS
forall (r :: * -> *) h. (Show1 r, Show h) => FlipRef r h -> String
showList :: [FlipRef r h] -> ShowS
$cshowList :: forall (r :: * -> *) h. (Show1 r, Show h) => [FlipRef r h] -> ShowS
show :: FlipRef r h -> String
$cshow :: forall (r :: * -> *) h. (Show1 r, Show h) => FlipRef r h -> String
showsPrec :: Int -> FlipRef r h -> ShowS
$cshowsPrec :: forall (r :: * -> *) h.
(Show1 r, Show h) =>
Int -> FlipRef r h -> ShowS
Show)

-- @f@ will be instantiated with @Cmd@ or @Resp@
-- @r@ will be instantiated with 'Symbolic' or 'Concrete'
newtype At f r = At { forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
At f r -> f (FlipRef r) (RealHandles (Test f))
unAt :: f (FlipRef r) (RealHandles (Test f)) }
type    f :@ r = At f r

deriving
  stock
  instance (Show (f (FlipRef r) (RealHandles (Test f)))) => Show (At f r)

{-------------------------------------------------------------------------------
  Model
-------------------------------------------------------------------------------}

data Model t r = Model {
      forall t (r :: * -> *). Model t r -> MockState t
modelState :: MockState t
    , forall t (r :: * -> *). Model t r -> Refss t r
modelRefss :: Refss t r
    }
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t (r :: * -> *) x. Rep (Model t r) x -> Model t r
forall t (r :: * -> *) x. Model t r -> Rep (Model t r) x
$cto :: forall t (r :: * -> *) x. Rep (Model t r) x -> Model t r
$cfrom :: forall t (r :: * -> *) x. Model t r -> Rep (Model t r) x
Generic)

deriving stock instance ( Show1 r
                        , Show (MockState t)
                        , All (And Show (Compose Show (MockHandle t))) (RealHandles t)
                        ) => Show (Model t r)

instance ( ToExpr (MockState t)
         , All (And ToExpr (Compose ToExpr (MockHandle t))) (RealHandles t)
         ) => ToExpr (Model t Concrete)

initModel :: StateMachineTest t m -> Model t r
initModel :: forall t (m :: * -> *) (r :: * -> *).
StateMachineTest t m -> Model t r
initModel StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
tag :: [Event t Symbolic] -> [Tag t]
cleanup :: Model t Concrete -> m ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
..} = forall t (r :: * -> *). MockState t -> Refss t r -> Model t r
Model MockState t
initMock (forall t (r :: * -> *). NP (Refs t r) (RealHandles t) -> Refss t r
Refss (forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure (forall t (r :: * -> *) a.
[(Reference a r, MockHandle t a)] -> Refs t r a
Refs [])))

{-------------------------------------------------------------------------------
  High level API
-------------------------------------------------------------------------------}

-- | State machine test
--
-- This captures the design patterns sketched in
-- <https://well-typed.com/blog/2019/01/qsm-in-depth/>.
data StateMachineTest t m =
    ( Monad m
    -- Requirements on the handles
    , All Typeable                                     (RealHandles t)
    , All Eq                                           (RealHandles t)
    , All (And Show   (Compose Show   (MockHandle t))) (RealHandles t)
    , All (And ToExpr (Compose ToExpr (MockHandle t))) (RealHandles t)
    -- Response
    , NTraversable (Resp t)
    , Eq   (Resp t (MockHandle t)     (RealHandles t))
    , Show (Resp t (MockHandle t)     (RealHandles t))
    , Show (Resp t (FlipRef Symbolic) (RealHandles t))
    , Show (Resp t (FlipRef Concrete) (RealHandles t))
    -- Command
    , NTraversable (Cmd t)
    , Show (Cmd t (FlipRef Symbolic) (RealHandles t))
    , Show (Cmd t (FlipRef Concrete) (RealHandles t))
    -- MockState
    , Show   (MockState t)
    , ToExpr (MockState t)
    -- Tags
    , Show (Tag t)
    ) => StateMachineTest {
      forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
runMock    :: Cmd t (MockHandle t) (RealHandles t) -> MockState t -> (Resp t (MockHandle t) (RealHandles t), MockState t)
    , forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runReal    :: Cmd t I              (RealHandles t) -> m (Resp t I (RealHandles t))
    , forall t (m :: * -> *). StateMachineTest t m -> MockState t
initMock   :: MockState t
    , forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles :: forall f. Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
    , forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator  :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
    , forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker   :: Model t Symbolic -> Cmd t :@ Symbolic -> [Cmd t :@ Symbolic]
    , forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
cleanup    :: Model t Concrete -> m ()
    , forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
tag        :: [Event t Symbolic] -> [Tag t]
    }

hoistStateMachineTest :: Monad n
                      => (forall a. m a -> n a)
                      -> StateMachineTest t m
                      -> StateMachineTest t n
hoistStateMachineTest :: forall (n :: * -> *) (m :: * -> *) t.
Monad n =>
(forall a. m a -> n a)
-> StateMachineTest t m -> StateMachineTest t n
hoistStateMachineTest forall a. m a -> n a
f StateMachineTest {MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
tag :: [Event t Symbolic] -> [Tag t]
cleanup :: Model t Concrete -> m ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
..} = StateMachineTest {
      runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
runMock    = Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
runMock
    , runReal :: Cmd t I (RealHandles t) -> n (Resp t I (RealHandles t))
runReal    = forall a. m a -> n a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runReal
    , initMock :: MockState t
initMock   = MockState t
initMock
    , newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles = forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles
    , generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator  = Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator
    , shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker   = Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker
    , cleanup :: Model t Concrete -> n ()
cleanup    = forall a. m a -> n a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model t Concrete -> m ()
cleanup
    , tag :: [Event t Symbolic] -> [Tag t]
tag        = [Event t Symbolic] -> [Tag t]
tag
    }

semantics :: StateMachineTest t m
          -> Cmd t :@ Concrete
          -> m (Resp t :@ Concrete)
semantics :: forall t (m :: * -> *).
StateMachineTest t m
-> (Cmd t :@ Concrete) -> m (Resp t :@ Concrete)
semantics StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
tag :: [Event t Symbolic] -> [Tag t]
cleanup :: Model t Concrete -> m ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
..} (At Cmd t (FlipRef Concrete) (RealHandles (Test (Cmd t)))
c) =
    forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (g :: k -> *)
       (h :: k -> *).
(NTraversable f, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> h a)
-> f g xs
-> f h xs
ncfmap (forall {k} (t :: k). Proxy t
Proxy @Typeable) (forall a b. a -> b -> a
const forall a. Typeable a => I a -> FlipRef Concrete a
wrapConcrete) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runReal (forall {k} (f :: (k -> *) -> [k] -> *) (xs :: [k]) (g :: k -> *)
       (h :: k -> *).
(NTraversable f, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> h a) -> f g xs -> f h xs
nfmap (forall a b. a -> b -> a
const forall a. FlipRef Concrete a -> I a
unwrapConcrete) Cmd t (FlipRef Concrete) (RealHandles (Test (Cmd t)))
c)

unwrapConcrete :: FlipRef Concrete a -> I a
unwrapConcrete :: forall a. FlipRef Concrete a -> I a
unwrapConcrete = forall a. a -> I a
I forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Reference a Concrete -> a
concrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef

wrapConcrete :: Typeable a => I a -> FlipRef Concrete a
wrapConcrete :: forall a. Typeable a => I a -> FlipRef Concrete a
wrapConcrete = forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Typeable a => a -> Reference a Concrete
reference  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. I a -> a
unI

-- | Turn @Cmd@ or @Resp@ in terms of (symbolic or concrete) references to
-- real handles into a command in terms of mock handles.
--
-- This is isomorphic to
--
-- > toMock :: Refss t Symbolic
--          -> Cmd (FlipRef r) (Handles t)
--          -> Cmd  ToMock     (Handles t)
toMockHandles :: (NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r)
              => Refss t r -> f :@ r -> f (MockHandle t) (RealHandles t)
toMockHandles :: forall (f :: (* -> *) -> [*] -> *) t (r :: * -> *).
(NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r) =>
Refss t r -> (f :@ r) -> f (MockHandle t) (RealHandles t)
toMockHandles Refss t r
rss (At f (FlipRef r) (RealHandles (Test f))
fr) =
    forall {k} (f :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
       (xs :: [k]) (proxy :: (k -> Constraint) -> *) (g :: k -> *)
       (h :: k -> *).
(NTraversable f, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> h a)
-> f g xs
-> f h xs
ncfmap (forall {k} (t :: k). Proxy t
Proxy @Eq) (\Elem (RealHandles t) a
pf -> forall a (r :: * -> *) t.
(Eq a, Eq1 r) =>
NP (Refs t r) (RealHandles t)
-> Elem (RealHandles t) a -> Reference a r -> MockHandle t a
find (forall t (r :: * -> *). Refss t r -> NP (Refs t r) (RealHandles t)
unRefss Refss t r
rss) Elem (RealHandles t) a
pf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef) f (FlipRef r) (RealHandles (Test f))
fr
  where
    find :: (Eq a, Eq1 r)
         => NP (Refs t r) (RealHandles t)
         -> Elem (RealHandles t) a
         -> Reference a r -> MockHandle t a
    find :: forall a (r :: * -> *) t.
(Eq a, Eq1 r) =>
NP (Refs t r) (RealHandles t)
-> Elem (RealHandles t) a -> Reference a r -> MockHandle t a
find NP (Refs t r) (RealHandles t)
refss Elem (RealHandles t) a
ix Reference a r
r = forall t (r :: * -> *) a.
Refs t r a -> [(Reference a r, MockHandle t a)]
unRefs (forall {k} (f :: k -> *) (xs :: [k]) (a :: k).
NP f xs -> Elem xs a -> f a
npAt NP (Refs t r) (RealHandles t)
refss Elem (RealHandles t) a
ix) forall k a. Eq k => [(k, a)] -> k -> a
! Reference a r
r

step :: Eq1 r
     => StateMachineTest t m
     -> Model t r
     -> Cmd t :@ r
     -> (Resp t (MockHandle t) (RealHandles t), MockState t)
step :: forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
step StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
tag :: [Event t Symbolic] -> [Tag t]
cleanup :: Model t Concrete -> m ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
..} (Model MockState t
st Refss t r
rss) Cmd t :@ r
cmd =
    Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
runMock (forall (f :: (* -> *) -> [*] -> *) t (r :: * -> *).
(NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r) =>
Refss t r -> (f :@ r) -> f (MockHandle t) (RealHandles t)
toMockHandles Refss t r
rss Cmd t :@ r
cmd) MockState t
st

data Event t r = Event {
      forall t (r :: * -> *). Event t r -> Model t r
before   :: Model t    r
    , forall t (r :: * -> *). Event t r -> Cmd t :@ r
cmd      :: Cmd   t :@ r
    , forall t (r :: * -> *). Event t r -> Model t r
after    :: Model t    r
    , forall t (r :: * -> *).
Event t r -> Resp t (MockHandle t) (RealHandles t)
mockResp :: Resp t (MockHandle t) (RealHandles t)
    }

lockstep :: forall t m r. Eq1 r
         => StateMachineTest t m
         -> Model t    r
         -> Cmd   t :@ r
         -> Resp  t :@ r
         -> Event t    r
lockstep :: forall t (m :: * -> *) (r :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
lockstep sm :: StateMachineTest t m
sm@StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
tag :: [Event t Symbolic] -> [Tag t]
cleanup :: Model t Concrete -> m ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
..} m :: Model t r
m@(Model MockState t
_ Refss t r
rss) Cmd t :@ r
c (At Resp t (FlipRef r) (RealHandles (Test (Resp t)))
resp) = Event {
      before :: Model t r
before   = Model t r
m
    , cmd :: Cmd t :@ r
cmd      = Cmd t :@ r
c
    , after :: Model t r
after    = forall t (r :: * -> *). MockState t -> Refss t r -> Model t r
Model MockState t
st' (Refss t r
rss forall a. Semigroup a => a -> a -> a
<> Refss t r
rss')
    , mockResp :: Resp t (MockHandle t) (RealHandles t)
mockResp = Resp t (MockHandle t) (RealHandles t)
resp'
    }
  where
    (Resp t (MockHandle t) (RealHandles t)
resp', MockState t
st') = forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
step StateMachineTest t m
sm Model t r
m Cmd t :@ r
c

    rss' :: Refss t r
    rss' :: Refss t r
rss' = forall t (r :: * -> *).
SListI (RealHandles t) =>
NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandle t) (RealHandles t) -> Refss t r
zipHandles (forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles Resp t (FlipRef r) (RealHandles (Test (Resp t)))
resp) (forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles Resp t (MockHandle t) (RealHandles t)
resp')

transition :: Eq1 r
           => StateMachineTest t m
           -> Model t    r
           -> Cmd   t :@ r
           -> Resp  t :@ r
           -> Model t    r
transition :: forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Model t r
transition StateMachineTest t m
sm Model t r
m Cmd t :@ r
c = forall t (r :: * -> *). Event t r -> Model t r
after forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (m :: * -> *) (r :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
lockstep StateMachineTest t m
sm Model t r
m Cmd t :@ r
c

postcondition :: StateMachineTest t m
              -> Model t    Concrete
              -> Cmd   t :@ Concrete
              -> Resp  t :@ Concrete
              -> Logic
postcondition :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Concrete
-> (Cmd t :@ Concrete)
-> (Resp t :@ Concrete)
-> Logic
postcondition sm :: StateMachineTest t m
sm@StateMachineTest{} Model t Concrete
m Cmd t :@ Concrete
c Resp t :@ Concrete
r =
    forall (f :: (* -> *) -> [*] -> *) t (r :: * -> *).
(NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r) =>
Refss t r -> (f :@ r) -> f (MockHandle t) (RealHandles t)
toMockHandles (forall t (r :: * -> *). Model t r -> Refss t r
modelRefss forall a b. (a -> b) -> a -> b
$ forall t (r :: * -> *). Event t r -> Model t r
after Event t Concrete
e) Resp t :@ Concrete
r forall a. (Eq a, Show a) => a -> a -> Logic
.== forall t (r :: * -> *).
Event t r -> Resp t (MockHandle t) (RealHandles t)
mockResp Event t Concrete
e
  where
    e :: Event t Concrete
e = forall t (m :: * -> *) (r :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
lockstep StateMachineTest t m
sm Model t Concrete
m Cmd t :@ Concrete
c Resp t :@ Concrete
r

symbolicResp :: StateMachineTest t m
             -> Model t Symbolic
             -> Cmd t :@ Symbolic
             -> GenSym (Resp t :@ Symbolic)
symbolicResp :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic
-> (Cmd t :@ Symbolic)
-> GenSym (Resp t :@ Symbolic)
symbolicResp sm :: StateMachineTest t m
sm@StateMachineTest{} Model t Symbolic
m Cmd t :@ Symbolic
c =
    forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: (k -> *) -> [k] -> *) (m :: * -> *)
       (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (g :: k -> *) (h :: k -> *).
(NTraversable f, Applicative m, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> m (h a))
-> f g xs
-> m (f h xs)
nctraverse (forall {k} (t :: k). Proxy t
Proxy @Typeable) (\Elem (RealHandles t) a
_ MockHandle t a
_ -> forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Typeable a => GenSym (Reference a Symbolic)
genSym) Resp t (MockHandle t) (RealHandles t)
resp
  where
    (Resp t (MockHandle t) (RealHandles t)
resp, MockState t
_mock') = forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
step StateMachineTest t m
sm Model t Symbolic
m Cmd t :@ Symbolic
c

precondition :: forall t. (NTraversable (Cmd t), All Eq (RealHandles t))
             => Model t Symbolic
             -> Cmd t :@ Symbolic
             -> Logic
precondition :: forall t.
(NTraversable (Cmd t), All Eq (RealHandles t)) =>
Model t Symbolic -> (Cmd t :@ Symbolic) -> Logic
precondition (Model MockState t
_ (Refss NP (Refs t Symbolic) (RealHandles t)
hs)) (At Cmd t (FlipRef Symbolic) (RealHandles (Test (Cmd t)))
c) =
    Bool -> Logic
Boolean (All -> Bool
M.getAll forall a b. (a -> b) -> a -> b
$ forall {k} (f :: (k -> *) -> [k] -> *) m (xs :: [k]) (g :: k -> *).
(NTraversable f, Monoid m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m) -> f g xs -> m
nfoldMap forall a. Elem (RealHandles t) a -> FlipRef Symbolic a -> All
check Cmd t (FlipRef Symbolic) (RealHandles (Test (Cmd t)))
c) Logic -> String -> Logic
.// String
"No undefined handles"
  where
    check :: Elem (RealHandles t) a -> FlipRef Symbolic a -> M.All
    check :: forall a. Elem (RealHandles t) a -> FlipRef Symbolic a -> All
check Elem (RealHandles t) a
ix (FlipRef Reference a Symbolic
a) = Bool -> All
M.All forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Reference a Symbolic -> Reference a Symbolic -> Bool
sameRef Reference a Symbolic
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (forall t (r :: * -> *) a.
Refs t r a -> [(Reference a r, MockHandle t a)]
unRefs (NP (Refs t Symbolic) (RealHandles t)
hs forall {k} (f :: k -> *) (xs :: [k]) (a :: k).
NP f xs -> Elem xs a -> f a
`npAt` Elem (RealHandles t) a
ix))

    -- TODO: Patch QSM
    sameRef :: Reference a Symbolic -> Reference a Symbolic -> Bool
    sameRef :: forall a. Reference a Symbolic -> Reference a Symbolic -> Bool
sameRef (QSM.Reference (QSM.Symbolic Var
v)) (QSM.Reference (QSM.Symbolic Var
v')) = Var
v forall a. Eq a => a -> a -> Bool
== Var
v'

toStateMachine :: StateMachineTest t m
               -> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine :: forall t (m :: * -> *).
StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine sm :: StateMachineTest t m
sm@StateMachineTest{} = StateMachine {
      initModel :: forall (r :: * -> *). Model t r
initModel     = forall t (m :: * -> *) (r :: * -> *).
StateMachineTest t m -> Model t r
initModel     StateMachineTest t m
sm
    , transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model t r -> At (Cmd t) r -> At (Resp t) r -> Model t r
transition    = forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Model t r
transition    StateMachineTest t m
sm
    , precondition :: Model t Symbolic -> At (Cmd t) Symbolic -> Logic
precondition  = forall t.
(NTraversable (Cmd t), All Eq (RealHandles t)) =>
Model t Symbolic -> (Cmd t :@ Symbolic) -> Logic
precondition
    , postcondition :: Model t Concrete
-> At (Cmd t) Concrete -> At (Resp t) Concrete -> Logic
postcondition = forall t (m :: * -> *).
StateMachineTest t m
-> Model t Concrete
-> (Cmd t :@ Concrete)
-> (Resp t :@ Concrete)
-> Logic
postcondition StateMachineTest t m
sm
    , generator :: Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
generator     = forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator     StateMachineTest t m
sm
    , shrinker :: Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
shrinker      = forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker      StateMachineTest t m
sm
    , semantics :: At (Cmd t) Concrete -> m (At (Resp t) Concrete)
semantics     = forall t (m :: * -> *).
StateMachineTest t m
-> (Cmd t :@ Concrete) -> m (Resp t :@ Concrete)
semantics     StateMachineTest t m
sm
    , mock :: Model t Symbolic
-> At (Cmd t) Symbolic -> GenSym (At (Resp t) Symbolic)
mock          = forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic
-> (Cmd t :@ Symbolic)
-> GenSym (Resp t :@ Symbolic)
symbolicResp  StateMachineTest t m
sm
    , cleanup :: Model t Concrete -> m ()
cleanup       = forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
cleanup       StateMachineTest t m
sm
    , invariant :: Maybe (Model t Concrete -> Logic)
invariant     = forall a. Maybe a
Nothing
    }

-- | Sequential test
prop_sequential :: forall t.
                   StateMachineTest t IO
                -> Maybe Int   -- ^ (Optional) minimum number of commands
                -> Property
prop_sequential :: forall t. StateMachineTest t IO -> Maybe Int -> Property
prop_sequential sm :: StateMachineTest t IO
sm@StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> IO ()
Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
Cmd t I (RealHandles t) -> IO (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
tag :: [Event t Symbolic] -> [Tag t]
cleanup :: Model t Concrete -> IO ()
shrinker :: Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> IO (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
..} Maybe Int
mMinSize =
    forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
 Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int -> (Commands cmd resp -> prop) -> Property
forAllCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' Maybe Int
mMinSize forall a b. (a -> b) -> a -> b
$ \Commands (At (Cmd t)) (At (Resp t))
cmds ->
      forall a. Testable a => PropertyM IO a -> Property
monadicIO forall a b. (a -> b) -> a -> b
$ do
        (History (At (Cmd t)) (At (Resp t))
hist, Model t Concrete
_model, Reason
res) <- forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadIO m) =>
StateMachine model cmd m resp
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
runCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' Commands (At (Cmd t)) (At (Resp t))
cmds
        forall (m :: * -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(MonadIO m, ToExpr (model Concrete), Show (cmd Concrete),
 Show (resp Concrete)) =>
StateMachine model cmd m resp
-> History cmd resp -> Property -> PropertyM m ()
prettyCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' History (At (Cmd t)) (At (Resp t))
hist
          forall a b. (a -> b) -> a -> b
$ forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Tags" (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Commands (At (Cmd t)) (At (Resp t)) -> [Tag t]
tagCmds Commands (At (Cmd t)) (At (Resp t))
cmds)
          forall a b. (a -> b) -> a -> b
$ Reason
res forall a. (Eq a, Show a) => a -> a -> Property
=== Reason
Ok
  where
    sm' :: StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' = forall t (m :: * -> *).
StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine StateMachineTest t IO
sm

    tagCmds :: QSM.Commands (At (Cmd t)) (At (Resp t)) -> [Tag t]
    tagCmds :: Commands (At (Cmd t)) (At (Resp t)) -> [Tag t]
tagCmds = [Event t Symbolic] -> [Tag t]
tag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall t (m :: * -> *).
StateMachineTest t m
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
fromLabelEvent StateMachineTest t IO
sm) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> Commands cmd resp -> [Event model cmd resp Symbolic]
Label.execCmds StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm'

-- | Parallel test
--
-- NOTE: This currently does not do labelling.
prop_parallel :: StateMachineTest t IO
              -> Maybe Int   -- ^ (Optional) minimum number of commands
              -> Property
prop_parallel :: forall t. StateMachineTest t IO -> Maybe Int -> Property
prop_parallel sm :: StateMachineTest t IO
sm@StateMachineTest{} Maybe Int
mMinSize =
    forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
 Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int -> (ParallelCommands cmd resp -> prop) -> Property
forAllParallelCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' Maybe Int
mMinSize forall a b. (a -> b) -> a -> b
$ \ParallelCommands (At (Cmd t)) (At (Resp t))
cmds ->
      forall a. Testable a => PropertyM IO a -> Property
monadicIO forall a b. (a -> b) -> a -> b
$ do
        [(History (At (Cmd t)) (At (Resp t)), Model t Concrete, Logic)]
hist <- forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' ParallelCommands (At (Cmd t)) (At (Resp t))
cmds
        -- TODO: Ideally we would tag here as well, but unlike 'prettyCommands',
        -- 'prettyParallelCommands' does not give us a hook to specify a
        -- 'Property', so this would require a change to the QSM core.
        forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       a.
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
 Foldable cmd) =>
ParallelCommands cmd resp
-> [(History cmd resp, a, Logic)] -> PropertyM m ()
prettyParallelCommands ParallelCommands (At (Cmd t)) (At (Resp t))
cmds [(History (At (Cmd t)) (At (Resp t)), Model t Concrete, Logic)]
hist
  where
    sm' :: StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' = forall t (m :: * -> *).
StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine StateMachineTest t IO
sm

{-------------------------------------------------------------------------------
  Labelling
-------------------------------------------------------------------------------}

-- | Translate QSM's 'Label.Event' into our 'Event'
--
-- The QSM 'Label.Event' is purely in terms of symbolic references. In order to
-- construct our 'Event' from this, we need to reconstruct the mock response.
-- We can do this, because we maintain a mapping between references and mock
-- handles in the model, irrespective of whether those references are symbolic
-- (as here) or concrete (during test execution). We can therefore apply this
-- mapping, and re-compute the mock response.
--
-- We could use 'lockstep' instead of 'step', but this would recompute the
-- new state, which is not necessary.
--
-- NOTE: This forgets the symbolic response in favour of the mock response.
-- This seems more in line with what we do elsewhere in the lockstep
-- infrastructure, but we could conceivably return both.
fromLabelEvent :: StateMachineTest t m
               -> Label.Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
               -> Event t Symbolic
fromLabelEvent :: forall t (m :: * -> *).
StateMachineTest t m
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
fromLabelEvent StateMachineTest t m
sm Label.Event{Model t Symbolic
At (Resp t) Symbolic
At (Cmd t) Symbolic
eventResp :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
Event model cmd resp r -> resp r
eventAfter :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
Event model cmd resp r -> model r
eventCmd :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
Event model cmd resp r -> cmd r
eventBefore :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
Event model cmd resp r -> model r
eventResp :: At (Resp t) Symbolic
eventAfter :: Model t Symbolic
eventCmd :: At (Cmd t) Symbolic
eventBefore :: Model t Symbolic
..} = Event{
      before :: Model t Symbolic
before   = Model t Symbolic
eventBefore
    , cmd :: At (Cmd t) Symbolic
cmd      = At (Cmd t) Symbolic
eventCmd
    , after :: Model t Symbolic
after    = Model t Symbolic
eventAfter
    , mockResp :: Resp t (MockHandle t) (RealHandles t)
mockResp = Resp t (MockHandle t) (RealHandles t)
resp'
    }
  where
    (Resp t (MockHandle t) (RealHandles t)
resp', MockState t
_st') = forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
step StateMachineTest t m
sm Model t Symbolic
eventBefore At (Cmd t) Symbolic
eventCmd

-- | Show minimal examples for each of the generated tags.
--
-- This is the analogue of 'Test.StateMachine.showLabelledExamples''.
-- See also 'showLabelledExamples'.
showLabelledExamples' :: StateMachineTest t m
                      -> Maybe Int
                      -- ^ Seed
                      -> Int
                      -- ^ Number of tests to run to find examples
                      -> (Tag t -> Bool)
                      -- ^ Tag filter (can be @const True@)
                      -> IO ()
showLabelledExamples' :: forall t (m :: * -> *).
StateMachineTest t m
-> Maybe Int -> Int -> (Tag t -> Bool) -> IO ()
showLabelledExamples' sm :: StateMachineTest t m
sm@StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
tag :: [Event t Symbolic] -> [Tag t]
cleanup :: Model t Concrete -> m ()
shrinker :: Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
..} Maybe Int
mReplay Int
numTests =
    forall tag (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (m :: * -> *).
(Show tag, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int
-> Int
-> ([Event model cmd resp Symbolic] -> [tag])
-> (tag -> Bool)
-> IO ()
Seq.showLabelledExamples'
      (forall t (m :: * -> *).
StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine StateMachineTest t m
sm)
      Maybe Int
mReplay
      Int
numTests
      ([Event t Symbolic] -> [Tag t]
tag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall t (m :: * -> *).
StateMachineTest t m
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
fromLabelEvent StateMachineTest t m
sm))

-- | Simplified form of 'showLabelledExamples''
showLabelledExamples :: StateMachineTest t m -> IO ()
showLabelledExamples :: forall t (m :: * -> *). StateMachineTest t m -> IO ()
showLabelledExamples sm :: StateMachineTest t m
sm@StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
tag :: [Event t Symbolic] -> [Tag t]
cleanup :: Model t Concrete -> m ()
shrinker :: Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
..} =
    forall tag (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (m :: * -> *).
(Show tag, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ([Event model cmd resp Symbolic] -> [tag]) -> IO ()
Seq.showLabelledExamples
      (forall t (m :: * -> *).
StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine StateMachineTest t m
sm)
      ([Event t Symbolic] -> [Tag t]
tag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall t (m :: * -> *).
StateMachineTest t m
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
fromLabelEvent StateMachineTest t m
sm))

{-------------------------------------------------------------------------------
  Rank2 instances
-------------------------------------------------------------------------------}

instance (NTraversable (Cmd t), SListI (RealHandles t))
      => Rank2.Functor (At (Cmd t)) where
  fmap :: forall p q. (forall a. p a -> q a) -> At (Cmd t) p -> At (Cmd t) q
  fmap :: forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> At (Cmd t) p -> At (Cmd t) q
fmap forall a. p a -> q a
f (At Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd) = forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At forall a b. (a -> b) -> a -> b
$ forall {k} (f :: (k -> *) -> [k] -> *) (xs :: [k]) (g :: k -> *)
       (h :: k -> *).
(NTraversable f, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> h a) -> f g xs -> f h xs
nfmap (forall a b. a -> b -> a
const forall a. FlipRef p a -> FlipRef q a
f') Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd
    where
      f' :: FlipRef p a -> FlipRef q a
      f' :: forall a. FlipRef p a -> FlipRef q a
f' = forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: (k -> *) -> *) (p :: k -> *) (q :: k -> *).
Functor f =>
(forall (x :: k). p x -> q x) -> f p -> f q
Rank2.fmap forall a. p a -> q a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef

instance (NTraversable (Cmd t), SListI (RealHandles t))
      => Rank2.Foldable (At (Cmd t)) where
  foldMap :: forall p m. Monoid m => (forall a. p a -> m) -> At (Cmd t) p -> m
  foldMap :: forall (p :: * -> *) m.
Monoid m =>
(forall a. p a -> m) -> At (Cmd t) p -> m
foldMap forall a. p a -> m
f (At Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd) = forall {k} (f :: (k -> *) -> [k] -> *) m (xs :: [k]) (g :: k -> *).
(NTraversable f, Monoid m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m) -> f g xs -> m
nfoldMap (forall a b. a -> b -> a
const forall a. FlipRef p a -> m
f') Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd
    where
      f' :: FlipRef p a -> m
      f' :: forall a. FlipRef p a -> m
f' = forall k (f :: (k -> *) -> *) m (p :: k -> *).
(Foldable f, Monoid m) =>
(forall (x :: k). p x -> m) -> f p -> m
Rank2.foldMap forall a. p a -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef

instance (NTraversable (Cmd t), SListI (RealHandles t))
      => Rank2.Traversable (At (Cmd t)) where
  traverse :: forall f p q. Applicative f
           => (forall a. p a -> f (q a)) -> At (Cmd t) p -> f (At (Cmd t) q)
  traverse :: forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> At (Cmd t) p -> f (At (Cmd t) q)
traverse forall a. p a -> f (q a)
f (At Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd) = forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (f :: (k -> *) -> [k] -> *) (m :: * -> *) (xs :: [k])
       (g :: k -> *) (h :: k -> *).
(NTraversable f, Applicative m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m (h a))
-> f g xs -> m (f h xs)
ntraverse (forall a b. a -> b -> a
const forall a. FlipRef p a -> f (FlipRef q a)
f') Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd
    where
      f' :: FlipRef p a -> f (FlipRef q a)
      f' :: forall a. FlipRef p a -> f (FlipRef q a)
f' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> *) (f :: * -> *) (p :: k -> *)
       (q :: k -> *).
(Traversable t, Applicative f) =>
(forall (a :: k). p a -> f (q a)) -> t p -> f (t q)
Rank2.traverse forall a. p a -> f (q a)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef

instance (NTraversable (Resp t), SListI (RealHandles t))
      => Rank2.Functor (At (Resp t)) where
  fmap :: forall p q. (forall a. p a -> q a) -> At (Resp t) p -> At (Resp t) q
  fmap :: forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> At (Resp t) p -> At (Resp t) q
fmap forall a. p a -> q a
f (At Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd) = forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At forall a b. (a -> b) -> a -> b
$ forall {k} (f :: (k -> *) -> [k] -> *) (xs :: [k]) (g :: k -> *)
       (h :: k -> *).
(NTraversable f, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> h a) -> f g xs -> f h xs
nfmap (forall a b. a -> b -> a
const forall a. FlipRef p a -> FlipRef q a
f') Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd
    where
      f' :: FlipRef p a -> FlipRef q a
      f' :: forall a. FlipRef p a -> FlipRef q a
f' = forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: (k -> *) -> *) (p :: k -> *) (q :: k -> *).
Functor f =>
(forall (x :: k). p x -> q x) -> f p -> f q
Rank2.fmap forall a. p a -> q a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef

instance (NTraversable (Resp t), SListI (RealHandles t))
      => Rank2.Foldable (At (Resp t)) where
  foldMap :: forall p m. Monoid m => (forall a. p a -> m) -> At (Resp t) p -> m
  foldMap :: forall (p :: * -> *) m.
Monoid m =>
(forall a. p a -> m) -> At (Resp t) p -> m
foldMap forall a. p a -> m
f (At Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd) = forall {k} (f :: (k -> *) -> [k] -> *) m (xs :: [k]) (g :: k -> *).
(NTraversable f, Monoid m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m) -> f g xs -> m
nfoldMap (forall a b. a -> b -> a
const forall a. FlipRef p a -> m
f') Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd
    where
      f' :: FlipRef p a -> m
      f' :: forall a. FlipRef p a -> m
f' = forall k (f :: (k -> *) -> *) m (p :: k -> *).
(Foldable f, Monoid m) =>
(forall (x :: k). p x -> m) -> f p -> m
Rank2.foldMap forall a. p a -> m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef

instance (NTraversable (Resp t), SListI (RealHandles t))
      => Rank2.Traversable (At (Resp t)) where
  traverse :: forall f p q. Applicative f
           => (forall a. p a -> f (q a)) -> At (Resp t) p -> f (At (Resp t) q)
  traverse :: forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> At (Resp t) p -> f (At (Resp t) q)
traverse forall a. p a -> f (q a)
f (At Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd) = forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (f :: (k -> *) -> [k] -> *) (m :: * -> *) (xs :: [k])
       (g :: k -> *) (h :: k -> *).
(NTraversable f, Applicative m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m (h a))
-> f g xs -> m (f h xs)
ntraverse (forall a b. a -> b -> a
const forall a. FlipRef p a -> f (FlipRef q a)
f') Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd
    where
      f' :: FlipRef p a -> f (FlipRef q a)
      f' :: forall a. FlipRef p a -> f (FlipRef q a)
f' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> *) (f :: * -> *) (p :: k -> *)
       (q :: k -> *).
(Traversable t, Applicative f) =>
(forall (a :: k). p a -> f (q a)) -> t p -> f (t q)
Rank2.traverse forall a. p a -> f (q a)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef

{-------------------------------------------------------------------------------
  Auxiliary
-------------------------------------------------------------------------------}

(!) :: Eq k => [(k, a)] -> k -> a
[(k, a)]
env ! :: forall k a. Eq k => [(k, a)] -> k -> a
! k
r = forall a. HasCallStack => Maybe a -> a
fromJust (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup k
r [(k, a)]
env)

zipHandles :: SListI (RealHandles t)
           => NP ([] :.: FlipRef r)    (RealHandles t)
           -> NP ([] :.: MockHandle t) (RealHandles t)
           -> Refss t r
zipHandles :: forall t (r :: * -> *).
SListI (RealHandles t) =>
NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandle t) (RealHandles t) -> Refss t r
zipHandles = \NP ([] :.: FlipRef r) (RealHandles t)
real NP ([] :.: MockHandle t) (RealHandles t)
mock -> forall t (r :: * -> *). NP (Refs t r) (RealHandles t) -> Refss t r
Refss forall a b. (a -> b) -> a -> b
$ forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith forall (r :: * -> *) a t.
(:.:) [] (FlipRef r) a -> (:.:) [] (MockHandle t) a -> Refs t r a
zip' NP ([] :.: FlipRef r) (RealHandles t)
real NP ([] :.: MockHandle t) (RealHandles t)
mock
  where
    zip' :: (:.:) [] (FlipRef r) a -> (:.:) [] (MockHandle t) a -> Refs t r a
    zip' :: forall (r :: * -> *) a t.
(:.:) [] (FlipRef r) a -> (:.:) [] (MockHandle t) a -> Refs t r a
zip' (Comp [FlipRef r a]
real) (Comp [MockHandle t a]
mock) = forall t (r :: * -> *) a.
[(Reference a r, MockHandle t a)] -> Refs t r a
Refs forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef [FlipRef r a]
real) [MockHandle t a]
mock