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

    {-# 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
      { forall sym.
    GenEvalEnv sym
    -> IntMap (Either (Prim sym) (SEval sym (GenValue sym)))
    envVars       :: !(IntMap.IntMap (Either (Prim sym) (SEval sym (GenValue sym))))
      , forall 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
    $cfrom :: forall sym x. GenEvalEnv sym -> Rep (GenEvalEnv sym) x
    from :: forall x. GenEvalEnv sym -> Rep (GenEvalEnv sym) x
    $cto :: forall sym x. Rep (GenEvalEnv sym) x -> GenEvalEnv sym
    to :: forall x. Rep (GenEvalEnv sym) x -> GenEvalEnv sym
    Generic

    instance Semigroup (GenEvalEnv sym) where
      GenEvalEnv sym
    l <> :: GenEvalEnv sym -> GenEvalEnv sym -> GenEvalEnv sym
    <> GenEvalEnv sym
    r = 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
        { 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 -> GenEvalEnv sym -> GenEvalEnv sym
    forall a. Semigroup a => a -> a -> a
    (<>)

    ppEnv :: Backend sym => sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc
    ppEnv :: forall sym.
    Backend sym =>
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 :: forall sym. 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 :: forall sym.
    Backend sym =>
    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 a.
    sym
    -> SEval sym a
    -> Maybe (SEval sym a)
    -> String
    -> SEval sym (SEval sym a)
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 :: forall sym.
    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 :: forall sym.
    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 :: forall sym. 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)