{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE ExistentialQuantification  #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs               #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE RecordWildCards            #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE UndecidableInstances       #-}

module Test.StateMachine.Lockstep.NAry (
    -- * Test type-level parameters
    MockState
  , Cmd
  , Resp
  , RealHandles
  , MockHandle
  , RealMonad
  , Test
    -- * Test term-level parameters
  , StateMachineTest(..)
    -- * Handle instantiation
  , At(..)
  , (:@)
    -- * Model state
  , Model(..)
  , Refs(..)
  , Refss(..)
  , FlipRef(..)
    -- * Running the tests
  , prop_sequential
  , prop_parallel
  -- * Translate to state machine model
  , 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

import qualified Data.Monoid                          as M
import qualified Data.TreeDiff                        as TD
import qualified Test.StateMachine.Types              as QSM
import qualified Test.StateMachine.Types.Rank2        as Rank2

import           Test.StateMachine.Lockstep.Auxiliary

{-------------------------------------------------------------------------------
  Test type-level parameters
-------------------------------------------------------------------------------}

type family MockState   t   :: Type
data family Cmd         t   :: (Type -> Type) -> [Type] -> Type
data family Resp        t   :: (Type -> Type) -> [Type] -> Type
type family RealHandles t   :: [Type]
data family MockHandle  t a :: Type
type family RealMonad   t   :: Type -> Type

{-------------------------------------------------------------------------------
  Reference environments
-------------------------------------------------------------------------------}

-- | Relation between real and mock references for single handle type @a@
newtype Refs t r a = Refs { Refs t r a -> [(Reference a r, MockHandle t a)]
unRefs :: [(Reference a r, MockHandle t a)] }
  deriving newtype (b -> Refs t r a -> Refs t r a
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
stimes :: b -> 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
sconcat :: NonEmpty (Refs t r a) -> Refs t r a
$csconcat :: forall t (r :: * -> *) a. NonEmpty (Refs t r a) -> Refs t r a
<> :: Refs t r a -> 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
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
mconcat :: [Refs t r a] -> Refs t r a
$cmconcat :: forall t (r :: * -> *) a. [Refs t r a] -> Refs t r a
mappend :: Refs t r a -> Refs t r a -> Refs t r a
$cmappend :: forall t (r :: * -> *) a. Refs t r a -> Refs t r a -> Refs t r a
mempty :: Refs t r a
$cmempty :: forall t (r :: * -> *) a. Refs t r a
$cp1Monoid :: forall t (r :: * -> *) a. Semigroup (Refs t r a)
Monoid, Rep (Refs t r a) x -> Refs t r a
Refs t r a -> Rep (Refs t r a) x
(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
to :: Rep (Refs t r a) x -> Refs t r a
$cto :: forall t (r :: * -> *) a x. Rep (Refs t r a) x -> Refs t r a
from :: 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
Generic)

deriving
  stock
  instance (Show1 r, Show a, Show (MockHandle t a)) => Show (Refs t r a)

deriving
  newtype
  instance (ToExpr a, ToExpr (MockHandle t a)) => ToExpr (Refs t Concrete a)

-- | Relation between real and mock references for /all/ handle types
newtype Refss t r = Refss { Refss t r -> NP (Refs t r) (RealHandles t)
unRefss :: NP (Refs t r) (RealHandles t) }

instance ( Show1 r
         , All (And Show (Compose Show (MockHandle 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]
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 (MockHandle t)))
-> (forall a.
    And Show (Compose Show (MockHandle 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 (Proxy (And Show (Compose Show (MockHandle t)))
forall k (t :: k). Proxy t
Proxy @(And Show (Compose Show (MockHandle t)))) forall a.
(Show a, Show (MockHandle t a)) =>
Refs t r a -> K String a
forall a.
And Show (Compose Show (MockHandle 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 (MockHandle t a))
              => Refs t r a -> K String a
      showOne :: 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 All (And ToExpr (Compose ToExpr (MockHandle t))) (RealHandles t)
      => ToExpr (Refss t Concrete) where
  toExpr :: Refss t Concrete -> Expr
toExpr = [Expr] -> Expr
TD.Lst
         ([Expr] -> Expr)
-> (Refss t Concrete -> [Expr]) -> Refss t Concrete -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K Expr) (RealHandles t) -> [Expr]
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
         (NP (K Expr) (RealHandles t) -> [Expr])
-> (Refss t Concrete -> NP (K Expr) (RealHandles t))
-> Refss t Concrete
-> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (And ToExpr (Compose ToExpr (MockHandle t)))
-> (forall a.
    And ToExpr (Compose ToExpr (MockHandle t)) a =>
    Refs t Concrete a -> K Expr a)
-> NP (Refs t Concrete) (RealHandles t)
-> NP (K Expr) (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 (Proxy (And ToExpr (Compose ToExpr (MockHandle t)))
forall k (t :: k). Proxy t
Proxy @(And ToExpr (Compose ToExpr (MockHandle t)))) forall a.
And ToExpr (Compose ToExpr (MockHandle t)) a =>
Refs t Concrete a -> K Expr a
forall a.
(ToExpr a, ToExpr (MockHandle t a)) =>
Refs t Concrete a -> K Expr a
toExprOne
         (NP (Refs t Concrete) (RealHandles t)
 -> NP (K Expr) (RealHandles t))
-> (Refss t Concrete -> NP (Refs t Concrete) (RealHandles t))
-> Refss t Concrete
-> NP (K Expr) (RealHandles t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refss t Concrete -> NP (Refs t Concrete) (RealHandles t)
forall t (r :: * -> *). Refss t r -> NP (Refs t r) (RealHandles t)
unRefss
    where
      toExprOne :: (ToExpr a, ToExpr (MockHandle t a))
                => Refs t Concrete a -> K (TD.Expr) a
      toExprOne :: Refs t Concrete a -> K Expr a
toExprOne = Expr -> K Expr a
forall k a (b :: k). a -> K a b
K (Expr -> K Expr a)
-> (Refs t Concrete a -> Expr) -> Refs t Concrete a -> K Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refs t Concrete a -> Expr
forall a. ToExpr a => a -> Expr
toExpr

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 forall a. Semigroup a => a -> a -> a
forall a. Refs t r a -> Refs t r a -> Refs t r a
(<>) NP (Refs t r) (RealHandles t)
Prod 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 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, MockHandle t a)] -> Refs t r a
forall t (r :: * -> *) a.
[(Reference a r, MockHandle t a)] -> Refs t r a
Refs [(Reference a r, MockHandle t a)]
forall a. Monoid a => a
mempty)

{-------------------------------------------------------------------------------
  Default instantiation to handles
-------------------------------------------------------------------------------}

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

newtype FlipRef r h = FlipRef { 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
showList :: [FlipRef r h] -> ShowS
$cshowList :: forall (r :: * -> *) h. (Show1 r, Show h) => [FlipRef r h] -> ShowS
show :: FlipRef r h -> String
$cshow :: forall (r :: * -> *) h. (Show1 r, Show h) => FlipRef r h -> String
showsPrec :: Int -> FlipRef r h -> ShowS
$cshowsPrec :: forall (r :: * -> *) h.
(Show1 r, Show h) =>
Int -> FlipRef r h -> ShowS
Show)

-- @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 (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)

{-------------------------------------------------------------------------------
  Model
-------------------------------------------------------------------------------}

data Model t r = Model {
      Model t r -> MockState t
modelState :: MockState t
    , 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
$cto :: forall t (r :: * -> *) x. Rep (Model t r) x -> Model t r
$cfrom :: forall t (r :: * -> *) x. Model t r -> Rep (Model t r) x
Generic)

deriving stock instance ( Show1 r
                        , Show (MockState t)
                        , All (And Show (Compose Show (MockHandle t))) (RealHandles t)
                        ) => Show (Model t r)

instance ( ToExpr (MockState t)
         , All (And ToExpr (Compose ToExpr (MockHandle t))) (RealHandles t)
         ) => ToExpr (Model t Concrete)

initModel :: StateMachineTest t -> Model t r
initModel :: StateMachineTest t -> Model t r
initModel StateMachineTest{MockState t
Model t Concrete -> RealMonad t ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> RealMonad t (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
cleanup :: forall t. StateMachineTest t -> Model t Concrete -> RealMonad t ()
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 (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t. StateMachineTest t -> MockState t
runReal :: forall t.
StateMachineTest t
-> Cmd t I (RealHandles t)
-> RealMonad t (Resp t I (RealHandles t))
runMock :: forall t.
StateMachineTest t
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
cleanup :: Model t Concrete -> RealMonad t ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> RealMonad t (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState 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 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, MockHandle t a)] -> Refs t r a
forall t (r :: * -> *) a.
[(Reference a r, MockHandle t a)] -> Refs t r a
Refs [])))

{-------------------------------------------------------------------------------
  High level API
-------------------------------------------------------------------------------}

data StateMachineTest t =
    ( Monad (RealMonad t)
    -- Requirements on the handles
    , 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)
    -- Response
    , 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))
    -- Command
    , NTraversable (Cmd t)
    , Show (Cmd t (FlipRef Symbolic) (RealHandles t))
    , Show (Cmd t (FlipRef Concrete) (RealHandles t))
    -- MockState
    , Show   (MockState t)
    , ToExpr (MockState t)
    ) => StateMachineTest {
      StateMachineTest t
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
runMock    :: Cmd t (MockHandle t) (RealHandles t) -> MockState t -> (Resp t (MockHandle t) (RealHandles t), MockState t)
    , StateMachineTest t
-> Cmd t I (RealHandles t)
-> RealMonad t (Resp t I (RealHandles t))
runReal    :: Cmd t I              (RealHandles t) -> RealMonad t (Resp t I (RealHandles t))
    , StateMachineTest t -> MockState t
initMock   :: MockState t
    , StateMachineTest t
-> forall (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles :: forall f. Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
    , 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 -> RealMonad t ()
cleanup    :: Model t Concrete -> RealMonad t ()
    }

semantics :: StateMachineTest t
          -> Cmd t :@ Concrete
          -> RealMonad t (Resp t :@ Concrete)
semantics :: StateMachineTest t
-> (Cmd t :@ Concrete) -> RealMonad t (Resp t :@ Concrete)
semantics StateMachineTest{MockState t
Model t Concrete -> RealMonad t ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> RealMonad t (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
cleanup :: Model t Concrete -> RealMonad t ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> RealMonad t (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
cleanup :: forall t. StateMachineTest t -> Model t Concrete -> RealMonad t ()
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 (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t. StateMachineTest t -> MockState t
runReal :: forall t.
StateMachineTest t
-> Cmd t I (RealHandles t)
-> RealMonad t (Resp t I (RealHandles t))
runMock :: forall t.
StateMachineTest t
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
..} (At Cmd t (FlipRef Concrete) (RealHandles (Test (Cmd t)))
c) =
    (Resp t (FlipRef Concrete) (RealHandles t) -> Resp t :@ Concrete
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At (Resp t (FlipRef Concrete) (RealHandles t) -> Resp t :@ Concrete)
-> (Resp t I (RealHandles t)
    -> Resp t (FlipRef Concrete) (RealHandles t))
-> Resp t I (RealHandles t)
-> 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 (Proxy Typeable
forall k (t :: k). 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) -> Resp t :@ Concrete)
-> RealMonad t (Resp t I (RealHandles t))
-> RealMonad t (Resp t :@ Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      Cmd t I (RealHandles t) -> RealMonad t (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 :: 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 :: 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

-- | Turn @Cmd@ or @Resp@ in terms of (symbolic or concrete) references to
-- real handles into a command in terms of mock handles.
--
-- This is isomorphic to
--
-- > toMock :: Refss t Symbolic
--          -> Cmd (FlipRef r) (Handles t)
--          -> Cmd  ToMock     (Handles t)
toMockHandles :: (NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r)
              => Refss t r -> f :@ r -> f (MockHandle t) (RealHandles t)
toMockHandles :: Refss t r -> (f :@ r) -> f (MockHandle t) (RealHandles t)
toMockHandles 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 -> MockHandle t a)
-> f (FlipRef r) (RealHandles t)
-> f (MockHandle 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 (Proxy Eq
forall k (t :: k). Proxy t
Proxy @Eq) (\Elem (RealHandles t) a
pf -> NP (Refs t r) (RealHandles t)
-> Elem (RealHandles t) a -> Reference a r -> MockHandle t a
forall a (r :: * -> *) t.
(Eq a, Eq1 r) =>
NP (Refs t r) (RealHandles t)
-> Elem (RealHandles t) a -> Reference a r -> MockHandle 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 -> MockHandle t a)
-> (FlipRef r a -> Reference a r) -> FlipRef r a -> MockHandle 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 -> MockHandle t a
    find :: NP (Refs t r) (RealHandles t)
-> Elem (RealHandles t) a -> Reference a r -> MockHandle 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, MockHandle t a)]
forall t (r :: * -> *) a.
Refs t r a -> [(Reference a r, MockHandle 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, MockHandle t a)]
-> Reference a r -> MockHandle t a
forall k a. Eq k => [(k, a)] -> k -> a
! Reference a r
r

step :: Eq1 r
     => StateMachineTest t
     -> Model t r
     -> Cmd t :@ r
     -> (Resp t (MockHandle t) (RealHandles t), MockState t)
step :: StateMachineTest t
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
step StateMachineTest{MockState t
Model t Concrete -> RealMonad t ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> RealMonad t (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
cleanup :: Model t Concrete -> RealMonad t ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> RealMonad t (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
cleanup :: forall t. StateMachineTest t -> Model t Concrete -> RealMonad t ()
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 (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t. StateMachineTest t -> MockState t
runReal :: forall t.
StateMachineTest t
-> Cmd t I (RealHandles t)
-> RealMonad t (Resp t I (RealHandles t))
runMock :: forall t.
StateMachineTest t
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
..} (Model MockState t
st Refss t r
rss) Cmd t :@ r
cmd =
    Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
runMock (Refss t r -> (Cmd t :@ r) -> Cmd t (MockHandle t) (RealHandles t)
forall (f :: (* -> *) -> [*] -> *) t (r :: * -> *).
(NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r) =>
Refss t r -> (f :@ r) -> f (MockHandle t) (RealHandles t)
toMockHandles Refss t r
rss Cmd t :@ r
cmd) MockState t
st

data Event t r = Event {
      Event t r -> Model t r
before   :: Model t    r
    , Event t r -> Cmd t :@ r
cmd      :: Cmd   t :@ r
    , Event t r -> Model t r
after    :: Model t    r
    , Event t r -> Resp t (MockHandle t) (RealHandles t)
mockResp :: Resp t (MockHandle t) (RealHandles t)
    }

lockstep :: forall t r. Eq1 r
         => StateMachineTest t
         -> Model t    r
         -> Cmd   t :@ r
         -> Resp  t :@ r
         -> Event t    r
lockstep :: StateMachineTest t
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
lockstep sm :: StateMachineTest t
sm@StateMachineTest{MockState t
Model t Concrete -> RealMonad t ()
Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
Cmd t I (RealHandles t) -> RealMonad t (Resp t I (RealHandles t))
Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
cleanup :: Model t Concrete -> RealMonad t ()
shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
newHandles :: forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: MockState t
runReal :: Cmd t I (RealHandles t) -> RealMonad t (Resp t I (RealHandles t))
runMock :: Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
cleanup :: forall t. StateMachineTest t -> Model t Concrete -> RealMonad t ()
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 (f :: * -> *).
   Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
initMock :: forall t. StateMachineTest t -> MockState t
runReal :: forall t.
StateMachineTest t
-> Cmd t I (RealHandles t)
-> RealMonad t (Resp t I (RealHandles t))
runMock :: forall t.
StateMachineTest t
-> Cmd t (MockHandle t) (RealHandles t)
-> MockState t
-> (Resp t (MockHandle t) (RealHandles t), MockState 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 :: forall t (r :: * -> *).
Model t r
-> (Cmd t :@ r)
-> Model t r
-> Resp t (MockHandle t) (RealHandles t)
-> Event t r
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 (MockHandle t) (RealHandles t)
mockResp = Resp t (MockHandle t) (RealHandles t)
resp'
    }
  where
    (Resp t (MockHandle t) (RealHandles t)
resp', MockState t
st') = StateMachineTest t
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (r :: * -> *) t.
Eq1 r =>
StateMachineTest t
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
step StateMachineTest t
sm Model t r
m Cmd t :@ r
c

    rss' :: Refss t r
    rss' :: Refss t r
rss' = NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandle t) (RealHandles t) -> Refss t r
forall t (r :: * -> *).
SListI (RealHandles t) =>
NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandle 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 (MockHandle t) (RealHandles t)
-> NP ([] :.: MockHandle t) (RealHandles t)
forall (f :: * -> *).
Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
newHandles Resp t (MockHandle t) (RealHandles t)
resp')

transition :: Eq1 r
           => StateMachineTest t
           -> Model t    r
           -> Cmd   t :@ r
           -> Resp  t :@ r
           -> Model t    r
transition :: StateMachineTest t
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Model t r
transition StateMachineTest t
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
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
forall t (r :: * -> *).
Eq1 r =>
StateMachineTest t
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
lockstep StateMachineTest t
sm Model t r
m Cmd t :@ r
c

postcondition :: StateMachineTest t
              -> Model t    Concrete
              -> Cmd   t :@ Concrete
              -> Resp  t :@ Concrete
              -> Logic
postcondition :: StateMachineTest t
-> Model t Concrete
-> (Cmd t :@ Concrete)
-> (Resp t :@ Concrete)
-> Logic
postcondition sm :: StateMachineTest t
sm@StateMachineTest{} Model t Concrete
m Cmd t :@ Concrete
c Resp t :@ Concrete
r =
    Refss t Concrete
-> (Resp t :@ Concrete) -> Resp t (MockHandle t) (RealHandles t)
forall (f :: (* -> *) -> [*] -> *) t (r :: * -> *).
(NTraversable f, t ~ Test f, All Eq (RealHandles t), Eq1 r) =>
Refss t r -> (f :@ r) -> f (MockHandle t) (RealHandles t)
toMockHandles (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 (MockHandle t) (RealHandles t)
-> Resp t (MockHandle t) (RealHandles t) -> Logic
forall a. (Eq a, Show a) => a -> a -> Logic
.== Event t Concrete -> Resp t (MockHandle t) (RealHandles t)
forall t (r :: * -> *).
Event t r -> Resp t (MockHandle t) (RealHandles t)
mockResp Event t Concrete
e
  where
    e :: Event t Concrete
e = StateMachineTest t
-> Model t Concrete
-> (Cmd t :@ Concrete)
-> (Resp t :@ Concrete)
-> Event t Concrete
forall t (r :: * -> *).
Eq1 r =>
StateMachineTest t
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Event t r
lockstep StateMachineTest t
sm Model t Concrete
m Cmd t :@ Concrete
c Resp t :@ Concrete
r

symbolicResp :: StateMachineTest t
             -> Model t Symbolic
             -> Cmd t :@ Symbolic
             -> GenSym (Resp t :@ Symbolic)
symbolicResp :: StateMachineTest t
-> Model t Symbolic
-> (Cmd t :@ Symbolic)
-> GenSym (Resp t :@ Symbolic)
symbolicResp sm :: StateMachineTest t
sm@StateMachineTest{} Model t Symbolic
m Cmd t :@ Symbolic
c =
    Resp t (FlipRef Symbolic) (RealHandles t) -> Resp t :@ Symbolic
forall (f :: (* -> *) -> [*] -> *) (r :: * -> *).
f (FlipRef r) (RealHandles (Test f)) -> At f r
At (Resp t (FlipRef Symbolic) (RealHandles t) -> Resp t :@ Symbolic)
-> GenSym (Resp t (FlipRef Symbolic) (RealHandles t))
-> GenSym (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
    -> MockHandle t a -> GenSym (FlipRef Symbolic a))
-> Resp t (MockHandle 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)
nctraverse (Proxy Typeable
forall k (t :: k). Proxy t
Proxy @Typeable) (\Elem (RealHandles t) a
_ MockHandle 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 (MockHandle t) (RealHandles t)
resp
  where
    (Resp t (MockHandle t) (RealHandles t)
resp, MockState t
_mock') = StateMachineTest t
-> Model t Symbolic
-> (Cmd t :@ Symbolic)
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
forall (r :: * -> *) t.
Eq1 r =>
StateMachineTest t
-> Model t r
-> (Cmd t :@ r)
-> (Resp t (MockHandle t) (RealHandles t), MockState t)
step StateMachineTest t
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 :: 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 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 :: 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 -> Bool) -> [Reference a Symbolic] -> 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] -> Bool
forall a b. (a -> b) -> a -> b
$ ((Reference a Symbolic, MockHandle t a) -> Reference a Symbolic)
-> [(Reference a Symbolic, MockHandle t a)]
-> [Reference a Symbolic]
forall a b. (a -> b) -> [a] -> [b]
map (Reference a Symbolic, MockHandle t a) -> Reference a Symbolic
forall a b. (a, b) -> a
fst (Refs t Symbolic a -> [(Reference a Symbolic, MockHandle t a)]
forall t (r :: * -> *) a.
Refs t r a -> [(Reference a r, MockHandle 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))

    -- TODO: Patch QSM
    sameRef :: Reference a Symbolic -> Reference a Symbolic -> Bool
    sameRef :: 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
               -> StateMachine (Model t) (At (Cmd t)) (RealMonad t) (At (Resp t))
toStateMachine :: StateMachineTest t
-> StateMachine (Model t) (At (Cmd t)) (RealMonad t) (At (Resp t))
toStateMachine sm :: StateMachineTest t
sm@StateMachineTest{} = StateMachine :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(forall (r :: * -> *). model r)
-> (forall (r :: * -> *).
    (Show1 r, Ord1 r) =>
    model r -> cmd r -> resp r -> model r)
-> (model Symbolic -> cmd Symbolic -> Logic)
-> (model Concrete -> cmd Concrete -> resp Concrete -> Logic)
-> Maybe (model Concrete -> Logic)
-> (model Symbolic -> Maybe (Gen (cmd Symbolic)))
-> (model Symbolic -> cmd Symbolic -> [cmd Symbolic])
-> (cmd Concrete -> m (resp Concrete))
-> (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic))
-> (model Concrete -> m ())
-> StateMachine model cmd m resp
StateMachine {
      initModel :: forall (r :: * -> *). Model t r
initModel     = StateMachineTest t -> Model t r
forall t (r :: * -> *). StateMachineTest t -> Model t r
initModel     StateMachineTest t
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
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Model t r
forall (r :: * -> *) t.
Eq1 r =>
StateMachineTest t
-> Model t r -> (Cmd t :@ r) -> (Resp t :@ r) -> Model t r
transition    StateMachineTest t
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
-> Model t Concrete
-> At (Cmd t) Concrete
-> At (Resp t) Concrete
-> Logic
forall t.
StateMachineTest t
-> Model t Concrete
-> (Cmd t :@ Concrete)
-> (Resp t :@ Concrete)
-> Logic
postcondition StateMachineTest t
sm
    , generator :: Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
generator     = StateMachineTest t
-> Model t Symbolic -> Maybe (Gen (At (Cmd t) Symbolic))
forall t.
StateMachineTest t
-> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
generator     StateMachineTest t
sm
    , shrinker :: Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
shrinker      = StateMachineTest t
-> Model t Symbolic -> At (Cmd t) Symbolic -> [At (Cmd t) Symbolic]
forall t.
StateMachineTest t
-> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
shrinker      StateMachineTest t
sm
    , semantics :: At (Cmd t) Concrete -> RealMonad t (At (Resp t) Concrete)
semantics     = StateMachineTest t
-> At (Cmd t) Concrete -> RealMonad t (At (Resp t) Concrete)
forall t.
StateMachineTest t
-> (Cmd t :@ Concrete) -> RealMonad t (Resp t :@ Concrete)
semantics     StateMachineTest t
sm
    , mock :: Model t Symbolic
-> At (Cmd t) Symbolic -> GenSym (At (Resp t) Symbolic)
mock          = StateMachineTest t
-> Model t Symbolic
-> At (Cmd t) Symbolic
-> GenSym (At (Resp t) Symbolic)
forall t.
StateMachineTest t
-> Model t Symbolic
-> (Cmd t :@ Symbolic)
-> GenSym (Resp t :@ Symbolic)
symbolicResp  StateMachineTest t
sm
    , cleanup :: Model t Concrete -> RealMonad t ()
cleanup       = StateMachineTest t -> Model t Concrete -> RealMonad t ()
forall t. StateMachineTest t -> Model t Concrete -> RealMonad t ()
cleanup       StateMachineTest t
sm
    , invariant :: Maybe (Model t Concrete -> Logic)
invariant     = Maybe (Model t Concrete -> Logic)
forall a. Maybe a
Nothing
    }

prop_sequential :: RealMonad t ~ IO
                => StateMachineTest t
                -> Maybe Int   -- ^ (Optional) minimum number of commands
                -> Property
prop_sequential :: StateMachineTest t -> Maybe Int -> Property
prop_sequential sm :: StateMachineTest t
sm@StateMachineTest{} 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))
StateMachine (Model t) (At (Cmd t)) (RealMonad t) (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))
StateMachine (Model t) (At (Cmd t)) (RealMonad t) (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, ToExpr (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))
StateMachine (Model t) (At (Cmd t)) (RealMonad t) (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
$ Reason
res Reason -> Reason -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Reason
Ok
  where
    sm' :: StateMachine (Model t) (At (Cmd t)) (RealMonad t) (At (Resp t))
sm' = StateMachineTest t
-> StateMachine (Model t) (At (Cmd t)) (RealMonad t) (At (Resp t))
forall t.
StateMachineTest t
-> StateMachine (Model t) (At (Cmd t)) (RealMonad t) (At (Resp t))
toStateMachine StateMachineTest t
sm

prop_parallel :: RealMonad t ~ IO
              => StateMachineTest t
              -> Maybe Int   -- ^ (Optional) minimum number of commands
              -> Property
prop_parallel :: StateMachineTest t -> Maybe Int -> Property
prop_parallel sm :: StateMachineTest t
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))
StateMachine (Model t) (At (Cmd t)) (RealMonad t) (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
$
            ParallelCommands (At (Cmd t)) (At (Resp t))
-> [(History (At (Cmd t)) (At (Resp t)), Logic)] -> PropertyM IO ()
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (m :: * -> *).
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
 Foldable cmd) =>
ParallelCommands cmd resp
-> [(History cmd resp, Logic)] -> PropertyM m ()
prettyParallelCommands ParallelCommands (At (Cmd t)) (At (Resp t))
cmds
        ([(History (At (Cmd t)) (At (Resp t)), Logic)] -> PropertyM IO ())
-> PropertyM IO [(History (At (Cmd t)) (At (Resp t)), Logic)]
-> PropertyM IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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)), 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, Logic)]
runParallelCommands StateMachine (Model t) (At (Cmd t)) IO (At (Resp t))
StateMachine (Model t) (At (Cmd t)) (RealMonad t) (At (Resp t))
sm' ParallelCommands (At (Cmd t)) (At (Resp t))
cmds
  where
    sm' :: StateMachine (Model t) (At (Cmd t)) (RealMonad t) (At (Resp t))
sm' = StateMachineTest t
-> StateMachine (Model t) (At (Cmd t)) (RealMonad t) (At (Resp t))
forall t.
StateMachineTest t
-> StateMachine (Model t) (At (Cmd t)) (RealMonad t) (At (Resp t))
toStateMachine StateMachineTest t
sm

{-------------------------------------------------------------------------------
  Rank2 instances
-------------------------------------------------------------------------------}

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 a. p a -> q a) -> 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' :: 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
Rank2.fmap 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 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' :: FlipRef p a -> m
f' = (forall a. p a -> 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 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 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
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' :: FlipRef p a -> f (FlipRef q a)
f' = (Reference a q -> FlipRef q a)
-> f (Reference a q) -> f (FlipRef q a)
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)
Rank2.traverse 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 a. p a -> q a) -> 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' :: 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
Rank2.fmap 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 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' :: FlipRef p a -> m
f' = (forall a. p a -> 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 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 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
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' :: FlipRef p a -> f (FlipRef q a)
f' = (Reference a q -> FlipRef q a)
-> f (Reference a q) -> f (FlipRef q a)
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)
Rank2.traverse 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

{-------------------------------------------------------------------------------
  Auxiliary
-------------------------------------------------------------------------------}

(!) :: Eq k => [(k, a)] -> k -> a
[(k, a)]
env ! :: [(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 ([] :.: MockHandle t) (RealHandles t)
           -> Refss t r
zipHandles :: NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandle t) (RealHandles t) -> Refss t r
zipHandles = \NP ([] :.: FlipRef r) (RealHandles t)
real NP ([] :.: MockHandle 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 -> (:.:) [] (MockHandle t) a -> Refs t r a)
-> Prod NP ([] :.: FlipRef r) (RealHandles t)
-> NP ([] :.: MockHandle 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 forall a.
(:.:) [] (FlipRef r) a -> (:.:) [] (MockHandle t) a -> Refs t r a
forall (r :: * -> *) a t.
(:.:) [] (FlipRef r) a -> (:.:) [] (MockHandle t) a -> Refs t r a
zip' NP ([] :.: FlipRef r) (RealHandles t)
Prod NP ([] :.: FlipRef r) (RealHandles t)
real NP ([] :.: MockHandle t) (RealHandles t)
mock
  where
    zip' :: (:.:) [] (FlipRef r) a -> (:.:) [] (MockHandle t) a -> Refs t r a
    zip' :: (:.:) [] (FlipRef r) a -> (:.:) [] (MockHandle t) a -> Refs t r a
zip' (Comp [FlipRef r a]
real) (Comp [MockHandle t a]
mock) = [(Reference a r, MockHandle t a)] -> Refs t r a
forall t (r :: * -> *) a.
[(Reference a r, MockHandle t a)] -> Refs t r a
Refs ([(Reference a r, MockHandle t a)] -> Refs t r a)
-> [(Reference a r, MockHandle t a)] -> Refs t r a
forall a b. (a -> b) -> a -> b
$ [Reference a r]
-> [MockHandle t a] -> [(Reference a r, MockHandle 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) [MockHandle t a]
mock