{-# LANGUAGE UndecidableInstances #-}
module Test.QuickCheck.StateModel.Lockstep.GVar (
GVar
, AnyGVar(..)
, unsafeMkGVar
, fromVar
, mapGVar
, lookUpGVar
, lookUpEnvF
, definedInEnvF
) where
import Prelude hiding (map)
import Data.Maybe (isJust, fromJust)
import Data.Typeable
import GHC.Show
import Test.QuickCheck.StateModel (Var, LookUp, Realized, HasVariables (..))
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
instance (forall x. Show (op x a)) => Show (GVar op a) where
showsPrec :: Int -> GVar op a -> ShowS
showsPrec Int
n (GVar Var x
v op x a
op) =
Bool -> ShowS -> ShowS
showParen (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"unsafeMkGVar "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Var x -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Var x
v
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
showSpace
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> op x a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 op x a
op
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') -> Var x -> Var x -> op x a -> op x a -> Bool
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)
forall a b. (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) (Var x, op x a) -> (Var x, op x a) -> Bool
forall a. Eq a => a -> a -> Bool
== (Var x
Var x'
x', op x a
op x' a
op')
instance HasVariables (GVar op f) where
getAllVariables :: GVar op f -> Set (Any Var)
getAllVariables (GVar Var x
v op x f
_) = Var x -> Set (Any Var)
forall a. HasVariables a => a -> Set (Any Var)
getAllVariables Var x
v
instance HasVariables (AnyGVar op) where
getAllVariables :: AnyGVar op -> Set (Any Var)
getAllVariables (SomeGVar GVar op y
v) = GVar op y -> Set (Any Var)
forall a. HasVariables a => a -> Set (Any Var)
getAllVariables GVar op y
v
unsafeMkGVar :: Typeable a => Var a -> op a b -> GVar op b
unsafeMkGVar :: forall a (op :: * -> * -> *) b.
Typeable a =>
Var a -> op a b -> GVar op b
unsafeMkGVar = Var a -> op a b -> GVar op b
forall a (op :: * -> * -> *) b.
Typeable a =>
Var a -> op a b -> GVar op b
GVar
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 = Var a -> op a a -> GVar op a
forall a (op :: * -> * -> *) b.
Typeable a =>
Var a -> op a b -> GVar op b
GVar Var a
var op a a
forall a. op a a
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) = Var x -> op x b -> GVar op b
forall a (op :: * -> * -> *) b.
Typeable a =>
Var a -> op a b -> GVar op b
GVar Var x
var (op x a -> op x b
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 = Realized m a -> WrapRealized m a
forall (m :: * -> *) a. Realized m a -> WrapRealized m a
WrapRealized (Var a -> Realized m a
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) =
WrapRealized m a -> Realized m a
forall (m :: * -> *) a. WrapRealized m a -> Realized m a
unwrapRealized (WrapRealized m a -> Realized m a)
-> WrapRealized m a -> Realized m a
forall a b. (a -> b) -> a -> b
$ Maybe (WrapRealized m a) -> WrapRealized m a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (WrapRealized m a) -> WrapRealized m a)
-> Maybe (WrapRealized m a) -> WrapRealized m a
forall a b. (a -> b) -> a -> b
$ op x a -> WrapRealized m x -> Maybe (WrapRealized m a)
forall a b. op a b -> WrapRealized m a -> Maybe (WrapRealized m b)
forall (op :: * -> * -> *) (f :: * -> *) a b.
InterpretOp op f =>
op a b -> f a -> Maybe (f b)
intOp op x a
op (Proxy m -> LookUp m -> Var x -> WrapRealized m x
forall a (m :: * -> *).
Typeable a =>
Proxy m -> LookUp m -> Var a -> WrapRealized m a
lookUpWrapped Proxy m
p Var a -> Realized m a
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) = Maybe (f a) -> f a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (f a) -> f a) -> Maybe (f a) -> f a
forall a b. (a -> b) -> a -> b
$
Var x -> EnvF f -> Maybe (f x)
forall (f :: * -> *) a.
(Typeable f, Typeable a) =>
Var a -> EnvF f -> Maybe (f a)
EnvF.lookup Var x
var EnvF f
env Maybe (f x) -> (f x -> Maybe (f a)) -> Maybe (f a)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= op x a -> f x -> Maybe (f a)
forall a b. op a b -> f a -> Maybe (f 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) = Maybe (f a) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (f a) -> Bool) -> Maybe (f a) -> Bool
forall a b. (a -> b) -> a -> b
$
Var x -> EnvF f -> Maybe (f x)
forall (f :: * -> *) a.
(Typeable f, Typeable a) =>
Var a -> EnvF f -> Maybe (f a)
EnvF.lookup Var x
var EnvF f
env Maybe (f x) -> (f x -> Maybe (f a)) -> Maybe (f a)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= op x a -> f x -> Maybe (f a)
forall a b. op a b -> f a -> Maybe (f b)
forall (op :: * -> * -> *) (f :: * -> *) a b.
InterpretOp op f =>
op a b -> f a -> Maybe (f b)
intOp op x a
op