| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Cryptol.ModuleSystem.Base
Description
This is the main driver---it provides entry points for the various passes.
Synopsis
- rename :: ModName -> NamingEnv -> RenameM a -> ModuleM a
- renameModule :: Module PName -> ModuleM RenamedModule
- noPat :: RemovePatterns a => a -> ModuleM a
- expandPropGuards :: Module PName -> ModuleM (Module PName)
- parseModule :: ModulePath -> ModuleM (Fingerprint, Set FilePath, [Module PName])
- loadModuleByPath :: Bool -> FilePath -> ModuleM TCTopEntity
- loadModuleFrom :: Bool -> ImportSource -> ModuleM (ModulePath, TCTopEntity)
- doLoadModule :: Bool -> Bool -> ImportSource -> ModulePath -> Fingerprint -> Set FilePath -> Module PName -> ModuleM TCTopEntity
- fullyQualified :: Import -> Import
- moduleFile :: ModName -> String -> FilePath
- findModule :: ModName -> ModuleM ModulePath
- findFile :: FilePath -> ModuleM FilePath
- addPrelude :: Module PName -> Module PName
- loadDeps :: ModuleG mname name -> ModuleM (Set ModName)
- findDeps :: ModuleG mname name -> [ImportSource]
- findDepsOfModule :: ModName -> ModuleM (ModulePath, FileInfo)
- findDepsOf :: ModulePath -> ModuleM (ModulePath, FileInfo)
- findModuleDeps :: ModuleG mname name -> Set ModName
- findDeps' :: ModuleG mname name -> (Any, Endo [ImportSource])
- checkExpr :: Expr PName -> ModuleM (Expr Name, Expr, Schema)
- checkDecls :: [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
- getPrimMap :: ModuleM PrimMap
- checkModule :: ImportSource -> Module PName -> ModuleM (NamingEnv, TCTopEntity)
- data TCLinter o = TCLinter {
- lintCheck :: o -> InferInput -> Either (Range, Error) [ProofObligation]
- lintModule :: Maybe ModName
- exprLinter :: TCLinter (Expr, Schema)
- declsLinter :: TCLinter ([DeclGroup], a)
- moduleLinter :: ModName -> TCLinter Module
- tcTopEntitytLinter :: ModName -> TCLinter TCTopEntity
- type Act i o = i -> InferInput -> IO (InferOutput o)
- data TCAction i o = TCAction {}
- typecheck :: (Show i, Show o, HasLoc i) => TCAction i o -> i -> ModContextParams -> IfaceDecls -> ModuleM o
- genInferInput :: Range -> PrimMap -> ModContextParams -> IfaceDecls -> ModuleM InferInput
- evalExpr :: Expr -> ModuleM Value
- benchmarkExpr :: Double -> Expr -> ModuleM BenchmarkStats
- evalDecls :: [DeclGroup] -> ModuleM ()
Documentation
renameModule :: Module PName -> ModuleM RenamedModule Source #
Rename a module in the context of its imported modules.
noPat :: RemovePatterns a => a -> ModuleM a Source #
Run the noPat pass.
parseModule :: ModulePath -> ModuleM (Fingerprint, Set FilePath, [Module PName]) Source #
Parse a module and expand includes
Returns a fingerprint of the module, and a set of dependencies due
to include directives.
Arguments
| :: Bool | evaluate declarations in the module |
| -> FilePath | |
| -> ModuleM TCTopEntity |
Load a module by its path.
Arguments
| :: Bool | quiet mode |
| -> ImportSource | |
| -> ModuleM (ModulePath, TCTopEntity) |
Load a module, unless it was previously loaded.
Arguments
| :: Bool | evaluate declarations in the module |
| -> Bool | quiet mode: true suppresses the "loading module" message |
| -> ImportSource | |
| -> ModulePath | |
| -> Fingerprint | |
| -> Set FilePath |
|
| -> Module PName | |
| -> ModuleM TCTopEntity |
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) ]
findModule :: ModName -> ModuleM ModulePath Source #
Discover a module.
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 :: ModuleG mname name -> ModuleM (Set ModName) Source #
Load the dependencies of a module into the environment.
findDeps :: ModuleG mname name -> [ImportSource] Source #
Find all imports in a module.
findDepsOfModule :: ModName -> ModuleM (ModulePath, FileInfo) Source #
findDepsOf :: ModulePath -> ModuleM (ModulePath, FileInfo) Source #
findModuleDeps :: ModuleG mname name -> Set ModName Source #
Find the set of top-level modules imported by a module.
findDeps' :: ModuleG mname name -> (Any, Endo [ImportSource]) Source #
A helper findDeps and findModuleDeps that actually does the searching.
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], Map Name TySyn) 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.
Arguments
| :: ImportSource | why are we loading this |
| -> Module PName | module to check |
| -> ModuleM (NamingEnv, TCTopEntity) |
Typecheck a single module.
Note: we assume that includes have already been processed
Constructors
| TCLinter | |
Fields
| |
declsLinter :: TCLinter ([DeclGroup], a) Source #
type Act i o = i -> InferInput -> IO (InferOutput o) Source #
typecheck :: (Show i, Show o, HasLoc i) => TCAction i o -> i -> ModContextParams -> IfaceDecls -> ModuleM o Source #
genInferInput :: Range -> PrimMap -> ModContextParams -> IfaceDecls -> ModuleM InferInput Source #
Generate input for the typechecker.
benchmarkExpr :: Double -> Expr -> ModuleM BenchmarkStats Source #