Cryptol.ModuleSystem.Env

Documentation

data ModuleEnv

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

Generic ModuleEnv

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

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: ModuleEnv -> ()

type Rep ModuleEnv

Defined in Cryptol.ModuleSystem.Env

type Rep ModuleEnv = D1 (MetaData "ModuleEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Should we run the linter?

Constructors

NoCoreLint

Don't run core lint

CoreLint

Run core lint

Instances

Generic CoreLint

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

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: CoreLint -> ()

type Rep CoreLint

Defined in Cryptol.ModuleSystem.Env

type Rep CoreLint = D1 (MetaData "CoreLint" "Cryptol.ModuleSystem.Env" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "NoCoreLint" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "CoreLint" PrefixI False) (U1 :: Type -> Type))

resetModuleEnv :: ModuleEnv -> ModuleEnv

initialModuleEnv :: IO ModuleEnv

focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv

Try to focus a loaded module in the module environment.

loadedModules :: ModuleEnv -> [Module]

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]

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

Are any parameterized modules loaded?

focusedEnv :: ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp)

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)

The unqualified declarations and name environment for the dynamic environment.

data LoadedModules

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

Show LoadedModules

Defined in Cryptol.ModuleSystem.Env

Methods

showsPrec :: Int -> LoadedModules -> ShowS

show :: LoadedModules -> String

showList :: [LoadedModules] -> ShowS

Generic LoadedModules

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep LoadedModules :: Type -> Type

Methods

from :: LoadedModules -> Rep LoadedModules x

to :: Rep LoadedModules x -> LoadedModules

Semigroup LoadedModules

Defined in Cryptol.ModuleSystem.Env

Methods

(<>) :: LoadedModules -> LoadedModules -> LoadedModules

sconcat :: NonEmpty LoadedModules -> LoadedModules

stimes :: Integral b => b -> LoadedModules -> LoadedModules

Monoid LoadedModules

Defined in Cryptol.ModuleSystem.Env

Methods

mempty :: LoadedModules

mappend :: LoadedModules -> LoadedModules -> LoadedModules

mconcat :: [LoadedModules] -> LoadedModules

NFData LoadedModules

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: LoadedModules -> ()

type Rep LoadedModules

Defined in Cryptol.ModuleSystem.Env

type Rep LoadedModules = D1 (MetaData "LoadedModules" "Cryptol.ModuleSystem.Env" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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]

data LoadedModule

Constructors

LoadedModule

Fields

• lmName :: ModName
• lmFilePath :: FilePath

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

• lmCanonicalPath :: FilePath

  The canonical version of the path of this module

• lmInterface :: Iface
• lmModule :: Module
• lmFingerprint :: Fingerprint

Instances

Show LoadedModule

Defined in Cryptol.ModuleSystem.Env

Methods

showsPrec :: Int -> LoadedModule -> ShowS

show :: LoadedModule -> String

showList :: [LoadedModule] -> ShowS

Generic LoadedModule

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep LoadedModule :: Type -> Type

Methods

from :: LoadedModule -> Rep LoadedModule x

to :: Rep LoadedModule x -> LoadedModule

NFData LoadedModule

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: LoadedModule -> ()

type Rep LoadedModule

Defined in Cryptol.ModuleSystem.Env

type Rep LoadedModule = D1 (MetaData "LoadedModule" "Cryptol.ModuleSystem.Env" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "LoadedModule" PrefixI True) ((S1 (MetaSel (Just "lmName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ModName) :*: (S1 (MetaSel (Just "lmFilePath") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FilePath) :*: S1 (MetaSel (Just "lmCanonicalPath") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FilePath))) :*: (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

Has this module been loaded already.

isLoadedParamMod :: ModName -> LoadedModules -> Bool

Is this a loaded parameterized module.

lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule

Try to find a previously loaded module

addLoadedModule :: FilePath -> FilePath -> Fingerprint -> Module -> LoadedModules -> LoadedModules

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

removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules

Remove a previously loaded module.

data DynamicEnv

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

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

Defined in Cryptol.ModuleSystem.Env

Methods

(<>) :: DynamicEnv -> DynamicEnv -> DynamicEnv

sconcat :: NonEmpty DynamicEnv -> DynamicEnv

stimes :: Integral b => b -> DynamicEnv -> DynamicEnv

Monoid DynamicEnv

Defined in Cryptol.ModuleSystem.Env

Methods

mempty :: DynamicEnv

mappend :: DynamicEnv -> DynamicEnv -> DynamicEnv

mconcat :: [DynamicEnv] -> DynamicEnv

NFData DynamicEnv

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: DynamicEnv -> ()

type Rep DynamicEnv

Defined in Cryptol.ModuleSystem.Env

type Rep DynamicEnv = D1 (MetaData "DynamicEnv" "Cryptol.ModuleSystem.Env" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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.