{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# 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
  , shrinkGVar
    -- * Internal: exposed for testing
  , pattern GVar
  ) where

import           Prelude hiding (map)

import           Control.Monad.Identity (Identity (..))

import           Data.Maybe (isJust)
import           Data.Typeable

import           GHC.Show

import           Test.QuickCheck.StateModel (HasVariables (..), LookUp, Var)

import qualified Test.QuickCheck.StateModel.Lockstep.EnvF as EnvF
import           Test.QuickCheck.StateModel.Lockstep.EnvF (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 'mapGVar'.
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 {k} a (op :: * -> k -> *) (b :: k).
Typeable a =>
Var a -> op a b -> GVar op b
unsafeMkGVar = Var a -> op a b -> GVar op b
forall {k} a (op :: * -> k -> *) (b :: k).
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 {k} a (op :: * -> k -> *) (b :: k).
Typeable a =>
Var a -> op a b -> GVar op b
GVar Var a
var op a a
forall a. op a a
forall {k} (op :: k -> k -> *) (a :: k). Operation op => op a a
opIdentity

mapGVar :: (forall x. op x a -> op x b) -> GVar op a -> GVar op b
mapGVar :: forall {k} (op :: * -> k -> *) (a :: k) (b :: k).
(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 {k} a (op :: * -> k -> *) (b :: k).
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 => LookUp -> Var a -> Identity a
lookUpWrapped :: forall a. Typeable a => LookUp -> Var a -> Identity a
lookUpWrapped LookUp
m Var a
v = a -> Identity a
forall a. a -> Identity a
Identity (Var a -> a
LookUp
m Var a
v)

-- | Lookup 'GVar' given a lookup function for 'Var'
--
-- The result is 'Just' if the variable is in the environment and evaluation
-- succeeds. This is normally guaranteed by the default test 'precondition'.
lookUpGVar ::
     InterpretOp op Identity
  => LookUp -> GVar op a -> Maybe a
lookUpGVar :: forall (op :: * -> * -> *) a.
InterpretOp op Identity =>
LookUp -> GVar op a -> Maybe a
lookUpGVar LookUp
lookUp (GVar Var x
var op x a
op) =
    Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Maybe (Identity a) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> op x a -> Identity x -> Maybe (Identity a)
forall a b. op a b -> Identity a -> Maybe (Identity b)
forall {k} (op :: k -> k -> *) (f :: k -> *) (a :: k) (b :: k).
InterpretOp op f =>
op a b -> f a -> Maybe (f b)
intOp op x a
op (LookUp -> Var x -> Identity x
forall a. Typeable a => LookUp -> Var a -> Identity a
lookUpWrapped Var a -> a
LookUp
lookUp Var x
var)

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

-- | Lookup 'GVar'
--
-- The result is 'Just' if the variable is in the environment and evaluation
-- succeeds. This is normally guaranteed by the default test 'precondition'.
lookUpEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> Maybe (f a)
lookUpEnvF :: forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> Maybe (f a)
lookUpEnvF EnvF f
env (GVar Var x
var op x a
op) =
    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 {k} (op :: k -> k -> *) (f :: k -> *) (a :: k) (b :: k).
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 op a
gvar = Maybe (f a) -> Bool
forall a. Maybe a -> Bool
isJust (EnvF f -> GVar op a -> Maybe (f a)
forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> Maybe (f a)
lookUpEnvF EnvF f
env GVar op a
gvar)

-- | Shrink a 'GVar' to earlier 'GVar's of the same type. It is guaranteed that
-- the shrunk variables are in the environment and that evaluation will succeed.
shrinkGVar :: (Typeable f, InterpretOp op f)  => EnvF f -> GVar op a -> [GVar op a]
shrinkGVar :: forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> [GVar op a]
shrinkGVar EnvF f
env (GVar Var x
var op x a
op) =
    [ GVar op a
gvar'
    | Var x
var' <- EnvF f -> Var x -> [Var x]
forall a (f :: * -> *). Typeable a => EnvF f -> Var a -> [Var a]
EnvF.shrinkVar EnvF f
env Var x
var
    , let gvar' :: GVar op a
gvar' = Var x -> op x a -> GVar op a
forall {k} a (op :: * -> k -> *) (b :: k).
Typeable a =>
Var a -> op a b -> GVar op b
GVar Var x
var' op x a
op
    , EnvF f -> GVar op a -> Bool
forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> Bool
definedInEnvF EnvF f
env GVar op a
gvar'
    ]