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

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

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)

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

-- | Bind a variable in the evaluation environment.
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) }

-- | Bind a variable to a value in the evaluation environment, without
--   creating a thunk.
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) }

-- | Lookup a variable in the environment.
{-# 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)

-- | Bind a type variable of kind *.
{-# 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) }

-- | Lookup a type variable.
{-# 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)