Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
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 = (EvalOpts, FilePath -> IO ByteString, 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 -> 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.
ModuleEnv | |
|
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 #
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 showsPrec :: Int -> ModuleError -> ShowS # show :: ModuleError -> String # showList :: [ModuleError] -> ShowS # | |
NFData ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad rnf :: ModuleError -> () # | |
PP ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad |
data ModuleWarning Source #
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 -> 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.
Iface | |
|
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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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 #
IfaceParams | |
|
Instances
data IfaceDecls Source #
IfaceDecls | |
|
Instances
Show IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface showsPrec :: Int -> IfaceDecls -> ShowS # show :: IfaceDecls -> String # showList :: [IfaceDecls] -> ShowS # | |
Generic IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface type Rep IfaceDecls :: Type -> Type # from :: IfaceDecls -> Rep IfaceDecls x # to :: Rep IfaceDecls x -> IfaceDecls # | |
Semigroup IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface (<>) :: IfaceDecls -> IfaceDecls -> IfaceDecls # sconcat :: NonEmpty IfaceDecls -> IfaceDecls # stimes :: Integral b => b -> IfaceDecls -> IfaceDecls # | |
Monoid IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface mempty :: IfaceDecls # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls # mconcat :: [IfaceDecls] -> IfaceDecls # | |
NFData IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface rnf :: IfaceDecls -> () # | |
type Rep IfaceDecls Source # | |
Defined in Cryptol.ModuleSystem.Interface |
type IfaceTySyn = TySyn Source #
IfaceDecl | |
|