cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois, Inc.
Safe HaskellNone






Module System

data ModuleEnv Source #


Generic ModuleEnv Source # 

Associated Types

type Rep ModuleEnv :: * -> * #

NFData ModuleEnv Source # 


rnf :: ModuleEnv -> () #

type Rep ModuleEnv Source # 

data DynamicEnv Source #

Extra information we need to carry around to dynamically extend an environment outside the context of a single module. Particularly useful when dealing with interactive declarations as in :let or it.



data ModuleError Source #


ModuleNotFound ModName [FilePath]

Unable to find the module given, tried looking in these paths

CantFindFile FilePath

Unable to open a file

OtherIOError FilePath IOException

Some other IO error occurred while reading this file

ModuleParseError FilePath ParseError

Generated this parse error when parsing the file for module m

RecursiveModules [ImportSource]

Recursive module group discovered

RenamerErrors ImportSource [RenamerError]

Problems during the renaming phase

NoPatErrors ImportSource [Error]

Problems during the NoPat phase

NoIncludeErrors ImportSource [IncludeError]

Problems during the NoInclude phase

TypeCheckingFailed ImportSource [(Range, Error)]

Problems during type checking

OtherFailure String

Problems after type checking, eg. specialization

ModuleNameMismatch ModName (Located ModName)

Module loaded by 'import' statement has the wrong module name

DuplicateModuleName ModName FilePath FilePath

Two modules loaded from different files have the same module name

findModule :: ModName -> ModuleCmd FilePath Source #

Find the file associated with a module name in the module search path.

loadModuleByPath :: FilePath -> ModuleCmd Module Source #

Load the module contained in the given file.

loadModule :: FilePath -> Module PName -> ModuleCmd Module Source #

Load the given parsed module.

checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema) Source #

Check the type of an expression. Give back the renamed expression, the core expression, and its type schema.

evalExpr :: Expr -> ModuleCmd Value Source #

Evaluate an expression.

checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup]) Source #

Typecheck top-level declarations.

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

Evaluate declarations and add them to the extended environment.

focusedEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp) Source #

Produce an ifaceDecls that represents the focused environment of the module system, as well as a NameDisp for pretty-printing names according to the imports.

XXX This could really do with some better error handling, just returning mempty when one of the imports fails isn't really desirable.


data Iface Source #

The resulting interface generated by a module that has been typechecked.




Show Iface Source # 


showsPrec :: Int -> Iface -> ShowS #

show :: Iface -> String #

showList :: [Iface] -> ShowS #

Generic Iface Source # 

Associated Types

type Rep Iface :: * -> * #


from :: Iface -> Rep Iface x #

to :: Rep Iface x -> Iface #

NFData Iface Source # 


rnf :: Iface -> () #

type Rep Iface Source # 
type Rep Iface = D1 (MetaData "Iface" "Cryptol.ModuleSystem.Interface" "cryptol-2.4.0-AtabUoGsZJn8kSvO8P84NP" False) (C1 (MetaCons "Iface" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "ifModName") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ModName)) ((:*:) (S1 (MetaSel (Just Symbol "ifPublic") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IfaceDecls)) (S1 (MetaSel (Just Symbol "ifPrivate") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IfaceDecls)))))

genIface :: Module -> Iface Source #

Generate an Iface from a typechecked module.