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

  • meLoadedModules :: LoadedModules

    Information about all loaded modules. See LoadedModule. Contains information such as the file where the module was loaded from, as well as the module's interface, used for type checking.

  • meNameSeeds :: NameSeeds

    A source of new names for the type checker.

  • meSolverConfig :: SolverConfig

    Configuration settings for the SMT solver used for type-checking.

  • meEvalEnv :: EvalEnv

    The evaluation environment. Contains the values for all loaded modules, both public and private.

  • meCoreLint :: CoreLint

    Should we run the linter to ensure sanity.

  • meMonoBinds :: !Bool

    Are we assuming that local bindings are monomorphic. XXX: We should probably remove this flag, and set it to True.

  • meFocusedModule :: Maybe ModName

    The "current" module. Used to decide how to print names, for example.

  • meSearchPath :: [FilePath]

    Where we look for things.

  • meDynEnv :: DynamicEnv

    This contains additional definitions that were made at the command line, and so they don't reside in any module.

  • meSupply :: !Supply

    Name source for the renamer

Instances

Instances details
Generic ModuleEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep ModuleEnv :: Type -> Type

Methods

from :: ModuleEnv -> Rep ModuleEnv x

to :: Rep ModuleEnv x -> 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

type Rep ModuleEnv = D1 ('MetaData "ModuleEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "ModuleEnv" 'PrefixI 'True) (((S1 ('MetaSel ('Just "meLoadedModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LoadedModules) :*: S1 ('MetaSel ('Just "meNameSeeds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameSeeds)) :*: (S1 ('MetaSel ('Just "meSolverConfig") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SolverConfig) :*: (S1 ('MetaSel ('Just "meEvalEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EvalEnv) :*: S1 ('MetaSel ('Just "meCoreLint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoreLint)))) :*: ((S1 ('MetaSel ('Just "meMonoBinds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :*: S1 ('MetaSel ('Just "meFocusedModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "meSearchPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :*: (S1 ('MetaSel ('Just "meDynEnv") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DynamicEnv) :*: S1 ('MetaSel ('Just "meSupply") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Supply))))))

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.8.0-8MjdO3NUDs4I9u4d2J06AM" '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

Methods

(==) :: ModulePath -> ModulePath -> Bool

(/=) :: ModulePath -> ModulePath -> Bool

Show ModulePath Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

showsPrec :: Int -> ModulePath -> ShowS

show :: ModulePath -> String

showList :: [ModulePath] -> ShowS

Generic ModulePath Source # 
Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep ModulePath :: Type -> Type

Methods

from :: ModulePath -> Rep ModulePath x

to :: Rep ModulePath x -> ModulePath

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

type Rep ModulePath = D1 ('MetaData "ModulePath" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "InFile" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath)) :+: C1 ('MetaCons "InMem" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ByteString)))

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

Methods

showsPrec :: Int -> LoadedModules -> ShowS

show :: LoadedModules -> String

showList :: [LoadedModules] -> ShowS

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-8MjdO3NUDs4I9u4d2J06AM" '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

Methods

showsPrec :: Int -> LoadedModule -> ShowS

show :: LoadedModule -> String

showList :: [LoadedModule] -> ShowS

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

type Rep LoadedModule = D1 ('MetaData "LoadedModule" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "LoadedModule" 'PrefixI 'True) ((S1 ('MetaSel ('Just "lmName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModName) :*: (S1 ('MetaSel ('Just "lmFilePath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModulePath) :*: S1 ('MetaSel ('Just "lmModuleId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :*: (S1 ('MetaSel ('Just "lmInterface") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Iface) :*: (S1 ('MetaSel ('Just "lmModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Module) :*: S1 ('MetaSel ('Just "lmFingerprint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fingerprint)))))

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

Methods

from :: DynamicEnv -> Rep DynamicEnv x

to :: Rep DynamicEnv x -> 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

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