{-# LANGUAGE Safe #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.Eval.Env where
import Cryptol.Eval.Monad( Eval, delay, ready, 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.Map.Strict as Map
import Data.Semigroup
import GHC.Generics (Generic)
import Control.DeepSeq
import Prelude ()
import Prelude.Compat
data GenEvalEnv b w i = EvalEnv
{ GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
envVars :: !(Map.Map Name (Eval (GenValue b w i)))
, GenEvalEnv b w i -> TypeEnv
envTypes :: !TypeEnv
} deriving ((forall x. GenEvalEnv b w i -> Rep (GenEvalEnv b w i) x)
-> (forall x. Rep (GenEvalEnv b w i) x -> GenEvalEnv b w i)
-> Generic (GenEvalEnv b w i)
forall x. Rep (GenEvalEnv b w i) x -> GenEvalEnv b w i
forall x. GenEvalEnv b w i -> Rep (GenEvalEnv b w i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall b w i x. Rep (GenEvalEnv b w i) x -> GenEvalEnv b w i
forall b w i x. GenEvalEnv b w i -> Rep (GenEvalEnv b w i) x
$cto :: forall b w i x. Rep (GenEvalEnv b w i) x -> GenEvalEnv b w i
$cfrom :: forall b w i x. GenEvalEnv b w i -> Rep (GenEvalEnv b w i) x
Generic, GenEvalEnv b w i -> ()
(GenEvalEnv b w i -> ()) -> NFData (GenEvalEnv b w i)
forall a. (a -> ()) -> NFData a
forall b w i.
(NFData b, NFData i, NFData w) =>
GenEvalEnv b w i -> ()
rnf :: GenEvalEnv b w i -> ()
$crnf :: forall b w i.
(NFData b, NFData i, NFData w) =>
GenEvalEnv b w i -> ()
NFData)
instance Semigroup (GenEvalEnv b w i) where
l :: GenEvalEnv b w i
l <> :: GenEvalEnv b w i -> GenEvalEnv b w i -> GenEvalEnv b w i
<> r :: GenEvalEnv b w i
r = $WEvalEnv :: forall b w i.
Map Name (Eval (GenValue b w i)) -> TypeEnv -> GenEvalEnv b w i
EvalEnv
{ envVars :: Map Name (Eval (GenValue b w i))
envVars = Map Name (Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
forall b w i. GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
envVars GenEvalEnv b w i
l) (GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
forall b w i. GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
envVars GenEvalEnv b w i
r)
, envTypes :: TypeEnv
envTypes = TypeEnv -> TypeEnv -> TypeEnv
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
l) (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
r)
}
instance Monoid (GenEvalEnv b w i) where
mempty :: GenEvalEnv b w i
mempty = $WEvalEnv :: forall b w i.
Map Name (Eval (GenValue b w i)) -> TypeEnv -> GenEvalEnv b w i
EvalEnv
{ envVars :: Map Name (Eval (GenValue b w i))
envVars = Map Name (Eval (GenValue b w i))
forall k a. Map k a
Map.empty
, envTypes :: TypeEnv
envTypes = TypeEnv
forall k a. Map k a
Map.empty
}
mappend :: GenEvalEnv b w i -> GenEvalEnv b w i -> GenEvalEnv b w i
mappend l :: GenEvalEnv b w i
l r :: GenEvalEnv b w i
r = GenEvalEnv b w i
l GenEvalEnv b w i -> GenEvalEnv b w i -> GenEvalEnv b w i
forall a. Semigroup a => a -> a -> a
<> GenEvalEnv b w i
r
ppEnv :: BitWord b w i => PPOpts -> GenEvalEnv b w i -> Eval Doc
ppEnv :: PPOpts -> GenEvalEnv b w i -> Eval Doc
ppEnv opts :: PPOpts
opts env :: GenEvalEnv b w i
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) -> Eval [Doc] -> Eval Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Name, Eval (GenValue b w i)) -> Eval Doc)
-> [(Name, Eval (GenValue b w i))] -> Eval [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, Eval (GenValue b w i)) -> Eval Doc
forall b w i a.
(BitWord b w i, PP a) =>
(a, Eval (GenValue b w i)) -> Eval Doc
bind (Map Name (Eval (GenValue b w i)) -> [(Name, Eval (GenValue b w i))]
forall k a. Map k a -> [(k, a)]
Map.toList (GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
forall b w i. GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
envVars GenEvalEnv b w i
env))
where
bind :: (a, Eval (GenValue b w i)) -> Eval Doc
bind (k :: a
k,v :: Eval (GenValue b w i)
v) = do Doc
vdoc <- PPOpts -> GenValue b w i -> Eval Doc
forall b w i. BitWord b w i => PPOpts -> GenValue b w i -> Eval Doc
ppValue PPOpts
opts (GenValue b w i -> Eval Doc) -> Eval (GenValue b w i) -> Eval Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (GenValue b w i)
v
Doc -> Eval Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Doc
forall a. PP a => a -> Doc
pp a
k Doc -> Doc -> Doc
<+> String -> Doc
text "->" Doc -> Doc -> Doc
<+> Doc
vdoc)
emptyEnv :: GenEvalEnv b w i
emptyEnv :: GenEvalEnv b w i
emptyEnv = GenEvalEnv b w i
forall a. Monoid a => a
mempty
bindVar :: Name
-> Eval (GenValue b w i)
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
bindVar :: Name
-> Eval (GenValue b w i)
-> GenEvalEnv b w i
-> Eval (GenEvalEnv b w i)
bindVar n :: Name
n val :: Eval (GenValue b w i)
val env :: GenEvalEnv b w i
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
Eval (GenValue b w i)
val' <- Maybe String
-> Eval (GenValue b w i) -> Eval (Eval (GenValue b w i))
forall a. Maybe String -> Eval a -> Eval (Eval a)
delay (String -> Maybe String
forall a. a -> Maybe a
Just String
nm) Eval (GenValue b w i)
val
GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenEvalEnv b w i -> Eval (GenEvalEnv b w i))
-> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
forall a b. (a -> b) -> a -> b
$ GenEvalEnv b w i
env{ envVars :: Map Name (Eval (GenValue b w i))
envVars = Name
-> Eval (GenValue b w i)
-> Map Name (Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n Eval (GenValue b w i)
val' (GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
forall b w i. GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
envVars GenEvalEnv b w i
env) }
bindVarDirect :: Name
-> GenValue b w i
-> GenEvalEnv b w i
-> GenEvalEnv b w i
bindVarDirect :: Name -> GenValue b w i -> GenEvalEnv b w i -> GenEvalEnv b w i
bindVarDirect n :: Name
n val :: GenValue b w i
val env :: GenEvalEnv b w i
env = do
GenEvalEnv b w i
env{ envVars :: Map Name (Eval (GenValue b w i))
envVars = Name
-> Eval (GenValue b w i)
-> Map Name (Eval (GenValue b w i))
-> Map Name (Eval (GenValue b w i))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n (GenValue b w i -> Eval (GenValue b w i)
forall a. a -> Eval a
ready GenValue b w i
val) (GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
forall b w i. GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
envVars GenEvalEnv b w i
env) }
{-# INLINE lookupVar #-}
lookupVar :: Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
lookupVar :: Name -> GenEvalEnv b w i -> Maybe (Eval (GenValue b w i))
lookupVar n :: Name
n env :: GenEvalEnv b w i
env = Name
-> Map Name (Eval (GenValue b w i))
-> Maybe (Eval (GenValue b w i))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n (GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
forall b w i. GenEvalEnv b w i -> Map Name (Eval (GenValue b w i))
envVars GenEvalEnv b w i
env)
{-# INLINE bindType #-}
bindType :: TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
bindType :: TVar -> Either Nat' TValue -> GenEvalEnv b w i -> GenEvalEnv b w i
bindType p :: TVar
p ty :: Either Nat' TValue
ty env :: GenEvalEnv b w i
env = GenEvalEnv b w i
env { envTypes :: TypeEnv
envTypes = TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TVar
p Either Nat' TValue
ty (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
env) }
{-# INLINE lookupType #-}
lookupType :: TVar -> GenEvalEnv b w i -> Maybe (Either Nat' TValue)
lookupType :: TVar -> GenEvalEnv b w i -> Maybe (Either Nat' TValue)
lookupType p :: TVar
p env :: GenEvalEnv b w i
env = TVar -> TypeEnv -> Maybe (Either Nat' TValue)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
p (GenEvalEnv b w i -> TypeEnv
forall b w i. GenEvalEnv b w i -> TypeEnv
envTypes GenEvalEnv b w i
env)