{-# LANGUAGE UndecidableInstances #-}

-- | Generalized variables
--
-- Intended for unqualified import.
module Test.QuickCheck.StateModel.Lockstep.GVar (
    GVar -- opaque
  , AnyGVar(..)
    -- * Construction
  , unsafeMkGVar
  , fromVar
  , mapGVar
    -- * Interop with 'Env'
  , lookUpGVar
    -- * Interop with 'EnvF'
  , 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

{-------------------------------------------------------------------------------
  Main type
-------------------------------------------------------------------------------}

-- | Generalized variables
--
-- The key difference between 'GVar' and the standard 'Var' type is that
-- 'GVar' have a functor-esque structure: see 'map'.
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

{-------------------------------------------------------------------------------
  Construction
-------------------------------------------------------------------------------}

-- | Only for pretty-printing counter-examples, do not use directly
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)

{-------------------------------------------------------------------------------
  Interop with 'Env'
-------------------------------------------------------------------------------}

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)

-- | Lookup 'GVar' given a lookup function for 'Var'
--
-- The variable must be in the environment and evaluation must succeed.
-- This is normally guaranteed by the default test 'precondition'.
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)

{-------------------------------------------------------------------------------
  Interop with EnvF
-------------------------------------------------------------------------------}

-- | Lookup 'GVar'
--
-- The variable must be in the environment and evaluation must succeed.
-- This is normally guaranteed by the default test 'precondition'.
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

-- | Check if the variable is well-defined and evaluation will succeed.
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