| 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 :: ImpName Name -> 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 {}
- findEnv :: Name -> Iface -> ModuleG a -> Maybe (NamingEnv, Set Name)
- modContextOf :: ImpName Name -> 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]
- getLoadedField :: Ord a => (forall b. LoadedModuleG b -> a) -> LoadedModules -> Set a
- getLoadedNames :: LoadedModules -> Set ModName
- getLoadedIds :: LoadedModules -> Set String
- 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 :: ImpName Name -> LoadedModules -> Bool
- isLoadedStrict :: ImpName Name -> String -> LoadedModules -> Bool
- isLoadedParamMod :: ImpName Name -> LoadedModules -> Bool
- isLoadedInterface :: ImpName Name -> LoadedModules -> Bool
- loadedParamModDeps :: FreeVars a => LoadedModules -> a -> (Set TParam, Set Name)
- lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG TCTopEntity)
- lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
- lookupModuleWith :: (LoadedModule -> Bool) -> ModuleEnv -> Maybe LoadedModule
- lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature
- lookupSignatureWith :: (LoadedSignature -> Bool) -> 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 -> Map FilePath Fingerprint -> 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 :: ImpName Name -> 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 :: ImpName Name -> 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 #
getLoadedField :: Ord a => (forall b. LoadedModuleG b -> a) -> LoadedModules -> Set a Source #
getLoadedNames :: LoadedModules -> Set ModName Source #
getLoadedIds :: LoadedModules -> Set String 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
isLoadedStrict :: ImpName Name -> String -> LoadedModules -> Bool Source #
isLoadedParamMod :: ImpName Name -> LoadedModules -> Bool Source #
Is this a loaded parameterized module.
isLoadedInterface :: ImpName Name -> LoadedModules -> Bool Source #
Is this a loaded interface module.
loadedParamModDeps :: FreeVars a => LoadedModules -> a -> (Set TParam, Set Name) Source #
Return the set of type parameters (Set TParamSet NameLoadedModules value that another
definition (of type a) depends on.
lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG TCTopEntity) Source #
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule Source #
Try to find a previously loaded module
lookupModuleWith :: (LoadedModule -> Bool) -> ModuleEnv -> Maybe LoadedModule Source #
lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature Source #
lookupSignatureWith :: (LoadedSignature -> Bool) -> 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.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "FileInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "fiFingerprint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fingerprint) :*: S1 ('MetaSel ('Just "fiIncludeDeps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map FilePath Fingerprint))) :*: (S1 ('MetaSel ('Just "fiImportDeps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set ModName)) :*: S1 ('MetaSel ('Just "fiForeignDeps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map FilePath Bool))))) | |
fileInfo :: Fingerprint -> Map FilePath Fingerprint -> Set ModName -> Maybe ForeignSrc -> FileInfo Source #
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.