cryptol-2.8.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | None
Language | Haskell2010

Cryptol.ModuleSystem.Env

Description

Synopsis

- data ModuleEnv = ModuleEnv {
  - meLoadedModules :: LoadedModules
  - meNameSeeds :: NameSeeds
  - meSolverConfig :: SolverConfig
  - meEvalEnv :: EvalEnv
  - meCoreLint :: CoreLint
  - meMonoBinds :: !Bool
  - meFocusedModule :: Maybe ModName
  - meSearchPath :: [FilePath]
  - meDynEnv :: DynamicEnv
  - meSupply :: !Supply
  }
- data CoreLint
  - = NoCoreLint
  - | CoreLint
- resetModuleEnv :: ModuleEnv -> ModuleEnv
- initialModuleEnv :: IO ModuleEnv
- focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv
- loadedModules :: ModuleEnv -> [Module]
- loadedNonParamModules :: ModuleEnv -> [Module]
- hasParamModules :: ModuleEnv -> Bool
- focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
- dynamicEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)
- data ModulePath
  - = InFile FilePath
  - | InMem String ByteString
- modulePathLabel :: ModulePath -> String
- data LoadedModules = LoadedModules {
  - lmLoadedModules :: [LoadedModule]
  - lmLoadedParamModules :: [LoadedModule]
  }
- getLoadedModules :: LoadedModules -> [LoadedModule]
- data LoadedModule = LoadedModule {
  - lmName :: ModName
  - lmFilePath :: ModulePath
  - lmModuleId :: String
  - lmInterface :: Iface
  - lmModule :: Module
  - lmFingerprint :: Fingerprint
  }
- isLoaded :: ModName -> LoadedModules -> Bool
- isLoadedParamMod :: ModName -> LoadedModules -> Bool
- lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
- addLoadedModule :: ModulePath -> String -> Fingerprint -> Module -> LoadedModules -> LoadedModules
- removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules
- data DynamicEnv = DEnv {
  - deNames :: NamingEnv
  - deDecls :: [DeclGroup]
  - deEnv :: EvalEnv
  }
- deIfaceDecls :: DynamicEnv -> IfaceDecls

# 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 Source # Methods from :: ModuleEnv -> Rep ModuleEnv x Source # to :: Rep ModuleEnv x -> ModuleEnv 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

type Rep ModuleEnv = D1 ('MetaData "ModuleEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source # Methods from :: CoreLint -> Rep CoreLint x Source # to :: Rep CoreLint x -> CoreLint 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))

resetModuleEnv :: ModuleEnv -> ModuleEnv Source #

initialModuleEnv :: IO ModuleEnv Source #

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 Source # (/=) :: ModulePath -> ModulePath -> Bool Source #
Show ModulePath Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> ModulePath -> ShowS Source # show :: ModulePath -> String Source # showList :: [ModulePath] -> ShowS Source #
Generic ModulePath Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Associated Types type Rep ModulePath :: Type -> Type Source # Methods from :: ModulePath -> Rep ModulePath x Source # to :: Rep ModulePath x -> ModulePath 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

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

- lmLoadedModules :: [LoadedModule]

  Invariants: 1) All the dependencies of any module `m` must precede `m` in the list. 2) Does not contain any parameterized modules.

- lmLoadedParamModules :: [LoadedModule]

  Loaded parameterized modules.

#### Instances

Instances details

Show LoadedModules Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> LoadedModules -> ShowS Source # show :: LoadedModules -> String Source # showList :: [LoadedModules] -> ShowS Source #
Generic LoadedModules Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Associated Types type Rep LoadedModules :: Type -> Type Source # Methods from :: LoadedModules -> Rep LoadedModules x Source # to :: Rep LoadedModules x -> LoadedModules Source #
Semigroup LoadedModules Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods (<>) :: LoadedModules -> LoadedModules -> LoadedModules Source # sconcat :: NonEmpty LoadedModules -> LoadedModules Source # stimes :: Integral b => b -> LoadedModules -> LoadedModules Source #
Monoid LoadedModules Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods mempty :: LoadedModules Source # mappend :: LoadedModules -> LoadedModules -> LoadedModules Source # mconcat :: [LoadedModules] -> LoadedModules Source #
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])))

getLoadedModules :: LoadedModules -> [LoadedModule] Source #

data LoadedModule Source #

Constructors

LoadedModule |

Fields

- lmName :: ModName
- lmFilePath :: ModulePath

  The file path used to load this module (may not be canonical)

- lmModuleId :: String

  An identifier used to identify the source of the bytes for the module. For files we just use the cononical path, for in memory things we use their label.

- lmInterface :: Iface
- lmModule :: Module
- lmFingerprint :: Fingerprint

#### Instances

Instances details

Show LoadedModule Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> LoadedModule -> ShowS Source # show :: LoadedModule -> String Source # showList :: [LoadedModule] -> ShowS Source #
Generic LoadedModule Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Associated Types type Rep LoadedModule :: Type -> Type Source # Methods from :: LoadedModule -> Rep LoadedModule x Source # to :: Rep LoadedModule x -> LoadedModule 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

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

Fields

- deNames :: NamingEnv
- deDecls :: [DeclGroup]
- deEnv :: EvalEnv

#### Instances

Instances details

Generic DynamicEnv Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Associated Types type Rep DynamicEnv :: Type -> Type Source # Methods from :: DynamicEnv -> Rep DynamicEnv x Source # to :: Rep DynamicEnv x -> DynamicEnv Source #
Semigroup DynamicEnv Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods (<>) :: DynamicEnv -> DynamicEnv -> DynamicEnv Source # sconcat :: NonEmpty DynamicEnv -> DynamicEnv Source # stimes :: Integral b => b -> DynamicEnv -> DynamicEnv Source #
Monoid DynamicEnv Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods mempty :: DynamicEnv Source # mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv Source # mconcat :: [DynamicEnv] -> DynamicEnv Source #
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.