cryptol-3.0.0: Cryptol: The Language of Cryptography

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 {
  - tcAction :: Act i o
  - tcLinter :: TCLinter o
  - tcPrims :: PrimMap
  }
- 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

rename :: ModName -> NamingEnv -> RenameM a -> ModuleM a Source #

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.

expandPropGuards :: Module PName -> ModuleM (Module PName) Source #

Run the expandPropGuards 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.

loadModuleByPath Source #

Arguments

:: Bool | evaluate declarations in the module
-> FilePath |
-> ModuleM TCTopEntity |

Load a module by its path.

loadModuleFrom Source #

Arguments

:: Bool | quiet mode
-> ImportSource |
-> ModuleM (ModulePath, TCTopEntity) |

Load a module, unless it was previously loaded.

doLoadModule Source #

Arguments

:: Bool | evaluate declarations in the module
-> Bool | quiet mode: true suppresses the "loading module" message
-> ImportSource |
-> ModulePath |
-> Fingerprint |
-> Set FilePath | `include` dependencies
-> 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) ]

moduleFile :: ModName -> String -> FilePath Source #

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.

checkModule Source #

Arguments

:: ImportSource | why are we loading this
-> Module PName | module to check
-> ModuleM (NamingEnv, TCTopEntity) |

Typecheck a single module. Note: we assume that `include`s have already been processed

data TCLinter o Source #

Constructors

TCLinter |

Fields

- lintCheck :: o -> InferInput -> Either (Range, Error) [ProofObligation]
- lintModule :: Maybe ModName

exprLinter :: TCLinter (Expr, Schema) Source #

declsLinter :: TCLinter ([DeclGroup], a) Source #

moduleLinter :: ModName -> TCLinter Module Source #

tcTopEntitytLinter :: ModName -> TCLinter TCTopEntity Source #

type Act i o = i -> InferInput -> IO (InferOutput o) Source #

data TCAction i o Source #

Constructors

TCAction |

Fields

- tcAction :: Act i o
- tcLinter :: TCLinter o
- tcPrims :: PrimMap

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.

evalExpr :: Expr -> ModuleM Value Source #

benchmarkExpr :: Double -> Expr -> ModuleM BenchmarkStats Source #

evalDecls :: [DeclGroup] -> ModuleM () Source #