{-# LANGUAGE UndecidableInstances #-}
module Test.QuickCheck.StateModel.Lockstep.GVar (
GVar
, AnyGVar(..)
, fromVar
, mapGVar
, lookUpGVar
, lookUpEnvF
, definedInEnvF
) where
import Prelude hiding (map)
import Data.Maybe (isJust, fromJust)
import Data.Typeable
import Test.QuickCheck.StateModel (Var(..), LookUp, Realized)
import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)
import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF
import Test.QuickCheck.StateModel.Lockstep.Op
data GVar op f where
GVar :: Typeable x => Var x -> op x y -> GVar op y
data AnyGVar op where
SomeGVar :: GVar op y -> AnyGVar op
deriving instance (forall x. Show (op x a)) => Show (GVar op a)
instance (forall x. Eq (op x a)) => Eq (GVar op a) where
== :: GVar op a -> GVar op a -> Bool
(==) = \(GVar Var x
x op x a
op) (GVar Var x
x' op x a
op') -> forall x x'.
(Typeable x, Typeable x') =>
Var x -> Var x' -> op x a -> op x' a -> Bool
aux Var x
x Var x
x' op x a
op op x a
op'
where
aux :: forall x x'.
(Typeable x, Typeable x')
=> Var x -> Var x' -> op x a -> op x' a -> Bool
aux :: forall x x'.
(Typeable x, Typeable x') =>
Var x -> Var x' -> op x a -> op x' a -> Bool
aux Var x
x Var x'
x' op x a
op op x' a
op' =
case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @x @x' of
Maybe (x :~: x')
Nothing -> Bool
False
Just x :~: x'
Refl -> (Var x
x, op x a
op) forall a. Eq a => a -> a -> Bool
== (Var x'
x', op x' a
op')
fromVar :: (Operation op, Typeable a) => Var a -> GVar op a
fromVar :: forall (op :: * -> * -> *) a.
(Operation op, Typeable a) =>
Var a -> GVar op a
fromVar Var a
var = forall x (op :: * -> * -> *) y.
Typeable x =>
Var x -> op x y -> GVar op y
GVar Var a
var forall (op :: * -> * -> *) a. Operation op => op a a
opIdentity
mapGVar :: (forall x. op x a -> op x b) -> GVar op a -> GVar op b
mapGVar :: forall (op :: * -> * -> *) a b.
(forall x. op x a -> op x b) -> GVar op a -> GVar op b
mapGVar forall x. op x a -> op x b
f (GVar Var x
var op x a
op) = forall x (op :: * -> * -> *) y.
Typeable x =>
Var x -> op x y -> GVar op y
GVar Var x
var (forall x. op x a -> op x b
f op x a
op)
lookUpWrapped :: Typeable a => Proxy m -> LookUp m -> Var a -> WrapRealized m a
lookUpWrapped :: forall a (m :: * -> *).
Typeable a =>
Proxy m -> LookUp m -> Var a -> WrapRealized m a
lookUpWrapped Proxy m
_ LookUp m
m Var a
v = forall (m :: * -> *) a. Realized m a -> WrapRealized m a
WrapRealized (LookUp m
m Var a
v)
lookUpGVar ::
InterpretOp op (WrapRealized m)
=> Proxy m -> LookUp m -> GVar op a -> Realized m a
lookUpGVar :: forall (op :: * -> * -> *) (m :: * -> *) a.
InterpretOp op (WrapRealized m) =>
Proxy m -> LookUp m -> GVar op a -> Realized m a
lookUpGVar Proxy m
p LookUp m
lookUp (GVar Var x
var op x a
op) =
forall (m :: * -> *) a. WrapRealized m a -> Realized m a
unwrapRealized forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall (op :: * -> * -> *) (f :: * -> *) a b.
InterpretOp op f =>
op a b -> f a -> Maybe (f b)
intOp op x a
op (forall a (m :: * -> *).
Typeable a =>
Proxy m -> LookUp m -> Var a -> WrapRealized m a
lookUpWrapped Proxy m
p LookUp m
lookUp Var x
var)
lookUpEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> f a
lookUpEnvF :: forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> f a
lookUpEnvF EnvF f
env (GVar Var x
var op x a
op) = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) a.
(Typeable f, Typeable a) =>
Var a -> EnvF f -> Maybe (f a)
EnvF.lookup Var x
var EnvF f
env forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (op :: * -> * -> *) (f :: * -> *) a b.
InterpretOp op f =>
op a b -> f a -> Maybe (f b)
intOp op x a
op
definedInEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> Bool
definedInEnvF :: forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> Bool
definedInEnvF EnvF f
env (GVar Var x
var op x a
op) = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) a.
(Typeable f, Typeable a) =>
Var a -> EnvF f -> Maybe (f a)
EnvF.lookup Var x
var EnvF f
env forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (op :: * -> * -> *) (f :: * -> *) a b.
InterpretOp op f =>
op a b -> f a -> Maybe (f b)
intOp op x a
op