{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Test.StateMachine.Lockstep.NAry (
MockState
, Cmd
, Resp
, RealHandles
, MockHandleN
, Test
, Tag
, StateMachineTest(..)
, Event(..)
, hoistStateMachineTest
, At(..)
, (:@)
, Model(..)
, Refs(..)
, Refss(..)
, FlipRef(..)
, prop_sequential
, prop_parallel
, showLabelledExamples'
, showLabelledExamples
, toStateMachine
) where
import Data.Functor.Classes
import Data.Kind
(Type)
import Data.Maybe
(fromJust)
import Data.Semigroup hiding
(All)
import Data.SOP
import Data.Typeable
import GHC.Generics
(Generic)
import Prelude
import Test.QuickCheck
import Test.QuickCheck.Monadic
import Test.StateMachine hiding
(showLabelledExamples, showLabelledExamples')
import qualified Data.Monoid as M
import qualified Test.StateMachine.Labelling as Label
import qualified Test.StateMachine.Sequential as Seq
import qualified Test.StateMachine.Types as QSM
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Test.StateMachine.Lockstep.Auxiliary
type family MockState t :: Type
type family RealHandles t :: [Type]
data family MockHandleN t a :: Type
data family Cmd t :: (Type -> Type) -> [Type] -> Type
data family Resp t :: (Type -> Type) -> [Type] -> Type
type family Tag t :: Type
newtype Refs t r a = Refs { forall t (r :: * -> *) a.
Refs t r a -> [(Reference a r, MockHandleN t a)]
unRefs :: [(Reference a r, MockHandleN t a)] }
deriving newtype (NonEmpty (Refs t r a) -> Refs t r a
Refs t r a -> Refs t r a -> Refs t r a
(Refs t r a -> Refs t r a -> Refs t r a)
-> (NonEmpty (Refs t r a) -> Refs t r a)
-> (forall b. Integral b => b -> Refs t r a -> Refs t r a)
-> Semigroup (Refs t r a)
forall b. Integral b => b -> Refs t r a -> Refs t r a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall t (r :: * -> *) a. NonEmpty (Refs t r a) -> Refs t r a
forall t (r :: * -> *) a. Refs t r a -> Refs t r a -> Refs t r a
forall t (r :: * -> *) a b.
Integral b =>
b -> Refs t r a -> Refs t r a
$c<> :: forall t (r :: * -> *) a. Refs t r a -> Refs t r a -> Refs t r a
<> :: Refs t r a -> Refs t r a -> Refs t r a
$csconcat :: forall t (r :: * -> *) a. NonEmpty (Refs t r a) -> Refs t r a
sconcat :: NonEmpty (Refs t r a) -> Refs t r a
$cstimes :: forall t (r :: * -> *) a b.
Integral b =>
b -> Refs t r a -> Refs t r a
stimes :: forall b. Integral b => b -> Refs t r a -> Refs t r a
Semigroup, Semigroup (Refs t r a)
Refs t r a
Semigroup (Refs t r a) =>
Refs t r a
-> (Refs t r a -> Refs t r a -> Refs t r a)
-> ([Refs t r a] -> Refs t r a)
-> Monoid (Refs t r a)
[Refs t r a] -> Refs t r a
Refs t r a -> Refs t r a -> Refs t r a
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall t (r :: * -> *) a. Semigroup (Refs t r a)
forall t (r :: * -> *) a. Refs t r a
forall t (r :: * -> *) a. [Refs t r a] -> Refs t r a
forall t (r :: * -> *) a. Refs t r a -> Refs t r a -> Refs t r a
$cmempty :: forall t (r :: * -> *) a. Refs t r a
mempty :: Refs t r a
$cmappend :: forall t (r :: * -> *) a. Refs t r a -> Refs t r a -> Refs t r a
mappend :: Refs t r a -> Refs t r a -> Refs t r a
$cmconcat :: forall t (r :: * -> *) a. [Refs t r a] -> Refs t r a
mconcat :: [Refs t r a] -> Refs t r a
Monoid, (forall x. Refs t r a -> Rep (Refs t r a) x)
-> (forall x. Rep (Refs t r a) x -> Refs t r a)
-> Generic (Refs t r a)
forall x. Rep (Refs t r a) x -> Refs t r a
forall x. Refs t r a -> Rep (Refs t r a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t (r :: * -> *) a x. Rep (Refs t r a) x -> Refs t r a
forall t (r :: * -> *) a x. Refs t r a -> Rep (Refs t r a) x
$cfrom :: forall t (r :: * -> *) a x. Refs t r a -> Rep (Refs t r a) x
from :: forall x. Refs t r a -> Rep (Refs t r a) x
$cto :: forall t (r :: * -> *) a x. Rep (Refs t r a) x -> Refs t r a
to :: forall x. Rep (Refs t r a) x -> Refs t r a
Generic)
deriving
stock
instance (Show1 r, Show a, Show (MockHandleN t a)) => Show (Refs t r a)
newtype Refss t r = Refss { forall t (r :: * -> *). Refss t r -> NP (Refs t r) (RealHandles t)
unRefss :: NP (Refs t r) (RealHandles t) }
instance ( Show1 r
, All (And Show (Compose Show (MockHandleN t))) (RealHandles t)
) => Show (Refss t r) where
show :: Refss t r -> String
show = [String] -> String
unlines
([String] -> String)
-> (Refss t r -> [String]) -> Refss t r -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K String) (RealHandles t) -> [String]
NP (K String) (RealHandles t) -> CollapseTo NP String
forall (xs :: [*]) a.
SListIN NP xs =>
NP (K a) xs -> CollapseTo NP a
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
(NP (K String) (RealHandles t) -> [String])
-> (Refss t r -> NP (K String) (RealHandles t))
-> Refss t r
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (And Show (Compose Show (MockHandleN t)))
-> (forall a.
And Show (Compose Show (MockHandleN t)) a =>
Refs t r a -> K String a)
-> NP (Refs t r) (RealHandles t)
-> NP (K String) (RealHandles t)
forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
(xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
(f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @(And Show (Compose Show (MockHandleN t)))) Refs t r a -> K String a
forall a.
(Show a, Show (MockHandleN t a)) =>
Refs t r a -> K String a
forall a.
And Show (Compose Show (MockHandleN t)) a =>
Refs t r a -> K String a
showOne
(NP (Refs t r) (RealHandles t) -> NP (K String) (RealHandles t))
-> (Refss t r -> NP (Refs t r) (RealHandles t))
-> Refss t r
-> NP (K String) (RealHandles t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refss t r -> NP (Refs t r) (RealHandles t)
forall t (r :: * -> *). Refss t r -> NP (Refs t r) (RealHandles t)
unRefss
where
showOne :: (Show a, Show (MockHandleN t a))
=> Refs t r a -> K String a
showOne :: forall a.
(Show a, Show (MockHandleN t a)) =>
Refs t r a -> K String a
showOne = String -> K String a
forall k a (b :: k). a -> K a b
K (String -> K String a)
-> (Refs t r a -> String) -> Refs t r a -> K String a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refs t r a -> String
forall a. Show a => a -> String
show
instance SListI (RealHandles t) => Semigroup (Refss t r) where
Refss NP (Refs t r) (RealHandles t)
rss <> :: Refss t r -> Refss t r -> Refss t r
<> Refss NP (Refs t r) (RealHandles t)
rss' = NP (Refs t r) (RealHandles t) -> Refss t r
forall t (r :: * -> *). NP (Refs t r) (RealHandles t) -> Refss t r
Refss (NP (Refs t r) (RealHandles t) -> Refss t r)
-> NP (Refs t r) (RealHandles t) -> Refss t r
forall a b. (a -> b) -> a -> b
$ (forall a. Refs t r a -> Refs t r a -> Refs t r a)
-> Prod NP (Refs t r) (RealHandles t)
-> NP (Refs t r) (RealHandles t)
-> NP (Refs t r) (RealHandles t)
forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
(f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith Refs t r a -> Refs t r a -> Refs t r a
forall a. Semigroup a => a -> a -> a
forall a. Refs t r a -> Refs t r a -> Refs t r a
(<>) Prod NP (Refs t r) (RealHandles t)
NP (Refs t r) (RealHandles t)
rss NP (Refs t r) (RealHandles t)
rss'
instance SListI (RealHandles t) => Monoid (Refss t r) where
mempty :: Refss t r
mempty = NP (Refs t r) (RealHandles t) -> Refss t r
forall t (r :: * -> *). NP (Refs t r) (RealHandles t) -> Refss t r
Refss (NP (Refs t r) (RealHandles t) -> Refss t r)
-> NP (Refs t r) (RealHandles t) -> Refss t r
forall a b. (a -> b) -> a -> b
$ (forall a. Refs t r a) -> NP (Refs t r) (RealHandles t)
forall (xs :: [*]) (f :: * -> *).
SListIN NP xs =>
(forall a. f a) -> NP f xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure ([(Reference a r, MockHandleN t a)] -> Refs t r a
forall t (r :: * -> *) a.
[(Reference a r, MockHandleN t a)] -> Refs t r a
Refs [(Reference a r, MockHandleN t a)]
forall a. Monoid a => a
mempty)
type family Test (f :: (Type -> Type) -> [Type] -> Type) :: Type where
Test (Cmd t) = t
Test (Resp t) = t
newtype FlipRef r h = FlipRef { forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef :: Reference h r }
deriving stock (Int -> FlipRef r h -> ShowS
[FlipRef r h] -> ShowS
FlipRef r h -> String
(Int -> FlipRef r h -> ShowS)
-> (FlipRef r h -> String)
-> ([FlipRef r h] -> ShowS)
-> Show (FlipRef r h)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (r :: * -> *) h.
(Show1 r, Show h) =>
Int -> FlipRef r h -> ShowS
forall (r :: * -> *) h. (Show1 r, Show h) => [FlipRef r h] -> ShowS
forall (r :: * -> *) h. (Show1 r, Show h) => FlipRef r h -> String
$cshowsPrec :: forall (r :: * -> *) h.
(Show1 r, Show h) =>
Int -> FlipRef r h -> ShowS
showsPrec :: Int -> FlipRef r h -> ShowS
$cshow :: forall (r :: * -> *) h. (Show1 r, Show h) => FlipRef r h -> String
show :: FlipRef r h -> String
$cshowList :: forall (r :: * -> *) h. (Show1 r, Show h) => [FlipRef r h] -> ShowS
showList :: [FlipRef r h] -> ShowS
Show)
newtype At f r = At { forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
At f r -> f (FlipRef r) (RealHandles (Test f))
unAt :: f (FlipRef r) (RealHandles (Test f)) }
type f :@ r = At f r
deriving
stock
instance (Show (f (FlipRef r) (RealHandles (Test f)))) => Show (At f r)
data Model t r = Model {
forall t (r :: * -> *). Model t r -> MockState t
modelState :: MockState t
, forall t (r :: * -> *). Model t r -> Refss t r
modelRefss :: Refss t r
}
deriving stock ((forall x. Model t r -> Rep (Model t r) x)
-> (forall x. Rep (Model t r) x -> Model t r)
-> Generic (Model t r)
forall x. Rep (Model t r) x -> Model t r
forall x. Model t r -> Rep (Model t r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t (r :: * -> *) x. Rep (Model t r) x -> Model t r
forall t (r :: * -> *) x. Model t r -> Rep (Model t r) x
$cfrom :: forall t (r :: * -> *) x. Model t r -> Rep (Model t r) x
from :: forall x. Model t r -> Rep (Model t r) x
$cto :: forall t (r :: * -> *) x. Rep (Model t r) x -> Model t r
to :: forall x. Rep (Model t r) x -> Model t r
Generic)
deriving stock instance ( Show1 r
, Show (MockState t)
, All (And Show (Compose Show (MockHandleN t))) (RealHandles t)
) => Show (Model t r)
initModel :: StateMachineTest t m -> Model t r
initModel :: forall t (m :: * -> *) (r :: * -> *).
StateMachineTest t m -> Model t r
initModel StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
runMock :: Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: MockState t
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: Model t Concrete -> m ()
tag :: [Event t Symbolic] -> [Tag t]
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
..} = MockState t -> Refss t r -> Model t r
forall t (r :: * -> *). MockState t -> Refss t r -> Model t r
Model MockState t
initMock (NP (Refs t r) (RealHandles t) -> Refss t r
forall t (r :: * -> *). NP (Refs t r) (RealHandles t) -> Refss t r
Refss ((forall a. Refs t r a) -> NP (Refs t r) (RealHandles t)
forall (xs :: [*]) (f :: * -> *).
SListIN NP xs =>
(forall a. f a) -> NP f xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure ([(Reference a r, MockHandleN t a)] -> Refs t r a
forall t (r :: * -> *) a.
[(Reference a r, MockHandleN t a)] -> Refs t r a
Refs [])))
data StateMachineTest t m =
( Monad m
, All Typeable (RealHandles t)
, All Eq (RealHandles t)
, All (And Show (Compose Show (MockHandleN t))) (RealHandles t)
, All (And CanDiff (Compose CanDiff (MockHandleN t))) (RealHandles t)
, NTraversable (Resp t)
, Eq (Resp t (MockHandleN t) (RealHandles t))
, Show (Resp t (MockHandleN 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)
, CanDiff (MockState t)
, Show (Tag t)
, CanDiff (Model t Concrete)
) => StateMachineTest {
forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runMock :: Cmd t (MockHandleN t) (RealHandles t) -> MockState t -> (Resp t (MockHandleN t) (RealHandles t), MockState t)
, forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
, forall t (m :: * -> *). StateMachineTest t m -> MockState t
initMock :: MockState t
, forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles :: forall f. Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
, forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
, forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker :: Model t Symbolic -> Cmd t :@ Symbolic -> [Cmd t :@ Symbolic]
, forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
cleanup :: Model t Concrete -> m ()
, forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
tag :: [Event t Symbolic] -> [Tag t]
}
hoistStateMachineTest :: Monad n
=> (forall a. m a -> n a)
-> StateMachineTest t m
-> StateMachineTest t n
hoistStateMachineTest :: forall (n :: * -> *) (m :: * -> *) t.
Monad n =>
(forall a. m a -> n a)
-> StateMachineTest t m -> StateMachineTest t n
hoistStateMachineTest forall a. m a -> n a
f StateMachineTest {MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
runMock :: Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: MockState t
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: Model t Concrete -> m ()
tag :: [Event t Symbolic] -> [Tag t]
..} = StateMachineTest {
runMock :: Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runMock = Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runMock
, runReal :: Cmd t I (RealHandles t) -> n (Resp t I (RealHandles t))
runReal = m (Resp t I (RealHandles t)) -> n (Resp t I (RealHandles t))
forall a. m a -> n a
f (m (Resp t I (RealHandles t)) -> n (Resp t I (RealHandles t)))
-> (Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t)))
-> Cmd t I (RealHandles t)
-> n (Resp t I (RealHandles t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runReal
, initMock :: MockState t
initMock = MockState t
initMock
, newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles = Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles
, generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator = Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator
, shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker = Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker
, cleanup :: Model t Concrete -> n ()
cleanup = m () -> n ()
forall a. m a -> n a
f (m () -> n ())
-> (Model t Concrete -> m ()) -> Model t Concrete -> n ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model t Concrete -> m ()
cleanup
, tag :: [Event t Symbolic] -> [Tag t]
tag = [Event t Symbolic] -> [Tag t]
tag
}
semantics :: StateMachineTest t m
-> Cmd t :@ Concrete
-> m (Resp t :@ Concrete)
semantics :: forall t (m :: * -> *).
StateMachineTest t m
-> (Cmd t :@ Concrete) -> m (Resp t :@ Concrete)
semantics StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
runMock :: Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: MockState t
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: Model t Concrete -> m ()
tag :: [Event t Symbolic] -> [Tag t]
..} (At Cmd t (FlipRef Concrete) (RealHandles (Test (Cmd t)))
c) =
Resp t (FlipRef Concrete) (RealHandles t) -> At (Resp t) Concrete
Resp t (FlipRef Concrete) (RealHandles (Test (Resp t)))
-> At (Resp t) Concrete
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At (Resp t (FlipRef Concrete) (RealHandles t) -> At (Resp t) Concrete)
-> (Resp t I (RealHandles t)
-> Resp t (FlipRef Concrete) (RealHandles t))
-> Resp t I (RealHandles t)
-> At (Resp t) Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy Typeable
-> (forall a.
Typeable a =>
Elem (RealHandles t) a -> I a -> FlipRef Concrete a)
-> Resp t I (RealHandles t)
-> Resp t (FlipRef Concrete) (RealHandles t)
forall {k} (f :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
(xs :: [k]) (proxy :: (k -> Constraint) -> *) (g :: k -> *)
(h :: k -> *).
(NTraversable f, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> h a)
-> f g xs
-> f h xs
ncfmap (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Typeable) ((I a -> FlipRef Concrete a)
-> Elem (RealHandles t) a -> I a -> FlipRef Concrete a
forall a b. a -> b -> a
const I a -> FlipRef Concrete a
forall a. Typeable a => I a -> FlipRef Concrete a
wrapConcrete) (Resp t I (RealHandles t) -> At (Resp t) Concrete)
-> m (Resp t I (RealHandles t)) -> m (At (Resp t) Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
runReal ((forall a. Elem (RealHandles t) a -> FlipRef Concrete a -> I a)
-> Cmd t (FlipRef Concrete) (RealHandles t)
-> Cmd t I (RealHandles t)
forall {k} (f :: (k -> *) -> [k] -> *) (xs :: [k]) (g :: k -> *)
(h :: k -> *).
(NTraversable f, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> h a) -> f g xs -> f h xs
nfmap ((FlipRef Concrete a -> I a)
-> Elem (RealHandles t) a -> FlipRef Concrete a -> I a
forall a b. a -> b -> a
const FlipRef Concrete a -> I a
forall a. FlipRef Concrete a -> I a
unwrapConcrete) Cmd t (FlipRef Concrete) (RealHandles t)
Cmd t (FlipRef Concrete) (RealHandles (Test (Cmd t)))
c)
unwrapConcrete :: FlipRef Concrete a -> I a
unwrapConcrete :: forall a. FlipRef Concrete a -> I a
unwrapConcrete = a -> I a
forall a. a -> I a
I (a -> I a)
-> (FlipRef Concrete a -> a) -> FlipRef Concrete a -> I a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reference a Concrete -> a
forall a. Reference a Concrete -> a
concrete (Reference a Concrete -> a)
-> (FlipRef Concrete a -> Reference a Concrete)
-> FlipRef Concrete a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlipRef Concrete a -> Reference a Concrete
forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef
wrapConcrete :: Typeable a => I a -> FlipRef Concrete a
wrapConcrete :: forall a. Typeable a => I a -> FlipRef Concrete a
wrapConcrete = Reference a Concrete -> FlipRef Concrete a
forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef (Reference a Concrete -> FlipRef Concrete a)
-> (I a -> Reference a Concrete) -> I a -> FlipRef Concrete a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Reference a Concrete
forall a. Typeable a => a -> Reference a Concrete
reference (a -> Reference a Concrete)
-> (I a -> a) -> I a -> Reference a Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I a -> a
forall a. I a -> a
unI
toMockHandleNs :: (NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r)
=> Refss t r -> f :@ r -> f (MockHandleN t) (RealHandles t)
toMockHandleNs :: forall (f :: (* -> *) -> [*] -> *) t (r :: * -> *).
(NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r) =>
Refss t r -> (f :@ r) -> f (MockHandleN t) (RealHandles t)
toMockHandleNs Refss t r
rss (At f (FlipRef r) (RealHandles (Test f))
fr) =
Proxy Eq
-> (forall a.
Eq a =>
Elem (RealHandles t) a -> FlipRef r a -> MockHandleN t a)
-> f (FlipRef r) (RealHandles t)
-> f (MockHandleN t) (RealHandles t)
forall {k} (f :: (k -> *) -> [k] -> *) (c :: k -> Constraint)
(xs :: [k]) (proxy :: (k -> Constraint) -> *) (g :: k -> *)
(h :: k -> *).
(NTraversable f, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> h a)
-> f g xs
-> f h xs
ncfmap (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq) (\Elem (RealHandles t) a
pf -> NP (Refs t r) (RealHandles t)
-> Elem (RealHandles t) a -> Reference a r -> MockHandleN t a
forall a (r :: * -> *) t.
(Eq a, Eq1 r) =>
NP (Refs t r) (RealHandles t)
-> Elem (RealHandles t) a -> Reference a r -> MockHandleN t a
find (Refss t r -> NP (Refs t r) (RealHandles t)
forall t (r :: * -> *). Refss t r -> NP (Refs t r) (RealHandles t)
unRefss Refss t r
rss) Elem (RealHandles t) a
pf (Reference a r -> MockHandleN t a)
-> (FlipRef r a -> Reference a r) -> FlipRef r a -> MockHandleN t a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlipRef r a -> Reference a r
forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef) f (FlipRef r) (RealHandles t)
f (FlipRef r) (RealHandles (Test f))
fr
where
find :: (Eq a, Eq1 r)
=> NP (Refs t r) (RealHandles t)
-> Elem (RealHandles t) a
-> Reference a r -> MockHandleN t a
find :: forall a (r :: * -> *) t.
(Eq a, Eq1 r) =>
NP (Refs t r) (RealHandles t)
-> Elem (RealHandles t) a -> Reference a r -> MockHandleN t a
find NP (Refs t r) (RealHandles t)
refss Elem (RealHandles t) a
ix Reference a r
r = Refs t r a -> [(Reference a r, MockHandleN t a)]
forall t (r :: * -> *) a.
Refs t r a -> [(Reference a r, MockHandleN t a)]
unRefs (NP (Refs t r) (RealHandles t)
-> Elem (RealHandles t) a -> Refs t r a
forall {k} (f :: k -> *) (xs :: [k]) (a :: k).
NP f xs -> Elem xs a -> f a
npAt NP (Refs t r) (RealHandles t)
refss Elem (RealHandles t) a
ix) [(Reference a r, MockHandleN t a)]
-> Reference a r -> MockHandleN t a
forall k a. Eq k => [(k, a)] -> k -> a
! Reference a r
r
step :: Eq1 r
=> StateMachineTest t m
-> Model t r
-> Cmd t :@ r
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
step :: forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
step StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
runMock :: Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: MockState t
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: Model t Concrete -> m ()
tag :: [Event t Symbolic] -> [Tag t]
..} (Model MockState t
st Refss t r
rss) Cmd t :@ r
cmd =
Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runMock (Refss t r -> (Cmd t :@ r) -> Cmd t (MockHandleN t) (RealHandles t)
forall (f :: (* -> *) -> [*] -> *) t (r :: * -> *).
(NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r) =>
Refss t r -> (f :@ r) -> f (MockHandleN t) (RealHandles t)
toMockHandleNs Refss t r
rss Cmd t :@ r
cmd) MockState t
st
data Event t r = Event {
forall t (r :: * -> *). Event t r -> Model t r
before :: Model t r
, forall t (r :: * -> *). Event t r -> Cmd t :@ r
cmd :: Cmd t :@ r
, forall t (r :: * -> *). Event t r -> Model t r
after :: Model t r
, forall t (r :: * -> *).
Event t r -> Resp t (MockHandleN t) (RealHandles t)
mockResp :: Resp t (MockHandleN t) (RealHandles t)
}
lockstep :: forall t m r. Eq1 r
=> StateMachineTest t m
-> Model t r
-> Cmd t :@ r
-> Resp t :@ r
-> Event t r
lockstep :: forall t (m :: * -> *) (r :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
lockstep sm :: StateMachineTest t m
sm@StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
runMock :: Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: MockState t
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: Model t Concrete -> m ()
tag :: [Event t Symbolic] -> [Tag t]
..} m :: Model t r
m@(Model MockState t
_ Refss t r
rss) Cmd t :@ r
c (At Resp t (FlipRef r) (RealHandles (Test (Resp t)))
resp) = Event {
before :: Model t r
before = Model t r
m
, cmd :: Cmd t :@ r
cmd = Cmd t :@ r
c
, after :: Model t r
after = MockState t -> Refss t r -> Model t r
forall t (r :: * -> *). MockState t -> Refss t r -> Model t r
Model MockState t
st' (Refss t r
rss Refss t r -> Refss t r -> Refss t r
forall a. Semigroup a => a -> a -> a
<> Refss t r
rss')
, mockResp :: Resp t (MockHandleN t) (RealHandles t)
mockResp = Resp t (MockHandleN t) (RealHandles t)
resp'
}
where
(Resp t (MockHandleN t) (RealHandles t)
resp', MockState t
st') = StateMachineTest t m
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
step StateMachineTest t m
sm Model t r
m Cmd t :@ r
c
rss' :: Refss t r
rss' :: Refss t r
rss' = NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandleN t) (RealHandles t) -> Refss t r
forall t (r :: * -> *).
SListI (RealHandles t) =>
NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandleN t) (RealHandles t) -> Refss t r
zipHandles (Resp t (FlipRef r) (RealHandles t)
-> NP ([] :.: FlipRef r) (RealHandles t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles Resp t (FlipRef r) (RealHandles t)
Resp t (FlipRef r) (RealHandles (Test (Resp t)))
resp) (Resp t (MockHandleN t) (RealHandles t)
-> NP ([] :.: MockHandleN t) (RealHandles t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles Resp t (MockHandleN t) (RealHandles t)
resp')
transition :: Eq1 r
=> StateMachineTest t m
-> Model t r
-> Cmd t :@ r
-> Resp t :@ r
-> Model t r
transition :: forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Model t r
transition StateMachineTest t m
sm Model t r
m Cmd t :@ r
c = Event t r -> Model t r
forall t (r :: * -> *). Event t r -> Model t r
after (Event t r -> Model t r)
-> ((Resp t :@ r) -> Event t r) -> (Resp t :@ r) -> Model t r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
forall t (m :: * -> *) (r :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
lockstep StateMachineTest t m
sm Model t r
m Cmd t :@ r
c
postcondition :: StateMachineTest t m
-> Model t Concrete
-> Cmd t :@ Concrete
-> Resp t :@ Concrete
-> Logic
postcondition :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Concrete
-> (Cmd t :@ Concrete)
-> (Resp t :@ Concrete)
-> Logic
postcondition sm :: StateMachineTest t m
sm@StateMachineTest{} Model t Concrete
m Cmd t :@ Concrete
c Resp t :@ Concrete
r =
Refss t Concrete
-> (Resp t :@ Concrete) -> Resp t (MockHandleN t) (RealHandles t)
forall (f :: (* -> *) -> [*] -> *) t (r :: * -> *).
(NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r) =>
Refss t r -> (f :@ r) -> f (MockHandleN t) (RealHandles t)
toMockHandleNs (Model t Concrete -> Refss t Concrete
forall t (r :: * -> *). Model t r -> Refss t r
modelRefss (Model t Concrete -> Refss t Concrete)
-> Model t Concrete -> Refss t Concrete
forall a b. (a -> b) -> a -> b
$ Event t Concrete -> Model t Concrete
forall t (r :: * -> *). Event t r -> Model t r
after Event t Concrete
e) Resp t :@ Concrete
r Resp t (MockHandleN t) (RealHandles t)
-> Resp t (MockHandleN t) (RealHandles t) -> Logic
forall a. (Eq a, Show a) => a -> a -> Logic
.== Event t Concrete -> Resp t (MockHandleN t) (RealHandles t)
forall t (r :: * -> *).
Event t r -> Resp t (MockHandleN t) (RealHandles t)
mockResp Event t Concrete
e
where
e :: Event t Concrete
e = StateMachineTest t m
-> Model t Concrete
-> (Cmd t :@ Concrete)
-> (Resp t :@ Concrete)
-> Event t Concrete
forall t (m :: * -> *) (r :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
lockstep StateMachineTest t m
sm Model t Concrete
m Cmd t :@ Concrete
c Resp t :@ Concrete
r
symbolicResp :: StateMachineTest t m
-> Model t Symbolic
-> Cmd t :@ Symbolic
-> GenSym (Resp t :@ Symbolic)
symbolicResp :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic
-> (Cmd t :@ Symbolic)
-> GenSym (Resp t :@ Symbolic)
symbolicResp sm :: StateMachineTest t m
sm@StateMachineTest{} Model t Symbolic
m Cmd t :@ Symbolic
c =
Resp t (FlipRef Symbolic) (RealHandles t) -> At (Resp t) Symbolic
Resp t (FlipRef Symbolic) (RealHandles (Test (Resp t)))
-> At (Resp t) Symbolic
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At (Resp t (FlipRef Symbolic) (RealHandles t) -> At (Resp t) Symbolic)
-> GenSym (Resp t (FlipRef Symbolic) (RealHandles t))
-> GenSym (At (Resp t) Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy Typeable
-> (forall a.
Typeable a =>
Elem (RealHandles t) a
-> MockHandleN t a -> GenSym (FlipRef Symbolic a))
-> Resp t (MockHandleN t) (RealHandles t)
-> GenSym (Resp t (FlipRef Symbolic) (RealHandles t))
forall k (f :: (k -> *) -> [k] -> *) (m :: * -> *)
(c :: k -> Constraint) (xs :: [k])
(proxy :: (k -> Constraint) -> *) (g :: k -> *) (h :: k -> *).
(NTraversable f, Applicative m, All c xs) =>
proxy c
-> (forall (a :: k). c a => Elem xs a -> g a -> m (h a))
-> f g xs
-> m (f h xs)
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 t g xs
-> m (Resp t h xs)
nctraverse (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Typeable) (\Elem (RealHandles t) a
_ MockHandleN t a
_ -> Reference a Symbolic -> FlipRef Symbolic a
forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef (Reference a Symbolic -> FlipRef Symbolic a)
-> GenSym (Reference a Symbolic) -> GenSym (FlipRef Symbolic a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenSym (Reference a Symbolic)
forall a. Typeable a => GenSym (Reference a Symbolic)
genSym) Resp t (MockHandleN t) (RealHandles t)
resp
where
(Resp t (MockHandleN t) (RealHandles t)
resp, MockState t
_mock') = StateMachineTest t m
-> Model t Symbolic
-> (Cmd t :@ Symbolic)
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
step StateMachineTest t m
sm Model t Symbolic
m Cmd t :@ Symbolic
c
precondition :: forall t. (NTraversable (Cmd t), All Eq (RealHandles t))
=> Model t Symbolic
-> Cmd t :@ Symbolic
-> Logic
precondition :: forall t.
(NTraversable (Cmd t), All Eq (RealHandles t)) =>
Model t Symbolic -> (Cmd t :@ Symbolic) -> Logic
precondition (Model MockState t
_ (Refss NP (Refs t Symbolic) (RealHandles t)
hs)) (At Cmd t (FlipRef Symbolic) (RealHandles (Test (Cmd t)))
c) =
Bool -> Logic
Boolean (All -> Bool
M.getAll (All -> Bool) -> All -> Bool
forall a b. (a -> b) -> a -> b
$ (forall a. Elem (RealHandles t) a -> FlipRef Symbolic a -> All)
-> Cmd t (FlipRef Symbolic) (RealHandles t) -> All
forall {k} (f :: (k -> *) -> [k] -> *) m (xs :: [k]) (g :: k -> *).
(NTraversable f, Monoid m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m) -> f g xs -> m
nfoldMap Elem (RealHandles t) a -> FlipRef Symbolic a -> All
forall a. Elem (RealHandles t) a -> FlipRef Symbolic a -> All
check Cmd t (FlipRef Symbolic) (RealHandles t)
Cmd t (FlipRef Symbolic) (RealHandles (Test (Cmd t)))
c) Logic -> String -> Logic
.// String
"No undefined handles"
where
check :: Elem (RealHandles t) a -> FlipRef Symbolic a -> M.All
check :: forall a. Elem (RealHandles t) a -> FlipRef Symbolic a -> All
check Elem (RealHandles t) a
ix (FlipRef Reference a Symbolic
a) = Bool -> All
M.All (Bool -> All) -> Bool -> All
forall a b. (a -> b) -> a -> b
$ ((Reference a Symbolic, MockHandleN t a) -> Bool)
-> [(Reference a Symbolic, MockHandleN t a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Reference a Symbolic -> Reference a Symbolic -> Bool
forall a. Reference a Symbolic -> Reference a Symbolic -> Bool
sameRef Reference a Symbolic
a (Reference a Symbolic -> Bool)
-> ((Reference a Symbolic, MockHandleN t a)
-> Reference a Symbolic)
-> (Reference a Symbolic, MockHandleN t a)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reference a Symbolic, MockHandleN t a) -> Reference a Symbolic
forall a b. (a, b) -> a
fst) (Refs t Symbolic a -> [(Reference a Symbolic, MockHandleN t a)]
forall t (r :: * -> *) a.
Refs t r a -> [(Reference a r, MockHandleN t a)]
unRefs (NP (Refs t Symbolic) (RealHandles t)
hs NP (Refs t Symbolic) (RealHandles t)
-> Elem (RealHandles t) a -> Refs t Symbolic a
forall {k} (f :: k -> *) (xs :: [k]) (a :: k).
NP f xs -> Elem xs a -> f a
`npAt` Elem (RealHandles t) a
ix))
sameRef :: Reference a Symbolic -> Reference a Symbolic -> Bool
sameRef :: forall a. Reference a Symbolic -> Reference a Symbolic -> Bool
sameRef (QSM.Reference (QSM.Symbolic Var
v)) (QSM.Reference (QSM.Symbolic Var
v')) = Var
v Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v'
toStateMachine :: StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine :: forall t (m :: * -> *).
StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine sm :: StateMachineTest t m
sm@StateMachineTest{} = StateMachine {
initModel :: forall (r :: * -> *). Model t r
initModel = StateMachineTest t m -> Model t r
forall t (m :: * -> *) (r :: * -> *).
StateMachineTest t m -> Model t r
initModel StateMachineTest t m
sm
, transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model t r -> At (Cmd t) r -> At (Resp t) r -> Model t r
transition = StateMachineTest t m
-> Model t r -> At (Cmd t) r -> At (Resp t) r -> Model t r
forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Model t r
transition StateMachineTest t m
sm
, precondition :: Model t Symbolic -> At (Cmd t) Symbolic -> Logic
precondition = Model t Symbolic -> At (Cmd t) Symbolic -> Logic
forall t.
(NTraversable (Cmd t), All Eq (RealHandles t)) =>
Model t Symbolic -> (Cmd t :@ Symbolic) -> Logic
precondition
, postcondition :: Model t Concrete
-> At (Cmd t) Concrete -> At (Resp t) Concrete -> Logic
postcondition = StateMachineTest t m
-> Model t Concrete
-> At (Cmd t) Concrete
-> At (Resp t) Concrete
-> Logic
forall t (m :: * -> *).
StateMachineTest t m
-> Model t Concrete
-> (Cmd t :@ Concrete)
-> (Resp t :@ Concrete)
-> Logic
postcondition StateMachineTest t m
sm
, generator :: Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
generator = StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator StateMachineTest t m
sm
, shrinker :: Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
shrinker = StateMachineTest t m
-> Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker StateMachineTest t m
sm
, semantics :: At (Cmd t) Concrete -> m (At (Resp t) Concrete)
semantics = StateMachineTest t m
-> At (Cmd t) Concrete -> m (At (Resp t) Concrete)
forall t (m :: * -> *).
StateMachineTest t m
-> (Cmd t :@ Concrete) -> m (Resp t :@ Concrete)
semantics StateMachineTest t m
sm
, mock :: Model t Symbolic
-> At (Cmd t) Symbolic -> GenSym (At (Resp t) Symbolic)
mock = StateMachineTest t m
-> Model t Symbolic
-> At (Cmd t) Symbolic
-> GenSym (At (Resp t) Symbolic)
forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic
-> (Cmd t :@ Symbolic)
-> GenSym (Resp t :@ Symbolic)
symbolicResp StateMachineTest t m
sm
, cleanup :: Model t Concrete -> m ()
cleanup = StateMachineTest t m -> Model t Concrete -> m ()
forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
cleanup StateMachineTest t m
sm
, invariant :: Maybe (Model t Concrete -> Logic)
invariant = Maybe (Model t Concrete -> Logic)
forall a. Maybe a
Nothing
}
prop_sequential :: forall t.
StateMachineTest t IO
-> Maybe Int
-> Property
prop_sequential :: forall t. StateMachineTest t IO -> Maybe Int -> Property
prop_sequential sm :: StateMachineTest t IO
sm@StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> IO ()
Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
Cmd t I (RealHandles t) -> IO (Resp t I (RealHandles t))
Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
runMock :: Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: Cmd t I (RealHandles t) -> IO (Resp t I (RealHandles t))
initMock :: MockState t
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
shrinker :: Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
cleanup :: Model t Concrete -> IO ()
tag :: [Event t Symbolic] -> [Tag t]
..} Maybe Int
mMinSize =
StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
-> Maybe Int
-> (Commands (At (Cmd t)) (At (Resp t)) -> Property)
-> Property
forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
(model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int -> (Commands cmd resp -> prop) -> Property
forAllCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' Maybe Int
mMinSize ((Commands (At (Cmd t)) (At (Resp t)) -> Property) -> Property)
-> (Commands (At (Cmd t)) (At (Resp t)) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Commands (At (Cmd t)) (At (Resp t))
cmds ->
PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO () -> Property) -> PropertyM IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
(History (At (Cmd t)) (At (Resp t))
hist, Model t Concrete
_model, Reason
res) <- StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
-> Commands (At (Cmd t)) (At (Resp t))
-> PropertyM
IO (History (At (Cmd t)) (At (Resp t)), Model t Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
Foldable resp, MonadMask m, MonadIO m) =>
StateMachine model cmd m resp
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
runCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' Commands (At (Cmd t)) (At (Resp t))
cmds
StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
-> History (At (Cmd t)) (At (Resp t))
-> Property
-> PropertyM IO ()
forall (m :: * -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(MonadIO m, CanDiff (model Concrete), Show (cmd Concrete),
Show (resp Concrete)) =>
StateMachine model cmd m resp
-> History cmd resp -> Property -> PropertyM m ()
prettyCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' History (At (Cmd t)) (At (Resp t))
hist
(Property -> PropertyM IO ()) -> Property -> PropertyM IO ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Tags" ((Tag t -> String) -> [Tag t] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Tag t -> String
forall a. Show a => a -> String
show ([Tag t] -> [String]) -> [Tag t] -> [String]
forall a b. (a -> b) -> a -> b
$ Commands (At (Cmd t)) (At (Resp t)) -> [Tag t]
tagCmds Commands (At (Cmd t)) (At (Resp t))
cmds)
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Reason
res Reason -> Reason -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Reason
Ok
where
sm' :: StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' = StateMachineTest t IO
-> StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
forall t (m :: * -> *).
StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine StateMachineTest t IO
sm
tagCmds :: QSM.Commands (At (Cmd t)) (At (Resp t)) -> [Tag t]
tagCmds :: Commands (At (Cmd t)) (At (Resp t)) -> [Tag t]
tagCmds = [Event t Symbolic] -> [Tag t]
tag ([Event t Symbolic] -> [Tag t])
-> (Commands (At (Cmd t)) (At (Resp t)) -> [Event t Symbolic])
-> Commands (At (Cmd t)) (At (Resp t))
-> [Tag t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic)
-> [Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
-> [Event t Symbolic]
forall a b. (a -> b) -> [a] -> [b]
map (StateMachineTest t IO
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
forall t (m :: * -> *).
StateMachineTest t m
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
fromLabelEvent StateMachineTest t IO
sm) ([Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
-> [Event t Symbolic])
-> (Commands (At (Cmd t)) (At (Resp t))
-> [Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic])
-> Commands (At (Cmd t)) (At (Resp t))
-> [Event t Symbolic]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
-> Commands (At (Cmd t)) (At (Resp t))
-> [Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> Commands cmd resp -> [Event model cmd resp Symbolic]
Label.execCmds StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm'
prop_parallel :: StateMachineTest t IO
-> Maybe Int
-> Property
prop_parallel :: forall t. StateMachineTest t IO -> Maybe Int -> Property
prop_parallel sm :: StateMachineTest t IO
sm@StateMachineTest{} Maybe Int
mMinSize =
StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
-> Maybe Int
-> (ParallelCommands (At (Cmd t)) (At (Resp t)) -> Property)
-> Property
forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
(model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int -> (ParallelCommands cmd resp -> prop) -> Property
forAllParallelCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' Maybe Int
mMinSize ((ParallelCommands (At (Cmd t)) (At (Resp t)) -> Property)
-> Property)
-> (ParallelCommands (At (Cmd t)) (At (Resp t)) -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \ParallelCommands (At (Cmd t)) (At (Resp t))
cmds ->
PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO () -> Property) -> PropertyM IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
[(History (At (Cmd t)) (At (Resp t)), Model t Concrete, Logic)]
hist <- StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
-> ParallelCommands (At (Cmd t)) (At (Resp t))
-> PropertyM
IO [(History (At (Cmd t)) (At (Resp t)), Model t Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
Foldable resp, MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' ParallelCommands (At (Cmd t)) (At (Resp t))
cmds
ParallelCommands (At (Cmd t)) (At (Resp t))
-> [(History (At (Cmd t)) (At (Resp t)), Model t Concrete, Logic)]
-> PropertyM IO ()
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
a.
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
Foldable cmd) =>
ParallelCommands cmd resp
-> [(History cmd resp, a, Logic)] -> PropertyM m ()
prettyParallelCommands ParallelCommands (At (Cmd t)) (At (Resp t))
cmds [(History (At (Cmd t)) (At (Resp t)), Model t Concrete, Logic)]
hist
where
sm' :: StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
sm' = StateMachineTest t IO
-> StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
forall t (m :: * -> *).
StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine StateMachineTest t IO
sm
fromLabelEvent :: StateMachineTest t m
-> Label.Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
fromLabelEvent :: forall t (m :: * -> *).
StateMachineTest t m
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
fromLabelEvent StateMachineTest t m
sm Label.Event{Model t Symbolic
At (Resp t) Symbolic
At (Cmd t) Symbolic
eventBefore :: Model t Symbolic
eventCmd :: At (Cmd t) Symbolic
eventAfter :: Model t Symbolic
eventResp :: At (Resp t) Symbolic
eventBefore :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *) (r :: * -> *).
Event model cmd resp r -> model r
eventCmd :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *) (r :: * -> *).
Event model cmd resp r -> cmd r
eventAfter :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *) (r :: * -> *).
Event model cmd resp r -> model r
eventResp :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *) (r :: * -> *).
Event model cmd resp r -> resp r
..} = Event{
before :: Model t Symbolic
before = Model t Symbolic
eventBefore
, cmd :: At (Cmd t) Symbolic
cmd = At (Cmd t) Symbolic
eventCmd
, after :: Model t Symbolic
after = Model t Symbolic
eventAfter
, mockResp :: Resp t (MockHandleN t) (RealHandles t)
mockResp = Resp t (MockHandleN t) (RealHandles t)
resp'
}
where
(Resp t (MockHandleN t) (RealHandles t)
resp', MockState t
_st') = StateMachineTest t m
-> Model t Symbolic
-> At (Cmd t) Symbolic
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (r :: * -> *) t (m :: * -> *).
Eq1 r =>
StateMachineTest t m
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
step StateMachineTest t m
sm Model t Symbolic
eventBefore At (Cmd t) Symbolic
eventCmd
showLabelledExamples' :: StateMachineTest t m
-> Maybe Int
-> Int
-> (Tag t -> Bool)
-> IO ()
showLabelledExamples' :: forall t (m :: * -> *).
StateMachineTest t m
-> Maybe Int -> Int -> (Tag t -> Bool) -> IO ()
showLabelledExamples' sm :: StateMachineTest t m
sm@StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
runMock :: Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: MockState t
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
shrinker :: Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
cleanup :: Model t Concrete -> m ()
tag :: [Event t Symbolic] -> [Tag t]
..} Maybe Int
mReplay Int
numTests =
StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
-> Maybe Int
-> Int
-> ([Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
-> [Tag t])
-> (Tag t -> Bool)
-> IO ()
forall tag (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *) (m :: * -> *).
(Show tag, Show (model Symbolic), Show (cmd Symbolic),
Show (resp Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int
-> Int
-> ([Event model cmd resp Symbolic] -> [tag])
-> (tag -> Bool)
-> IO ()
Seq.showLabelledExamples'
(StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
forall t (m :: * -> *).
StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine StateMachineTest t m
sm)
Maybe Int
mReplay
Int
numTests
([Event t Symbolic] -> [Tag t]
tag ([Event t Symbolic] -> [Tag t])
-> ([Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
-> [Event t Symbolic])
-> [Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
-> [Tag t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic)
-> [Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
-> [Event t Symbolic]
forall a b. (a -> b) -> [a] -> [b]
map (StateMachineTest t m
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
forall t (m :: * -> *).
StateMachineTest t m
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
fromLabelEvent StateMachineTest t m
sm))
showLabelledExamples :: StateMachineTest t m -> IO ()
showLabelledExamples :: forall t (m :: * -> *). StateMachineTest t m -> IO ()
showLabelledExamples sm :: StateMachineTest t m
sm@StateMachineTest{MockState t
[Event t Symbolic] -> [Tag t]
Model t Concrete -> m ()
Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
runMock :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: forall t (m :: * -> *).
StateMachineTest t m
-> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: forall t (m :: * -> *). StateMachineTest t m -> MockState t
newHandles :: forall t (m :: * -> *).
StateMachineTest t m
-> forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
shrinker :: forall t (m :: * -> *).
StateMachineTest t m
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
cleanup :: forall t (m :: * -> *).
StateMachineTest t m -> Model t Concrete -> m ()
tag :: forall t (m :: * -> *).
StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
runMock :: Cmd t (MockHandleN t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandleN t) (RealHandles t), MockState t)
runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
initMock :: MockState t
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
generator :: Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
shrinker :: Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
cleanup :: Model t Concrete -> m ()
tag :: [Event t Symbolic] -> [Tag t]
..} =
StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
-> ([Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
-> [Tag t])
-> IO ()
forall tag (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *) (m :: * -> *).
(Show tag, Show (model Symbolic), Show (cmd Symbolic),
Show (resp Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ([Event model cmd resp Symbolic] -> [tag]) -> IO ()
Seq.showLabelledExamples
(StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
forall t (m :: * -> *).
StateMachineTest t m
-> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
toStateMachine StateMachineTest t m
sm)
([Event t Symbolic] -> [Tag t]
tag ([Event t Symbolic] -> [Tag t])
-> ([Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
-> [Event t Symbolic])
-> [Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
-> [Tag t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic)
-> [Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic]
-> [Event t Symbolic]
forall a b. (a -> b) -> [a] -> [b]
map (StateMachineTest t m
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
forall t (m :: * -> *).
StateMachineTest t m
-> Event (Model t) (At (Cmd t)) (At (Resp t)) Symbolic
-> Event t Symbolic
fromLabelEvent StateMachineTest t m
sm))
instance (NTraversable (Cmd t), SListI (RealHandles t))
=> Rank2.Functor (At (Cmd t)) where
fmap :: forall p q. (forall a. p a -> q a) -> At (Cmd t) p -> At (Cmd t) q
fmap :: forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> At (Cmd t) p -> At (Cmd t) q
fmap forall a. p a -> q a
f (At Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd) = Cmd t (FlipRef q) (RealHandles (Test (Cmd t))) -> At (Cmd t) q
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At (Cmd t (FlipRef q) (RealHandles (Test (Cmd t))) -> At (Cmd t) q)
-> Cmd t (FlipRef q) (RealHandles (Test (Cmd t))) -> At (Cmd t) q
forall a b. (a -> b) -> a -> b
$ (forall a. Elem (RealHandles t) a -> FlipRef p a -> FlipRef q a)
-> Cmd t (FlipRef p) (RealHandles t)
-> Cmd t (FlipRef q) (RealHandles t)
forall {k} (f :: (k -> *) -> [k] -> *) (xs :: [k]) (g :: k -> *)
(h :: k -> *).
(NTraversable f, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> h a) -> f g xs -> f h xs
nfmap ((FlipRef p a -> FlipRef q a)
-> Elem (RealHandles t) a -> FlipRef p a -> FlipRef q a
forall a b. a -> b -> a
const FlipRef p a -> FlipRef q a
forall a. FlipRef p a -> FlipRef q a
f') Cmd t (FlipRef p) (RealHandles t)
Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd
where
f' :: FlipRef p a -> FlipRef q a
f' :: forall a. FlipRef p a -> FlipRef q a
f' = Reference a q -> FlipRef q a
forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef (Reference a q -> FlipRef q a)
-> (FlipRef p a -> Reference a q) -> FlipRef p a -> FlipRef q a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. p a -> q a) -> Reference a p -> Reference a q
forall k (f :: (k -> *) -> *) (p :: k -> *) (q :: k -> *).
Functor f =>
(forall (x :: k). p x -> q x) -> f p -> f q
forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> Reference a p -> Reference a q
Rank2.fmap p x -> q x
forall a. p a -> q a
f (Reference a p -> Reference a q)
-> (FlipRef p a -> Reference a p) -> FlipRef p a -> Reference a q
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlipRef p a -> Reference a p
forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef
instance (NTraversable (Cmd t), SListI (RealHandles t))
=> Rank2.Foldable (At (Cmd t)) where
foldMap :: forall p m. Monoid m => (forall a. p a -> m) -> At (Cmd t) p -> m
foldMap :: forall (p :: * -> *) m.
Monoid m =>
(forall a. p a -> m) -> At (Cmd t) p -> m
foldMap forall a. p a -> m
f (At Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd) = (forall a. Elem (RealHandles t) a -> FlipRef p a -> m)
-> Cmd t (FlipRef p) (RealHandles t) -> m
forall {k} (f :: (k -> *) -> [k] -> *) m (xs :: [k]) (g :: k -> *).
(NTraversable f, Monoid m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m) -> f g xs -> m
nfoldMap ((FlipRef p a -> m) -> Elem (RealHandles t) a -> FlipRef p a -> m
forall a b. a -> b -> a
const FlipRef p a -> m
forall a. FlipRef p a -> m
f') Cmd t (FlipRef p) (RealHandles t)
Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd
where
f' :: FlipRef p a -> m
f' :: forall a. FlipRef p a -> m
f' = (forall a. p a -> m) -> Reference a p -> m
forall m (p :: * -> *).
Monoid m =>
(forall x. p x -> m) -> Reference a p -> m
forall k (f :: (k -> *) -> *) m (p :: k -> *).
(Foldable f, Monoid m) =>
(forall (x :: k). p x -> m) -> f p -> m
Rank2.foldMap p x -> m
forall a. p a -> m
f (Reference a p -> m)
-> (FlipRef p a -> Reference a p) -> FlipRef p a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlipRef p a -> Reference a p
forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef
instance (NTraversable (Cmd t), SListI (RealHandles t))
=> Rank2.Traversable (At (Cmd t)) where
traverse :: forall f p q. Applicative f
=> (forall a. p a -> f (q a)) -> At (Cmd t) p -> f (At (Cmd t) q)
traverse :: forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> At (Cmd t) p -> f (At (Cmd t) q)
traverse forall a. p a -> f (q a)
f (At Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd) = Cmd t (FlipRef q) (RealHandles t) -> At (Cmd t) q
Cmd t (FlipRef q) (RealHandles (Test (Cmd t))) -> At (Cmd t) q
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At (Cmd t (FlipRef q) (RealHandles t) -> At (Cmd t) q)
-> f (Cmd t (FlipRef q) (RealHandles t)) -> f (At (Cmd t) q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a.
Elem (RealHandles t) a -> FlipRef p a -> f (FlipRef q a))
-> Cmd t (FlipRef p) (RealHandles t)
-> f (Cmd t (FlipRef q) (RealHandles t))
forall {k} (f :: (k -> *) -> [k] -> *) (m :: * -> *) (xs :: [k])
(g :: k -> *) (h :: k -> *).
(NTraversable f, Applicative m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m (h a))
-> f g xs -> m (f h xs)
ntraverse ((FlipRef p a -> f (FlipRef q a))
-> Elem (RealHandles t) a -> FlipRef p a -> f (FlipRef q a)
forall a b. a -> b -> a
const FlipRef p a -> f (FlipRef q a)
forall a. FlipRef p a -> f (FlipRef q a)
f') Cmd t (FlipRef p) (RealHandles t)
Cmd t (FlipRef p) (RealHandles (Test (Cmd t)))
cmd
where
f' :: FlipRef p a -> f (FlipRef q a)
f' :: forall a. FlipRef p a -> f (FlipRef q a)
f' = (Reference a q -> FlipRef q a)
-> f (Reference a q) -> f (FlipRef q a)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reference a q -> FlipRef q a
forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef (f (Reference a q) -> f (FlipRef q a))
-> (FlipRef p a -> f (Reference a q))
-> FlipRef p a
-> f (FlipRef q a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. p a -> f (q a)) -> Reference a p -> f (Reference a q)
forall k (t :: (k -> *) -> *) (f :: * -> *) (p :: k -> *)
(q :: k -> *).
(Traversable t, Applicative f) =>
(forall (a :: k). p a -> f (q a)) -> t p -> f (t q)
forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> Reference a p -> f (Reference a q)
Rank2.traverse p a -> f (q a)
forall a. p a -> f (q a)
f (Reference a p -> f (Reference a q))
-> (FlipRef p a -> Reference a p)
-> FlipRef p a
-> f (Reference a q)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlipRef p a -> Reference a p
forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef
instance (NTraversable (Resp t), SListI (RealHandles t))
=> Rank2.Functor (At (Resp t)) where
fmap :: forall p q. (forall a. p a -> q a) -> At (Resp t) p -> At (Resp t) q
fmap :: forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> At (Resp t) p -> At (Resp t) q
fmap forall a. p a -> q a
f (At Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd) = Resp t (FlipRef q) (RealHandles (Test (Resp t))) -> At (Resp t) q
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At (Resp t (FlipRef q) (RealHandles (Test (Resp t))) -> At (Resp t) q)
-> Resp t (FlipRef q) (RealHandles (Test (Resp t)))
-> At (Resp t) q
forall a b. (a -> b) -> a -> b
$ (forall a. Elem (RealHandles t) a -> FlipRef p a -> FlipRef q a)
-> Resp t (FlipRef p) (RealHandles t)
-> Resp t (FlipRef q) (RealHandles t)
forall {k} (f :: (k -> *) -> [k] -> *) (xs :: [k]) (g :: k -> *)
(h :: k -> *).
(NTraversable f, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> h a) -> f g xs -> f h xs
nfmap ((FlipRef p a -> FlipRef q a)
-> Elem (RealHandles t) a -> FlipRef p a -> FlipRef q a
forall a b. a -> b -> a
const FlipRef p a -> FlipRef q a
forall a. FlipRef p a -> FlipRef q a
f') Resp t (FlipRef p) (RealHandles t)
Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd
where
f' :: FlipRef p a -> FlipRef q a
f' :: forall a. FlipRef p a -> FlipRef q a
f' = Reference a q -> FlipRef q a
forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef (Reference a q -> FlipRef q a)
-> (FlipRef p a -> Reference a q) -> FlipRef p a -> FlipRef q a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. p a -> q a) -> Reference a p -> Reference a q
forall k (f :: (k -> *) -> *) (p :: k -> *) (q :: k -> *).
Functor f =>
(forall (x :: k). p x -> q x) -> f p -> f q
forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> Reference a p -> Reference a q
Rank2.fmap p x -> q x
forall a. p a -> q a
f (Reference a p -> Reference a q)
-> (FlipRef p a -> Reference a p) -> FlipRef p a -> Reference a q
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlipRef p a -> Reference a p
forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef
instance (NTraversable (Resp t), SListI (RealHandles t))
=> Rank2.Foldable (At (Resp t)) where
foldMap :: forall p m. Monoid m => (forall a. p a -> m) -> At (Resp t) p -> m
foldMap :: forall (p :: * -> *) m.
Monoid m =>
(forall a. p a -> m) -> At (Resp t) p -> m
foldMap forall a. p a -> m
f (At Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd) = (forall a. Elem (RealHandles t) a -> FlipRef p a -> m)
-> Resp t (FlipRef p) (RealHandles t) -> m
forall {k} (f :: (k -> *) -> [k] -> *) m (xs :: [k]) (g :: k -> *).
(NTraversable f, Monoid m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m) -> f g xs -> m
nfoldMap ((FlipRef p a -> m) -> Elem (RealHandles t) a -> FlipRef p a -> m
forall a b. a -> b -> a
const FlipRef p a -> m
forall a. FlipRef p a -> m
f') Resp t (FlipRef p) (RealHandles t)
Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd
where
f' :: FlipRef p a -> m
f' :: forall a. FlipRef p a -> m
f' = (forall a. p a -> m) -> Reference a p -> m
forall m (p :: * -> *).
Monoid m =>
(forall x. p x -> m) -> Reference a p -> m
forall k (f :: (k -> *) -> *) m (p :: k -> *).
(Foldable f, Monoid m) =>
(forall (x :: k). p x -> m) -> f p -> m
Rank2.foldMap p x -> m
forall a. p a -> m
f (Reference a p -> m)
-> (FlipRef p a -> Reference a p) -> FlipRef p a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlipRef p a -> Reference a p
forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef
instance (NTraversable (Resp t), SListI (RealHandles t))
=> Rank2.Traversable (At (Resp t)) where
traverse :: forall f p q. Applicative f
=> (forall a. p a -> f (q a)) -> At (Resp t) p -> f (At (Resp t) q)
traverse :: forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> At (Resp t) p -> f (At (Resp t) q)
traverse forall a. p a -> f (q a)
f (At Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd) = Resp t (FlipRef q) (RealHandles t) -> At (Resp t) q
Resp t (FlipRef q) (RealHandles (Test (Resp t))) -> At (Resp t) q
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At (Resp t (FlipRef q) (RealHandles t) -> At (Resp t) q)
-> f (Resp t (FlipRef q) (RealHandles t)) -> f (At (Resp t) q)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a.
Elem (RealHandles t) a -> FlipRef p a -> f (FlipRef q a))
-> Resp t (FlipRef p) (RealHandles t)
-> f (Resp t (FlipRef q) (RealHandles t))
forall {k} (f :: (k -> *) -> [k] -> *) (m :: * -> *) (xs :: [k])
(g :: k -> *) (h :: k -> *).
(NTraversable f, Applicative m, SListI xs) =>
(forall (a :: k). Elem xs a -> g a -> m (h a))
-> f g xs -> m (f h xs)
ntraverse ((FlipRef p a -> f (FlipRef q a))
-> Elem (RealHandles t) a -> FlipRef p a -> f (FlipRef q a)
forall a b. a -> b -> a
const FlipRef p a -> f (FlipRef q a)
forall a. FlipRef p a -> f (FlipRef q a)
f') Resp t (FlipRef p) (RealHandles t)
Resp t (FlipRef p) (RealHandles (Test (Resp t)))
cmd
where
f' :: FlipRef p a -> f (FlipRef q a)
f' :: forall a. FlipRef p a -> f (FlipRef q a)
f' = (Reference a q -> FlipRef q a)
-> f (Reference a q) -> f (FlipRef q a)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reference a q -> FlipRef q a
forall (r :: * -> *) h. Reference h r -> FlipRef r h
FlipRef (f (Reference a q) -> f (FlipRef q a))
-> (FlipRef p a -> f (Reference a q))
-> FlipRef p a
-> f (FlipRef q a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. p a -> f (q a)) -> Reference a p -> f (Reference a q)
forall k (t :: (k -> *) -> *) (f :: * -> *) (p :: k -> *)
(q :: k -> *).
(Traversable t, Applicative f) =>
(forall (a :: k). p a -> f (q a)) -> t p -> f (t q)
forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> Reference a p -> f (Reference a q)
Rank2.traverse p a -> f (q a)
forall a. p a -> f (q a)
f (Reference a p -> f (Reference a q))
-> (FlipRef p a -> Reference a p)
-> FlipRef p a
-> f (Reference a q)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlipRef p a -> Reference a p
forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef
(!) :: Eq k => [(k, a)] -> k -> a
[(k, a)]
env ! :: forall k a. Eq k => [(k, a)] -> k -> a
! k
r = Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (k -> [(k, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup k
r [(k, a)]
env)
zipHandles :: SListI (RealHandles t)
=> NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandleN t) (RealHandles t)
-> Refss t r
zipHandles :: forall t (r :: * -> *).
SListI (RealHandles t) =>
NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandleN t) (RealHandles t) -> Refss t r
zipHandles = \NP ([] :.: FlipRef r) (RealHandles t)
real NP ([] :.: MockHandleN t) (RealHandles t)
mock -> NP (Refs t r) (RealHandles t) -> Refss t r
forall t (r :: * -> *). NP (Refs t r) (RealHandles t) -> Refss t r
Refss (NP (Refs t r) (RealHandles t) -> Refss t r)
-> NP (Refs t r) (RealHandles t) -> Refss t r
forall a b. (a -> b) -> a -> b
$ (forall a.
(:.:) [] (FlipRef r) a -> (:.:) [] (MockHandleN t) a -> Refs t r a)
-> Prod NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandleN t) (RealHandles t)
-> NP (Refs t r) (RealHandles t)
forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
(f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith (:.:) [] (FlipRef r) a -> (:.:) [] (MockHandleN t) a -> Refs t r a
forall a.
(:.:) [] (FlipRef r) a -> (:.:) [] (MockHandleN t) a -> Refs t r a
forall (r :: * -> *) a t.
(:.:) [] (FlipRef r) a -> (:.:) [] (MockHandleN t) a -> Refs t r a
zip' Prod NP ([] :.: FlipRef r) (RealHandles t)
NP ([] :.: FlipRef r) (RealHandles t)
real NP ([] :.: MockHandleN t) (RealHandles t)
mock
where
zip' :: (:.:) [] (FlipRef r) a -> (:.:) [] (MockHandleN t) a -> Refs t r a
zip' :: forall (r :: * -> *) a t.
(:.:) [] (FlipRef r) a -> (:.:) [] (MockHandleN t) a -> Refs t r a
zip' (Comp [FlipRef r a]
real) (Comp [MockHandleN t a]
mock) = [(Reference a r, MockHandleN t a)] -> Refs t r a
forall t (r :: * -> *) a.
[(Reference a r, MockHandleN t a)] -> Refs t r a
Refs ([(Reference a r, MockHandleN t a)] -> Refs t r a)
-> [(Reference a r, MockHandleN t a)] -> Refs t r a
forall a b. (a -> b) -> a -> b
$ [Reference a r]
-> [MockHandleN t a] -> [(Reference a r, MockHandleN t a)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((FlipRef r a -> Reference a r) -> [FlipRef r a] -> [Reference a r]
forall a b. (a -> b) -> [a] -> [b]
map FlipRef r a -> Reference a r
forall (r :: * -> *) h. FlipRef r h -> Reference h r
unFlipRef [FlipRef r a]
real) [MockHandleN t a]
mock