| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| 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 (IfaceDecls, NamingEnv, Module Name)
- noPat :: RemovePatterns a => a -> ModuleM a
- parseModule :: ModulePath -> ModuleM (Fingerprint, Module PName)
- loadModuleByPath :: FilePath -> ModuleM Module
- loadModuleFrom :: ImportSource -> ModuleM (ModulePath, Module)
- doLoadModule :: ImportSource -> ModulePath -> Fingerprint -> Module PName -> ModuleM Module
- fullyQualified :: Import -> Import
- importIface :: Import -> ModuleM (IfaceDecls, NamingEnv)
- importIfaces :: [Import] -> ModuleM (IfaceDecls, NamingEnv)
- moduleFile :: ModName -> String -> FilePath
- findModule :: ModName -> ModuleM ModulePath
- findFile :: FilePath -> ModuleM FilePath
- addPrelude :: Module PName -> Module PName
- loadDeps :: Module name -> ModuleM ()
- checkExpr :: Expr PName -> ModuleM (Expr Name, Expr, Schema)
- checkDecls :: [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup])
- getPrimMap :: ModuleM PrimMap
- checkModule :: ImportSource -> ModulePath -> Module PName -> ModuleM Module
- checkSingleModule :: Act (Module Name) Module -> ImportSource -> ModulePath -> 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
- 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 -> IfaceParams -> IfaceDecls -> ModuleM o
- genInferInput :: Range -> PrimMap -> IfaceParams -> 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.
parseModule :: ModulePath -> ModuleM (Fingerprint, Module PName) Source #
loadModuleFrom :: ImportSource -> ModuleM (ModulePath, Module) Source #
Load a module, unless it was previously loaded.
doLoadModule :: ImportSource -> ModulePath -> Fingerprint -> 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.
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 :: Module name -> ModuleM () Source #
Load the dependencies of a module into the 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.
checkModule :: ImportSource -> ModulePath -> Module PName -> ModuleM Module Source #
Load a module, be it a normal module or a functor instantiation.
Arguments
| :: Act (Module Name) Module | how to check |
| -> ImportSource | why are we loading this |
| -> ModulePath | |
| -> Module PName | module to check |
| -> ModuleM Module |
Typecheck a single module. If the module is an instantiation
of a functor, then this just type-checks the instantiating parameters.
See checkModule
Constructors
| TCLinter | |
Fields
| |
declsLinter :: TCLinter [DeclGroup] Source #
type Act i o = i -> InferInput -> IO (InferOutput o) Source #
typecheck :: (Show i, Show o, HasLoc i) => TCAction i o -> i -> IfaceParams -> IfaceDecls -> ModuleM o Source #
genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM InferInput Source #
Generate input for the typechecker.