cryptol-2.9.0: Cryptol: The Language of Cryptography

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

Cryptol.ModuleSystem

Contents

Description

 
Synopsis

Module System

data ModuleEnv Source #

This is the current state of the interpreter.

Constructors

ModuleEnv 

Fields

Instances
Generic ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep ModuleEnv :: Type -> Type #

NFData ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: ModuleEnv -> () #

type Rep ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

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.

Constructors

DEnv 

data ModuleError Source #

Constructors

ModuleNotFound ModName [FilePath]

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

CantFindFile FilePath

Unable to open a file

BadUtf8 ModulePath UnicodeException

Bad UTF-8 encoding in while decoding this file

OtherIOError FilePath IOException

Some other IO error occurred while reading this file

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

ImportedParamModule ModName

Attempt to import a parametrized module that was not instantiated.

FailedToParameterizeModDefs ModName [Name]

Failed to add the module parameters to all definitions in a module.

NotAParameterizedModule ModName 
ErrorInFile ModulePath ModuleError

This is just a tag on the error, indicating the file containing it. It is convenient when we had to look for the module, and we'd like to communicate the location of pthe problematic module to the handler.

Instances
Show ModuleError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

NFData ModuleError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Methods

rnf :: ModuleError -> () #

PP ModuleError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Methods

ppPrec :: Int -> ModuleError -> Doc Source #

data ModuleWarning Source #

Instances
Show ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Generic ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Associated Types

type Rep ModuleWarning :: Type -> Type #

NFData ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Methods

rnf :: ModuleWarning -> () #

PP ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

type Rep ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

type Rep ModuleWarning = D1 (MetaData "ModuleWarning" "Cryptol.ModuleSystem.Monad" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" False) (C1 (MetaCons "TypeCheckWarnings" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Range, Warning)])) :+: C1 (MetaCons "RenamerWarnings" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [RenamerWarning])))

findModule :: ModName -> ModuleCmd ModulePath Source #

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

loadModuleByPath :: FilePath -> ModuleCmd (ModulePath, Module) Source #

Load the module contained in the given file.

loadModuleByName :: ModName -> ModuleCmd (ModulePath, 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 -> ModContext Source #

Given the state of the environment, compute information about what's in scope on the REPL. This includes what's in the focused module, plus any additional definitions from the REPL (e.g., let bound names, and it).

Interfaces

data Iface Source #

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

Constructors

Iface 

Fields

Instances
Show Iface Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> Iface -> ShowS #

show :: Iface -> String #

showList :: [Iface] -> ShowS #

Generic Iface Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Associated Types

type Rep Iface :: Type -> Type #

Methods

from :: Iface -> Rep Iface x #

to :: Rep Iface x -> Iface #

NFData Iface Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: Iface -> () #

type Rep Iface Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

data IfaceParams Source #

Constructors

IfaceParams 

Fields

Instances
Show IfaceParams Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Generic IfaceParams Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Associated Types

type Rep IfaceParams :: Type -> Type #

NFData IfaceParams Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceParams -> () #

type Rep IfaceParams Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceParams = D1 (MetaData "IfaceParams" "Cryptol.ModuleSystem.Interface" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" False) (C1 (MetaCons "IfaceParams" PrefixI True) (S1 (MetaSel (Just "ifParamTypes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Name ModTParam)) :*: (S1 (MetaSel (Just "ifParamConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Located Prop]) :*: S1 (MetaSel (Just "ifParamFuns") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map Name ModVParam)))))

genIface :: Module -> Iface Source #

Generate an Iface from a typechecked module.

data IfaceDecl Source #

Constructors

IfaceDecl 

Fields

Instances
Show IfaceDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Generic IfaceDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Associated Types

type Rep IfaceDecl :: Type -> Type #

NFData IfaceDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceDecl -> () #

type Rep IfaceDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface