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 {
- meLoadedModules :: LoadedModules
- meNameSeeds :: NameSeeds
- meSolverConfig :: SolverConfig
- meEvalEnv :: EvalEnv
- meCoreLint :: CoreLint
- meMonoBinds :: !Bool
- meFocusedModule :: Maybe ModName
- meSearchPath :: [FilePath]
- meDynEnv :: DynamicEnv
- meSupply :: !Supply
- 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
Generic ModuleEnv Source # | |
NFData ModuleEnv Source # | |
Defined in Cryptol.ModuleSystem.Env | |
type Rep ModuleEnv Source # | |
Defined in Cryptol.ModuleSystem.Env type Rep ModuleEnv = D1 ('MetaData "ModuleEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "ModuleEnv" 'PrefixI 'True) (((S1 ('MetaSel ('Just "meLoadedModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LoadedModules) :*: S1 ('MetaSel ('Just "meNameSeeds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameSeeds)) :*: (S1 ('MetaSel ('Just "meSolverConfig") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SolverConfig) :*: (S1 ('MetaSel ('Just "meEvalEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EvalEnv) :*: S1 ('MetaSel ('Just "meCoreLint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoreLint)))) :*: ((S1 ('MetaSel ('Just "meMonoBinds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :*: S1 ('MetaSel ('Just "meFocusedModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "meSearchPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :*: (S1 ('MetaSel ('Just "meDynEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DynamicEnv) :*: S1 ('MetaSel ('Just "meSupply") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Supply)))))) |
Should we run the linter?
Constructors
NoCoreLint | Don't run core lint |
CoreLint | Run core lint |
Instances
Generic CoreLint Source # | |
NFData CoreLint Source # | |
Defined in Cryptol.ModuleSystem.Env | |
type Rep CoreLint Source # | |
Defined in Cryptol.ModuleSystem.Env type Rep CoreLint = D1 ('MetaData "CoreLint" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "NoCoreLint" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoreLint" 'PrefixI 'False) (U1 :: Type -> Type)) |
resetModuleEnv :: ModuleEnv -> ModuleEnv Source #
initialModuleEnv :: IO 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
Instances
Eq ModulePath Source # | In-memory things are compared by label. |
Defined in Cryptol.ModuleSystem.Env | |
Show ModulePath Source # | |
Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> ModulePath -> ShowS show :: ModulePath -> String showList :: [ModulePath] -> ShowS | |
Generic ModulePath Source # | |
Defined in Cryptol.ModuleSystem.Env Associated Types type Rep ModulePath :: Type -> Type | |
NFData ModulePath Source # | |
Defined in Cryptol.ModuleSystem.Env Methods rnf :: ModulePath -> () | |
PP ModulePath Source # | |
Defined in Cryptol.ModuleSystem.Env Methods ppPrec :: Int -> ModulePath -> Doc Source # | |
type Rep ModulePath Source # | |
Defined in Cryptol.ModuleSystem.Env type Rep ModulePath = D1 ('MetaData "ModulePath" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "InFile" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath)) :+: C1 ('MetaCons "InMem" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ByteString))) |
modulePathLabel :: ModulePath -> String Source #
The name of the content---either the file path, or the provided label.
data LoadedModules Source #
Constructors
LoadedModules | |
Fields
|
Instances
Show LoadedModules Source # | |
Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> LoadedModules -> ShowS show :: LoadedModules -> String showList :: [LoadedModules] -> ShowS | |
Generic LoadedModules Source # | |
Defined in Cryptol.ModuleSystem.Env Associated Types type Rep LoadedModules :: Type -> Type | |
Semigroup LoadedModules Source # | |
Defined in Cryptol.ModuleSystem.Env Methods (<>) :: LoadedModules -> LoadedModules -> LoadedModules # sconcat :: NonEmpty LoadedModules -> LoadedModules # stimes :: Integral b => b -> LoadedModules -> LoadedModules # | |
Monoid LoadedModules Source # | |
Defined in Cryptol.ModuleSystem.Env Methods mempty :: LoadedModules # mappend :: LoadedModules -> LoadedModules -> LoadedModules # mconcat :: [LoadedModules] -> LoadedModules # | |
NFData LoadedModules Source # | |
Defined in Cryptol.ModuleSystem.Env Methods rnf :: LoadedModules -> () | |
type Rep LoadedModules Source # | |
Defined in Cryptol.ModuleSystem.Env type Rep LoadedModules = D1 ('MetaData "LoadedModules" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "LoadedModules" 'PrefixI 'True) (S1 ('MetaSel ('Just "lmLoadedModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LoadedModule]) :*: S1 ('MetaSel ('Just "lmLoadedParamModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LoadedModule]))) |
getLoadedModules :: LoadedModules -> [LoadedModule] Source #
data LoadedModule Source #
Constructors
LoadedModule | |
Fields
|
Instances
Show LoadedModule Source # | |
Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> LoadedModule -> ShowS show :: LoadedModule -> String showList :: [LoadedModule] -> ShowS | |
Generic LoadedModule Source # | |
Defined in Cryptol.ModuleSystem.Env Associated Types type Rep LoadedModule :: Type -> Type | |
NFData LoadedModule Source # | |
Defined in Cryptol.ModuleSystem.Env Methods rnf :: LoadedModule -> () | |
type Rep LoadedModule Source # | |
Defined in Cryptol.ModuleSystem.Env type Rep LoadedModule = D1 ('MetaData "LoadedModule" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "LoadedModule" 'PrefixI 'True) ((S1 ('MetaSel ('Just "lmName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModName) :*: (S1 ('MetaSel ('Just "lmFilePath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModulePath) :*: S1 ('MetaSel ('Just "lmModuleId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :*: (S1 ('MetaSel ('Just "lmInterface") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Iface) :*: (S1 ('MetaSel ('Just "lmModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Module) :*: S1 ('MetaSel ('Just "lmFingerprint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fingerprint))))) |
isLoaded :: ModName -> LoadedModules -> Bool Source #
Has this module been loaded already.
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
Generic DynamicEnv Source # | |
Defined in Cryptol.ModuleSystem.Env Associated Types type Rep DynamicEnv :: Type -> Type | |
Semigroup DynamicEnv Source # | |
Defined in Cryptol.ModuleSystem.Env Methods (<>) :: DynamicEnv -> DynamicEnv -> DynamicEnv # sconcat :: NonEmpty DynamicEnv -> DynamicEnv # stimes :: Integral b => b -> DynamicEnv -> DynamicEnv # | |
Monoid DynamicEnv Source # | |
Defined in Cryptol.ModuleSystem.Env Methods mempty :: DynamicEnv # mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv # mconcat :: [DynamicEnv] -> DynamicEnv # | |
NFData DynamicEnv Source # | |
Defined in Cryptol.ModuleSystem.Env Methods rnf :: DynamicEnv -> () | |
type Rep DynamicEnv Source # | |
Defined in Cryptol.ModuleSystem.Env type Rep DynamicEnv = D1 ('MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "DEnv" 'PrefixI 'True) (S1 ('MetaSel ('Just "deNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamingEnv) :*: (S1 ('MetaSel ('Just "deDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DeclGroup]) :*: S1 ('MetaSel ('Just "deEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EvalEnv)))) |
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.