{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE DerivingStrategies        #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE RecordWildCards           #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE StandaloneDeriving        #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}

module Test.StateMachine.Lockstep.Simple (
    -- * Test type-level parameters
    MockState
  , Cmd
  , Resp
  , RealHandle
  , MockHandle
  , Test
  , Tag
    -- * Test term-level parameters
  , StateMachineTest(..)
  , Event(..)
    -- * Handle instantiation
  , At(..)
  , (:@)
    -- * Model state
  , Model(..)
    -- * Running the tests
  , prop_sequential
  , prop_parallel
    -- * Translate to n-ary model model
  , fromSimple
  ) where

import           Data.Bifunctor
import           Data.Functor.Classes
import           Data.Kind
                   (Type)
import           Data.SOP
import           Data.Typeable
import           Prelude
import           Test.QuickCheck
import           Test.StateMachine
import           Test.StateMachine.Lockstep.Auxiliary
import           Test.StateMachine.Lockstep.NAry
                   (MockState, Tag)

import qualified Test.StateMachine.Lockstep.NAry      as NAry

{-------------------------------------------------------------------------------
  Top-level parameters
-------------------------------------------------------------------------------}

-- | The type of the real handle in the system under test
--
-- The key difference between the " simple " lockstep infrastructure and the
-- n-ary lockstep infrastructure is that the former only supports a single
-- real handle, whereas the latter supports an arbitrary list of them.
data family RealHandle t :: Type

-- | The type of the mock handle
--
-- NOTE: In the n-ary infrastructure, 'MockHandle' is a type family of /two/
-- arguments, because we have a mock handle for each real handle. Here, however,
-- we only /have/ a single real handle, so the " corresponding " real handle
-- is implicitly @RealHandle t@.
data family MockHandle t :: Type

-- | Commands
--
-- In @Cmd t h@, @h@ is the type of the handle
--
-- > Cmd t (RealHandle t)  -- for the system under test
-- > Cmd t (MockHandle t)  -- for the mock
data family Cmd t :: Type -> Type

-- | Responses
--
-- In @Resp t h@, @h@ is the type of the handle
--
-- > Resp t (RealHandle t)  -- for the system under test
-- > Resp t (MockHandle t)  -- for the mock
data family Resp t :: Type -> Type

{-------------------------------------------------------------------------------
  Default handle instantiation
-------------------------------------------------------------------------------}

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

-- @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 (Reference (RealHandle (Test f)) r)
unAt :: f (Reference (RealHandle (Test f)) r) }
type    f :@ r = At f r

{-------------------------------------------------------------------------------
  Simplified model
-------------------------------------------------------------------------------}

data Model t r = Model {
      forall t (r :: * -> *). Model t r -> MockState t
modelState :: MockState t
    , forall t (r :: * -> *).
Model t r -> [(Reference (RealHandle t) r, MockHandle t)]
modelRefs  :: [(Reference (RealHandle t) r, MockHandle t)]
    }

modelToSimple :: NAry.Model (Simple t) r -> Model t r
modelToSimple :: forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple NAry.Model{modelRefss :: forall t (r :: * -> *). Model t r -> Refss t r
modelRefss = NAry.Refss (NAry.Refs [(Reference x r, MockHandle (Simple t) x)]
rs :* NP (Refs (Simple t) r) xs
Nil), MockState (Simple t)
modelState :: forall t (r :: * -> *). Model t r -> MockState t
modelState :: MockState (Simple t)
..} = Model {
      modelState :: MockState t
modelState = MockState (Simple t)
modelState
    , modelRefs :: [(Reference (RealHandle t) r, MockHandle t)]
modelRefs  = forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock) [(Reference x r, MockHandle (Simple t) x)]
rs
    }

{-------------------------------------------------------------------------------
  Simplified event
-------------------------------------------------------------------------------}

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)
mockResp :: Resp t (MockHandle t)
    }

eventToSimple :: (Functor (Cmd t), Functor (Resp t))
              => NAry.Event (Simple t) r -> Event t r
eventToSimple :: forall t (r :: * -> *).
(Functor (Cmd t), Functor (Resp t)) =>
Event (Simple t) r -> Event t r
eventToSimple NAry.Event{Model (Simple t) r
Cmd (Simple t) :@ r
Resp (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t))
mockResp :: forall t (r :: * -> *).
Event t r -> Resp t (MockHandle t) (RealHandles t)
after :: forall t (r :: * -> *). Event t r -> Model t r
cmd :: forall t (r :: * -> *). Event t r -> Cmd t :@ r
before :: forall t (r :: * -> *). Event t r -> Model t r
mockResp :: Resp (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t))
after :: Model (Simple t) r
cmd :: Cmd (Simple t) :@ r
before :: Model (Simple t) r
..} = Event{
      before :: Model t r
before   = forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple Model (Simple t) r
before
    , cmd :: Cmd t :@ r
cmd      = forall t (r :: * -> *).
Functor (Cmd t) =>
(Cmd (Simple t) :@ r) -> Cmd t :@ r
cmdAtToSimple Cmd (Simple t) :@ r
cmd
    , after :: Model t r
after    = forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple Model (Simple t) r
after
    , mockResp :: Resp t (MockHandle t)
mockResp = forall t.
Functor (Resp t) =>
Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Resp t (MockHandle t)
respMockToSimple Resp (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t))
mockResp
    }

{-------------------------------------------------------------------------------
  Wrap and unwrap
-------------------------------------------------------------------------------}

cmdAtFromSimple :: Functor (Cmd t) => Cmd t :@ r -> NAry.Cmd (Simple t) NAry.:@ r
cmdAtFromSimple :: forall t (r :: * -> *).
Functor (Cmd t) =>
(Cmd t :@ r) -> Cmd (Simple t) :@ r
cmdAtFromSimple = forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
NAry.At forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (f :: * -> *) ks. Cmd t (f ks) -> Cmd (Simple t) f '[ks]
SimpleCmd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (r :: * -> *) h. Reference h r -> FlipRef r h
NAry.FlipRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (r :: * -> *).
At f r -> f (Reference (RealHandle (Test f)) r)
unAt

cmdAtToSimple :: Functor (Cmd t) => NAry.Cmd (Simple t) NAry.:@ r -> Cmd t :@ r
cmdAtToSimple :: forall t (r :: * -> *).
Functor (Cmd t) =>
(Cmd (Simple t) :@ r) -> Cmd t :@ r
cmdAtToSimple = forall (f :: * -> *) (r :: * -> *).
f (Reference (RealHandle (Test f)) r) -> At f r
At forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (r :: * -> *) h. FlipRef r h -> Reference h r
NAry.unFlipRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (f :: * -> *) h. Cmd (Simple t) f '[h] -> Cmd t (f h)
unSimpleCmd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
At f r -> f (FlipRef r) (RealHandles (Test f))
NAry.unAt

cmdMockToSimple :: Functor (Cmd t)
                => NAry.Cmd (Simple t) (NAry.MockHandle (Simple t)) '[RealHandle t]
                -> Cmd t (MockHandle t)
cmdMockToSimple :: forall t.
Functor (Cmd t) =>
Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
cmdMockToSimple = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (f :: * -> *) h. Cmd (Simple t) f '[h] -> Cmd t (f h)
unSimpleCmd

cmdRealToSimple :: Functor (Cmd t)
                => NAry.Cmd (Simple t) I '[RealHandle t]
                -> Cmd t (RealHandle t)
cmdRealToSimple :: forall t.
Functor (Cmd t) =>
Cmd (Simple t) I '[RealHandle t] -> Cmd t (RealHandle t)
cmdRealToSimple = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. I a -> a
unI forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (f :: * -> *) h. Cmd (Simple t) f '[h] -> Cmd t (f h)
unSimpleCmd

respMockFromSimple :: Functor (Resp t)
                   => Resp t (MockHandle t)
                   -> NAry.Resp (Simple t) (NAry.MockHandle (Simple t)) '[RealHandle t]
respMockFromSimple :: forall t.
Functor (Resp t) =>
Resp t (MockHandle t)
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
respMockFromSimple = forall t (f :: * -> *) ks. Resp t (f ks) -> Resp (Simple t) f '[ks]
SimpleResp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. MockHandle t -> MockHandle (Simple t) (RealHandle t)
SimpleToMock

respMockToSimple :: Functor (Resp t)
                 => NAry.Resp (Simple t) (NAry.MockHandle (Simple t)) '[RealHandle t]
                 -> Resp t (MockHandle t)
respMockToSimple :: forall t.
Functor (Resp t) =>
Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Resp t (MockHandle t)
respMockToSimple = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (f :: * -> *) h. Resp (Simple t) f '[h] -> Resp t (f h)
unSimpleResp

respRealFromSimple :: Functor (Resp t)
                   => Resp t (RealHandle t)
                   -> NAry.Resp (Simple t) I '[RealHandle t]
respRealFromSimple :: forall t.
Functor (Resp t) =>
Resp t (RealHandle t) -> Resp (Simple t) I '[RealHandle t]
respRealFromSimple = forall t (f :: * -> *) ks. Resp t (f ks) -> Resp (Simple t) f '[ks]
SimpleResp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> I a
I

{-------------------------------------------------------------------------------
  User defined values
-------------------------------------------------------------------------------}

-- | State machine test
--
-- This captures the design patterns sketched in
-- <https://well-typed.com/blog/2019/01/qsm-in-depth/> for the case where there
-- is exactly one real handle. See "Test.StateMachine.Lockstep.NAry" for the
-- generalization to @n@ handles.
data StateMachineTest t =
    ( Typeable t
      -- Response
    , Eq   (Resp t (MockHandle t))
    , Show (Resp t (Reference (RealHandle t) Symbolic))
    , Show (Resp t (Reference (RealHandle t) Concrete))
    , Show (Resp t (MockHandle t))
    , Traversable (Resp t)
      -- Command
    , Show (Cmd t (Reference (RealHandle t) Symbolic))
    , Show (Cmd t (Reference (RealHandle t) Concrete))
    , Traversable (Cmd t)
      -- Real handles
    , Eq     (RealHandle t)
    , Show   (RealHandle t)
    , ToExpr (RealHandle t)
      -- Mock handles
    , Eq     (MockHandle t)
    , Show   (MockHandle t)
    , ToExpr (MockHandle t)
      -- Mock state
    , Show   (MockState t)
    , ToExpr (MockState t)
      -- Tags
    , Show (Tag t)
    ) => StateMachineTest {
      forall t.
StateMachineTest t
-> Cmd t (MockHandle t)
-> MockState t
-> (Resp t (MockHandle t), MockState t)
runMock    :: Cmd t (MockHandle t) -> MockState t -> (Resp t (MockHandle t), MockState t)
    , forall t.
StateMachineTest t
-> Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
runReal    :: Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
    , forall t. StateMachineTest t -> MockState t
initMock   :: MockState t
    , forall t. StateMachineTest t -> forall h. Resp t h -> [h]
newHandles :: forall h. Resp t h -> [h]
    , forall t.
StateMachineTest t
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator  :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
    , forall t.
StateMachineTest t
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker   :: Model t Symbolic -> Cmd t :@ Symbolic -> [Cmd t :@ Symbolic]
    , forall t. StateMachineTest t -> Model t Concrete -> IO ()
cleanup    :: Model t Concrete -> IO ()
    , forall t. StateMachineTest t -> [Event t Symbolic] -> [Tag t]
tag        :: [Event t Symbolic] -> [Tag t]
    }

data Simple t

type instance NAry.MockState   (Simple t) = MockState t
type instance NAry.RealHandles (Simple t) = '[RealHandle t]
type instance NAry.Tag         (Simple t) = Tag t

data instance NAry.Cmd (Simple _) _f _hs where
    SimpleCmd :: Cmd t (f h) -> NAry.Cmd (Simple t) f '[h]

data instance NAry.Resp (Simple _) _f _hs where
    SimpleResp :: Resp t (f h) -> NAry.Resp (Simple t) f '[h]

newtype instance NAry.MockHandle (Simple t) (RealHandle t) =
    SimpleToMock { forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock :: MockHandle t }

unSimpleCmd :: NAry.Cmd (Simple t) f '[h] -> Cmd t (f h)
unSimpleCmd :: forall t (f :: * -> *) h. Cmd (Simple t) f '[h] -> Cmd t (f h)
unSimpleCmd (SimpleCmd Cmd t (f h)
cmd) = Cmd t (f h)
cmd

unSimpleResp :: NAry.Resp (Simple t) f '[h] -> Resp t (f h)
unSimpleResp :: forall t (f :: * -> *) h. Resp (Simple t) f '[h] -> Resp t (f h)
unSimpleResp (SimpleResp Resp t (f h)
resp) = Resp t (f h)
resp

instance ( Functor (Resp t)
         , Eq (Resp t (MockHandle t))
         , Eq (MockHandle t)
         ) => Eq (NAry.Resp (Simple t) (NAry.MockHandle (Simple t)) '[RealHandle t]) where
  SimpleResp Resp t (MockHandle (Simple t) h)
r == :: Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t] -> Bool
== SimpleResp Resp t (MockHandle (Simple t) h)
r' = (forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp t (MockHandle (Simple t) h)
r) forall a. Eq a => a -> a -> Bool
== (forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp t (MockHandle (Simple t) h)
r')

instance ( Functor (Resp t)
         , Show (Resp t (MockHandle t))
         ) => Show (NAry.Resp (Simple t) (NAry.MockHandle (Simple t)) '[RealHandle t]) where
  show :: Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t] -> String
show (SimpleResp Resp t (MockHandle (Simple t) h)
r) = forall a. Show a => a -> String
show (forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp t (MockHandle (Simple t) h)
r)

instance ( Functor (Resp t)
         , Show (Resp t (Reference (RealHandle t) r))
         , Show1 r
         ) => Show (NAry.Resp (Simple t) (NAry.FlipRef r) '[RealHandle t]) where
  show :: Resp (Simple t) (FlipRef r) '[RealHandle t] -> String
show (SimpleResp Resp t (FlipRef r h)
r) = forall a. Show a => a -> String
show (forall (r :: * -> *) h. FlipRef r h -> Reference h r
NAry.unFlipRef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp t (FlipRef r h)
r)

instance ( Functor (Cmd t)
         , Show (Cmd t (Reference (RealHandle t) r))
         , Show1 r
         ) => Show (NAry.Cmd (Simple t) (NAry.FlipRef r) '[RealHandle t]) where
  show :: Cmd (Simple t) (FlipRef r) '[RealHandle t] -> String
show (SimpleCmd Cmd t (FlipRef r h)
r) = forall a. Show a => a -> String
show (forall (r :: * -> *) h. FlipRef r h -> Reference h r
NAry.unFlipRef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Cmd t (FlipRef r h)
r)

deriving stock instance Eq   (MockHandle t) => Eq   (NAry.MockHandle (Simple t) (RealHandle t))
deriving stock instance Show (MockHandle t) => Show (NAry.MockHandle (Simple t) (RealHandle t))

instance Traversable (Resp t) => NTraversable (NAry.Resp (Simple t)) where
  nctraverse :: forall (m :: * -> *) (c :: * -> Constraint) (xs :: [*])
       (proxy :: (* -> Constraint) -> *) (g :: * -> *) (h :: * -> *).
(Applicative m, All c xs) =>
proxy c
-> (forall a. c a => Elem xs a -> g a -> m (h a))
-> Resp (Simple t) g xs
-> m (Resp (Simple t) h xs)
nctraverse proxy c
_ forall a. c a => Elem xs a -> g a -> m (h a)
f (SimpleResp Resp t (g h)
x) = forall t (f :: * -> *) ks. Resp t (f ks) -> Resp (Simple t) f '[ks]
SimpleResp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a. c a => Elem xs a -> g a -> m (h a)
f forall {k} (k :: k) (ks :: [k]). Elem (k : ks) k
ElemHead) Resp t (g h)
x

instance Traversable (Cmd t) => NTraversable (NAry.Cmd (Simple t)) where
  nctraverse :: forall (m :: * -> *) (c :: * -> Constraint) (xs :: [*])
       (proxy :: (* -> Constraint) -> *) (g :: * -> *) (h :: * -> *).
(Applicative m, All c xs) =>
proxy c
-> (forall a. c a => Elem xs a -> g a -> m (h a))
-> Cmd (Simple t) g xs
-> m (Cmd (Simple t) h xs)
nctraverse proxy c
_ forall a. c a => Elem xs a -> g a -> m (h a)
f (SimpleCmd Cmd t (g h)
x) = forall t (f :: * -> *) ks. Cmd t (f ks) -> Cmd (Simple t) f '[ks]
SimpleCmd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a. c a => Elem xs a -> g a -> m (h a)
f forall {k} (k :: k) (ks :: [k]). Elem (k : ks) k
ElemHead) Cmd t (g h)
x

instance ToExpr (MockHandle t)
      => ToExpr (NAry.MockHandle (Simple t) (RealHandle t)) where
  toExpr :: MockHandle (Simple t) (RealHandle t) -> Expr
toExpr (SimpleToMock MockHandle t
h) = forall a. ToExpr a => a -> Expr
toExpr MockHandle t
h

fromSimple :: StateMachineTest t -> NAry.StateMachineTest (Simple t) IO
fromSimple :: forall t. StateMachineTest t -> StateMachineTest (Simple t) IO
fromSimple StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> IO ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t (MockHandle t)
-> MockState t -> (Resp t (MockHandle t), MockState t)
Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
forall h. Resp t h -> [h]
tag :: [Event t Symbolic] -> [Tag t]
cleanup :: Model t Concrete -> IO ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall h. Resp t h -> [h]
initMock :: MockState t
runReal :: Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
runMock :: Cmd t (MockHandle t)
-> MockState t -> (Resp t (MockHandle t), MockState t)
tag :: forall t. StateMachineTest t -> [Event t Symbolic] -> [Tag t]
cleanup :: forall t. StateMachineTest t -> Model t Concrete -> IO ()
shrinker :: forall t.
StateMachineTest t
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: forall t.
StateMachineTest t
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall t. StateMachineTest t -> forall h. Resp t h -> [h]
initMock :: forall t. StateMachineTest t -> MockState t
runReal :: forall t.
StateMachineTest t
-> Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
runMock :: forall t.
StateMachineTest t
-> Cmd t (MockHandle t)
-> MockState t
-> (Resp t (MockHandle t), MockState t)
..} = NAry.StateMachineTest {
      runMock :: Cmd (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t))
-> MockState (Simple t)
-> (Resp
      (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t)),
    MockState (Simple t))
runMock    = \Cmd (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t))
cmd MockState (Simple t)
st -> forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall t.
Functor (Resp t) =>
Resp t (MockHandle t)
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
respMockFromSimple (Cmd t (MockHandle t)
-> MockState t -> (Resp t (MockHandle t), MockState t)
runMock (forall t.
Functor (Cmd t) =>
Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
cmdMockToSimple Cmd (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t))
cmd) MockState (Simple t)
st)
    , runReal :: Cmd (Simple t) I (RealHandles (Simple t))
-> IO (Resp (Simple t) I (RealHandles (Simple t)))
runReal    = \Cmd (Simple t) I (RealHandles (Simple t))
cmd -> forall t.
Functor (Resp t) =>
Resp t (RealHandle t) -> Resp (Simple t) I '[RealHandle t]
respRealFromSimple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
runReal (forall t.
Functor (Cmd t) =>
Cmd (Simple t) I '[RealHandle t] -> Cmd t (RealHandle t)
cmdRealToSimple Cmd (Simple t) I (RealHandles (Simple t))
cmd)
    , initMock :: MockState (Simple t)
initMock   = MockState t
initMock
    , newHandles :: forall (f :: * -> *).
Resp (Simple t) f (RealHandles (Simple t))
-> NP ([] :.: f) (RealHandles (Simple t))
newHandles = \Resp (Simple t) f (RealHandles (Simple t))
r -> forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (forall h. Resp t h -> [h]
newHandles (forall t (f :: * -> *) h. Resp (Simple t) f '[h] -> Resp t (f h)
unSimpleResp Resp (Simple t) f (RealHandles (Simple t))
r)) forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {k} (a :: k -> *). NP a '[]
Nil
    , generator :: Model (Simple t) Symbolic
-> Maybe (Gen (Cmd (Simple t) :@ Symbolic))
generator  = \Model (Simple t) Symbolic
m     -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t (r :: * -> *).
Functor (Cmd t) =>
(Cmd t :@ r) -> Cmd (Simple t) :@ r
cmdAtFromSimple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator (forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple Model (Simple t) Symbolic
m)
    , shrinker :: Model (Simple t) Symbolic
-> (Cmd (Simple t) :@ Symbolic) -> [Cmd (Simple t) :@ Symbolic]
shrinker   = \Model (Simple t) Symbolic
m Cmd (Simple t) :@ Symbolic
cmd ->      forall t (r :: * -> *).
Functor (Cmd t) =>
(Cmd t :@ r) -> Cmd (Simple t) :@ r
cmdAtFromSimple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker  (forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple Model (Simple t) Symbolic
m) (forall t (r :: * -> *).
Functor (Cmd t) =>
(Cmd (Simple t) :@ r) -> Cmd t :@ r
cmdAtToSimple Cmd (Simple t) :@ Symbolic
cmd)
    , cleanup :: Model (Simple t) Concrete -> IO ()
cleanup    = Model t Concrete -> IO ()
cleanup   forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple
    , tag :: [Event (Simple t) Symbolic] -> [Tag (Simple t)]
tag        = [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 (r :: * -> *).
(Functor (Cmd t), Functor (Resp t)) =>
Event (Simple t) r -> Event t r
eventToSimple
    }

{-------------------------------------------------------------------------------
  Running the tests
-------------------------------------------------------------------------------}

prop_sequential :: StateMachineTest t
                -> Maybe Int   -- ^ (Optional) minimum number of commands
                -> Property
prop_sequential :: forall t. StateMachineTest t -> Maybe Int -> Property
prop_sequential = forall t. StateMachineTest t IO -> Maybe Int -> Property
NAry.prop_sequential forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. StateMachineTest t -> StateMachineTest (Simple t) IO
fromSimple

prop_parallel :: StateMachineTest t
              -> Maybe Int   -- ^ (Optional) minimum number of commands
              -> Property
prop_parallel :: forall t. StateMachineTest t -> Maybe Int -> Property
prop_parallel = forall t. StateMachineTest t IO -> Maybe Int -> Property
NAry.prop_parallel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. StateMachineTest t -> StateMachineTest (Simple t) IO
fromSimple