cryptol-2.8.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | None
Language | Haskell2010

Cryptol.ModuleSystem

Contents

- Module System
- Interfaces

Description

Synopsis

- data ModuleEnv = ModuleEnv {
  - meLoadedModules :: LoadedModules
  - meNameSeeds :: NameSeeds
  - meSolverConfig :: SolverConfig
  - meEvalEnv :: EvalEnv
  - meCoreLint :: CoreLint
  - meMonoBinds :: !Bool
  - meFocusedModule :: Maybe ModName
  - meSearchPath :: [FilePath]
  - meDynEnv :: DynamicEnv
  - meSupply :: !Supply
  }
- initialModuleEnv :: IO ModuleEnv
- data DynamicEnv = DEnv {
  - deNames :: NamingEnv
  - deDecls :: [DeclGroup]
  - deEnv :: EvalEnv
  }
- data ModuleError
  - = ModuleNotFound ModName [FilePath]
  - | CantFindFile FilePath
  - | BadUtf8 ModulePath UnicodeException
  - | OtherIOError FilePath IOException
  - | ModuleParseError ModulePath ParseError
  - | RecursiveModules [ImportSource]
  - | RenamerErrors ImportSource [RenamerError]
  - | NoPatErrors ImportSource [Error]
  - | NoIncludeErrors ImportSource [IncludeError]
  - | TypeCheckingFailed ImportSource [(Range, Error)]
  - | OtherFailure String
  - | ModuleNameMismatch ModName (Located ModName)
  - | DuplicateModuleName ModName FilePath FilePath
  - | ImportedParamModule ModName
  - | FailedToParameterizeModDefs ModName [Name]
  - | NotAParameterizedModule ModName
  - | ErrorInFile ModulePath ModuleError
- data ModuleWarning
  - = TypeCheckWarnings [(Range, Warning)]
  - | RenamerWarnings [RenamerWarning]
- type ModuleCmd a = (EvalOpts, ModuleEnv) -> IO (ModuleRes a)
- type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- findModule :: ModName -> ModuleCmd ModulePath
- loadModuleByPath :: FilePath -> ModuleCmd (ModulePath, Module)
- loadModuleByName :: ModName -> ModuleCmd (ModulePath, Module)
- checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema)
- evalExpr :: Expr -> ModuleCmd Value
- checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup])
- evalDecls :: [DeclGroup] -> ModuleCmd ()
- noPat :: RemovePatterns a => a -> ModuleCmd a
- focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
- getPrimMap :: ModuleCmd PrimMap
- renameVar :: NamingEnv -> PName -> ModuleCmd Name
- renameType :: NamingEnv -> PName -> ModuleCmd Name
- data Iface = Iface {
  - ifModName :: !ModName
  - ifPublic :: IfaceDecls
  - ifPrivate :: IfaceDecls
  - ifParams :: IfaceParams
  }
- data IfaceParams = IfaceParams {
  - ifParamTypes :: Map Name ModTParam
  - ifParamConstraints :: [Located Prop]
  - ifParamFuns :: Map Name ModVParam
  }
- data IfaceDecls = IfaceDecls {
  - ifTySyns :: Map Name IfaceTySyn
  - ifNewtypes :: Map Name IfaceNewtype
  - ifAbstractTypes :: Map Name IfaceAbstractType
  - ifDecls :: Map Name IfaceDecl
  }
- genIface :: Module -> Iface
- type IfaceTySyn = TySyn
- data IfaceDecl = IfaceDecl {
  - ifDeclName :: !Name
  - ifDeclSig :: Schema
  - ifDeclPragmas :: [Pragma]
  - ifDeclInfix :: Bool
  - ifDeclFixity :: Maybe Fixity
  - ifDeclDoc :: Maybe String
  }

# 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 Source # Methods from :: ModuleEnv -> Rep ModuleEnv x Source # to :: Rep ModuleEnv x -> ModuleEnv Source #
NFData ModuleEnv Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods rnf :: ModuleEnv -> () Source #
type Rep ModuleEnv Source # |

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep ModuleEnv = D1 ('MetaData "ModuleEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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))))))

initialModuleEnv :: IO 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`.

Constructors

DEnv |

Fields

- deNames :: NamingEnv
- deDecls :: [DeclGroup]
- deEnv :: EvalEnv

#### Instances

Instances details

Generic DynamicEnv Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Associated Types type Rep DynamicEnv :: Type -> Type Source # Methods from :: DynamicEnv -> Rep DynamicEnv x Source # to :: Rep DynamicEnv x -> DynamicEnv Source #
Semigroup DynamicEnv Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods (<>) :: DynamicEnv -> DynamicEnv -> DynamicEnv Source # sconcat :: NonEmpty DynamicEnv -> DynamicEnv Source # stimes :: Integral b => b -> DynamicEnv -> DynamicEnv Source #
Monoid DynamicEnv Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods mempty :: DynamicEnv Source # mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv Source # mconcat :: [DynamicEnv] -> DynamicEnv Source #
NFData DynamicEnv Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods rnf :: DynamicEnv -> () Source #
type Rep DynamicEnv Source # |

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep DynamicEnv = D1 ('MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source # show :: ModuleError -> String Source # showList :: [ModuleError] -> ShowS Source #
NFData ModuleError Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleError -> () Source #
PP ModuleError Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods ppPrec :: Int -> ModuleError -> Doc Source #

data ModuleWarning Source #

Constructors

TypeCheckWarnings [(Range, Warning)] |
RenamerWarnings [RenamerWarning] |

#### Instances

Instances details

Show ModuleWarning Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleWarning -> ShowS Source # show :: ModuleWarning -> String Source # showList :: [ModuleWarning] -> ShowS Source #
Generic ModuleWarning Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Associated Types type Rep ModuleWarning :: Type -> Type Source # Methods from :: ModuleWarning -> Rep ModuleWarning x Source # to :: Rep ModuleWarning x -> ModuleWarning Source #
NFData ModuleWarning Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleWarning -> () Source #
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-11Z6ZaBuQbo1UTYpHYMeUg" '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])))

type ModuleCmd a = (EvalOpts, ModuleEnv) -> IO (ModuleRes a) Source #

type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning]) Source #

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.

noPat :: RemovePatterns a => a -> ModuleCmd a Source #

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.

getPrimMap :: ModuleCmd PrimMap Source #

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

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

# Interfaces

data Iface Source #

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

Constructors

Iface |

Fields

- ifModName :: !ModName

  Module name

- ifPublic :: IfaceDecls

  Exported definitions

- ifPrivate :: IfaceDecls

  Private defintiions

- ifParams :: IfaceParams

  Uninterpreted constants (aka module params)

#### Instances

Instances details

Show Iface Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> Iface -> ShowS Source # show :: Iface -> String Source # showList :: [Iface] -> ShowS Source #
Generic Iface Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep Iface :: Type -> Type Source # Methods from :: Iface -> Rep Iface x Source # to :: Rep Iface x -> Iface Source #
NFData Iface Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: Iface -> () Source #
type Rep Iface Source # |

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep Iface = D1 ('MetaData "Iface" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

- ifParamTypes :: Map Name ModTParam
- ifParamConstraints :: [Located Prop]

  Constraints on param. types

- ifParamFuns :: Map Name ModVParam

#### Instances

Instances details

Show IfaceParams Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceParams -> ShowS Source # show :: IfaceParams -> String Source # showList :: [IfaceParams] -> ShowS Source #
Generic IfaceParams Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceParams :: Type -> Type Source # Methods from :: IfaceParams -> Rep IfaceParams x Source # to :: Rep IfaceParams x -> IfaceParams Source #
NFData IfaceParams Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceParams -> () Source #
type Rep IfaceParams Source # |

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceParams = D1 ('MetaData "IfaceParams" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

- ifTySyns :: Map Name IfaceTySyn
- ifNewtypes :: Map Name IfaceNewtype
- ifAbstractTypes :: Map Name IfaceAbstractType
- ifDecls :: Map Name IfaceDecl

#### Instances

Instances details

Show IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecls -> ShowS Source # show :: IfaceDecls -> String Source # showList :: [IfaceDecls] -> ShowS Source #
Generic IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceDecls :: Type -> Type Source # Methods from :: IfaceDecls -> Rep IfaceDecls x Source # to :: Rep IfaceDecls x -> IfaceDecls Source #
Semigroup IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods (<>) :: IfaceDecls -> IfaceDecls -> IfaceDecls Source # sconcat :: NonEmpty IfaceDecls -> IfaceDecls Source # stimes :: Integral b => b -> IfaceDecls -> IfaceDecls Source #
Monoid IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods mempty :: IfaceDecls Source # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls Source # mconcat :: [IfaceDecls] -> IfaceDecls Source #
NFData IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecls -> () Source #
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.

type IfaceTySyn = TySyn Source #

data IfaceDecl Source #

Constructors

IfaceDecl |

Fields

- ifDeclName :: !Name

  Name of thing

- ifDeclSig :: Schema

  Type

- ifDeclPragmas :: [Pragma]

  Pragmas

- ifDeclInfix :: Bool

  Is this an infix thing

- ifDeclFixity :: Maybe Fixity

  Fixity information

- ifDeclDoc :: Maybe String

  Documentation

#### Instances

Instances details

Show IfaceDecl Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecl -> ShowS Source # show :: IfaceDecl -> String Source # showList :: [IfaceDecl] -> ShowS Source #
Generic IfaceDecl Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceDecl :: Type -> Type Source # Methods from :: IfaceDecl -> Rep IfaceDecl x Source # to :: Rep IfaceDecl x -> IfaceDecl Source #
NFData IfaceDecl Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecl -> () Source #
type Rep IfaceDecl Source # |

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceDecl = D1 ('MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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))))))