Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
Cryptol.ModuleSystem
Contents
Description
Synopsis
- data ModuleEnv = ModuleEnv {}
- initialModuleEnv :: IO ModuleEnv
- data DynamicEnv = DEnv {}
- 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
- 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 {}
- data IfaceParams = IfaceParams {}
- 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
This is the current state of the interpreter.
Constructors
ModuleEnv | |
Fields
|
Instances
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
.
Instances
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 # | |
Defined in Cryptol.ModuleSystem.Monad Methods showsPrec :: Int -> ModuleError -> ShowS # show :: ModuleError -> String # showList :: [ModuleError] -> ShowS # | |
NFData ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad Methods rnf :: ModuleError -> () # | |
PP ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad |
data ModuleWarning Source #
Constructors
TypeCheckWarnings [(Range, Warning)] | |
RenamerWarnings [RenamerWarning] |
Instances
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.
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.
Interfaces
The resulting interface generated by a module that has been typechecked.
Constructors
Iface | |
Fields
|
Instances
Show Iface Source # | |
Generic Iface Source # | |
NFData Iface Source # | |
Defined in Cryptol.ModuleSystem.Interface | |
type Rep Iface Source # | |
Defined in Cryptol.ModuleSystem.Interface type Rep Iface = D1 (MetaData "Iface" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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
data IfaceDecls Source #
Constructors
IfaceDecls | |
Fields
|
Instances
Show IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecls -> ShowS # show :: IfaceDecls -> String # showList :: [IfaceDecls] -> ShowS # | |
Generic IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceDecls :: Type -> Type # | |
Semigroup IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface Methods (<>) :: IfaceDecls -> IfaceDecls -> IfaceDecls # sconcat :: NonEmpty IfaceDecls -> IfaceDecls # stimes :: Integral b => b -> IfaceDecls -> IfaceDecls # | |
Monoid IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface Methods mempty :: IfaceDecls # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls # mconcat :: [IfaceDecls] -> IfaceDecls # | |
NFData IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecls -> () # | |
type Rep IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface |
type IfaceTySyn = TySyn Source #
Constructors
IfaceDecl | |
Fields
|
Instances
Show IfaceDecl Source # | |
Generic IfaceDecl Source # | |
NFData IfaceDecl Source # | |
Defined in Cryptol.ModuleSystem.Interface | |
type Rep IfaceDecl Source # | |
Defined in Cryptol.ModuleSystem.Interface type Rep IfaceDecl = D1 (MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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)))))) |