| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Cryptol.ModuleSystem.Env
Description
Synopsis
- data ModuleEnv = ModuleEnv {}
- data CoreLint
- resetModuleEnv :: ModuleEnv -> ModuleEnv
- initialModuleEnv :: IO ModuleEnv
- focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv
- loadedModules :: ModuleEnv -> [Module]
- loadedNonParamModules :: ModuleEnv -> [Module]
- hasParamModules :: ModuleEnv -> Bool
- allDeclGroups :: ModuleEnv -> [DeclGroup]
- data ModContext = ModContext {}
- data DeclProvenance
- focusedEnv :: ModuleEnv -> ModContext
- data ModulePath
- modulePathLabel :: ModulePath -> String
- data LoadedModules = LoadedModules {}
- getLoadedModules :: LoadedModules -> [LoadedModule]
- data LoadedModule = LoadedModule {}
- isLoaded :: ModName -> LoadedModules -> Bool
- isLoadedParamMod :: ModName -> LoadedModules -> Bool
- lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
- addLoadedModule :: ModulePath -> String -> Fingerprint -> Module -> LoadedModules -> LoadedModules
- removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules
- data DynamicEnv = DEnv {}
- deIfaceDecls :: DynamicEnv -> IfaceDecls
Documentation
This is the current state of the interpreter.
Constructors
| ModuleEnv | |
Fields
| |
Instances
Should we run the linter?
Constructors
| NoCoreLint | Don't run core lint |
| CoreLint | Run core lint |
resetModuleEnv :: ModuleEnv -> ModuleEnv Source #
focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv Source #
Try to focus a loaded module in the module environment.
loadedModules :: ModuleEnv -> [Module] Source #
Get a list of all the loaded modules. Each module in the resulting list depends only on other modules that precede it. Note that this includes parameterized modules.
loadedNonParamModules :: ModuleEnv -> [Module] Source #
Get a list of all the loaded non-parameterized modules. These are the modules that can be used for evaluation, proving etc.
hasParamModules :: ModuleEnv -> Bool Source #
Are any parameterized modules loaded?
allDeclGroups :: ModuleEnv -> [DeclGroup] Source #
data ModContext Source #
Contains enough information to browse what's in scope, or type check new expressions.
Constructors
| ModContext | |
Fields | |
data DeclProvenance Source #
Specifies how a declared name came to be in scope.
Constructors
| NameIsImportedFrom ModName | |
| NameIsLocalPublic | |
| NameIsLocalPrivate | |
| NameIsParameter | |
| NameIsDynamicDecl |
Instances
| Eq DeclProvenance Source # | |
Defined in Cryptol.ModuleSystem.Env Methods (==) :: DeclProvenance -> DeclProvenance -> Bool # (/=) :: DeclProvenance -> DeclProvenance -> Bool # | |
| Ord DeclProvenance Source # | |
Defined in Cryptol.ModuleSystem.Env Methods compare :: DeclProvenance -> DeclProvenance -> Ordering # (<) :: DeclProvenance -> DeclProvenance -> Bool # (<=) :: DeclProvenance -> DeclProvenance -> Bool # (>) :: DeclProvenance -> DeclProvenance -> Bool # (>=) :: DeclProvenance -> DeclProvenance -> Bool # max :: DeclProvenance -> DeclProvenance -> DeclProvenance # min :: DeclProvenance -> DeclProvenance -> DeclProvenance # | |
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).
data ModulePath Source #
The location of a module
Constructors
| InFile FilePath | |
| InMem String ByteString | Label, content |
Instances
modulePathLabel :: ModulePath -> String Source #
The name of the content---either the file path, or the provided label.
data LoadedModules Source #
Constructors
| LoadedModules | |
Fields
| |
Instances
getLoadedModules :: LoadedModules -> [LoadedModule] Source #
data LoadedModule Source #
Constructors
| LoadedModule | |
Fields
| |
Instances
isLoadedParamMod :: ModName -> LoadedModules -> Bool Source #
Is this a loaded parameterized module.
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule Source #
Try to find a previously loaded module
addLoadedModule :: ModulePath -> String -> Fingerprint -> Module -> LoadedModules -> LoadedModules Source #
Add a freshly loaded module. If it was previously loaded, then the new version is ignored.
removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules Source #
Remove a previously loaded module.
Note that this removes exactly the modules specified by the predicate.
One should be carfule to preserve the invariant on LoadedModules.
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
deIfaceDecls :: DynamicEnv -> IfaceDecls Source #
Build IfaceDecls that correspond to all of the bindings in the
dynamic environment.
XXX: if we ever add type synonyms or newtypes at the REPL, revisit this.