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

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

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

import qualified Test.StateMachine.Lockstep.NAry      as NAry

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

data family Cmd        t :: Type -> Type
data family Resp       t :: Type -> Type
data family RealHandle t :: Type
data family MockHandle t :: Type

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

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

-- @f@ will be instantiated with @Cmd@ or @Resp@
-- @r@ will be instantiated with 'Symbolic' or 'Concrete'
newtype At f r = At { At f r -> f (Reference (RealHandle (Test f)) r)
unAt :: f (Reference (RealHandle (Test f)) r) }
type    f :@ r = At f r

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

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

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

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

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

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

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

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

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

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

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

data StateMachineTest t =
    ( Typeable t
      -- Response
    , Eq   (Resp t (MockHandle t))
    , Show (Resp t (Reference (RealHandle t) Symbolic))
    , Show (Resp t (Reference (RealHandle t) Concrete))
    , Show (Resp t (MockHandle t))
    , Traversable (Resp t)
      -- Command
    , Show (Cmd t (Reference (RealHandle t) Symbolic))
    , Show (Cmd t (Reference (RealHandle t) Concrete))
    , Traversable (Cmd t)
      -- Real handles
    , Eq     (RealHandle t)
    , Show   (RealHandle t)
    , ToExpr (RealHandle t)
      -- Mock handles
    , Eq     (MockHandle t)
    , Show   (MockHandle t)
    , ToExpr (MockHandle t)
      -- Mock state
    , Show   (MockState t)
    , ToExpr (MockState t)
    ) => StateMachineTest {
      StateMachineTest t
-> Cmd t (MockHandle t)
-> MockState t
-> (Resp t (MockHandle t), MockState t)
runMock    :: Cmd t (MockHandle t) -> MockState t -> (Resp t (MockHandle t), MockState t)
    , StateMachineTest t
-> Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
runReal    :: Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
    , StateMachineTest t -> MockState t
initMock   :: MockState t
    , StateMachineTest t -> forall h. Resp t h -> [h]
newHandles :: forall h. Resp t h -> [h]
    , StateMachineTest t
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator  :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
    , StateMachineTest t
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker   :: Model t Symbolic -> Cmd t :@ Symbolic -> [Cmd t :@ Symbolic]
    , StateMachineTest t -> Model t Concrete -> IO ()
cleanup    :: Model t Concrete -> IO ()
    }

data Simple t

type instance NAry.MockState   (Simple t) = MockState t
type instance NAry.RealHandles (Simple t) = '[RealHandle t]
type instance NAry.RealMonad   (Simple _) = IO

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

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

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

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

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

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

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

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

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

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

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

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

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

fromSimple :: StateMachineTest t -> NAry.StateMachineTest (Simple t)
fromSimple :: StateMachineTest t -> StateMachineTest (Simple t)
fromSimple StateMachineTest{MockState t
Model t Concrete -> IO ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t (MockHandle t)
-> MockState t -> (Resp t (MockHandle t), MockState t)
Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
forall h. Resp t h -> [h]
cleanup :: Model t Concrete -> IO ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall h. Resp t h -> [h]
initMock :: MockState t
runReal :: Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
runMock :: Cmd t (MockHandle t)
-> MockState t -> (Resp t (MockHandle t), MockState t)
cleanup :: forall t. StateMachineTest t -> Model t Concrete -> IO ()
shrinker :: forall t.
StateMachineTest t
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: forall t.
StateMachineTest t
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall t. StateMachineTest t -> forall h. Resp t h -> [h]
initMock :: forall t. StateMachineTest t -> MockState t
runReal :: forall t.
StateMachineTest t
-> Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
runMock :: forall t.
StateMachineTest t
-> Cmd t (MockHandle t)
-> MockState t
-> (Resp t (MockHandle t), MockState t)
..} = StateMachineTest :: forall t.
(Monad (RealMonad t), All Typeable (RealHandles t),
 All Eq (RealHandles t),
 All (And Show (Compose Show (MockHandle t))) (RealHandles t),
 All (And ToExpr (Compose ToExpr (MockHandle t))) (RealHandles t),
 NTraversable (Resp t), Eq (Resp t (MockHandle t) (RealHandles t)),
 Show (Resp t (MockHandle t) (RealHandles t)),
 Show (Resp t (FlipRef Symbolic) (RealHandles t)),
 Show (Resp t (FlipRef Concrete) (RealHandles t)),
 NTraversable (Cmd t),
 Show (Cmd t (FlipRef Symbolic) (RealHandles t)),
 Show (Cmd t (FlipRef Concrete) (RealHandles t)),
 Show (MockState t), ToExpr (MockState t)) =>
(Cmd t (MockHandle t) (RealHandles t)
 -> MockState t
 -> (Resp t (MockHandle t) (RealHandles t), MockState t))
-> (Cmd t I (RealHandles t)
    -> RealMonad t (Resp t I (RealHandles t)))
-> MockState t
-> (forall (f :: * -> *).
    Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t))
-> (Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic)))
-> (Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic])
-> (Model t Concrete -> RealMonad t ())
-> StateMachineTest t
NAry.StateMachineTest {
      runMock :: Cmd (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t))
-> MockState (Simple t)
-> (Resp
      (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t)),
    MockState (Simple t))
runMock    = \Cmd (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t))
cmd MockState (Simple t)
st -> (Resp t (MockHandle t)
 -> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t])
-> (Resp t (MockHandle t), MockState t)
-> (Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t],
    MockState t)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Resp t (MockHandle t)
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
forall t.
Functor (Resp t) =>
Resp t (MockHandle t)
-> Resp (Simple t) (MockHandle (Simple t)) '[RealHandle t]
respMockFromSimple (Cmd t (MockHandle t)
-> MockState t -> (Resp t (MockHandle t), MockState t)
runMock (Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
forall t.
Functor (Cmd t) =>
Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
-> Cmd t (MockHandle t)
cmdMockToSimple Cmd (Simple t) (MockHandle (Simple t)) '[RealHandle t]
Cmd (Simple t) (MockHandle (Simple t)) (RealHandles (Simple t))
cmd) MockState t
MockState (Simple t)
st)
    , runReal :: Cmd (Simple t) I (RealHandles (Simple t))
-> RealMonad
     (Simple t) (Resp (Simple t) I (RealHandles (Simple t)))
runReal    = \Cmd (Simple t) I (RealHandles (Simple t))
cmd -> Resp t (RealHandle t) -> Resp (Simple t) I '[RealHandle t]
forall t.
Functor (Resp t) =>
Resp t (RealHandle t) -> Resp (Simple t) I '[RealHandle t]
respRealFromSimple (Resp t (RealHandle t) -> Resp (Simple t) I '[RealHandle t])
-> IO (Resp t (RealHandle t))
-> IO (Resp (Simple t) I '[RealHandle t])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
runReal (Cmd (Simple t) I '[RealHandle t] -> Cmd t (RealHandle t)
forall t.
Functor (Cmd t) =>
Cmd (Simple t) I '[RealHandle t] -> Cmd t (RealHandle t)
cmdRealToSimple Cmd (Simple t) I '[RealHandle t]
Cmd (Simple t) I (RealHandles (Simple t))
cmd))
    , initMock :: MockState (Simple t)
initMock   = MockState t
MockState (Simple t)
initMock
    , newHandles :: forall (f :: * -> *).
Resp (Simple t) f (RealHandles (Simple t))
-> NP ([] :.: f) (RealHandles (Simple t))
newHandles = \Resp (Simple t) f (RealHandles (Simple t))
r -> [f (RealHandle t)] -> (:.:) [] f (RealHandle t)
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (Resp t (f (RealHandle t)) -> [f (RealHandle t)]
forall h. Resp t h -> [h]
newHandles (Resp (Simple t) f '[RealHandle t] -> Resp t (f (RealHandle t))
forall t (f :: * -> *) h. Resp (Simple t) f '[h] -> Resp t (f h)
unSimpleResp Resp (Simple t) f '[RealHandle t]
Resp (Simple t) f (RealHandles (Simple t))
r)) (:.:) [] f (RealHandle t)
-> NP ([] :.: f) '[] -> NP ([] :.: f) '[RealHandle t]
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP ([] :.: f) '[]
forall k (a :: k -> *). NP a '[]
Nil
    , generator :: Model (Simple t) Symbolic
-> Maybe (Gen (Cmd (Simple t) :@ Symbolic))
generator  = \Model (Simple t) Symbolic
m     -> ((Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic)
-> Gen (Cmd t :@ Symbolic) -> Gen (Cmd (Simple t) :@ Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic
forall t.
Functor (Cmd t) =>
(Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic
cmdAtFromSimple (Gen (Cmd t :@ Symbolic) -> Gen (Cmd (Simple t) :@ Symbolic))
-> Maybe (Gen (Cmd t :@ Symbolic))
-> Maybe (Gen (Cmd (Simple t) :@ Symbolic))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator (Model (Simple t) Symbolic -> Model t Symbolic
forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple Model (Simple t) Symbolic
m)
    , shrinker :: Model (Simple t) Symbolic
-> (Cmd (Simple t) :@ Symbolic) -> [Cmd (Simple t) :@ Symbolic]
shrinker   = \Model (Simple t) Symbolic
m Cmd (Simple t) :@ Symbolic
cmd ->      (Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic
forall t.
Functor (Cmd t) =>
(Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic
cmdAtFromSimple ((Cmd t :@ Symbolic) -> Cmd (Simple t) :@ Symbolic)
-> [Cmd t :@ Symbolic] -> [Cmd (Simple t) :@ Symbolic]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker  (Model (Simple t) Symbolic -> Model t Symbolic
forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple Model (Simple t) Symbolic
m) ((Cmd (Simple t) :@ Symbolic) -> Cmd t :@ Symbolic
forall t.
Functor (Cmd t) =>
(Cmd (Simple t) :@ Symbolic) -> Cmd t :@ Symbolic
cmdAtToSimple Cmd (Simple t) :@ Symbolic
cmd)
    , cleanup :: Model (Simple t) Concrete -> RealMonad (Simple t) ()
cleanup    = Model t Concrete -> IO ()
cleanup   (Model t Concrete -> IO ())
-> (Model (Simple t) Concrete -> Model t Concrete)
-> Model (Simple t) Concrete
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model (Simple t) Concrete -> Model t Concrete
forall t (r :: * -> *). Model (Simple t) r -> Model t r
modelToSimple
    }

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

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

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