-- |
-- 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.Backend.Monad( PPOpts )

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 (SEval sym (GenValue sym))
envVars       :: !(IntMap.IntMap (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 (SEval sym (GenValue sym)) -> TypeEnv -> GenEvalEnv sym
EvalEnv
    { envVars :: IntMap (SEval sym (GenValue sym))
envVars     = IntMap (SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union (GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
forall sym. GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
envVars GenEvalEnv sym
l) (GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
forall sym. GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
envVars GenEvalEnv sym
r)
    , envTypes :: TypeEnv
envTypes    = TypeEnv -> TypeEnv -> TypeEnv
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union (GenEvalEnv sym -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
envTypes GenEvalEnv sym
l) (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 (SEval sym (GenValue sym)) -> TypeEnv -> GenEvalEnv sym
EvalEnv
    { envVars :: IntMap (SEval sym (GenValue sym))
envVars       = IntMap (SEval sym (GenValue sym))
forall a. IntMap a
IntMap.empty
    , envTypes :: TypeEnv
envTypes      = TypeEnv
forall a. IntMap a
IntMap.empty
    }

  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, SEval sym (GenValue sym)) -> SEval sym Doc)
-> [(Key, 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, SEval sym (GenValue sym)) -> SEval sym Doc
bind (IntMap (SEval sym (GenValue sym))
-> [(Key, SEval sym (GenValue sym))]
forall a. IntMap a -> [(Key, a)]
IntMap.toList (GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
forall sym. GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
envVars GenEvalEnv sym
env))
  where
   bind :: (Key, SEval sym (GenValue sym)) -> SEval sym Doc
bind (Key
k,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
-> Maybe String
-> SEval sym (GenValue sym)
-> SEval sym (SEval sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Maybe String -> SEval sym a -> SEval sym (SEval sym a)
sDelay sym
sym (String -> Maybe String
forall a. a -> Maybe a
Just String
nm) SEval sym (GenValue sym)
val
  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 (SEval sym (GenValue sym))
envVars = Key
-> SEval sym (GenValue sym)
-> IntMap (SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert (Name -> Key
nameUnique Name
n) SEval sym (GenValue sym)
val' (GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
forall sym. GenEvalEnv sym -> IntMap (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 ->
  GenValue sym ->
  GenEvalEnv sym ->
  GenEvalEnv sym
bindVarDirect :: Name -> GenValue sym -> GenEvalEnv sym -> GenEvalEnv sym
bindVarDirect Name
n GenValue sym
val GenEvalEnv sym
env = do
  GenEvalEnv sym
env{ envVars :: IntMap (SEval sym (GenValue sym))
envVars = Key
-> SEval sym (GenValue sym)
-> IntMap (SEval sym (GenValue sym))
-> IntMap (SEval sym (GenValue sym))
forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert (Name -> Key
nameUnique Name
n) (GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
val) (GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
forall sym. GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
envVars GenEvalEnv sym
env) }

-- | Lookup a variable in the environment.
{-# INLINE lookupVar #-}
lookupVar :: Name -> GenEvalEnv sym -> Maybe (SEval sym (GenValue sym))
lookupVar :: Name -> GenEvalEnv sym -> Maybe (SEval sym (GenValue sym))
lookupVar Name
n GenEvalEnv sym
env = Key
-> IntMap (SEval sym (GenValue sym))
-> Maybe (SEval sym (GenValue sym))
forall a. Key -> IntMap a -> Maybe a
IntMap.lookup (Name -> Key
nameUnique Name
n) (GenEvalEnv sym -> IntMap (SEval sym (GenValue sym))
forall sym. GenEvalEnv sym -> IntMap (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 = Key -> Either Nat' TValue -> TypeEnv -> TypeEnv
forall a. Key -> a -> IntMap a -> IntMap a
IntMap.insert (TVar -> Key
tvUnique 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 = Key -> TypeEnv -> Maybe (Either Nat' TValue)
forall a. Key -> IntMap a -> Maybe a
IntMap.lookup (TVar -> Key
tvUnique TVar
p) (GenEvalEnv sym -> TypeEnv
forall sym. GenEvalEnv sym -> TypeEnv
envTypes GenEvalEnv sym
env)