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

    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE BlockArguments #-}

    module Cryptol.ModuleSystem (
        -- * Module System
        ModuleEnv(..), initialModuleEnv
      , DynamicEnv(..)
      , ModuleError(..), ModuleWarning(..)
      , ModuleCmd, ModuleRes
      , ModuleInput(..)
      , findModule
      , loadModuleByPath
      , loadModuleByName
      , checkModuleByPath
      , checkExpr
      , evalExpr
      , benchmarkExpr
      , checkDecls
      , evalDecls
      , noPat
      , focusedEnv
      , getPrimMap
      , renameVar
      , renameType

        -- * Interfaces
      , Iface, IfaceG(..), IfaceDecls(..), T.genIface, IfaceDecl(..)

        -- * Dependencies
      , getFileDependencies
      , getModuleDependencies
      ) where

    import Data.Map (Map)

    import qualified Cryptol.Eval.Concrete as Concrete
    import           Cryptol.ModuleSystem.Env
    import           Cryptol.ModuleSystem.Interface
    import           Cryptol.ModuleSystem.Monad
    import           Cryptol.ModuleSystem.Name (Name,PrimMap)
    import qualified Cryptol.ModuleSystem.Renamer as R
    import qualified Cryptol.ModuleSystem.Base as Base
    import qualified Cryptol.Parser.AST        as P
    import           Cryptol.Parser.Name (PName)
    import           Cryptol.Parser.NoPat (RemovePatterns)
    import qualified Cryptol.TypeCheck.AST     as T
    import qualified Cryptol.TypeCheck.Interface as T
    import           Cryptol.Utils.Benchmark (BenchmarkStats)
    import qualified Cryptol.Utils.Ident as M

    -- Public Interface ------------------------------------------------------------

    type ModuleCmd a = ModuleInput IO -> IO (ModuleRes a)

    type ModuleRes a = (Either ModuleError (a,ModuleEnv), [ModuleWarning])

    getPrimMap :: ModuleCmd PrimMap
    getPrimMap :: ModuleCmd PrimMap
    getPrimMap ModuleInput IO
    me = ModuleInput IO
    -> ModuleM PrimMap
    -> IO (Either ModuleError (PrimMap, ModuleEnv), [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    me ModuleM PrimMap
    Base.getPrimMap

    -- | Find the file associated with a module name in the module search path.
    findModule :: P.ModName -> ModuleCmd ModulePath
    findModule :: ModName -> ModuleCmd ModulePath
    findModule ModName
    n ModuleInput IO
    env = ModuleInput IO
    -> ModuleM ModulePath
    -> IO (Either ModuleError (ModulePath, ModuleEnv), [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env (ModName -> ModuleM ModulePath
    Base.findModule ModName
    n)

    -- | Load the module contained in the given file.
    loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.TCTopEntity)
    loadModuleByPath :: FilePath -> ModuleCmd (ModulePath, TCTopEntity)
    loadModuleByPath FilePath
    path ModuleInput IO
    minp = do
      ModuleEnv
    moduleEnv' <- ModuleEnv -> IO ModuleEnv
    resetModuleEnv (ModuleEnv -> IO ModuleEnv) -> ModuleEnv -> IO ModuleEnv
    forall a b. (a -> b) -> a -> b
    $ ModuleInput IO -> ModuleEnv
    forall (m :: * -> *). ModuleInput m -> ModuleEnv
    minpModuleEnv ModuleInput IO
    minp
      ModuleInput IO
    -> ModuleM (ModulePath, TCTopEntity)
    -> IO (ModuleRes (ModulePath, TCTopEntity))
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    minp{ minpModuleEnv :: ModuleEnv
    minpModuleEnv = ModuleEnv
    moduleEnv' } (ModuleM (ModulePath, TCTopEntity)
     -> IO (ModuleRes (ModulePath, TCTopEntity)))
    -> ModuleM (ModulePath, TCTopEntity)
    -> IO (ModuleRes (ModulePath, TCTopEntity))
    forall a b. (a -> b) -> a -> b
    $ do
        (forall a. LoadedModuleG a -> Bool) -> ModuleM ()
    unloadModule ((FilePath -> ModulePath
    InFile FilePath
    path ModulePath -> ModulePath -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (ModulePath -> Bool)
    -> (LoadedModuleG a -> ModulePath) -> LoadedModuleG a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LoadedModuleG a -> ModulePath
    forall a. LoadedModuleG a -> ModulePath
    lmFilePath)
        TCTopEntity
    m <- Bool -> FilePath -> ModuleM TCTopEntity
    Base.loadModuleByPath Bool
    True FilePath
    path
        ModName -> ModuleM ()
    setFocusedModule (TCTopEntity -> ModName
    T.tcTopEntitytName TCTopEntity
    m)
        (ModulePath, TCTopEntity) -> ModuleM (ModulePath, TCTopEntity)
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FilePath -> ModulePath
    InFile FilePath
    path,TCTopEntity
    m)

    -- | Load the given parsed module.
    loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.TCTopEntity)
    loadModuleByName :: ModName -> ModuleCmd (ModulePath, TCTopEntity)
    loadModuleByName ModName
    n ModuleInput IO
    minp = do
      ModuleEnv
    moduleEnv' <- ModuleEnv -> IO ModuleEnv
    resetModuleEnv (ModuleEnv -> IO ModuleEnv) -> ModuleEnv -> IO ModuleEnv
    forall a b. (a -> b) -> a -> b
    $ ModuleInput IO -> ModuleEnv
    forall (m :: * -> *). ModuleInput m -> ModuleEnv
    minpModuleEnv ModuleInput IO
    minp
      ModuleInput IO
    -> ModuleM (ModulePath, TCTopEntity)
    -> IO (ModuleRes (ModulePath, TCTopEntity))
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    minp{ minpModuleEnv :: ModuleEnv
    minpModuleEnv = ModuleEnv
    moduleEnv' } (ModuleM (ModulePath, TCTopEntity)
     -> IO (ModuleRes (ModulePath, TCTopEntity)))
    -> ModuleM (ModulePath, TCTopEntity)
    -> IO (ModuleRes (ModulePath, TCTopEntity))
    forall a b. (a -> b) -> a -> b
    $ do
        (forall a. LoadedModuleG a -> Bool) -> ModuleM ()
    unloadModule ((ModName
    n ModName -> ModName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (ModName -> Bool)
    -> (LoadedModuleG a -> ModName) -> LoadedModuleG a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LoadedModuleG a -> ModName
    forall a. LoadedModuleG a -> ModName
    lmName)
        (ModulePath
    path,TCTopEntity
    m') <- Bool -> ImportSource -> ModuleM (ModulePath, TCTopEntity)
    Base.loadModuleFrom Bool
    False (ModName -> ImportSource
    FromModule ModName
    n)
        ModName -> ModuleM ()
    setFocusedModule (TCTopEntity -> ModName
    T.tcTopEntitytName TCTopEntity
    m')
        (ModulePath, TCTopEntity) -> ModuleM (ModulePath, TCTopEntity)
    forall a. a -> ModuleT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ModulePath
    path,TCTopEntity
    m')

    -- | Parse and typecheck a module, but don't evaluate or change the environment.
    checkModuleByPath :: FilePath -> ModuleCmd (ModulePath, T.TCTopEntity)
    checkModuleByPath :: FilePath -> ModuleCmd (ModulePath, TCTopEntity)
    checkModuleByPath FilePath
    path ModuleInput IO
    minp = do
      (Either ModuleError (TCTopEntity, ModuleEnv)
    res, [ModuleWarning]
    warns) <- ModuleInput IO
    -> ModuleM TCTopEntity
    -> IO
         (Either ModuleError (TCTopEntity, ModuleEnv), [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    minp (ModuleM TCTopEntity
     -> IO
          (Either ModuleError (TCTopEntity, ModuleEnv), [ModuleWarning]))
    -> ModuleM TCTopEntity
    -> IO
         (Either ModuleError (TCTopEntity, ModuleEnv), [ModuleWarning])
    forall a b. (a -> b) -> a -> b
    $ Bool -> FilePath -> ModuleM TCTopEntity
    Base.loadModuleByPath Bool
    False FilePath
    path
      -- restore the old environment
      let res1 :: Either ModuleError ((ModulePath, TCTopEntity), ModuleEnv)
    res1 = do (TCTopEntity
    x,ModuleEnv
    _newEnv) <- Either ModuleError (TCTopEntity, ModuleEnv)
    res
                    ((ModulePath, TCTopEntity), ModuleEnv)
    -> Either ModuleError ((ModulePath, TCTopEntity), ModuleEnv)
    forall a. a -> Either ModuleError a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((FilePath -> ModulePath
    InFile FilePath
    path, TCTopEntity
    x), ModuleInput IO -> ModuleEnv
    forall (m :: * -> *). ModuleInput m -> ModuleEnv
    minpModuleEnv ModuleInput IO
    minp)
      ModuleRes (ModulePath, TCTopEntity)
    -> IO (ModuleRes (ModulePath, TCTopEntity))
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Either ModuleError ((ModulePath, TCTopEntity), ModuleEnv)
    res1, [ModuleWarning]
    warns)

    -- Extended Environments -------------------------------------------------------

    -- These functions are particularly useful for interactive modes, as
    -- they allow for expressions to be evaluated in an environment that
    -- can extend dynamically outside of the context of a module.

    -- | Check the type of an expression.  Give back the renamed expression, the
    -- core expression, and its type schema.
    checkExpr :: P.Expr PName -> ModuleCmd (P.Expr Name,T.Expr,T.Schema)
    checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema)
    checkExpr Expr PName
    e ModuleInput IO
    env = ModuleInput IO
    -> ModuleM (Expr Name, Expr, Schema)
    -> IO
         (Either ModuleError ((Expr Name, Expr, Schema), ModuleEnv),
          [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env (ModuleM (Expr Name, Expr, Schema)
    -> ModuleM (Expr Name, Expr, Schema)
    forall a. ModuleM a -> ModuleM a
    interactive (Expr PName -> ModuleM (Expr Name, Expr, Schema)
    Base.checkExpr Expr PName
    e))

    -- | Evaluate an expression.
    evalExpr :: T.Expr -> ModuleCmd Concrete.Value
    evalExpr :: Expr -> ModuleCmd Value
    evalExpr Expr
    e ModuleInput IO
    env = ModuleInput IO
    -> ModuleM Value
    -> IO (Either ModuleError (Value, ModuleEnv), [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env (ModuleM Value -> ModuleM Value
    forall a. ModuleM a -> ModuleM a
    interactive (Expr -> ModuleM Value
    Base.evalExpr Expr
    e))

    -- | Benchmark an expression.
    benchmarkExpr :: Double -> T.Expr -> ModuleCmd BenchmarkStats
    benchmarkExpr :: Double -> Expr -> ModuleCmd BenchmarkStats
    benchmarkExpr Double
    period Expr
    e ModuleInput IO
    env =
      ModuleInput IO
    -> ModuleM BenchmarkStats
    -> IO
         (Either ModuleError (BenchmarkStats, ModuleEnv), [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env (ModuleM BenchmarkStats -> ModuleM BenchmarkStats
    forall a. ModuleM a -> ModuleM a
    interactive (Double -> Expr -> ModuleM BenchmarkStats
    Base.benchmarkExpr Double
    period Expr
    e))

    -- | Typecheck top-level declarations.
    checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup], Map Name T.TySyn)
    checkDecls :: [TopDecl PName]
    -> ModuleCmd (NamingEnv, [DeclGroup], Map Name TySyn)
    checkDecls [TopDecl PName]
    ds ModuleInput IO
    env = ModuleInput IO
    -> ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
    -> IO
         (Either
            ModuleError ((NamingEnv, [DeclGroup], Map Name TySyn), ModuleEnv),
          [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env
                      (ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
     -> IO
          (Either
             ModuleError ((NamingEnv, [DeclGroup], Map Name TySyn), ModuleEnv),
           [ModuleWarning]))
    -> ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
    -> IO
         (Either
            ModuleError ((NamingEnv, [DeclGroup], Map Name TySyn), ModuleEnv),
          [ModuleWarning])
    forall a b. (a -> b) -> a -> b
    $ ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
    -> ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
    forall a. ModuleM a -> ModuleM a
    interactive
                      (ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
     -> ModuleM (NamingEnv, [DeclGroup], Map Name TySyn))
    -> ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
    -> ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
    forall a b. (a -> b) -> a -> b
    $ [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
    Base.checkDecls [TopDecl PName]
    ds

    -- | Evaluate declarations and add them to the extended environment.
    evalDecls :: [T.DeclGroup] -> ModuleCmd ()
    evalDecls :: [DeclGroup] -> ModuleCmd ()
    evalDecls [DeclGroup]
    dgs ModuleInput IO
    env = ModuleInput IO
    -> ModuleM ()
    -> IO (Either ModuleError ((), ModuleEnv), [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env (ModuleM () -> ModuleM ()
    forall a. ModuleM a -> ModuleM a
    interactive ([DeclGroup] -> ModuleM ()
    Base.evalDecls [DeclGroup]
    dgs))

    noPat :: RemovePatterns a => a -> ModuleCmd a
    noPat :: forall a. RemovePatterns a => a -> ModuleCmd a
    noPat a
    a ModuleInput IO
    env = ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env (ModuleM a -> ModuleM a
    forall a. ModuleM a -> ModuleM a
    interactive (a -> ModuleM a
    forall a. RemovePatterns a => a -> ModuleM a
    Base.noPat a
    a))

    -- | Rename a *use* of a value name. The distinction between uses and
    -- binding is used to keep track of dependencies.
    renameVar :: R.NamingEnv -> PName -> ModuleCmd Name
    renameVar :: NamingEnv -> PName -> ModuleCmd Name
    renameVar NamingEnv
    names PName
    n ModuleInput IO
    env = ModuleInput IO
    -> ModuleM Name
    -> IO (Either ModuleError (Name, ModuleEnv), [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env (ModuleM Name
     -> IO (Either ModuleError (Name, ModuleEnv), [ModuleWarning]))
    -> ModuleM Name
    -> IO (Either ModuleError (Name, ModuleEnv), [ModuleWarning])
    forall a b. (a -> b) -> a -> b
    $ ModuleM Name -> ModuleM Name
    forall a. ModuleM a -> ModuleM a
    interactive (ModuleM Name -> ModuleM Name) -> ModuleM Name -> ModuleM Name
    forall a b. (a -> b) -> a -> b
    $
      ModName -> NamingEnv -> RenameM Name -> ModuleM Name
    forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
    Base.rename ModName
    M.interactiveName NamingEnv
    names (NameType -> PName -> RenameM Name
    R.renameVar NameType
    R.NameUse PName
    n)

    -- | Rename a *use* of a type name. The distinction between uses and
    -- binding is used to keep track of dependencies.
    renameType :: R.NamingEnv -> PName -> ModuleCmd Name
    renameType :: NamingEnv -> PName -> ModuleCmd Name
    renameType NamingEnv
    names PName
    n ModuleInput IO
    env = ModuleInput IO
    -> ModuleM Name
    -> IO (Either ModuleError (Name, ModuleEnv), [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env (ModuleM Name
     -> IO (Either ModuleError (Name, ModuleEnv), [ModuleWarning]))
    -> ModuleM Name
    -> IO (Either ModuleError (Name, ModuleEnv), [ModuleWarning])
    forall a b. (a -> b) -> a -> b
    $ ModuleM Name -> ModuleM Name
    forall a. ModuleM a -> ModuleM a
    interactive (ModuleM Name -> ModuleM Name) -> ModuleM Name -> ModuleM Name
    forall a b. (a -> b) -> a -> b
    $
      ModName -> NamingEnv -> RenameM Name -> ModuleM Name
    forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
    Base.rename ModName
    M.interactiveName NamingEnv
    names (NameType -> PName -> RenameM Name
    R.renameType NameType
    R.NameUse PName
    n)

    --------------------------------------------------------------------------------
    -- Dependencies

    -- | Get information about the dependencies of a file.
    getFileDependencies :: FilePath -> ModuleCmd (ModulePath, FileInfo)
    getFileDependencies :: FilePath -> ModuleCmd (ModulePath, FileInfo)
    getFileDependencies FilePath
    f ModuleInput IO
    env = ModuleInput IO
    -> ModuleM (ModulePath, FileInfo)
    -> IO
         (Either ModuleError ((ModulePath, FileInfo), ModuleEnv),
          [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env (ModulePath -> ModuleM (ModulePath, FileInfo)
    Base.findDepsOf (FilePath -> ModulePath
    InFile FilePath
    f))

    -- | Get information about the dependencies of a module.
    getModuleDependencies :: M.ModName -> ModuleCmd (ModulePath, FileInfo)
    getModuleDependencies :: ModName -> ModuleCmd (ModulePath, FileInfo)
    getModuleDependencies ModName
    m ModuleInput IO
    env = ModuleInput IO
    -> ModuleM (ModulePath, FileInfo)
    -> IO
         (Either ModuleError ((ModulePath, FileInfo), ModuleEnv),
          [ModuleWarning])
    forall a.
    ModuleInput IO
    -> ModuleM a
    -> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
    runModuleM ModuleInput IO
    env (ModName -> ModuleM (ModulePath, FileInfo)
    Base.findDepsOfModule ModName
    m)