cryptol-2.11.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 #

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

Instances details
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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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?

data ModContext Source #

Contains enough information to browse what's in scope, or type check new expressions.

focusedEnv :: ModuleEnv -> ModContext Source #

Given the state of the environment, compute information about what's in scope on the REPL. This includes what's in the focused module, plus any additional definitions from the REPL (e.g., let bound names, and it).

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 #

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

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 #

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 #

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.

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. Note that this removes exactly the modules specified by the predicate. One should be carfule to preserve the invariant on LoadedModules.

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 #

Semigroup DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Monoid DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep DynamicEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

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