cryptol-2.6.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.ModuleSystem.Env

Description

 
Synopsis

Documentation

data ModuleEnv Source #

This is the current state of the interpreter.

Constructors

ModuleEnv 

Fields

Instances
Generic ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep ModuleEnv :: * -> * #

NFData ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: ModuleEnv -> () #

type Rep ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

data CoreLint Source #

Should we run the linter?

Constructors

NoCoreLint

Don't run core lint

CoreLint

Run core lint

Instances
Generic CoreLint Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep CoreLint :: * -> * #

Methods

from :: CoreLint -> Rep CoreLint x #

to :: Rep CoreLint x -> CoreLint #

NFData CoreLint Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: CoreLint -> () #

type Rep CoreLint Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep CoreLint = D1 (MetaData "CoreLint" "Cryptol.ModuleSystem.Env" "cryptol-2.6.0-24w5HMDd2znGLrodkM4xJM" False) (C1 (MetaCons "NoCoreLint" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "CoreLint" PrefixI False) (U1 :: * -> *))

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 -> (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 LoadedModules Source #

Constructors

LoadedModules 

Fields

Instances
Show LoadedModules Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Generic LoadedModules Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep LoadedModules :: * -> * #

Semigroup LoadedModules Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Monoid LoadedModules Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

NFData LoadedModules Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: LoadedModules -> () #

type Rep LoadedModules Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep LoadedModules = D1 (MetaData "LoadedModules" "Cryptol.ModuleSystem.Env" "cryptol-2.6.0-24w5HMDd2znGLrodkM4xJM" False) (C1 (MetaCons "LoadedModules" PrefixI True) (S1 (MetaSel (Just "lmLoadedModules") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [LoadedModule]) :*: S1 (MetaSel (Just "lmLoadedParamModules") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [LoadedModule])))

data LoadedModule Source #

Constructors

LoadedModule 

Fields

Instances
Show LoadedModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Generic LoadedModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep LoadedModule :: * -> * #

NFData LoadedModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: LoadedModule -> () #

type Rep LoadedModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

isLoaded :: ModName -> LoadedModules -> Bool Source #

Has this module been loaded already.

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

Try to find a previously loaded module

addLoadedModule :: FilePath -> FilePath -> 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.

Constructors

DEnv 
Instances
Generic DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep DynamicEnv :: * -> * #

Semigroup DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Monoid DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

NFData DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: DynamicEnv -> () #

type Rep DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

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.