cryptol-2.3.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell98

Cryptol.ModuleSystem.Base

Description

 

Synopsis

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.

loadModuleByPath :: FilePath -> ModuleM Module Source

Load a module by its path.

loadImport :: Located Import -> ModuleM () Source

Load the module specified by an import.

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.

findModule :: ModName -> ModuleM FilePath 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.

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.

checkModule :: FilePath -> Module PName -> ModuleM Module Source

Typecheck a module.

data TCAction i o Source

Constructors

TCAction 

typecheck :: (Show i, Show o, HasLoc i) => TCAction i o -> i -> IfaceDecls -> ModuleM o Source

genInferInput :: Range -> PrimMap -> IfaceDecls -> ModuleM InferInput Source

Generate input for the typechecker.