cryptol-2.8.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
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 :: Type -> Type #

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 :: Type -> Type #

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.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" False) (C1 (MetaCons "NoCoreLint" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "CoreLint" PrefixI False) (U1 :: Type -> Type))

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

Constructors

InFile FilePath 
InMem String ByteString

Label, content

Instances
Eq ModulePath Source #

In-memory things are compared by label.

Instance details

Defined in Cryptol.ModuleSystem.Env

Show ModulePath Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Generic ModulePath Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep ModulePath :: Type -> Type #

NFData ModulePath Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: ModulePath -> () #

PP ModulePath Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

ppPrec :: Int -> ModulePath -> Doc Source #

type Rep ModulePath Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

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 # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Generic LoadedModules Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep LoadedModules :: Type -> Type #

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.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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

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.

Constructors

DEnv 
Instances
Generic DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep DynamicEnv :: Type -> Type #

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.