| 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 NameMap [(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 = ModuleInput IO -> IO (ModuleRes a)
- type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning])
- data ModuleInput m = ModuleInput {
- minpCallStacks :: Bool
- minpEvalOpts :: m EvalOpts
- minpByteReader :: FilePath -> m ByteString
- minpModuleEnv :: ModuleEnv
- minpTCSolver :: Solver
- 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 -> ModContext
- 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 Text
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 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 |
| 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 NameMap [(Range, Warning)] | |
| RenamerWarnings [RenamerWarning] |
Instances
type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning]) Source #
data ModuleInput m Source #
Constructors
| ModuleInput | |
Fields
| |
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 -> 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).
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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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
| |