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

Instances details
Generic ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep ModuleEnv :: Type -> Type Source #

NFData ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: ModuleEnv -> () Source #

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

Instances details
Generic CoreLint Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep CoreLint :: Type -> Type Source #

NFData CoreLint Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: CoreLint -> () Source #

type Rep CoreLint Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep CoreLint = D1 ('MetaData "CoreLint" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

Instances details
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 Source #

NFData ModulePath Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: ModulePath -> () Source #

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

Instances details
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 Source #

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

type Rep LoadedModules Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep LoadedModules = D1 ('MetaData "LoadedModules" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

Instances details
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 :: Type -> Type Source #

NFData LoadedModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: LoadedModule -> () Source #

type Rep LoadedModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

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

Instances details
Generic DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep DynamicEnv :: Type -> Type Source #

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

type Rep DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep DynamicEnv = D1 ('MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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.