cryptol-2.4.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
Language | Haskell98

Cryptol.ModuleSystem.Env

Description

Synopsis

- data ModuleEnv = ModuleEnv {
  - meLoadedModules :: LoadedModules
  - meNameSeeds :: NameSeeds
  - meEvalEnv :: EvalEnv
  - meFocusedModule :: Maybe ModName
  - meSearchPath :: [FilePath]
  - meDynEnv :: DynamicEnv
  - meMonoBinds :: !Bool
  - meSolverConfig :: SolverConfig
  - meCoreLint :: CoreLint
  - meSupply :: !Supply
  }
- data CoreLint
  - = NoCoreLint
  - | CoreLint
- resetModuleEnv :: ModuleEnv -> ModuleEnv
- initialModuleEnv :: IO ModuleEnv
- focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv
- loadedModules :: ModuleEnv -> [Module]
- focusedEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)
- dynamicEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)
- qualifiedEnv :: ModuleEnv -> IfaceDecls
- newtype LoadedModules = LoadedModules {
  - getLoadedModules :: [LoadedModule]
  }
- data LoadedModule = LoadedModule {
  - lmName :: ModName
  - lmFilePath :: FilePath
  - lmInterface :: Iface
  - lmModule :: Module
  }
- isLoaded :: ModName -> LoadedModules -> Bool
- lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
- addLoadedModule :: FilePath -> Module -> LoadedModules -> LoadedModules
- removeLoadedModule :: FilePath -> LoadedModules -> LoadedModules
- data DynamicEnv = DEnv {
  - deNames :: NamingEnv
  - deDecls :: [DeclGroup]
  - deEnv :: EvalEnv
  }
- deIfaceDecls :: DynamicEnv -> IfaceDecls

# Documentation

data ModuleEnv Source #

Constructors

ModuleEnv |

Fields

- meLoadedModules :: LoadedModules
- meNameSeeds :: NameSeeds
- meEvalEnv :: EvalEnv
- meFocusedModule :: Maybe ModName
- meSearchPath :: [FilePath]
- meDynEnv :: DynamicEnv
- meMonoBinds :: !Bool
- meSolverConfig :: SolverConfig
- meCoreLint :: CoreLint
- meSupply :: !Supply

Instances

Generic ModuleEnv Source # |
Associated Types type Rep ModuleEnv :: * -> * # Methods from :: ModuleEnv -> Rep ModuleEnv x # to :: Rep ModuleEnv x -> ModuleEnv #
NFData ModuleEnv Source # |
Methods rnf :: ModuleEnv -> () #
type Rep ModuleEnv Source # |

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

data CoreLint Source #

Constructors

NoCoreLint | Don't run core lint
CoreLint | Run core lint

Instances

Generic CoreLint Source # |
Associated Types type Rep CoreLint :: * -> * # Methods from :: CoreLint -> Rep CoreLint x # to :: Rep CoreLint x -> CoreLint #
NFData CoreLint Source # |
Methods rnf :: CoreLint -> () #
type Rep CoreLint Source # |
type Rep CoreLint = D1 (MetaData "CoreLint" "Cryptol.ModuleSystem.Env" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "NoCoreLint" PrefixI False) U1) (C1 (MetaCons "CoreLint" PrefixI False) U1))

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.

focusedEnv :: ModuleEnv -> (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.

dynamicEnv :: ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp) Source #

The unqualified declarations and name environment for the dynamic environment.

qualifiedEnv :: ModuleEnv -> IfaceDecls Source #

Retrieve all `IfaceDecls` referenced by a module, as well as all of its public and private declarations, checking expressions

newtype LoadedModules Source #

Invariant: All the dependencies of any module `m` must precede `m` in the list.

Constructors

LoadedModules |

Fields

- getLoadedModules :: [LoadedModule]

Instances

Show LoadedModules Source # |
Methods showsPrec :: Int -> LoadedModules -> ShowS # show :: LoadedModules -> String # showList :: [LoadedModules] -> ShowS #
Generic LoadedModules Source # |
Associated Types type Rep LoadedModules :: * -> * # Methods from :: LoadedModules -> Rep LoadedModules x # to :: Rep LoadedModules x -> LoadedModules #
Monoid LoadedModules Source # |
Methods mempty :: LoadedModules # mappend :: LoadedModules -> LoadedModules -> LoadedModules # mconcat :: [LoadedModules] -> LoadedModules #
NFData LoadedModules Source # |
Methods rnf :: LoadedModules -> () #
type Rep LoadedModules Source # |
type Rep LoadedModules = D1 (MetaData "LoadedModules" "Cryptol.ModuleSystem.Env" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" True) (C1 (MetaCons "LoadedModules" PrefixI True) (S1 (MetaSel (Just Symbol "getLoadedModules") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [LoadedModule])))

data LoadedModule Source #

Constructors

LoadedModule |

Fields

- lmName :: ModName
- lmFilePath :: FilePath
- lmInterface :: Iface
- lmModule :: Module

Instances

Show LoadedModule Source # |
Methods showsPrec :: Int -> LoadedModule -> ShowS # show :: LoadedModule -> String # showList :: [LoadedModule] -> ShowS #
Generic LoadedModule Source # |
Associated Types type Rep LoadedModule :: * -> * # Methods from :: LoadedModule -> Rep LoadedModule x # to :: Rep LoadedModule x -> LoadedModule #
NFData LoadedModule Source # |
Methods rnf :: LoadedModule -> () #
type Rep LoadedModule Source # |

type Rep LoadedModule = D1 (MetaData "LoadedModule" "Cryptol.ModuleSystem.Env" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "LoadedModule" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "lmName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ModName)) (S1 (MetaSel (Just Symbol "lmFilePath") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FilePath))) ((:*:) (S1 (MetaSel (Just Symbol "lmInterface") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Iface)) (S1 (MetaSel (Just Symbol "lmModule") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Module)))))

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

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

addLoadedModule :: FilePath -> Module -> LoadedModules -> LoadedModules Source #

removeLoadedModule :: FilePath -> LoadedModules -> LoadedModules 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]
- deEnv :: EvalEnv

Instances

Generic DynamicEnv Source # |
Associated Types type Rep DynamicEnv :: * -> * # Methods from :: DynamicEnv -> Rep DynamicEnv x # to :: Rep DynamicEnv x -> DynamicEnv #
Monoid DynamicEnv Source # |
Methods mempty :: DynamicEnv # mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv # mconcat :: [DynamicEnv] -> DynamicEnv #
NFData DynamicEnv Source # |
Methods rnf :: DynamicEnv -> () #
type Rep DynamicEnv Source # |

type Rep DynamicEnv = D1 (MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "DEnv" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "deNames") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NamingEnv)) ((:*:) (S1 (MetaSel (Just Symbol "deDecls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [DeclGroup])) (S1 (MetaSel (Just Symbol "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.