cryptol-2.9.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.9.0-4aSi1YZNBynFQwh9aOpllR" 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
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.9.0-4aSi1YZNBynFQwh9aOpllR" 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. 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 

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.