cryptol-3.1.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Cryptol.ModuleSystem

Description

 
Synopsis

Module System

data ModuleEnv Source #

This is the current state of the interpreter.

Constructors

ModuleEnv 

Fields

Instances

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

Instances

Instances details
Monoid DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Semigroup DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Generic DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep DynamicEnv :: Type -> Type #

type Rep DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep DynamicEnv = D1 ('MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "DEnv" 'PrefixI 'True) ((S1 ('MetaSel ('Just "deNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamingEnv) :*: S1 ('MetaSel ('Just "deDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup])) :*: (S1 ('MetaSel ('Just "deTySyns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name TySyn)) :*: S1 ('MetaSel ('Just "deEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EvalEnv))))

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

ExpandPropGuardsError ImportSource Error

Problems during the ExpandPropGuards phase

NoIncludeErrors ImportSource [IncludeError]

Problems during the NoInclude phase

TypeCheckingFailed ImportSource NameMap [(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

FFILoadErrors ModName [FFILoadError]

Errors loading foreign function implementations

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

Instances details
Show ModuleError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

PP ModuleError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Methods

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

NFData ModuleError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Methods

rnf :: ModuleError -> () #

data ModuleWarning Source #

Instances

Instances details
Generic ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Associated Types

type Rep ModuleWarning :: Type -> Type #

Show ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

PP ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

NFData ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Methods

rnf :: ModuleWarning -> () #

type Rep ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

type Rep ModuleWarning = D1 ('MetaData "ModuleWarning" "Cryptol.ModuleSystem.Monad" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "TypeCheckWarnings" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameMap) :*: 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, TCTopEntity) Source #

Load the module contained in the given file.

loadModuleByName :: ModName -> ModuleCmd (ModulePath, TCTopEntity) Source #

Load the given parsed module.

checkModuleByPath :: FilePath -> ModuleCmd (ModulePath, TCTopEntity) Source #

Parse and typecheck a module, but don't evaluate or change the environment.

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.

benchmarkExpr :: Double -> Expr -> ModuleCmd BenchmarkStats Source #

Benchmark an expression.

checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup], Map Name TySyn) 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).

renameVar :: NamingEnv -> PName -> ModuleCmd Name Source #

Rename a *use* of a value name. The distinction between uses and binding is used to keep track of dependencies.

renameType :: NamingEnv -> PName -> ModuleCmd Name Source #

Rename a *use* of a type name. The distinction between uses and binding is used to keep track of dependencies.

Interfaces

data IfaceG name Source #

The interface repersenting a typecheck top-level module.

Constructors

Iface 

Fields

Instances

Instances details
Generic (IfaceG name) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Associated Types

type Rep (IfaceG name) :: Type -> Type #

Methods

from :: IfaceG name -> Rep (IfaceG name) x #

to :: Rep (IfaceG name) x -> IfaceG name #

Show name => Show (IfaceG name) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> IfaceG name -> ShowS #

show :: IfaceG name -> String #

showList :: [IfaceG name] -> ShowS #

NFData name => NFData (IfaceG name) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceG name -> () #

type Rep (IfaceG name) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep (IfaceG name) = D1 ('MetaData "IfaceG" "Cryptol.ModuleSystem.Interface" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "Iface" 'PrefixI 'True) (S1 ('MetaSel ('Just "ifNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IfaceNames name)) :*: (S1 ('MetaSel ('Just "ifParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunctorParams) :*: S1 ('MetaSel ('Just "ifDefines") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceDecls))))

data IfaceDecls Source #

Declarations in a module. Note that this includes things from nested modules, but not things from nested functors, which are in ifFunctors.

Constructors

IfaceDecls 

Fields

Instances

Instances details
Monoid IfaceDecls Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Semigroup IfaceDecls Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Generic IfaceDecls Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Associated Types

type Rep IfaceDecls :: Type -> Type #

Show IfaceDecls Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

NFData IfaceDecls Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceDecls -> () #

type Rep IfaceDecls Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

genIface :: ModuleG name -> IfaceG name Source #

data IfaceDecl Source #

Constructors

IfaceDecl 

Fields

Instances

Instances details
Generic IfaceDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Associated Types

type Rep IfaceDecl :: Type -> Type #

Show IfaceDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

NFData IfaceDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceDecl -> () #

type Rep IfaceDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceDecl = D1 ('MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "IfaceDecl" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifDeclName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :*: (S1 ('MetaSel ('Just "ifDeclSig") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Schema) :*: S1 ('MetaSel ('Just "ifDeclIsPrim") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "ifDeclPragmas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pragma]) :*: S1 ('MetaSel ('Just "ifDeclInfix") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "ifDeclFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)) :*: S1 ('MetaSel ('Just "ifDeclDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))))

Dependencies

getFileDependencies :: FilePath -> ModuleCmd (ModulePath, FileInfo) Source #

Get information about the dependencies of a file.

getModuleDependencies :: ModName -> ModuleCmd (ModulePath, FileInfo) Source #

Get information about the dependencies of a module.