Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe-Inferred |
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]
- | ExpandPropGuardsError ImportSource Error
- | NoIncludeErrors ImportSource [IncludeError]
- | TypeCheckingFailed ImportSource NameMap [(Range, Error)]
- | OtherFailure String
- | ModuleNameMismatch ModName (Located ModName)
- | DuplicateModuleName ModName FilePath FilePath
- | FFILoadErrors ModName [FFILoadError]
- | 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, TCTopEntity)
- loadModuleByName :: ModName -> ModuleCmd (ModulePath, TCTopEntity)
- checkModuleByPath :: FilePath -> ModuleCmd (ModulePath, TCTopEntity)
- checkExpr :: Expr PName -> ModuleCmd (Expr Name, Expr, Schema)
- evalExpr :: Expr -> ModuleCmd Value
- benchmarkExpr :: Double -> Expr -> ModuleCmd BenchmarkStats
- checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup], Map Name TySyn)
- 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
- type Iface = IfaceG ModName
- data IfaceG name = Iface {
- ifNames :: IfaceNames name
- ifParams :: FunctorParams
- ifDefines :: IfaceDecls
- data IfaceDecls = IfaceDecls {
- ifTySyns :: Map Name TySyn
- ifNominalTypes :: Map Name NominalType
- ifDecls :: Map Name IfaceDecl
- ifModules :: !(Map Name (IfaceNames Name))
- ifSignatures :: !(Map Name ModParamNames)
- ifFunctors :: !(Map Name (IfaceG Name))
- genIface :: ModuleG name -> IfaceG name
- data IfaceDecl = IfaceDecl {
- ifDeclName :: !Name
- ifDeclSig :: Schema
- ifDeclIsPrim :: !Bool
- ifDeclPragmas :: [Pragma]
- ifDeclInfix :: Bool
- ifDeclFixity :: Maybe Fixity
- ifDeclDoc :: Maybe Text
- getFileDependencies :: FilePath -> ModuleCmd (ModulePath, FileInfo)
- getModuleDependencies :: ModName -> ModuleCmd (ModulePath, FileInfo)
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 |
ExpandPropGuardsError ImportSource Error | Problems during the ExpandPropGuards 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 |
FFILoadErrors ModName [FFILoadError] | Errors loading foreign function implementations |
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 # | |
PP ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad | |
NFData ModuleError Source # | |
Defined in Cryptol.ModuleSystem.Monad rnf :: ModuleError -> () # |
data ModuleWarning Source #
Instances
type ModuleRes a = (Either ModuleError (a, ModuleEnv), [ModuleWarning]) Source #
data ModuleInput m Source #
ModuleInput | |
|
findModule :: ModName -> ModuleCmd ModulePath Source #
Find the file associated with a module name in the module search path.
loadModuleByPath :: FilePath -> ModuleCmd (ModulePath, TCTopEntity) Source #
Load the module contained in the given file.
loadModuleByName :: ModName -> ModuleCmd (ModulePath, TCTopEntity) Source #
Load the given parsed module.
checkModuleByPath :: FilePath -> ModuleCmd (ModulePath, TCTopEntity) Source #
Parse and typecheck a module, but don't evaluate or change the environment.
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.
benchmarkExpr :: Double -> Expr -> ModuleCmd BenchmarkStats Source #
Benchmark an expression.
checkDecls :: [TopDecl PName] -> ModuleCmd (NamingEnv, [DeclGroup], Map Name TySyn) 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
).
renameVar :: NamingEnv -> PName -> ModuleCmd Name Source #
Rename a *use* of a value name. The distinction between uses and binding is used to keep track of dependencies.
renameType :: NamingEnv -> PName -> ModuleCmd Name Source #
Rename a *use* of a type name. The distinction between uses and binding is used to keep track of dependencies.
Interfaces
The interface repersenting a typecheck top-level module.
Iface | |
|
Instances
Generic (IfaceG name) Source # | |
Show name => Show (IfaceG name) Source # | |
NFData name => NFData (IfaceG name) Source # | |
Defined in Cryptol.ModuleSystem.Interface | |
type Rep (IfaceG name) Source # | |
Defined in Cryptol.ModuleSystem.Interface type Rep (IfaceG name) = D1 ('MetaData "IfaceG" "Cryptol.ModuleSystem.Interface" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "Iface" 'PrefixI 'True) (S1 ('MetaSel ('Just "ifNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IfaceNames name)) :*: (S1 ('MetaSel ('Just "ifParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunctorParams) :*: S1 ('MetaSel ('Just "ifDefines") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceDecls)))) |
data IfaceDecls Source #
Declarations in a module. Note that this includes things from nested
modules, but not things from nested functors, which are in ifFunctors
.
IfaceDecls | |
|
Instances
IfaceDecl | |
|
Instances
Dependencies
getFileDependencies :: FilePath -> ModuleCmd (ModulePath, FileInfo) Source #
Get information about the dependencies of a file.
getModuleDependencies :: ModName -> ModuleCmd (ModulePath, FileInfo) Source #
Get information about the dependencies of a module.