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

Cryptol.ModuleSystem

Description

 
Synopsis

Module System

data ModuleEnv Source #

This is the current state of the interpreter.

Constructors

ModuleEnv 

Fields

  • meLoadedModules :: LoadedModules

    Information about all loaded modules. See LoadedModule. Contains information such as the file where the module was loaded from, as well as the module's interface, used for type checking.

  • meNameSeeds :: NameSeeds

    A source of new names for the type checker.

  • meSolverConfig :: SolverConfig

    Configuration settings for the SMT solver used for type-checking.

  • meEvalEnv :: EvalEnv

    The evaluation environment. Contains the values for all loaded modules, both public and private.

  • meCoreLint :: CoreLint

    Should we run the linter to ensure sanity.

  • meMonoBinds :: !Bool

    Are we assuming that local bindings are monomorphic. XXX: We should probably remove this flag, and set it to True.

  • meFocusedModule :: Maybe ModName

    The "current" module. Used to decide how to print names, for example.

  • meSearchPath :: [FilePath]

    Where we look for things.

  • meDynEnv :: DynamicEnv

    This contains additional definitions that were made at the command line, and so they don't reside in any module.

  • meSupply :: !Supply

    Name source for the renamer

Instances

Instances details
Generic ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep ModuleEnv :: Type -> Type

Methods

from :: ModuleEnv -> Rep ModuleEnv x

to :: Rep ModuleEnv x -> ModuleEnv

NFData ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: ModuleEnv -> ()

type Rep ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep ModuleEnv = D1 ('MetaData "ModuleEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "ModuleEnv" 'PrefixI 'True) (((S1 ('MetaSel ('Just "meLoadedModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LoadedModules) :*: S1 ('MetaSel ('Just "meNameSeeds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameSeeds)) :*: (S1 ('MetaSel ('Just "meSolverConfig") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SolverConfig) :*: (S1 ('MetaSel ('Just "meEvalEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EvalEnv) :*: S1 ('MetaSel ('Just "meCoreLint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoreLint)))) :*: ((S1 ('MetaSel ('Just "meMonoBinds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :*: S1 ('MetaSel ('Just "meFocusedModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "meSearchPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :*: (S1 ('MetaSel ('Just "meDynEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DynamicEnv) :*: S1 ('MetaSel ('Just "meSupply") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Supply))))))

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
Generic DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep DynamicEnv :: Type -> Type

Methods

from :: DynamicEnv -> Rep DynamicEnv x

to :: Rep DynamicEnv x -> DynamicEnv

Semigroup DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Monoid DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

NFData DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: DynamicEnv -> ()

type Rep DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep DynamicEnv = D1 ('MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 "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

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

Instances details
Show ModuleError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Methods

showsPrec :: Int -> ModuleError -> ShowS

show :: ModuleError -> String

showList :: [ModuleError] -> ShowS

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

Instances details
Show ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

Methods

showsPrec :: Int -> ModuleWarning -> ShowS

show :: ModuleWarning -> String

showList :: [ModuleWarning] -> ShowS

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

Methods

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

type Rep ModuleWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Monad

type Rep ModuleWarning = D1 ('MetaData "ModuleWarning" "Cryptol.ModuleSystem.Monad" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 -> (IfaceParams, 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.

XXX: This is not quite right. For example, it does not take into account *how* things were imported in a module (e.g., qualified). It would be simpler to simply store the naming environment that was actually used when we renamed the module.

Interfaces

data Iface Source #

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

Constructors

Iface 

Fields

Instances

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

type Rep Iface = D1 ('MetaData "Iface" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "Iface" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifModName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModName) :*: S1 ('MetaSel ('Just "ifPublic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceDecls)) :*: (S1 ('MetaSel ('Just "ifPrivate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceDecls) :*: S1 ('MetaSel ('Just "ifParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceParams))))

data IfaceParams Source #

Constructors

IfaceParams 

Fields

Instances

Instances details
Show IfaceParams Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> IfaceParams -> ShowS

show :: IfaceParams -> String

showList :: [IfaceParams] -> ShowS

Generic IfaceParams Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Associated Types

type Rep IfaceParams :: Type -> Type

Methods

from :: IfaceParams -> Rep IfaceParams x

to :: Rep IfaceParams x -> IfaceParams

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.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))))

data IfaceDecls Source #

Constructors

IfaceDecls 

Fields

Instances

Instances details
Show IfaceDecls Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> IfaceDecls -> ShowS

show :: IfaceDecls -> String

showList :: [IfaceDecls] -> ShowS

Generic IfaceDecls Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Associated Types

type Rep IfaceDecls :: Type -> Type

Methods

from :: IfaceDecls -> Rep IfaceDecls x

to :: Rep IfaceDecls x -> IfaceDecls

Semigroup IfaceDecls Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Monoid 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

type Rep IfaceDecls

genIface :: Module -> Iface Source #

Generate an Iface from a typechecked module.

data IfaceDecl Source #

Constructors

IfaceDecl 

Fields

Instances

Instances details
Show IfaceDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> IfaceDecl -> ShowS

show :: IfaceDecl -> String

showList :: [IfaceDecl] -> ShowS

Generic IfaceDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Interface

Associated Types

type Rep IfaceDecl :: Type -> Type

Methods

from :: IfaceDecl -> Rep IfaceDecl x

to :: Rep IfaceDecl x -> IfaceDecl

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-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 "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 String))))))