{-# 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 (
MockState
, Cmd
, Resp
, RealHandle
, MockHandle
, Test
, Tag
, StateMachineTest(..)
, Event(..)
, At(..)
, (:@)
, Model(..)
, prop_sequential
, prop_parallel
, 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
data family RealHandle t :: Type
data family MockHandle t :: Type
data family Cmd t :: Type -> Type
data family Resp t :: Type -> Type
type family Test (f :: Type -> Type) :: Type where
Test (Cmd t) = t
Test (Resp t) = t
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
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
}
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
}
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
data StateMachineTest t =
( Typeable t
, 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)
, Show (Cmd t (Reference (RealHandle t) Symbolic))
, Show (Cmd t (Reference (RealHandle t) Concrete))
, Traversable (Cmd t)
, Eq (RealHandle t)
, Show (RealHandle t)
, ToExpr (RealHandle t)
, Eq (MockHandle t)
, Show (MockHandle t)
, ToExpr (MockHandle t)
, Show (MockState t)
, ToExpr (MockState t)
, 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
}
prop_sequential :: StateMachineTest t
-> Maybe Int
-> 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
-> 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