cryptol-2.2.6: Cryptol: The Language of Cryptography

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

Cryptol.ModuleSystem

Contents

- Module System
- Interfaces

Description

Synopsis

- data ModuleEnv = ModuleEnv {
  - meLoadedModules :: LoadedModules
  - meNameSeeds :: NameSeeds
  - meEvalEnv :: EvalEnv
  - meFocusedModule :: Maybe ModName
  - meSearchPath :: [FilePath]
  - meDynEnv :: DynamicEnv
  - meMonoBinds :: !Bool
  }
- initialModuleEnv :: IO ModuleEnv
- data DynamicEnv = DEnv {
  - deNames :: NamingEnv
  - deDecls :: [DeclGroup]
  - deEnv :: EvalEnv
  }
- data ModuleError
  - = ModuleNotFound ModName [FilePath]
  - | CantFindFile FilePath
  - | OtherIOError FilePath IOException
  - | ModuleParseError FilePath 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
- data ModuleWarning
  - = TypeCheckWarnings [(Range, Warning)]
  - | RenamerWarnings [RenamerWarning]
- type ModuleCmd a = ModuleEnv -> IO (ModuleRes a)
- type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- findModule :: ModName -> ModuleCmd FilePath
- loadModuleByPath :: FilePath -> ModuleCmd Module
- loadModule :: FilePath -> Module -> ModuleCmd Module
- checkExpr :: Expr -> ModuleCmd (Expr, Schema)
- evalExpr :: Expr -> ModuleCmd Value
- checkDecls :: (HasLoc d, Rename d, FromDecl d) => [d] -> ModuleCmd [DeclGroup]
- evalDecls :: [DeclGroup] -> ModuleCmd ()
- noPat :: RemovePatterns a => a -> ModuleCmd a
- focusedEnv :: ModuleEnv -> IfaceDecls
- data Iface = Iface {
  - ifModName :: ModName
  - ifPublic :: IfaceDecls
  - ifPrivate :: IfaceDecls
  }
- data IfaceDecls = IfaceDecls {
  - ifTySyns :: Map QName [IfaceTySyn]
  - ifNewtypes :: Map QName [IfaceNewtype]
  - ifDecls :: Map QName [IfaceDecl]
  }
- genIface :: Module -> Iface
- type IfaceTySyn = TySyn
- data IfaceDecl = IfaceDecl {
  - ifDeclName :: QName
  - ifDeclSig :: Schema
  - ifDeclPragmas :: [Pragma]
  }

# Module System

data ModuleEnv Source

Constructors

ModuleEnv |

Fields

meLoadedModules :: LoadedModules
meNameSeeds :: NameSeeds
meEvalEnv :: EvalEnv
meFocusedModule :: Maybe ModName
meSearchPath :: [FilePath]
meDynEnv :: DynamicEnv
meMonoBinds :: !Bool

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

Monoid DynamicEnv Source |

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

Instances

Show ModuleError Source |
PP ModuleError Source |

data ModuleWarning Source

Constructors

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

Instances

Show ModuleWarning Source |
PP ModuleWarning Source |

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

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

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 -> ModuleCmd Module Source

Load the given parsed module.

checkExpr :: Expr -> ModuleCmd (Expr, Schema) Source

Check the type of an expression.

evalExpr :: Expr -> ModuleCmd Value Source

Evaluate an expression.

checkDecls :: (HasLoc d, Rename d, FromDecl d) => [d] -> ModuleCmd [DeclGroup] Source

Typecheck declarations.

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

Evaluate declarations and add them to the extended environment.

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

focusedEnv :: ModuleEnv -> IfaceDecls Source

Produce an ifaceDecls that represents the focused environment of the module system.

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

# Interfaces

data Iface Source

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

Constructors

Iface |

Fields

ifModName :: ModName
ifPublic :: IfaceDecls
ifPrivate :: IfaceDecls

Instances

Show Iface Source |
BindsNames Iface Source | Produce a naming environment from an interface file, that contains a mapping only from unqualified names to qualified ones.

data IfaceDecls Source

Constructors

IfaceDecls |

Fields

ifTySyns :: Map QName [IfaceTySyn]
ifNewtypes :: Map QName [IfaceNewtype]
ifDecls :: Map QName [IfaceDecl]

Instances

Show IfaceDecls Source |
Monoid IfaceDecls Source |
BindsNames IfaceDecls Source | Translate a set of declarations from an interface into a naming environment.

genIface :: Module -> Iface Source

Generate an Iface from a typechecked module.

type IfaceTySyn = TySyn Source

data IfaceDecl Source

Constructors

IfaceDecl |

Fields

ifDeclName :: QName
ifDeclSig :: Schema
ifDeclPragmas :: [Pragma]

Instances

Show IfaceDecl Source |