1-- | 2-- Module : Cryptol.ModuleSystem 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8 9{-# LANGUAGE FlexibleContexts #-} 10 11module Cryptol.ModuleSystem ( 12 -- * Module System 13 ModuleEnv(..), initialModuleEnv 14 , DynamicEnv(..) 15 , ModuleError(..), ModuleWarning(..) 16 , ModuleCmd, ModuleRes 17 , ModuleInput(..) 18 , findModule 19 , loadModuleByPath 20 , loadModuleByName 21 , checkExpr 22 , evalExpr 23 , checkDecls 24 , evalDecls 25 , noPat 26 , focusedEnv 27 , getPrimMap 28 , renameVar 29 , renameType 30 31 -- * Interfaces 32 , Iface(..), IfaceParams(..), IfaceDecls(..), genIface 33 , IfaceTySyn, IfaceDecl(..) 34 ) where 35 36import qualified Cryptol.Eval.Concrete as Concrete 37import Cryptol.ModuleSystem.Env 38import Cryptol.ModuleSystem.Interface 39import Cryptol.ModuleSystem.Monad 40import Cryptol.ModuleSystem.Name (Name,PrimMap) 41import qualified Cryptol.ModuleSystem.Renamer as R 42import qualified Cryptol.ModuleSystem.Base as Base 43import qualified Cryptol.Parser.AST as P 44import Cryptol.Parser.Name (PName) 45import Cryptol.Parser.NoPat (RemovePatterns) 46import qualified Cryptol.TypeCheck.AST as T 47import qualified Cryptol.Utils.Ident as M 48 49-- Public Interface ------------------------------------------------------------ 50 51type ModuleCmd a = ModuleInput IO -> IO (ModuleRes a) 52 53type ModuleRes a = (Either ModuleError (a,ModuleEnv), [ModuleWarning]) 54 55getPrimMap :: ModuleCmd PrimMap 56getPrimMap me = runModuleM me Base.getPrimMap 57 58-- | Find the file associated with a module name in the module search path. 59findModule :: P.ModName -> ModuleCmd ModulePath 60findModule n env = runModuleM env (Base.findModule n) 61 62-- | Load the module contained in the given file. 63loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.Module) 64loadModuleByPath path minp = 65 runModuleM minp{ minpModuleEnv = resetModuleEnv (minpModuleEnv minp) } $ do 66 unloadModule ((InFile path ==) . lmFilePath) 67 m <- Base.loadModuleByPath path 68 setFocusedModule (T.mName m) 69 return (InFile path,m) 70 71-- | Load the given parsed module. 72loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module) 73loadModuleByName n minp = 74 runModuleM minp{ minpModuleEnv = resetModuleEnv (minpModuleEnv minp) } $ do 75 unloadModule ((n ==) . lmName) 76 (path,m') <- Base.loadModuleFrom False (FromModule n) 77 setFocusedModule (T.mName m') 78 return (path,m') 79 80-- Extended Environments ------------------------------------------------------- 81 82-- These functions are particularly useful for interactive modes, as 83-- they allow for expressions to be evaluated in an environment that 84-- can extend dynamically outside of the context of a module. 85 86-- | Check the type of an expression. Give back the renamed expression, the 87-- core expression, and its type schema. 88checkExpr :: P.Expr PName -> ModuleCmd (P.Expr Name,T.Expr,T.Schema) 89checkExpr e env = runModuleM env (interactive (Base.checkExpr e)) 90 91-- | Evaluate an expression. 92evalExpr :: T.Expr -> ModuleCmd Concrete.Value 93evalExpr e env = runModuleM env (interactive (Base.evalExpr e)) 94 95-- | Typecheck top-level declarations. 96checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup]) 97checkDecls ds env = runModuleM env 98 $ interactive 99 $ Base.checkDecls ds 100 101-- | Evaluate declarations and add them to the extended environment. 102evalDecls :: [T.DeclGroup] -> ModuleCmd () 103evalDecls dgs env = runModuleM env (interactive (Base.evalDecls dgs)) 104 105noPat :: RemovePatterns a => a -> ModuleCmd a 106noPat a env = runModuleM env (interactive (Base.noPat a)) 107 108renameVar :: R.NamingEnv -> PName -> ModuleCmd Name 109renameVar names n env = runModuleM env $ interactive $ 110 Base.rename M.interactiveName names (R.renameVar n) 111 112renameType :: R.NamingEnv -> PName -> ModuleCmd Name 113renameType names n env = runModuleM env $ interactive $ 114 Base.rename M.interactiveName names (R.renameType n) 115