cryptol-3.0.0: Cryptol: The Language of Cryptography

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

Cryptol.ModuleSystem.Env

Description

Synopsis

- data ModuleEnv = ModuleEnv {
  - meLoadedModules :: LoadedModules
  - meNameSeeds :: NameSeeds
  - meEvalEnv :: EvalEnv
  - meCoreLint :: CoreLint
  - meMonoBinds :: !Bool
  - meFocusedModule :: Maybe ModName
  - meSearchPath :: [FilePath]
  - meDynEnv :: DynamicEnv
  - meSupply :: !Supply
  }
- data CoreLint
  - = NoCoreLint
  - | CoreLint
- resetModuleEnv :: ModuleEnv -> IO ModuleEnv
- initialModuleEnv :: IO ModuleEnv
- focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv
- loadedModules :: ModuleEnv -> [Module]
- loadedNonParamModules :: ModuleEnv -> [Module]
- loadedNewtypes :: ModuleEnv -> Map Name Newtype
- hasParamModules :: ModuleEnv -> Bool
- allDeclGroups :: ModuleEnv -> [DeclGroup]
- data ModContextParams
  - = InterfaceParams ModParamNames
  - | FunctorParams FunctorParams
  - | NoParams
- modContextParamNames :: ModContextParams -> ModParamNames
- data ModContext = ModContext {
  - mctxParams :: ModContextParams
  - mctxExported :: Set Name
  - mctxDecls :: IfaceDecls
  - mctxNames :: NamingEnv
  - mctxNameDisp :: NameDisp
  }
- modContextOf :: ModName -> ModuleEnv -> Maybe ModContext
- dynModContext :: ModuleEnv -> ModContext
- focusedEnv :: ModuleEnv -> ModContext
- data ModulePath
  - = InFile FilePath
  - | InMem String ByteString
- modulePathLabel :: ModulePath -> String
- data LoadedModules = LoadedModules {
  - lmLoadedModules :: [LoadedModule]
  - lmLoadedParamModules :: [LoadedModule]
  - lmLoadedSignatures :: ![LoadedSignature]
  }
- data LoadedEntity
  - = ALoadedModule LoadedModule
  - | ALoadedFunctor LoadedModule
  - | ALoadedInterface LoadedSignature
- getLoadedEntities :: LoadedModules -> Map ModName LoadedEntity
- getLoadedModules :: LoadedModules -> [LoadedModule]
- getLoadedNames :: LoadedModules -> Set ModName
- data LoadedModuleG a = LoadedModule {
  - lmName :: ModName
  - lmFilePath :: ModulePath
  - lmModuleId :: String
  - lmNamingEnv :: !NamingEnv
  - lmFileInfo :: !FileInfo
  - lmData :: a
  }
- type LoadedModule = LoadedModuleG LoadedModuleData
- lmModule :: LoadedModule -> Module
- lmInterface :: LoadedModule -> Iface
- data LoadedModuleData = LoadedModuleData {
  - lmdInterface :: Iface
  - lmdModule :: Module
  - lmForeignSrc :: Maybe ForeignSrc
  }
- type LoadedSignature = LoadedModuleG ModParamNames
- isLoaded :: ModName -> LoadedModules -> Bool
- isLoadedParamMod :: ModName -> LoadedModules -> Bool
- isLoadedInterface :: ModName -> LoadedModules -> Bool
- lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG TCTopEntity)
- lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
- lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature
- addLoadedSignature :: ModulePath -> String -> FileInfo -> NamingEnv -> ModName -> ModParamNames -> LoadedModules -> LoadedModules
- addLoadedModule :: ModulePath -> String -> FileInfo -> NamingEnv -> Maybe ForeignSrc -> Module -> LoadedModules -> LoadedModules
- removeLoadedModule :: (forall a. LoadedModuleG a -> Bool) -> LoadedModules -> LoadedModules
- data FileInfo = FileInfo {
  - fiFingerprint :: Fingerprint
  - fiIncludeDeps :: Set FilePath
  - fiImportDeps :: Set ModName
  - fiForeignDeps :: Set FilePath
  }
- fileInfo :: Fingerprint -> Set FilePath -> Set ModName -> Maybe ForeignSrc -> FileInfo
- data DynamicEnv = DEnv {
  - deNames :: NamingEnv
  - deDecls :: [DeclGroup]
  - deTySyns :: Map Name TySyn
  - 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 `LoadedModuleG`. 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.

- 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-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 "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-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "NoCoreLint" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoreLint" 'PrefixI 'False) (U1 :: Type -> Type))

resetModuleEnv :: ModuleEnv -> IO 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.

loadedNewtypes :: ModuleEnv -> Map Name Newtype Source #

hasParamModules :: ModuleEnv -> Bool Source #

Are any parameterized modules loaded?

allDeclGroups :: ModuleEnv -> [DeclGroup] Source #

data ModContextParams Source #

Constructors

InterfaceParams ModParamNames |
FunctorParams FunctorParams |
NoParams |

modContextParamNames :: ModContextParams -> ModParamNames Source #

data ModContext Source #

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

Constructors

ModContext |

Fields

- mctxParams :: ModContextParams
- mctxExported :: Set Name
- mctxDecls :: IfaceDecls

  Should contain at least names in NamingEnv, but may have more

- mctxNames :: NamingEnv

  What's in scope inside the module

- mctxNameDisp :: NameDisp

#### Instances

Instances details

Monoid ModContext Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods mempty :: ModContext Source # mappend :: ModContext -> ModContext -> ModContext Source # mconcat :: [ModContext] -> ModContext Source #
Semigroup ModContext Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods (<>) :: ModContext -> ModContext -> ModContext Source # sconcat :: NonEmpty ModContext -> ModContext Source # stimes :: Integral b => b -> ModContext -> ModContext Source #

modContextOf :: ModName -> ModuleEnv -> Maybe ModContext Source #

dynModContext :: ModuleEnv -> ModContext Source #

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

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 #
Show ModulePath Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> ModulePath -> ShowS Source # show :: ModulePath -> String Source # showList :: [ModulePath] -> ShowS Source #
PP ModulePath Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods ppPrec :: Int -> ModulePath -> Doc Source #
NFData ModulePath Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods rnf :: ModulePath -> () Source #
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 #
Ord ModulePath Source # | In-memory things are compared by label.

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

compare :: ModulePath -> ModulePath -> Ordering Source #

(<) :: ModulePath -> ModulePath -> Bool Source #

(<=) :: ModulePath -> ModulePath -> Bool Source #

(>) :: ModulePath -> ModulePath -> Bool Source #

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

max :: ModulePath -> ModulePath -> ModulePath Source #

min :: ModulePath -> ModulePath -> ModulePath Source #

type Rep ModulePath Source # |

Instance details

Defined in Cryptol.ModuleSystem.Env

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

- lmLoadedSignatures :: ![LoadedSignature]

#### Instances

Instances details

Monoid LoadedModules Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods mempty :: LoadedModules Source # mappend :: LoadedModules -> LoadedModules -> LoadedModules Source # mconcat :: [LoadedModules] -> 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 #
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 #
Show LoadedModules Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> LoadedModules -> ShowS Source # show :: LoadedModules -> String Source # showList :: [LoadedModules] -> ShowS 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-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "LoadedModules" 'PrefixI 'True) (S1 ('MetaSel ('Just "lmLoadedModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LoadedModule]) :*: (S1 ('MetaSel ('Just "lmLoadedParamModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LoadedModule]) :*: S1 ('MetaSel ('Just "lmLoadedSignatures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [LoadedSignature]))))

data LoadedEntity Source #

Constructors

ALoadedModule LoadedModule |
ALoadedFunctor LoadedModule |
ALoadedInterface LoadedSignature |

getLoadedEntities :: LoadedModules -> Map ModName LoadedEntity Source #

getLoadedModules :: LoadedModules -> [LoadedModule] Source #

getLoadedNames :: LoadedModules -> Set ModName Source #

data LoadedModuleG a Source #

A generic type for loaded things. The things can be either modules or signatures.

Constructors

LoadedModule |

Fields

- lmName :: ModName

  The name of this module. Should match what's in `lmModule`

- 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.

- lmNamingEnv :: !NamingEnv

  What's in scope in this module

- lmFileInfo :: !FileInfo
- lmData :: a

#### Instances

Instances details

Generic (LoadedModuleG a) Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Associated Types type Rep (LoadedModuleG a) :: Type -> Type Source # Methods from :: LoadedModuleG a -> Rep (LoadedModuleG a) x Source # to :: Rep (LoadedModuleG a) x -> LoadedModuleG a Source #
Show a => Show (LoadedModuleG a) Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> LoadedModuleG a -> ShowS Source # show :: LoadedModuleG a -> String Source # showList :: [LoadedModuleG a] -> ShowS Source #
NFData a => NFData (LoadedModuleG a) Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods rnf :: LoadedModuleG a -> () Source #
type Rep (LoadedModuleG a) Source # |

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep (LoadedModuleG a) = D1 ('MetaData "LoadedModuleG" "Cryptol.ModuleSystem.Env" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 "lmNamingEnv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 NamingEnv) :*: (S1 ('MetaSel ('Just "lmFileInfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FileInfo) :*: S1 ('MetaSel ('Just "lmData") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))))

type LoadedModule = LoadedModuleG LoadedModuleData Source #

lmModule :: LoadedModule -> Module Source #

lmInterface :: LoadedModule -> Iface Source #

data LoadedModuleData Source #

Constructors

LoadedModuleData |

Fields

- lmdInterface :: Iface

  The module's interface.

- lmdModule :: Module

  The actual type-checked module

- lmForeignSrc :: Maybe ForeignSrc

  The dynamically loaded source for any foreign functions in the module

#### Instances

Instances details

Generic LoadedModuleData Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Associated Types type Rep LoadedModuleData :: Type -> Type Source # Methods from :: LoadedModuleData -> Rep LoadedModuleData x Source # to :: Rep LoadedModuleData x -> LoadedModuleData Source #
Show LoadedModuleData Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> LoadedModuleData -> ShowS Source # show :: LoadedModuleData -> String Source # showList :: [LoadedModuleData] -> ShowS Source #
NFData LoadedModuleData Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods rnf :: LoadedModuleData -> () Source #
type Rep LoadedModuleData Source # |

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep LoadedModuleData = D1 ('MetaData "LoadedModuleData" "Cryptol.ModuleSystem.Env" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "LoadedModuleData" 'PrefixI 'True) (S1 ('MetaSel ('Just "lmdInterface") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Iface) :*: (S1 ('MetaSel ('Just "lmdModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Module) :*: S1 ('MetaSel ('Just "lmForeignSrc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ForeignSrc)))))

type LoadedSignature = LoadedModuleG ModParamNames Source #

isLoaded :: ModName -> LoadedModules -> Bool Source #

Has this module been loaded already.

isLoadedParamMod :: ModName -> LoadedModules -> Bool Source #

Is this a loaded parameterized module.

isLoadedInterface :: ModName -> LoadedModules -> Bool Source #

Is this a loaded interface module.

lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG TCTopEntity) Source #

lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule Source #

Try to find a previously loaded module

lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature Source #

addLoadedSignature :: ModulePath -> String -> FileInfo -> NamingEnv -> ModName -> ModParamNames -> LoadedModules -> LoadedModules Source #

addLoadedModule :: ModulePath -> String -> FileInfo -> NamingEnv -> Maybe ForeignSrc -> Module -> LoadedModules -> LoadedModules Source #

Add a freshly loaded module. If it was previously loaded, then the new version is ignored.

removeLoadedModule :: (forall a. LoadedModuleG a -> 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 FileInfo Source #

Constructors

FileInfo |

Fields

- fiFingerprint :: Fingerprint
- fiIncludeDeps :: Set FilePath
- fiImportDeps :: Set ModName
- fiForeignDeps :: Set FilePath

#### Instances

Instances details

Generic FileInfo Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Associated Types type Rep FileInfo :: Type -> Type Source # Methods from :: FileInfo -> Rep FileInfo x Source # to :: Rep FileInfo x -> FileInfo Source #
Show FileInfo Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods showsPrec :: Int -> FileInfo -> ShowS Source # show :: FileInfo -> String Source # showList :: [FileInfo] -> ShowS Source #
NFData FileInfo Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods rnf :: FileInfo -> () Source #
type Rep FileInfo Source # |

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep FileInfo = D1 ('MetaData "FileInfo" "Cryptol.ModuleSystem.Env" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "FileInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "fiFingerprint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fingerprint) :*: S1 ('MetaSel ('Just "fiIncludeDeps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set FilePath))) :*: (S1 ('MetaSel ('Just "fiImportDeps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set ModName)) :*: S1 ('MetaSel ('Just "fiForeignDeps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set FilePath)))))

fileInfo :: Fingerprint -> Set FilePath -> Set ModName -> Maybe ForeignSrc -> FileInfo Source #

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]
- deTySyns :: Map Name TySyn
- deEnv :: EvalEnv

#### Instances

Instances details

Monoid DynamicEnv Source # |
Instance details Defined in Cryptol.ModuleSystem.Env Methods mempty :: DynamicEnv Source # mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv Source # mconcat :: [DynamicEnv] -> 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 #
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 #
type Rep DynamicEnv Source # |

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep DynamicEnv = D1 ('MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 "deTySyns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name TySyn)) :*: 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 add newtypes, etc. at the REPL, revisit this.