-- |
-- 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
  , setFocusedModule
  , Base.renameImpNameInCurrentEnv
  , impNameTopModule

    -- * 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,nameTopModule)
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' } (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
    ImpName Name -> ModuleM ()
setFocusedModule (ModName -> ImpName Name
forall name. ModName -> ImpName name
P.ImpTop (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' } (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)
    ImpName Name -> ModuleM ()
setFocusedModule (ModName -> ImpName Name
forall name. ModName -> ImpName name
P.ImpTop (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)

--------------------------------------------------------------------------------
-- ImpName utilities

impNameTopModule :: P.ImpName Name -> M.ModName
impNameTopModule :: ImpName Name -> ModName
impNameTopModule ImpName Name
impName =
    case ImpName Name
impName of
      P.ImpTop ModName
m -> ModName
m
      P.ImpNested Name
n -> Name -> ModName
nameTopModule Name
n