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