{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Test.StateMachine.Lockstep.Simple (
MockState
, Cmd
, Resp
, RealHandle
, MockHandle
, Test
, StateMachineTest(..)
, 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)
import qualified Test.StateMachine.Lockstep.NAry as NAry
data family Cmd t :: Type -> Type
data family Resp t :: Type -> Type
data family RealHandle t :: Type
data family MockHandle t :: Type
type family Test (f :: Type -> Type) :: Type where
Test (Cmd t) = t
Test (Resp t) = t
newtype At f r = At { 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 {
Model t r -> MockState t
modelState :: MockState t
, 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 :: 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 :: forall t (r :: * -> *).
MockState t
-> [(Reference (RealHandle t) r, MockHandle t)] -> Model t r
Model {
modelState :: MockState t
modelState = MockState t
MockState (Simple t)
modelState
, modelRefs :: [(Reference (RealHandle t) r, MockHandle t)]
modelRefs = ((Reference x r, MockHandle (Simple t) (RealHandle t))
-> (Reference x r, MockHandle t))
-> [(Reference x r, MockHandle (Simple t) (RealHandle t))]
-> [(Reference x r, MockHandle t)]
forall a b. (a -> b) -> [a] -> [b]
map ((MockHandle (Simple t) (RealHandle t) -> MockHandle t)
-> (Reference x r, MockHandle (Simple t) (RealHandle t))
-> (Reference x r, MockHandle t)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second MockHandle (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock) [(Reference x r, MockHandle (Simple t) x)]
[(Reference x r, MockHandle (Simple t) (RealHandle t))]
rs
}
cmdAtFromSimple :: Functor (Cmd t)
=> Cmd t :@ Symbolic -> NAry.Cmd (Simple t) NAry.:@ Symbolic
cmdAtFromSimple :: (Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic
cmdAtFromSimple = Cmd (Simple t) (FlipRef Symbolic) '[RealHandle t]
-> Cmd (Simple t) :@ Symbolic
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
NAry.At (Cmd (Simple t) (FlipRef Symbolic) '[RealHandle t]
-> Cmd (Simple t) :@ Symbolic)
-> ((Cmd t :@ Symbolic)
-> Cmd (Simple t) (FlipRef Symbolic) '[RealHandle t])
-> (Cmd t :@ Symbolic)
-> Cmd (Simple t) :@ Symbolic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cmd t (FlipRef Symbolic (RealHandle t))
-> Cmd (Simple t) (FlipRef Symbolic) '[RealHandle t]
forall t (f :: * -> *) h. Cmd t (f h) -> Cmd (Simple t) f '[h]
SimpleCmd (Cmd t (FlipRef Symbolic (RealHandle t))
-> Cmd (Simple t) (FlipRef Symbolic) '[RealHandle t])
-> ((Cmd t :@ Symbolic) -> Cmd t (FlipRef Symbolic (RealHandle t)))
-> (Cmd t :@ Symbolic)
-> Cmd (Simple t) (FlipRef Symbolic) '[RealHandle t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reference (RealHandle t) Symbolic
-> FlipRef Symbolic (RealHandle t))
-> Cmd t (Reference (RealHandle t) Symbolic)
-> Cmd t (FlipRef Symbolic (RealHandle t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reference (RealHandle t) Symbolic
-> FlipRef Symbolic (RealHandle t)
forall (r :: * -> *) h. Reference h r -> FlipRef r h
NAry.FlipRef (Cmd t (Reference (RealHandle t) Symbolic)
-> Cmd t (FlipRef Symbolic (RealHandle t)))
-> ((Cmd t :@ Symbolic)
-> Cmd t (Reference (RealHandle t) Symbolic))
-> (Cmd t :@ Symbolic)
-> Cmd t (FlipRef Symbolic (RealHandle t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cmd t :@ Symbolic) -> Cmd t (Reference (RealHandle t) Symbolic)
forall (f :: * -> *) (r :: * -> *).
At f r -> f (Reference (RealHandle (Test f)) r)
unAt
cmdAtToSimple :: Functor (Cmd t)
=> NAry.Cmd (Simple t) NAry.:@ Symbolic -> Cmd t :@ Symbolic
cmdAtToSimple :: (Cmd (Simple t) :@ Symbolic) -> Cmd t :@ Symbolic
cmdAtToSimple = Cmd t (Reference (RealHandle t) Symbolic) -> Cmd t :@ Symbolic
forall (f :: * -> *) (r :: * -> *).
f (Reference (RealHandle (Test f)) r) -> At f r
At (Cmd t (Reference (RealHandle t) Symbolic) -> Cmd t :@ Symbolic)
-> ((Cmd (Simple t) :@ Symbolic)
-> Cmd t (Reference (RealHandle t) Symbolic))
-> (Cmd (Simple t) :@ Symbolic)
-> Cmd t :@ Symbolic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FlipRef Symbolic (RealHandle t)
-> Reference (RealHandle t) Symbolic)
-> Cmd t (FlipRef Symbolic (RealHandle t))
-> Cmd t (Reference (RealHandle t) Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FlipRef Symbolic (RealHandle t)
-> Reference (RealHandle t) Symbolic
forall (r :: * -> *) h. FlipRef r h -> Reference h r
NAry.unFlipRef) (Cmd t (FlipRef Symbolic (RealHandle t))
-> Cmd t (Reference (RealHandle t) Symbolic))
-> ((Cmd (Simple t) :@ Symbolic)
-> Cmd t (FlipRef Symbolic (RealHandle t)))
-> (Cmd (Simple t) :@ Symbolic)
-> Cmd t (Reference (RealHandle t) Symbolic)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cmd (Simple t) (FlipRef Symbolic) '[RealHandle t]
-> Cmd t (FlipRef Symbolic (RealHandle t))
forall t (f :: * -> *) h. Cmd (Simple t) f '[h] -> Cmd t (f h)
unSimpleCmd (Cmd (Simple t) (FlipRef Symbolic) '[RealHandle t]
-> Cmd t (FlipRef Symbolic (RealHandle t)))
-> ((Cmd (Simple t) :@ Symbolic)
-> Cmd (Simple t) (FlipRef Symbolic) '[RealHandle t])
-> (Cmd (Simple t) :@ Symbolic)
-> Cmd t (FlipRef Symbolic (RealHandle t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cmd (Simple t) :@ Symbolic)
-> Cmd (Simple t) (FlipRef Symbolic) '[RealHandle t]
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 :: Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
cmdMockToSimple = (MockHandle (Simple t) (RealHandle t) -> MockHandle t)
-> Cmd t (MockHandle (Simple t) (RealHandle t))
-> Cmd t (MockHandle t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MockHandle (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock (Cmd t (MockHandle (Simple t) (RealHandle t))
-> Cmd t (MockHandle t))
-> (Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle (Simple t) (RealHandle t)))
-> Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle (Simple t) (RealHandle t))
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 :: Cmd (Simple t) I '[RealHandle t] -> Cmd t (RealHandle t)
cmdRealToSimple = (I (RealHandle t) -> RealHandle t)
-> Cmd t (I (RealHandle t)) -> Cmd t (RealHandle t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap I (RealHandle t) -> RealHandle t
forall a. I a -> a
unI (Cmd t (I (RealHandle t)) -> Cmd t (RealHandle t))
-> (Cmd (Simple t) I '[RealHandle t] -> Cmd t (I (RealHandle t)))
-> Cmd (Simple t) I '[RealHandle t]
-> Cmd t (RealHandle t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cmd (Simple t) I '[RealHandle t] -> Cmd t (I (RealHandle t))
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 :: Resp t (MockHandle t)
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
respMockFromSimple = Resp t (MockHandle (Simple t) (RealHandle t))
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
forall t (f :: * -> *) h. Resp t (f h) -> Resp (Simple t) f '[h]
SimpleResp (Resp t (MockHandle (Simple t) (RealHandle t))
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t])
-> (Resp t (MockHandle t)
-> Resp t (MockHandle (Simple t) (RealHandle t)))
-> Resp t (MockHandle t)
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MockHandle t -> MockHandle (Simple t) (RealHandle t))
-> Resp t (MockHandle t)
-> Resp t (MockHandle (Simple t) (RealHandle t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MockHandle t -> MockHandle (Simple t) (RealHandle t)
forall t. MockHandle t -> MockHandle (Simple t) (RealHandle t)
SimpleToMock
respRealFromSimple :: Functor (Resp t)
=> Resp t (RealHandle t)
-> NAry.Resp (Simple t) I '[RealHandle t]
respRealFromSimple :: Resp t (RealHandle t) -> Resp (Simple t) I '[RealHandle t]
respRealFromSimple = Resp t (I (RealHandle t)) -> Resp (Simple t) I '[RealHandle t]
forall t (f :: * -> *) h. Resp t (f h) -> Resp (Simple t) f '[h]
SimpleResp (Resp t (I (RealHandle t)) -> Resp (Simple t) I '[RealHandle t])
-> (Resp t (RealHandle t) -> Resp t (I (RealHandle t)))
-> Resp t (RealHandle t)
-> Resp (Simple t) I '[RealHandle t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RealHandle t -> I (RealHandle t))
-> Resp t (RealHandle t) -> Resp t (I (RealHandle t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RealHandle t -> I (RealHandle t)
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)
) => StateMachineTest {
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)
, StateMachineTest t
-> Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
runReal :: Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
, StateMachineTest t -> MockState t
initMock :: MockState t
, StateMachineTest t -> forall h. Resp t h -> [h]
newHandles :: forall h. Resp t h -> [h]
, StateMachineTest t
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
, StateMachineTest t
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker :: Model t Symbolic -> Cmd t :@ Symbolic -> [Cmd t :@ Symbolic]
, StateMachineTest t -> Model t Concrete -> IO ()
cleanup :: Model t Concrete -> IO ()
}
data Simple t
type instance NAry.MockState (Simple t) = MockState t
type instance NAry.RealHandles (Simple t) = '[RealHandle t]
type instance NAry.RealMonad (Simple _) = IO
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 { MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock :: MockHandle t }
unSimpleCmd :: NAry.Cmd (Simple t) f '[h] -> Cmd t (f h)
unSimpleCmd :: Cmd (Simple t) f '[h] -> Cmd t (f h)
unSimpleCmd (SimpleCmd cmd) = Cmd t (f h)
Cmd t (f h)
cmd
unSimpleResp :: NAry.Resp (Simple t) f '[h] -> Resp t (f h)
unSimpleResp :: Resp (Simple t) f '[h] -> Resp t (f h)
unSimpleResp (SimpleResp resp) = Resp t (f h)
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 r == :: Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t] -> Bool
== SimpleResp r' = (MockHandle (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock (MockHandle (Simple t) (RealHandle t) -> MockHandle t)
-> Resp t (MockHandle (Simple t) (RealHandle t))
-> Resp t (MockHandle t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp t (MockHandle (Simple t) h)
Resp t (MockHandle (Simple t) (RealHandle t))
r) Resp t (MockHandle t) -> Resp t (MockHandle t) -> Bool
forall a. Eq a => a -> a -> Bool
== (MockHandle (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock (MockHandle (Simple t) (RealHandle t) -> MockHandle t)
-> Resp t (MockHandle (Simple t) (RealHandle t))
-> Resp t (MockHandle t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp t (MockHandle (Simple t) h)
Resp t (MockHandle (Simple t) (RealHandle t))
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 r) = Resp t (MockHandle t) -> String
forall a. Show a => a -> String
show (MockHandle (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandle (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock (MockHandle (Simple t) (RealHandle t) -> MockHandle t)
-> Resp t (MockHandle (Simple t) (RealHandle t))
-> Resp t (MockHandle t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp t (MockHandle (Simple t) h)
Resp t (MockHandle (Simple t) (RealHandle t))
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 r) = Resp t (Reference h r) -> String
forall a. Show a => a -> String
show (FlipRef r h -> Reference h r
forall (r :: * -> *) h. FlipRef r h -> Reference h r
NAry.unFlipRef (FlipRef r h -> Reference h r)
-> Resp t (FlipRef r h) -> Resp t (Reference h r)
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 r) = Cmd t (Reference h r) -> String
forall a. Show a => a -> String
show (FlipRef r h -> Reference h r
forall (r :: * -> *) h. FlipRef r h -> Reference h r
NAry.unFlipRef (FlipRef r h -> Reference h r)
-> Cmd t (FlipRef r h) -> Cmd t (Reference h r)
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 :: 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 x) = Resp t (h h) -> Resp (Simple t) h '[h]
forall t (f :: * -> *) h. Resp t (f h) -> Resp (Simple t) f '[h]
SimpleResp (Resp t (h h) -> Resp (Simple t) h '[h])
-> m (Resp t (h h)) -> m (Resp (Simple t) h '[h])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (g h -> m (h h)) -> Resp t (g h) -> m (Resp t (h h))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Elem xs h -> g h -> m (h h)
forall a. c a => Elem xs a -> g a -> m (h a)
f Elem xs h
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 :: 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 x) = Cmd t (h h) -> Cmd (Simple t) h '[h]
forall t (f :: * -> *) h. Cmd t (f h) -> Cmd (Simple t) f '[h]
SimpleCmd (Cmd t (h h) -> Cmd (Simple t) h '[h])
-> m (Cmd t (h h)) -> m (Cmd (Simple t) h '[h])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (g h -> m (h h)) -> Cmd t (g h) -> m (Cmd t (h h))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Elem xs h -> g h -> m (h h)
forall a. c a => Elem xs a -> g a -> m (h a)
f Elem xs h
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 h) = MockHandle t -> Expr
forall a. ToExpr a => a -> Expr
toExpr MockHandle t
h
fromSimple :: StateMachineTest t -> NAry.StateMachineTest (Simple t)
fromSimple :: StateMachineTest t -> StateMachineTest (Simple t)
fromSimple StateMachineTest{MockState 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]
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)
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)
..} = StateMachineTest :: forall t.
(Monad (RealMonad t), 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),
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)),
NTraversable (Cmd t),
Show (Cmd t (FlipRef Symbolic) (RealHandles t)),
Show (Cmd t (FlipRef Concrete) (RealHandles t)),
Show (MockState t), ToExpr (MockState t)) =>
(Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t))
-> (Cmd t I (RealHandles t)
-> RealMonad t (Resp t I (RealHandles t)))
-> MockState t
-> (forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t))
-> (Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic)))
-> (Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic])
-> (Model t Concrete -> RealMonad t ())
-> StateMachineTest 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 -> (Resp t (MockHandle t)
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t])
-> (Resp t (MockHandle t), MockState t)
-> (Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t],
MockState t)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Resp t (MockHandle t)
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
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 (Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
forall t.
Functor (Cmd t) =>
Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
cmdMockToSimple Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
Cmd (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t))
cmd) MockState t
MockState (Simple t)
st)
, runReal :: Cmd (Simple t) I (RealHandles (Simple t))
-> RealMonad
(Simple t) (Resp (Simple t) I (RealHandles (Simple t)))
runReal = \Cmd (Simple t) I (RealHandles (Simple t))
cmd -> Resp t (RealHandle t) -> Resp (Simple t) I '[RealHandle t]
forall t.
Functor (Resp t) =>
Resp t (RealHandle t) -> Resp (Simple t) I '[RealHandle t]
respRealFromSimple (Resp t (RealHandle t) -> Resp (Simple t) I '[RealHandle t])
-> IO (Resp t (RealHandle t))
-> IO (Resp (Simple t) I '[RealHandle t])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
runReal (Cmd (Simple t) I '[RealHandle t] -> Cmd t (RealHandle t)
forall t.
Functor (Cmd t) =>
Cmd (Simple t) I '[RealHandle t] -> Cmd t (RealHandle t)
cmdRealToSimple Cmd (Simple t) I '[RealHandle t]
Cmd (Simple t) I (RealHandles (Simple t))
cmd))
, initMock :: MockState (Simple t)
initMock = MockState t
MockState (Simple 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 -> [f (RealHandle t)] -> (:.:) [] f (RealHandle t)
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (Resp t (f (RealHandle t)) -> [f (RealHandle t)]
forall h. Resp t h -> [h]
newHandles (Resp (Simple t) f '[RealHandle t] -> Resp t (f (RealHandle t))
forall t (f :: * -> *) h. Resp (Simple t) f '[h] -> Resp t (f h)
unSimpleResp Resp (Simple t) f '[RealHandle t]
Resp (Simple t) f (RealHandles (Simple t))
r)) (:.:) [] f (RealHandle t)
-> NP ([] :.: f) '[] -> NP ([] :.: f) '[RealHandle t]
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP ([] :.: f) '[]
forall k (a :: k -> *). NP a '[]
Nil
, generator :: Model (Simple t) Symbolic
-> Maybe (Gen (Cmd (Simple t) :@ Symbolic))
generator = \Model (Simple t) Symbolic
m -> ((Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic)
-> Gen (Cmd t :@ Symbolic) -> Gen (Cmd (Simple t) :@ Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic
forall t.
Functor (Cmd t) =>
(Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic
cmdAtFromSimple (Gen (Cmd t :@ Symbolic) -> Gen (Cmd (Simple t) :@ Symbolic))
-> Maybe (Gen (Cmd t :@ Symbolic))
-> Maybe (Gen (Cmd (Simple t) :@ Symbolic))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator (Model (Simple t) Symbolic -> Model t Symbolic
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 -> (Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic
forall t.
Functor (Cmd t) =>
(Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic
cmdAtFromSimple ((Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic)
-> [Cmd t :@ Symbolic] -> [Cmd (Simple t) :@ Symbolic]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker (Model (Simple t) Symbolic -> Model t Symbolic
forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple Model (Simple t) Symbolic
m) ((Cmd (Simple t) :@ Symbolic) -> Cmd t :@ Symbolic
forall t.
Functor (Cmd t) =>
(Cmd (Simple t) :@ Symbolic) -> Cmd t :@ Symbolic
cmdAtToSimple Cmd (Simple t) :@ Symbolic
cmd)
, cleanup :: Model (Simple t) Concrete -> RealMonad (Simple t) ()
cleanup = Model t Concrete -> IO ()
cleanup (Model t Concrete -> IO ())
-> (Model (Simple t) Concrete -> Model t Concrete)
-> Model (Simple t) Concrete
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model (Simple t) Concrete -> Model t Concrete
forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple
}
prop_sequential :: StateMachineTest t
-> Maybe Int
-> Property
prop_sequential :: StateMachineTest t -> Maybe Int -> Property
prop_sequential = StateMachineTest (Simple t) -> Maybe Int -> Property
forall t.
(RealMonad t ~ IO) =>
StateMachineTest t -> Maybe Int -> Property
NAry.prop_sequential (StateMachineTest (Simple t) -> Maybe Int -> Property)
-> (StateMachineTest t -> StateMachineTest (Simple t))
-> StateMachineTest t
-> Maybe Int
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachineTest t -> StateMachineTest (Simple t)
forall t. StateMachineTest t -> StateMachineTest (Simple t)
fromSimple
prop_parallel :: StateMachineTest t
-> Maybe Int
-> Property
prop_parallel :: StateMachineTest t -> Maybe Int -> Property
prop_parallel = StateMachineTest (Simple t) -> Maybe Int -> Property
forall t.
(RealMonad t ~ IO) =>
StateMachineTest t -> Maybe Int -> Property
NAry.prop_parallel (StateMachineTest (Simple t) -> Maybe Int -> Property)
-> (StateMachineTest t -> StateMachineTest (Simple t))
-> StateMachineTest t
-> Maybe Int
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachineTest t -> StateMachineTest (Simple t)
forall t. StateMachineTest t -> StateMachineTest (Simple t)
fromSimple