{-# 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
, Simple
, NAry.MockHandleN(SimpleToMock)
) 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, MockHandleN (Simple t) x)]
rs :* NP (Refs (Simple t) r) xs
Nil), MockState (Simple t)
modelState :: MockState (Simple t)
modelState :: forall t (r :: * -> *). Model t r -> MockState t
..} = Model {
modelState :: MockState t
modelState = MockState t
MockState (Simple t)
modelState
, modelRefs :: [(Reference (RealHandle t) r, MockHandle t)]
modelRefs = ((Reference (RealHandle t) r,
MockHandleN (Simple t) (RealHandle t))
-> (Reference (RealHandle t) r, MockHandle t))
-> [(Reference (RealHandle t) r,
MockHandleN (Simple t) (RealHandle t))]
-> [(Reference (RealHandle t) r, MockHandle t)]
forall a b. (a -> b) -> [a] -> [b]
map ((MockHandleN (Simple t) (RealHandle t) -> MockHandle t)
-> (Reference (RealHandle t) r,
MockHandleN (Simple t) (RealHandle t))
-> (Reference (RealHandle t) r, MockHandle t)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second MockHandleN (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandleN (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock) [(Reference x r, MockHandleN (Simple t) x)]
[(Reference (RealHandle t) r,
MockHandleN (Simple t) (RealHandle t))]
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) (MockHandleN (Simple t)) (RealHandles (Simple t))
before :: Model (Simple t) r
cmd :: Cmd (Simple t) :@ r
after :: Model (Simple t) r
mockResp :: Resp (Simple t) (MockHandleN (Simple t)) (RealHandles (Simple t))
before :: forall t (r :: * -> *). Event t r -> Model t r
cmd :: forall t (r :: * -> *). Event t r -> Cmd t :@ r
after :: forall t (r :: * -> *). Event t r -> Model t r
mockResp :: forall t (r :: * -> *).
Event t r -> Resp t (MockHandleN t) (RealHandles t)
..} = Event{
before :: Model t r
before = Model (Simple t) r -> Model t r
forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple Model (Simple t) r
before
, cmd :: Cmd t :@ r
cmd = (Cmd (Simple t) :@ r) -> Cmd t :@ r
forall t (r :: * -> *).
Functor (Cmd t) =>
(Cmd (Simple t) :@ r) -> Cmd t :@ r
cmdAtToSimple Cmd (Simple t) :@ r
cmd
, after :: Model t r
after = Model (Simple t) r -> Model t r
forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple Model (Simple t) r
after
, mockResp :: Resp t (MockHandle t)
mockResp = Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Resp t (MockHandle t)
forall t.
Functor (Resp t) =>
Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Resp t (MockHandle t)
respMockToSimple Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
Resp (Simple t) (MockHandleN (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 = Cmd (Simple t) (FlipRef r) '[RealHandle t] -> At (Cmd (Simple t)) r
Cmd (Simple t) (FlipRef r) (RealHandles (Test (Cmd (Simple t))))
-> At (Cmd (Simple t)) r
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
NAry.At (Cmd (Simple t) (FlipRef r) '[RealHandle t]
-> At (Cmd (Simple t)) r)
-> ((Cmd t :@ r) -> Cmd (Simple t) (FlipRef r) '[RealHandle t])
-> (Cmd t :@ r)
-> At (Cmd (Simple t)) r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cmd t (FlipRef r (RealHandle t))
-> Cmd (Simple t) (FlipRef r) '[RealHandle t]
forall t (f :: * -> *) h. Cmd t (f h) -> Cmd (Simple t) f '[h]
SimpleCmd (Cmd t (FlipRef r (RealHandle t))
-> Cmd (Simple t) (FlipRef r) '[RealHandle t])
-> ((Cmd t :@ r) -> Cmd t (FlipRef r (RealHandle t)))
-> (Cmd t :@ r)
-> Cmd (Simple t) (FlipRef r) '[RealHandle t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reference (RealHandle t) r -> FlipRef r (RealHandle t))
-> Cmd t (Reference (RealHandle t) r)
-> Cmd t (FlipRef r (RealHandle t))
forall a b. (a -> b) -> Cmd t a -> Cmd t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reference (RealHandle t) r -> FlipRef r (RealHandle t)
forall (r :: * -> *) h. Reference h r -> FlipRef r h
NAry.FlipRef (Cmd t (Reference (RealHandle t) r)
-> Cmd t (FlipRef r (RealHandle t)))
-> ((Cmd t :@ r) -> Cmd t (Reference (RealHandle t) r))
-> (Cmd t :@ r)
-> Cmd t (FlipRef r (RealHandle t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cmd t :@ r) -> Cmd t (Reference (RealHandle t) r)
(Cmd t :@ r) -> Cmd t (Reference (RealHandle (Test (Cmd t))) r)
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 = Cmd t (Reference (RealHandle t) r) -> At (Cmd t) r
Cmd t (Reference (RealHandle (Test (Cmd t))) r) -> At (Cmd t) r
forall (f :: * -> *) (r :: * -> *).
f (Reference (RealHandle (Test f)) r) -> At f r
At (Cmd t (Reference (RealHandle t) r) -> At (Cmd t) r)
-> ((Cmd (Simple t) :@ r) -> Cmd t (Reference (RealHandle t) r))
-> (Cmd (Simple t) :@ r)
-> At (Cmd t) r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FlipRef r (RealHandle t) -> Reference (RealHandle t) r)
-> Cmd t (FlipRef r (RealHandle t))
-> Cmd t (Reference (RealHandle t) r)
forall a b. (a -> b) -> Cmd t a -> Cmd t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FlipRef r (RealHandle t) -> Reference (RealHandle t) r
forall (r :: * -> *) h. FlipRef r h -> Reference h r
NAry.unFlipRef (Cmd t (FlipRef r (RealHandle t))
-> Cmd t (Reference (RealHandle t) r))
-> ((Cmd (Simple t) :@ r) -> Cmd t (FlipRef r (RealHandle t)))
-> (Cmd (Simple t) :@ r)
-> Cmd t (Reference (RealHandle t) r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cmd (Simple t) (FlipRef r) '[RealHandle t]
-> Cmd t (FlipRef r (RealHandle t))
forall t (f :: * -> *) h. Cmd (Simple t) f '[h] -> Cmd t (f h)
unSimpleCmd (Cmd (Simple t) (FlipRef r) '[RealHandle t]
-> Cmd t (FlipRef r (RealHandle t)))
-> ((Cmd (Simple t) :@ r)
-> Cmd (Simple t) (FlipRef r) '[RealHandle t])
-> (Cmd (Simple t) :@ r)
-> Cmd t (FlipRef r (RealHandle t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cmd (Simple t) :@ r) -> Cmd (Simple t) (FlipRef r) '[RealHandle t]
(Cmd (Simple t) :@ r)
-> Cmd (Simple t) (FlipRef r) (RealHandles (Test (Cmd (Simple t))))
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
At f r -> f (FlipRef r) (RealHandles (Test f))
NAry.unAt
cmdMockToSimple :: Functor (Cmd t)
=> NAry.Cmd (Simple t) (NAry.MockHandleN (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
cmdMockToSimple :: forall t.
Functor (Cmd t) =>
Cmd (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
cmdMockToSimple = (MockHandleN (Simple t) (RealHandle t) -> MockHandle t)
-> Cmd t (MockHandleN (Simple t) (RealHandle t))
-> Cmd t (MockHandle t)
forall a b. (a -> b) -> Cmd t a -> Cmd t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MockHandleN (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandleN (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock (Cmd t (MockHandleN (Simple t) (RealHandle t))
-> Cmd t (MockHandle t))
-> (Cmd (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Cmd t (MockHandleN (Simple t) (RealHandle t)))
-> Cmd (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cmd (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Cmd t (MockHandleN (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 :: forall t.
Functor (Cmd t) =>
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 a b. (a -> b) -> Cmd t a -> Cmd t b
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.MockHandleN (Simple t)) '[RealHandle t]
respMockFromSimple :: forall t.
Functor (Resp t) =>
Resp t (MockHandle t)
-> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
respMockFromSimple = Resp t (MockHandleN (Simple t) (RealHandle t))
-> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
forall t (f :: * -> *) h. Resp t (f h) -> Resp (Simple t) f '[h]
SimpleResp (Resp t (MockHandleN (Simple t) (RealHandle t))
-> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t])
-> (Resp t (MockHandle t)
-> Resp t (MockHandleN (Simple t) (RealHandle t)))
-> Resp t (MockHandle t)
-> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MockHandle t -> MockHandleN (Simple t) (RealHandle t))
-> Resp t (MockHandle t)
-> Resp t (MockHandleN (Simple t) (RealHandle t))
forall a b. (a -> b) -> Resp t a -> Resp t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MockHandle t -> MockHandleN (Simple t) (RealHandle t)
forall t. MockHandle t -> MockHandleN (Simple t) (RealHandle t)
SimpleToMock
respMockToSimple :: Functor (Resp t)
=> NAry.Resp (Simple t) (NAry.MockHandleN (Simple t)) '[RealHandle t]
-> Resp t (MockHandle t)
respMockToSimple :: forall t.
Functor (Resp t) =>
Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Resp t (MockHandle t)
respMockToSimple = (MockHandleN (Simple t) (RealHandle t) -> MockHandle t)
-> Resp t (MockHandleN (Simple t) (RealHandle t))
-> Resp t (MockHandle t)
forall a b. (a -> b) -> Resp t a -> Resp t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MockHandleN (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandleN (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock (Resp t (MockHandleN (Simple t) (RealHandle t))
-> Resp t (MockHandle t))
-> (Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Resp t (MockHandleN (Simple t) (RealHandle t)))
-> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Resp t (MockHandle t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Resp t (MockHandleN (Simple t) (RealHandle t))
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 = 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 a b. (a -> b) -> Resp t a -> Resp t b
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)
, CanDiff (RealHandle t)
, Eq (MockHandle t)
, Show (MockHandle t)
, CanDiff (MockHandle t)
, CanDiff (NAry.MockHandleN (Simple t) (RealHandle t))
, Show (MockState t)
, CanDiff (MockState t)
, Show (Tag t)
, CanDiff (NAry.Model (Simple t) Concrete)
) => 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.MockHandleN (Simple t) (RealHandle t) =
SimpleToMock { forall t. MockHandleN (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 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 t (f h)
resp
instance ( Functor (Resp t)
, Eq (Resp t (MockHandle t))
, Eq (MockHandle t)
) => Eq (NAry.Resp (Simple t) (NAry.MockHandleN (Simple t)) '[RealHandle t]) where
SimpleResp Resp t (MockHandleN (Simple t) h)
r == :: Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> Bool
== SimpleResp Resp t (MockHandleN (Simple t) h)
r' = (MockHandleN (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandleN (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock (MockHandleN (Simple t) (RealHandle t) -> MockHandle t)
-> Resp t (MockHandleN (Simple t) (RealHandle t))
-> Resp t (MockHandle t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp t (MockHandleN (Simple t) h)
Resp t (MockHandleN (Simple t) (RealHandle t))
r) Resp t (MockHandle t) -> Resp t (MockHandle t) -> Bool
forall a. Eq a => a -> a -> Bool
== (MockHandleN (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandleN (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock (MockHandleN (Simple t) (RealHandle t) -> MockHandle t)
-> Resp t (MockHandleN (Simple t) (RealHandle t))
-> Resp t (MockHandle t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp t (MockHandleN (Simple t) h)
Resp t (MockHandleN (Simple t) (RealHandle t))
r')
instance ( Functor (Resp t)
, Show (Resp t (MockHandle t))
) => Show (NAry.Resp (Simple t) (NAry.MockHandleN (Simple t)) '[RealHandle t]) where
show :: Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> String
show (SimpleResp Resp t (MockHandleN (Simple t) h)
r) = Resp t (MockHandle t) -> String
forall a. Show a => a -> String
show (MockHandleN (Simple t) (RealHandle t) -> MockHandle t
forall t. MockHandleN (Simple t) (RealHandle t) -> MockHandle t
unSimpleToMock (MockHandleN (Simple t) (RealHandle t) -> MockHandle t)
-> Resp t (MockHandleN (Simple t) (RealHandle t))
-> Resp t (MockHandle t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp t (MockHandleN (Simple t) h)
Resp t (MockHandleN (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 Resp t (FlipRef r h)
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 Cmd t (FlipRef r h)
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.MockHandleN (Simple t) (RealHandle t))
deriving stock instance Show (MockHandle t) => Show (NAry.MockHandleN (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) = Resp t (h h) -> Resp (Simple t) h xs
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 xs)
-> m (Resp t (h h)) -> m (Resp (Simple t) h xs)
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Resp t a -> f (Resp 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
Elem '[h] h
forall {k} (a :: k) (ks :: [k]). Elem (a : ks) a
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) = Cmd t (h h) -> Cmd (Simple t) h xs
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 xs)
-> m (Cmd t (h h)) -> m (Cmd (Simple t) h xs)
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Cmd t a -> f (Cmd 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
Elem '[h] h
forall {k} (a :: k) (ks :: [k]). Elem (a : ks) a
ElemHead) Cmd t (g h)
x
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]
runMock :: forall t.
StateMachineTest t
-> Cmd t (MockHandle t)
-> MockState t
-> (Resp t (MockHandle t), MockState t)
runReal :: forall t.
StateMachineTest t
-> Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
initMock :: forall t. StateMachineTest t -> MockState t
newHandles :: forall t. StateMachineTest t -> forall h. Resp t h -> [h]
generator :: forall t.
StateMachineTest t
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: forall t.
StateMachineTest t
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: forall t. StateMachineTest t -> Model t Concrete -> IO ()
tag :: forall t. StateMachineTest t -> [Event t Symbolic] -> [Tag t]
runMock :: Cmd t (MockHandle t)
-> MockState t -> (Resp t (MockHandle t), MockState t)
runReal :: Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
initMock :: MockState t
newHandles :: forall h. Resp t h -> [h]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: Model t Concrete -> IO ()
tag :: [Event t Symbolic] -> [Tag t]
..} = NAry.StateMachineTest {
runMock :: Cmd (Simple t) (MockHandleN (Simple t)) (RealHandles (Simple t))
-> MockState (Simple t)
-> (Resp
(Simple t) (MockHandleN (Simple t)) (RealHandles (Simple t)),
MockState (Simple t))
runMock = \Cmd (Simple t) (MockHandleN (Simple t)) (RealHandles (Simple t))
cmd MockState (Simple t)
st -> (Resp t (MockHandle t)
-> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t])
-> (Resp t (MockHandle t), MockState t)
-> (Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t],
MockState t)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Resp t (MockHandle t)
-> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
forall t.
Functor (Resp t) =>
Resp t (MockHandle t)
-> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
respMockFromSimple (Cmd t (MockHandle t)
-> MockState t -> (Resp t (MockHandle t), MockState t)
runMock (Cmd (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
forall t.
Functor (Cmd t) =>
Cmd (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
cmdMockToSimple Cmd (Simple t) (MockHandleN (Simple t)) '[RealHandle t]
Cmd (Simple t) (MockHandleN (Simple t)) (RealHandles (Simple t))
cmd) MockState t
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 -> 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 a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic
forall t (r :: * -> *).
Functor (Cmd t) =>
(Cmd t :@ r) -> Cmd (Simple t) :@ r
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 (r :: * -> *).
Functor (Cmd t) =>
(Cmd t :@ r) -> Cmd (Simple t) :@ r
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 (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 (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
, tag :: [Event (Simple t) Symbolic] -> [Tag (Simple t)]
tag = [Event t Symbolic] -> [Tag t]
tag ([Event t Symbolic] -> [Tag t])
-> ([Event (Simple t) Symbolic] -> [Event t Symbolic])
-> [Event (Simple t) Symbolic]
-> [Tag t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Event (Simple t) Symbolic -> Event t Symbolic)
-> [Event (Simple t) Symbolic] -> [Event t Symbolic]
forall a b. (a -> b) -> [a] -> [b]
map Event (Simple t) Symbolic -> Event t Symbolic
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 = StateMachineTest (Simple t) IO -> Maybe Int -> Property
forall t. StateMachineTest t IO -> Maybe Int -> Property
NAry.prop_sequential (StateMachineTest (Simple t) IO -> Maybe Int -> Property)
-> (StateMachineTest t -> StateMachineTest (Simple t) IO)
-> StateMachineTest t
-> Maybe Int
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachineTest t -> StateMachineTest (Simple t) IO
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 = StateMachineTest (Simple t) IO -> Maybe Int -> Property
forall t. StateMachineTest t IO -> Maybe Int -> Property
NAry.prop_parallel (StateMachineTest (Simple t) IO -> Maybe Int -> Property)
-> (StateMachineTest t -> StateMachineTest (Simple t) IO)
-> StateMachineTest t
-> Maybe Int
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachineTest t -> StateMachineTest (Simple t) IO
forall t. StateMachineTest t -> StateMachineTest (Simple t) IO
fromSimple