| 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
- focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
- dynamicEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)
- 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?
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.
dynamicEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp) Source #
The unqualified declarations and name environment for the dynamic environment.
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.
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.