-- |
-- Module      :  Cryptol.Eval.Env
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE Safe #-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.Eval.Env where

import Cryptol.Backend

import Cryptol.Eval.Prims
import Cryptol.Eval.Type
import Cryptol.Eval.Value
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat
import Cryptol.Utils.PP

import qualified Data.IntMap.Strict as IntMap
import Data.Semigroup

import GHC.Generics (Generic)

import Prelude ()
import Prelude.Compat

-- Evaluation Environment ------------------------------------------------------

data GenEvalEnv sym = EvalEnv
  { GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars       :: !(IntMap.IntMap (Either (Prim sym) (SEval sym (GenValue sym))))
  , GenEvalEnv sym -> TypeEnv
envTypes      :: !TypeEnv
  } deriving (forall x. GenEvalEnv sym -> Rep (GenEvalEnv sym) x)
-> (forall x. Rep (GenEvalEnv sym) x -> GenEvalEnv sym)
-> Generic (GenEvalEnv sym)
forall x. Rep (GenEvalEnv sym) x -> GenEvalEnv sym
forall x. GenEvalEnv sym -> Rep (GenEvalEnv sym) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall sym x. Rep (GenEvalEnv sym) x -> GenEvalEnv sym
forall sym x. GenEvalEnv sym -> Rep (GenEvalEnv sym) x
$cto :: forall sym x. Rep (GenEvalEnv sym) x -> GenEvalEnv sym
$cfrom :: forall sym x. GenEvalEnv sym -> Rep (GenEvalEnv sym) x
Generic

instance Semigroup (GenEvalEnv sym) where
  GenEvalEnv sym
l <> :: GenEvalEnv sym -> GenEvalEnv sym -> GenEvalEnv sym
<> GenEvalEnv sym
r = EvalEnv :: forall sym.
IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> TypeEnv -> GenEvalEnv sym
EvalEnv
    { envVars :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars     = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union (GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall sym.
GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars GenEvalEnv sym
l) (GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall sym.
GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars GenEvalEnv sym
r)
    , envTypes :: TypeEnv
envTypes    = GenEvalEnv sym -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
envTypes GenEvalEnv sym
l TypeEnv -> TypeEnv -> TypeEnv
forall a. Semigroup a => a -> a -> a
<> GenEvalEnv sym -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
envTypes GenEvalEnv sym
r
    }

instance Monoid (GenEvalEnv sym) where
  mempty :: GenEvalEnv sym
mempty = EvalEnv :: forall sym.
IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> TypeEnv -> GenEvalEnv sym
EvalEnv
    { envVars :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars       = IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall a. IntMap a
IntMap.empty
    , envTypes :: TypeEnv
envTypes      = TypeEnv
forall a. Monoid a => a
mempty
    }
  mappend :: GenEvalEnv sym -> GenEvalEnv sym -> GenEvalEnv sym
mappend GenEvalEnv sym
l GenEvalEnv sym
r = GenEvalEnv sym
l GenEvalEnv sym -> GenEvalEnv sym -> GenEvalEnv sym
forall a. Semigroup a => a -> a -> a
<> GenEvalEnv sym
r

ppEnv :: Backend sym => sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc
ppEnv :: sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc
ppEnv sym
sym PPOpts
opts GenEvalEnv sym
env = Doc -> Doc
brackets (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep ([Doc] -> Doc) -> SEval sym [Doc] -> SEval sym Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Key, Either (Prim sym) (SEval sym (GenValue sym)))
 -> SEval sym Doc)
-> [(Key, Either (Prim sym) (SEval sym (GenValue sym)))]
-> SEval sym [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Key, Either (Prim sym) (SEval sym (GenValue sym)))
-> SEval sym Doc
forall a.
(Key, Either a (SEval sym (GenValue sym))) -> SEval sym Doc
bind (IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> [(Key, Either (Prim sym) (SEval sym (GenValue sym)))]
forall a. IntMap a -> [(Key, a)]
IntMap.toList (GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall sym.
GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars GenEvalEnv sym
env))
  where
   bind :: (Key, Either a (SEval sym (GenValue sym))) -> SEval sym Doc
bind (Key
k,Left a
_) =
      do Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Key -> Doc
int Key
k Doc -> Doc -> Doc
<+> String -> Doc
text String
"<<prim>>")
   bind (Key
k,Right SEval sym (GenValue sym)
v) =
      do Doc
vdoc <- sym -> PPOpts -> GenValue sym -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue sym
sym PPOpts
opts (GenValue sym -> SEval sym Doc)
-> SEval sym (GenValue sym) -> SEval sym Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
v
         Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Key -> Doc
int Key
k Doc -> Doc -> Doc
<+> String -> Doc
text String
"->" Doc -> Doc -> Doc
<+> Doc
vdoc)

-- | Evaluation environment with no bindings
emptyEnv :: GenEvalEnv sym
emptyEnv :: GenEvalEnv sym
emptyEnv  = GenEvalEnv sym
forall a. Monoid a => a
mempty

-- | Bind a variable in the evaluation environment.
bindVar ::
  Backend sym =>
  sym ->
  Name ->
  SEval sym (GenValue sym) ->
  GenEvalEnv sym ->
  SEval sym (GenEvalEnv sym)
bindVar :: sym
-> Name
-> SEval sym (GenValue sym)
-> GenEvalEnv sym
-> SEval sym (GenEvalEnv sym)
bindVar sym
sym Name
n SEval sym (GenValue sym)
val GenEvalEnv sym
env = do
  let nm :: String
nm = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Name -> Doc
ppLocName Name
n
  SEval sym (GenValue sym)
val' <- sym
-> SEval sym (GenValue sym)
-> Maybe (SEval sym (GenValue sym))
-> String
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym
-> SEval sym a
-> Maybe (SEval sym a)
-> String
-> SEval sym (SEval sym a)
sDelayFill sym
sym SEval sym (GenValue sym)
val Maybe (SEval sym (GenValue sym))
forall a. Maybe a
Nothing String
nm
  GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenEvalEnv sym -> SEval sym (GenEvalEnv sym))
-> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
forall a b. (a -> b) -> a -> b
$ GenEvalEnv sym
env{ envVars :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars = Key
-> Either (Prim sym) (SEval sym (GenValue sym))
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert (Name -> Key
nameUnique Name
n) (SEval sym (GenValue sym)
-> Either (Prim sym) (SEval sym (GenValue sym))
forall a b. b -> Either a b
Right SEval sym (GenValue sym)
val') (GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall sym.
GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars GenEvalEnv sym
env) }

-- | Bind a variable to a value in the evaluation environment, without
--   creating a thunk.
bindVarDirect ::
  Backend sym =>
  Name ->
  Prim sym ->
  GenEvalEnv sym ->
  GenEvalEnv sym
bindVarDirect :: Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
bindVarDirect Name
n Prim sym
val GenEvalEnv sym
env = do
  GenEvalEnv sym
env{ envVars :: IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars = Key
-> Either (Prim sym) (SEval sym (GenValue sym))
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert (Name -> Key
nameUnique Name
n) (Prim sym -> Either (Prim sym) (SEval sym (GenValue sym))
forall a b. a -> Either a b
Left Prim sym
val) (GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall sym.
GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars GenEvalEnv sym
env) }

-- | Lookup a variable in the environment.
{-# INLINE lookupVar #-}
lookupVar :: Name -> GenEvalEnv sym -> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
lookupVar :: Name
-> GenEvalEnv sym
-> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
lookupVar Name
n GenEvalEnv sym
env = Key
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
-> Maybe (Either (Prim sym) (SEval sym (GenValue sym)))
forall a. Key -> IntMap a -> Maybe a
IntMap.lookup (Name -> Key
nameUnique Name
n) (GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
forall sym.
GenEvalEnv sym
-> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
envVars GenEvalEnv sym
env)

-- | Bind a type variable of kind *.
{-# INLINE bindType #-}
bindType :: TVar -> Either Nat' TValue -> GenEvalEnv sym -> GenEvalEnv sym
bindType :: TVar -> Either Nat' TValue -> GenEvalEnv sym -> GenEvalEnv sym
bindType TVar
p Either Nat' TValue
ty GenEvalEnv sym
env = GenEvalEnv sym
env{ envTypes :: TypeEnv
envTypes = TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
bindTypeVar TVar
p Either Nat' TValue
ty (GenEvalEnv sym -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
envTypes GenEvalEnv sym
env) }

-- | Lookup a type variable.
{-# INLINE lookupType #-}
lookupType :: TVar -> GenEvalEnv sym -> Maybe (Either Nat' TValue)
lookupType :: TVar -> GenEvalEnv sym -> Maybe (Either Nat' TValue)
lookupType TVar
p GenEvalEnv sym
env = TVar -> TypeEnv -> Maybe (Either Nat' TValue)
lookupTypeVar TVar
p (GenEvalEnv sym -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
envTypes GenEvalEnv sym
env)