{-# LANGUAGE UndecidableInstances #-}

-- | Generalized variables
--
-- Intended for unqualified import.
module Test.QuickCheck.StateModel.Lockstep.GVar (
    GVar -- opaque
  , AnyGVar(..)
    -- * Construction
  , 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 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

{-------------------------------------------------------------------------------
  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

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')

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

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)

{-------------------------------------------------------------------------------
  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 = forall (m :: * -> *) a. Realized m a -> WrapRealized m a
WrapRealized (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) =
    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)

{-------------------------------------------------------------------------------
  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) = 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

-- | 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) = 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