| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell98 |
Cryptol.ModuleSystem.Base
Description
- rename :: ModName -> NamingEnv -> RenameM a -> ModuleM a
- renameModule :: Module PName -> ModuleM (IfaceDecls, NamingEnv, Module Name)
- noPat :: RemovePatterns a => a -> ModuleM a
- parseModule :: FilePath -> ModuleM (Module PName)
- loadModuleByPath :: FilePath -> ModuleM Module
- loadImport :: Located Import -> ModuleM ()
- loadModule :: FilePath -> Module PName -> ModuleM Module
- fullyQualified :: Import -> Import
- importIface :: Import -> ModuleM (IfaceDecls, NamingEnv)
- importIfaces :: [Import] -> ModuleM (IfaceDecls, NamingEnv)
- moduleFile :: ModName -> String -> FilePath
- findModule :: ModName -> ModuleM FilePath
- findFile :: FilePath -> ModuleM FilePath
- addPrelude :: Module PName -> Module PName
- loadDeps :: Module name -> ModuleM ()
- getLocalEnv :: ModuleM (IfaceDecls, NamingEnv)
- checkExpr :: Expr PName -> ModuleM (Expr Name, Expr, Schema)
- checkDecls :: [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup])
- getPrimMap :: ModuleM PrimMap
- checkModule :: FilePath -> Module PName -> ModuleM Module
- data TCLinter o = TCLinter {
- lintCheck :: o -> InferInput -> Either Error [ProofObligation]
- lintModule :: Maybe ModName
- exprLinter :: TCLinter (Expr, Schema)
- declsLinter :: TCLinter [DeclGroup]
- moduleLinter :: ModName -> TCLinter Module
- data TCAction i o = TCAction {
- tcAction :: i -> InferInput -> IO (InferOutput o)
- tcLinter :: TCLinter o
- tcPrims :: PrimMap
- typecheck :: (Show i, Show o, HasLoc i) => TCAction i o -> i -> IfaceDecls -> ModuleM o
- genInferInput :: Range -> PrimMap -> IfaceDecls -> ModuleM InferInput
- evalExpr :: Expr -> ModuleM Value
- evalDecls :: [DeclGroup] -> ModuleM ()
Documentation
renameModule :: Module PName -> ModuleM (IfaceDecls, NamingEnv, Module Name) Source #
Rename a module in the context of its imported modules.
noPat :: RemovePatterns a => a -> ModuleM a Source #
Run the noPat pass.
loadModule :: FilePath -> Module PName -> ModuleM Module Source #
Load dependencies, typecheck, and add to the eval environment.
fullyQualified :: Import -> Import Source #
Rewrite an import declaration to be of the form:
import foo as foo [ [hiding] (a,b,c) ]
importIface :: Import -> ModuleM (IfaceDecls, NamingEnv) Source #
Find the interface referenced by an import, and generate the naming environment that it describes.
importIfaces :: [Import] -> ModuleM (IfaceDecls, NamingEnv) Source #
Load a series of interfaces, merging their public interfaces.
findFile :: FilePath -> ModuleM FilePath Source #
Discover a file. This is distinct from findModule in that we
assume we've already been given a particular file name.
addPrelude :: Module PName -> Module PName Source #
Add the prelude to the import list if it's not already mentioned.
loadDeps :: Module name -> ModuleM () Source #
Load the dependencies of a module into the environment.
getLocalEnv :: ModuleM (IfaceDecls, NamingEnv) Source #
Load the local environment, which consists of the environment for the currently opened module, shadowed by the dynamic environment.
checkExpr :: Expr PName -> ModuleM (Expr Name, Expr, Schema) Source #
Typecheck a single expression, yielding a renamed parsed expression, typechecked core expression, and a type schema.
checkDecls :: [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup]) Source #
Typecheck a group of declarations.
INVARIANT: This assumes that NoPat has already been run on the declarations.
getPrimMap :: ModuleM PrimMap Source #
Generate the primitive map. If the prelude is currently being loaded, this should be generated directly from the naming environment given to the renamer instead.
Constructors
| TCLinter | |
Fields
| |
declsLinter :: TCLinter [DeclGroup] Source #
Constructors
| TCAction | |
Fields
| |
genInferInput :: Range -> PrimMap -> IfaceDecls -> ModuleM InferInput Source #
Generate input for the typechecker.