cryptol-2.8.0: Cryptol: The Language of Cryptography

Cryptol.ModuleSystem.Base

Description

This is the main driver---it provides entry points for the various passes.

Synopsis

# Documentation

Rename a module in the context of its imported modules.

noPat :: RemovePatterns a => a -> ModuleM a Source #

Run the noPat pass.

Load a module by its path.

Rewrite an import declaration to be of the form:

import foo as foo [ [hiding] (a,b,c) ]

Find the interface referenced by an import, and generate the naming environment that it describes.

Load a series of interfaces, merging their public interfaces.

Discover a module.

Discover a file. This is distinct from findModule in that we assume we've already been given a particular file name.

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.

Load the local environment, which consists of the environment for the currently opened module, shadowed by the dynamic environment.

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.

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.

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

data TCLinter o Source #

Constructors

 TCLinter FieldslintCheck :: o -> InferInput -> Either Error [ProofObligation] lintModule :: Maybe ModName

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

data TCAction i o Source #

Constructors

 TCAction FieldstcAction :: Act i o tcLinter :: TCLinter o tcPrims :: PrimMap

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

Generate input for the typechecker.