Copyright	(c) 2013-2016 Galois, Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell98

Cryptol.ModuleSystem.Env

Description

Synopsis

Documentation

data ModuleEnv Source

Constructors

ModuleEnv
Fields meLoadedModules :: LoadedModules meNameSeeds :: NameSeeds meEvalEnv :: EvalEnv meFocusedModule :: Maybe ModName meSearchPath :: [FilePath] meDynEnv :: DynamicEnv meMonoBinds :: !Bool meSolverConfig :: SolverConfig meCoreLint :: CoreLint meSupply :: !Supply

Instances

Generic ModuleEnv Source
NFData ModuleEnv Source
type Rep ModuleEnv Source

data CoreLint Source

Constructors

NoCoreLint	Don't run core lint
CoreLint	Run core lint

Instances

Generic CoreLint Source
NFData CoreLint Source
type Rep CoreLint Source

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.

focusedEnv :: ModuleEnv -> (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.

dynamicEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp) Source

The unqualified declarations and name environment for the dynamic environment.

qualifiedEnv :: ModuleEnv -> IfaceDecls Source

Retrieve all IfaceDecls referenced by a module, as well as all of its public and private declarations, checking expressions

newtype LoadedModules Source

Invariant: All the dependencies of any module m must precede m in the list.

Constructors

LoadedModules
Fields getLoadedModules :: [LoadedModule]

Instances

Show LoadedModules Source
Generic LoadedModules Source
Monoid LoadedModules Source
NFData LoadedModules Source
type Rep LoadedModules Source

data LoadedModule Source

Constructors

LoadedModule
Fields lmName :: ModName lmFilePath :: FilePath lmInterface :: Iface lmModule :: Module

Instances

Show LoadedModule Source
Generic LoadedModule Source
NFData LoadedModule Source
type Rep LoadedModule Source

isLoaded :: ModName -> LoadedModules -> Bool Source

lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule Source

addLoadedModule :: FilePath -> Module -> LoadedModules -> LoadedModules Source

removeLoadedModule :: FilePath -> LoadedModules -> LoadedModules 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
Fields deNames :: NamingEnv deDecls :: [DeclGroup] deEnv :: EvalEnv

Instances

Generic DynamicEnv Source
Monoid DynamicEnv Source
NFData DynamicEnv Source
type Rep DynamicEnv Source

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.