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

{-# LANGUAGE FlexibleContexts #-}

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

    -- * Interfaces
  , Iface(..), IfaceParams(..), IfaceDecls(..), genIface
  , IfaceTySyn, IfaceDecl(..)
  ) where

import qualified Cryptol.Eval as E
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.Utils.Ident as M

import Data.ByteString (ByteString)

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

type ModuleCmd a = (E.EvalOpts, FilePath -> IO ByteString, ModuleEnv) -> IO (ModuleRes a)

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

getPrimMap :: ModuleCmd PrimMap
getPrimMap :: ModuleCmd PrimMap
getPrimMap (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
me = (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM PrimMap
-> IO (Either ModuleError (PrimMap, ModuleEnv), [ModuleWarning])
forall a.
(EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
runModuleM (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
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 (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
env = (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM ModulePath
-> IO (Either ModuleError (ModulePath, ModuleEnv), [ModuleWarning])
forall a.
(EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
runModuleM (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
env (ModName -> ModuleM ModulePath
Base.findModule ModName
n)

-- | Load the module contained in the given file.
loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.Module)
loadModuleByPath :: FilePath -> ModuleCmd (ModulePath, Module)
loadModuleByPath FilePath
path (EvalOpts
evo, FilePath -> IO ByteString
byteReader, ModuleEnv
env) =
  (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM (ModulePath, Module)
-> IO
     (Either ModuleError ((ModulePath, Module), ModuleEnv),
      [ModuleWarning])
forall a.
(EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
runModuleM (EvalOpts
evo, FilePath -> IO ByteString
byteReader, ModuleEnv -> ModuleEnv
resetModuleEnv ModuleEnv
env) (ModuleM (ModulePath, Module)
 -> IO
      (Either ModuleError ((ModulePath, Module), ModuleEnv),
       [ModuleWarning]))
-> ModuleM (ModulePath, Module)
-> IO
     (Either ModuleError ((ModulePath, Module), ModuleEnv),
      [ModuleWarning])
forall a b. (a -> b) -> a -> b
$ do
    (LoadedModule -> Bool) -> ModuleM ()
unloadModule ((FilePath -> ModulePath
InFile FilePath
path ModulePath -> ModulePath -> Bool
forall a. Eq a => a -> a -> Bool
==) (ModulePath -> Bool)
-> (LoadedModule -> ModulePath) -> LoadedModule -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoadedModule -> ModulePath
lmFilePath)
    Module
m <- FilePath -> ModuleM Module
Base.loadModuleByPath FilePath
path
    ModName -> ModuleM ()
setFocusedModule (Module -> ModName
T.mName Module
m)
    (ModulePath, Module) -> ModuleM (ModulePath, Module)
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> ModulePath
InFile FilePath
path,Module
m)

-- | Load the given parsed module.
loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module)
loadModuleByName :: ModName -> ModuleCmd (ModulePath, Module)
loadModuleByName ModName
n (EvalOpts
evo, FilePath -> IO ByteString
byteReader, ModuleEnv
env) =
  (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM (ModulePath, Module)
-> IO
     (Either ModuleError ((ModulePath, Module), ModuleEnv),
      [ModuleWarning])
forall a.
(EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
runModuleM (EvalOpts
evo, FilePath -> IO ByteString
byteReader, ModuleEnv -> ModuleEnv
resetModuleEnv ModuleEnv
env) (ModuleM (ModulePath, Module)
 -> IO
      (Either ModuleError ((ModulePath, Module), ModuleEnv),
       [ModuleWarning]))
-> ModuleM (ModulePath, Module)
-> IO
     (Either ModuleError ((ModulePath, Module), ModuleEnv),
      [ModuleWarning])
forall a b. (a -> b) -> a -> b
$ do
    (LoadedModule -> Bool) -> ModuleM ()
unloadModule ((ModName
n ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
==) (ModName -> Bool)
-> (LoadedModule -> ModName) -> LoadedModule -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoadedModule -> ModName
lmName)
    (ModulePath
path,Module
m') <- Bool -> ImportSource -> ModuleM (ModulePath, Module)
Base.loadModuleFrom Bool
False (ModName -> ImportSource
FromModule ModName
n)
    ModName -> ModuleM ()
setFocusedModule (Module -> ModName
T.mName Module
m')
    (ModulePath, Module) -> ModuleM (ModulePath, Module)
forall (m :: * -> *) a. Monad m => a -> m a
return (ModulePath
path,Module
m')

-- 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 (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
env = (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM (Expr Name, Expr, Schema)
-> IO
     (Either ModuleError ((Expr Name, Expr, Schema), ModuleEnv),
      [ModuleWarning])
forall a.
(EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
runModuleM (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
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 (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
env = (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM Value
-> IO (Either ModuleError (Value, ModuleEnv), [ModuleWarning])
forall a.
(EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
runModuleM (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
env (ModuleM Value -> ModuleM Value
forall a. ModuleM a -> ModuleM a
interactive (Expr -> ModuleM Value
Base.evalExpr Expr
e))

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

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

noPat :: RemovePatterns a => a -> ModuleCmd a
noPat :: a -> ModuleCmd a
noPat a
a (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
env = (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
forall a.
(EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
runModuleM (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
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))

renameVar :: R.NamingEnv -> PName -> ModuleCmd Name
renameVar :: NamingEnv -> PName -> ModuleCmd Name
renameVar NamingEnv
names PName
n (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
env = (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM Name
-> IO (Either ModuleError (Name, ModuleEnv), [ModuleWarning])
forall a.
(EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
runModuleM (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
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 (PName -> RenameM Name
R.renameVar PName
n)

renameType :: R.NamingEnv -> PName -> ModuleCmd Name
renameType :: NamingEnv -> PName -> ModuleCmd Name
renameType NamingEnv
names PName
n (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
env = (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM Name
-> IO (Either ModuleError (Name, ModuleEnv), [ModuleWarning])
forall a.
(EvalOpts, FilePath -> IO ByteString, ModuleEnv)
-> ModuleM a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
runModuleM (EvalOpts, FilePath -> IO ByteString, ModuleEnv)
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 (PName -> RenameM Name
R.renameType PName
n)