Cryptol.ModuleSystem.Base

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

Documentation

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

renameModule :: Module PName -> ModuleM (IfaceDecls, NamingEnv, Module Name)

Rename a module in the context of its imported modules.

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

Run the noPat pass.

parseModule :: FilePath -> ModuleM (Fingerprint, Module PName)

loadModuleByPath :: FilePath -> ModuleM Module

Load a module by its path.

loadModuleFrom :: ImportSource -> ModuleM (FilePath, Module)

Load a module, unless it was previously loaded.

doLoadModule :: ImportSource -> FilePath -> Fingerprint -> Module PName -> ModuleM Module

Load dependencies, typecheck, and add to the eval environment.

fullyQualified :: Import -> Import

Rewrite an import declaration to be of the form:

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

importIface :: Import -> ModuleM (IfaceDecls, NamingEnv)

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

importIfaces :: [Import] -> ModuleM (IfaceDecls, NamingEnv)

Load a series of interfaces, merging their public interfaces.

moduleFile :: ModName -> String -> FilePath

findModule :: ModName -> ModuleM FilePath

Discover a module.

findFile :: FilePath -> ModuleM FilePath

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

Add the prelude to the import list if it's not already mentioned.

loadDeps :: Module name -> ModuleM ()

Load the dependencies of a module into the environment.

getLocalEnv :: ModuleM (IfaceParams, IfaceDecls, NamingEnv)

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)

Typecheck a single expression, yielding a renamed parsed expression, typechecked core expression, and a type schema.

checkDecls :: [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup])

Typecheck a group of declarations.

INVARIANT: This assumes that NoPat has already been run on the declarations.

getPrimMap :: ModuleM PrimMap

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 -> FilePath -> Module PName -> ModuleM Module

Load a module, be it a normal module or a functor instantiation.

checkSingleModule

Arguments

:: Act (Module Name) Module

how to check

-> ImportSource

why are we loading this

-> FilePath

-> 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

Constructors

TCLinter

Fields

• 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

Constructors

TCAction

Fields

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

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

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

Generate input for the typechecker.

evalExpr :: Expr -> ModuleM Value

evalDecls :: [DeclGroup] -> ModuleM ()