| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Cryptol.ModuleSystem.Env
Description
Synopsis
- data ModuleEnv = ModuleEnv {}
- data CoreLint
- data EvalForeignPolicy
- defaultEvalForeignPolicy :: EvalForeignPolicy
- resetModuleEnv :: ModuleEnv -> IO ModuleEnv
- initialModuleEnv :: IO ModuleEnv
- focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv
- loadedModules :: ModuleEnv -> [Module]
- loadedNonParamModules :: ModuleEnv -> [Module]
- loadedNominalTypes :: ModuleEnv -> Map Name NominalType
- hasParamModules :: ModuleEnv -> Bool
- allDeclGroups :: ModuleEnv -> [DeclGroup]
- data ModContextParams
- modContextParamNames :: ModContextParams -> ModParamNames
- data ModContext = ModContext {}
- modContextOf :: ModName -> ModuleEnv -> Maybe ModContext
- dynModContext :: ModuleEnv -> ModContext
- focusedEnv :: ModuleEnv -> ModContext
- data ModulePath
- modulePathLabel :: ModulePath -> String
- data LoadedModules = LoadedModules {}
- data LoadedEntity
- getLoadedEntities :: LoadedModules -> Map ModName LoadedEntity
- getLoadedModules :: LoadedModules -> [LoadedModule]
- getLoadedNames :: LoadedModules -> Set ModName
- data LoadedModuleG a = LoadedModule {
- lmName :: ModName
- lmFilePath :: ModulePath
- lmModuleId :: String
- lmNamingEnv :: !NamingEnv
- lmFileInfo :: !FileInfo
- lmData :: a
- type LoadedModule = LoadedModuleG LoadedModuleData
- lmModule :: LoadedModule -> Module
- lmInterface :: LoadedModule -> Iface
- data LoadedModuleData = LoadedModuleData {}
- type LoadedSignature = LoadedModuleG ModParamNames
- isLoaded :: ModName -> LoadedModules -> Bool
- isLoadedParamMod :: ModName -> LoadedModules -> Bool
- isLoadedInterface :: ModName -> LoadedModules -> Bool
- lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG TCTopEntity)
- lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
- lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature
- addLoadedSignature :: ModulePath -> String -> FileInfo -> NamingEnv -> ModName -> ModParamNames -> LoadedModules -> LoadedModules
- addLoadedModule :: ModulePath -> String -> FileInfo -> NamingEnv -> Maybe ForeignSrc -> Module -> LoadedModules -> LoadedModules
- removeLoadedModule :: (forall a. LoadedModuleG a -> Bool) -> LoadedModules -> LoadedModules
- data FileInfo = FileInfo {}
- fileInfo :: Fingerprint -> Set FilePath -> Set ModName -> Maybe ForeignSrc -> FileInfo
- 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 |
data EvalForeignPolicy Source #
How to evaluate foreign bindings.
Constructors
| AlwaysEvalForeign | Use foreign implementation and report an error at module load time if it is unavailable. |
| PreferEvalForeign | Use foreign implementation by default, and when unavailable, fall back to cryptol implementation if present and report runtime error otherwise. |
| NeverEvalForeign | Always use cryptol implementation if present, and report runtime error otherwise. |
Instances
| Eq EvalForeignPolicy Source # | |
Defined in Cryptol.ModuleSystem.Env Methods (==) :: EvalForeignPolicy -> EvalForeignPolicy -> Bool # (/=) :: EvalForeignPolicy -> EvalForeignPolicy -> Bool # | |
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 ModContextParams Source #
Constructors
| InterfaceParams ModParamNames | |
| FunctorParams FunctorParams | |
| NoParams |
data ModContext Source #
Contains enough information to browse what's in scope, or type check new expressions.
Constructors
| ModContext | |
Fields
| |
Instances
| Monoid ModContext Source # | |
Defined in Cryptol.ModuleSystem.Env Methods mempty :: ModContext # mappend :: ModContext -> ModContext -> ModContext # mconcat :: [ModContext] -> ModContext # | |
| Semigroup ModContext Source # | |
Defined in Cryptol.ModuleSystem.Env Methods (<>) :: ModContext -> ModContext -> ModContext # sconcat :: NonEmpty ModContext -> ModContext # stimes :: Integral b => b -> ModContext -> ModContext # | |
modContextOf :: ModName -> ModuleEnv -> Maybe ModContext Source #
dynModContext :: ModuleEnv -> ModContext 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).
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
data LoadedEntity Source #
getLoadedModules :: LoadedModules -> [LoadedModule] Source #
getLoadedNames :: LoadedModules -> Set ModName Source #
data LoadedModuleG a Source #
A generic type for loaded things. The things can be either modules or signatures.
Constructors
| LoadedModule | |
Fields
| |
Instances
lmModule :: LoadedModule -> Module Source #
lmInterface :: LoadedModule -> Iface Source #
data LoadedModuleData Source #
Constructors
| LoadedModuleData | |
Fields
| |
Instances
isLoadedParamMod :: ModName -> LoadedModules -> Bool Source #
Is this a loaded parameterized module.
isLoadedInterface :: ModName -> LoadedModules -> Bool Source #
Is this a loaded interface module.
lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG TCTopEntity) Source #
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule Source #
Try to find a previously loaded module
lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature Source #
addLoadedSignature :: ModulePath -> String -> FileInfo -> NamingEnv -> ModName -> ModParamNames -> LoadedModules -> LoadedModules Source #
addLoadedModule :: ModulePath -> String -> FileInfo -> NamingEnv -> Maybe ForeignSrc -> Module -> LoadedModules -> LoadedModules Source #
Add a freshly loaded module. If it was previously loaded, then the new version is ignored.
removeLoadedModule :: (forall a. LoadedModuleG a -> 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.
Constructors
| FileInfo | |
Fields | |
Instances
| Generic FileInfo Source # | |
| Show FileInfo Source # | |
| NFData FileInfo Source # | |
Defined in Cryptol.ModuleSystem.Env | |
| type Rep FileInfo Source # | |
Defined in Cryptol.ModuleSystem.Env type Rep FileInfo = D1 ('MetaData "FileInfo" "Cryptol.ModuleSystem.Env" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "FileInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "fiFingerprint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fingerprint) :*: S1 ('MetaSel ('Just "fiIncludeDeps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set FilePath))) :*: (S1 ('MetaSel ('Just "fiImportDeps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set ModName)) :*: S1 ('MetaSel ('Just "fiForeignDeps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map FilePath Bool))))) | |
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.
Constructors
| DEnv | |
Instances
deIfaceDecls :: DynamicEnv -> IfaceDecls Source #
Build IfaceDecls that correspond to all of the bindings in the
dynamic environment.
XXX: if we add newtypes, etc. at the REPL, revisit this.