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
- meEvalEnv :: EvalEnv
- meCoreLint :: CoreLint
- meMonoBinds :: !Bool
- meFocusedModule :: Maybe (ImpName Name)
- meSearchPath :: [FilePath]
- meDynEnv :: DynamicEnv
- meSupply :: !Supply
- meEvalForeignPolicy :: EvalForeignPolicy
}
data CoreLint
- = NoCoreLint
- | CoreLint
data EvalForeignPolicy
- = AlwaysEvalForeign
- | PreferEvalForeign
- | NeverEvalForeign
defaultEvalForeignPolicy :: EvalForeignPolicy
resetModuleEnv :: ModuleEnv -> IO ModuleEnv
initialModuleEnv :: IO ModuleEnv
focusModule :: ImpName Name -> ModuleEnv -> Maybe ModuleEnv
loadedModules :: ModuleEnv -> [Module]
loadedNonParamModules :: ModuleEnv -> [Module]
loadedNominalTypes :: ModuleEnv -> Map Name NominalType
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
}
findEnv :: Name -> Iface -> ModuleG a -> Maybe (NamingEnv, Set Name)
modContextOf :: ImpName Name -> ModuleEnv -> Maybe ModContext
mainContexts :: ModuleEnv -> [ModContext]
lmModContext :: ModuleEnv -> LoadedModule -> ModContext
lmSignatureContext :: ModuleEnv -> LoadedSignature -> ModContext
dynModContext :: ModuleEnv -> ModContext
focusedEnv :: ModuleEnv -> ModContext
focusedEnv' :: Maybe (ImpName Name) -> 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
withLoadedEntity :: LoadedEntity -> (forall a. LoadedModuleG a -> b) -> b
getLoadedModules :: LoadedModules -> [LoadedModule]
getLoadedField :: Ord a => (forall b. LoadedModuleG b -> a) -> LoadedModules -> Set a
getLoadedFieldMap :: Ord k => (forall b. LoadedModuleG b -> (k, v)) -> LoadedModules -> Map k v
getLoadedNames :: LoadedModules -> Set ModName
getLoadedIds :: LoadedModules -> Set String
getLoadedFiles :: LoadedModules -> Map ModulePath FileInfo
data LoadedModuleG a = LoadedModule {
- lmName :: ModName
- lmFilePath :: ModulePath
- lmModuleId :: String
- lmNamingEnv :: !NamingEnv
- lmFileInfo :: !FileInfo
- lmRenamedModule :: Maybe (Module Name)
- 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 :: ImpName Name -> LoadedModules -> Bool
isLoadedStrict :: ImpName Name -> String -> LoadedModules -> Bool
isLoadedParamMod :: ImpName Name -> LoadedModules -> Bool
isLoadedInterface :: ImpName Name -> LoadedModules -> Bool
loadedParamModDeps :: FreeVars a => LoadedModules -> a -> (Set TParam, Set Name)
lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG TCTopEntity)
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
lookupMainModules :: ModuleEnv -> [LoadedModule]
lookupModuleWith :: (LoadedModule -> Bool) -> ModuleEnv -> Maybe LoadedModule
lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature
lookupSignatureWith :: (LoadedSignature -> Bool) -> ModuleEnv -> Maybe LoadedSignature
addLoadedSignature :: ModulePath -> String -> FileInfo -> NamingEnv -> ModName -> Maybe (Module Name) -> ModParamNames -> LoadedModules -> LoadedModules
addLoadedModule :: ModulePath -> String -> FileInfo -> NamingEnv -> Maybe ForeignSrc -> Maybe (Module Name) -> Module -> LoadedModules -> LoadedModules
removeLoadedModule :: (forall a. LoadedModuleG a -> Bool) -> LoadedModules -> LoadedModules
data FileInfo = FileInfo {
- fiFingerprint :: Fingerprint
- fiIncludeDeps :: Map FilePath Fingerprint
- fiImportDeps :: Set ModName
- fiForeignDeps :: Map FilePath Bool
}
fileInfo :: Fingerprint -> Map FilePath Fingerprint -> 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 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.
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 (ImpName Name)
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
meEvalForeignPolicy :: EvalForeignPolicy
How to evaluate foreign bindings.

Instances

Instances details

Generic ModuleEnv Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep ModuleEnv

Instance details

Defined in Cryptol.ModuleSystem.Env

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

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
Instance details Defined in Cryptol.ModuleSystem.Env type Rep CoreLint = D1 ('MetaData "CoreLint" "Cryptol.ModuleSystem.Env" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "NoCoreLint" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoreLint" 'PrefixI 'False) (U1 :: 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-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "NoCoreLint" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoreLint" 'PrefixI 'False) (U1 :: Type -> Type))

data EvalForeignPolicy Source #

How to evaluate foreign bindings.

Constructors

AlwaysEvalForeign	Use foreign implementation and report an error at module load time if it is unavailable.
PreferEvalForeign	Use foreign implementation by default, and when unavailable, fall back to cryptol implementation if present and report runtime error otherwise.
NeverEvalForeign	Always use cryptol implementation if present, and report runtime error otherwise.

Instances

Instances details

Eq EvalForeignPolicy Source #
Instance details Defined in Cryptol.ModuleSystem.Env Methods (==) :: EvalForeignPolicy -> EvalForeignPolicy -> Bool # (/=) :: EvalForeignPolicy -> EvalForeignPolicy -> Bool #

defaultEvalForeignPolicy :: EvalForeignPolicy Source #

resetModuleEnv :: ModuleEnv -> IO ModuleEnv Source #

initialModuleEnv :: IO ModuleEnv Source #

focusModule :: ImpName Name -> ModuleEnv -> Maybe ModuleEnv Source #

Try to focus a loaded module in the module environment. FIXME: This function is dead code. (And confusingly, there is another function of same name.)

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.

loadedNominalTypes :: ModuleEnv -> Map Name NominalType Source #

Get a Map of all the loaded nominal types, where the keys of the Map are the Names of each nominal type. Note that this includes parameterized modules.

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

findEnv :: Name -> Iface -> ModuleG a -> Maybe (NamingEnv, Set Name) Source #

modContextOf :: ImpName Name -> ModuleEnv -> Maybe ModContext Source #

mainContexts :: ModuleEnv -> [ModContext] Source #

Find all normal modules named Main

lmModContext :: ModuleEnv -> LoadedModule -> ModContext Source #

lmSignatureContext :: ModuleEnv -> LoadedSignature -> ModContext Source #

dynModContext :: ModuleEnv -> ModContext Source #

focusedEnv :: ModuleEnv -> ModContext Source #

focusedEnv me - Given me, the state of the environment, compute information about what's in scope on the REPL. This includes what's in the focused module (`meFocusedModule me`), plus any additional definitions from the REPL (e.g., let bound names, and it).

focusedEnv' :: Maybe (ImpName Name) -> ModuleEnv -> ModContext Source #

focusedEnv' mfm me - Given me (the state of the environment), compute information about what's in scope on the REPL. It also includes additional definitions from the REPL (e.g., let bound names, and it).

In contrast to focusedEnv, - it does not include (`meFocusedModule me`) - it optionally includes mfm

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

Instance details

Defined in Cryptol.ModuleSystem.Env

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

Methods

from :: ModulePath -> Rep ModulePath x #

to :: Rep ModulePath x -> ModulePath #

Read ModulePath Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

readsPrec :: Int -> ReadS ModulePath #

readList :: ReadS [ModulePath] #

readPrec :: ReadPrec ModulePath #

readListPrec :: ReadPrec [ModulePath] #

Show ModulePath Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

showsPrec :: Int -> ModulePath -> ShowS #

show :: ModulePath -> String #

showList :: [ModulePath] -> ShowS #

PP ModulePath Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

ppPrec :: Int -> ModulePath -> Doc Source #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> ModulePath -> Doc Source #

NFData ModulePath Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: ModulePath -> () #

Eq ModulePath Source #

In-memory things are compared by label.

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

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

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

Ord ModulePath Source #

In-memory things are compared by label.

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

compare :: ModulePath -> ModulePath -> Ordering #

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

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

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

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

max :: ModulePath -> ModulePath -> ModulePath #

min :: ModulePath -> ModulePath -> ModulePath #

type Rep ModulePath Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

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

mappend :: LoadedModules -> LoadedModules -> LoadedModules #

mconcat :: [LoadedModules] -> LoadedModules #

Semigroup LoadedModules Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

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

sconcat :: NonEmpty LoadedModules -> LoadedModules #

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

Generic LoadedModules Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep LoadedModules

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep LoadedModules = D1 ('MetaData "LoadedModules" "Cryptol.ModuleSystem.Env" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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]))))

Methods

from :: LoadedModules -> Rep LoadedModules x #

to :: Rep LoadedModules x -> LoadedModules #

Show LoadedModules Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

showsPrec :: Int -> LoadedModules -> ShowS #

show :: LoadedModules -> String #

showList :: [LoadedModules] -> ShowS #

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-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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 #

withLoadedEntity :: LoadedEntity -> (forall a. LoadedModuleG a -> b) -> b Source #

getLoadedModules :: LoadedModules -> [LoadedModule] Source #

getLoadedField :: Ord a => (forall b. LoadedModuleG b -> a) -> LoadedModules -> Set a Source #

getLoadedFieldMap :: Ord k => (forall b. LoadedModuleG b -> (k, v)) -> LoadedModules -> Map k v Source #

getLoadedNames :: LoadedModules -> Set ModName Source #

getLoadedIds :: LoadedModules -> Set String Source #

getLoadedFiles :: LoadedModules -> Map ModulePath FileInfo 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 canonical path, for in-memory things we use their label.
lmNamingEnv :: !NamingEnv
What's in scope in this module
lmFileInfo :: !FileInfo
lmRenamedModule :: Maybe (Module Name)
The renamed AST, if we chose to save it
lmData :: a

Instances

Instances details

Generic (LoadedModuleG a) Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep (LoadedModuleG a)

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep (LoadedModuleG a) = D1 ('MetaData "LoadedModuleG" "Cryptol.ModuleSystem.Env" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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 "lmRenamedModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Module Name))) :*: S1 ('MetaSel ('Just "lmData") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))))

Methods

from :: LoadedModuleG a -> Rep (LoadedModuleG a) x #

to :: Rep (LoadedModuleG a) x -> LoadedModuleG a #

Show a => Show (LoadedModuleG a) Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

showsPrec :: Int -> LoadedModuleG a -> ShowS #

show :: LoadedModuleG a -> String #

showList :: [LoadedModuleG a] -> ShowS #

NFData a => NFData (LoadedModuleG a) Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: LoadedModuleG a -> () #

type Rep (LoadedModuleG a) Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep (LoadedModuleG a) = D1 ('MetaData "LoadedModuleG" "Cryptol.ModuleSystem.Env" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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 "lmRenamedModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Module Name))) :*: 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

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep LoadedModuleData = D1 ('MetaData "LoadedModuleData" "Cryptol.ModuleSystem.Env" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))))

Methods

from :: LoadedModuleData -> Rep LoadedModuleData x #

to :: Rep LoadedModuleData x -> LoadedModuleData #

Show LoadedModuleData Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

showsPrec :: Int -> LoadedModuleData -> ShowS #

show :: LoadedModuleData -> String #

showList :: [LoadedModuleData] -> ShowS #

NFData LoadedModuleData Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: LoadedModuleData -> () #

type Rep LoadedModuleData Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

type Rep LoadedModuleData = D1 ('MetaData "LoadedModuleData" "Cryptol.ModuleSystem.Env" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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 :: ImpName Name -> LoadedModules -> Bool Source #

Has this module been loaded already.

isLoadedStrict :: ImpName Name -> String -> LoadedModules -> Bool Source #

isLoadedParamMod :: ImpName Name -> LoadedModules -> Bool Source #

Is this a loaded parameterized module.

isLoadedInterface :: ImpName Name -> LoadedModules -> Bool Source #

Is this a loaded interface module.

loadedParamModDeps :: FreeVars a => LoadedModules -> a -> (Set TParam, Set Name) Source #

Return the set of type parameters (Set TParam) and definitions (Set Name) from the supplied LoadedModules value that another definition (of type a) depends on.

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

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

Try to find a previously loaded module

lookupMainModules :: ModuleEnv -> [LoadedModule] Source #

Find all loaded Main modules

lookupModuleWith :: (LoadedModule -> Bool) -> ModuleEnv -> Maybe LoadedModule Source #

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

lookupSignatureWith :: (LoadedSignature -> Bool) -> ModuleEnv -> Maybe LoadedSignature Source #

addLoadedSignature :: ModulePath -> String -> FileInfo -> NamingEnv -> ModName -> Maybe (Module Name) -> ModParamNames -> LoadedModules -> LoadedModules Source #

addLoadedModule :: ModulePath -> String -> FileInfo -> NamingEnv -> Maybe ForeignSrc -> Maybe (Module Name) -> 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 careful to preserve the invariant on LoadedModules.

data FileInfo Source #

Constructors

FileInfo
Fields fiFingerprint :: Fingerprint fiIncludeDeps :: Map FilePath Fingerprint fiImportDeps :: Set ModName fiForeignDeps :: Map FilePath Bool The bool indicates if the library for the foreign import exists.

Instances

Instances details

Generic FileInfo Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Associated Types

type Rep FileInfo

Instance details

Defined in Cryptol.ModuleSystem.Env

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

Methods

from :: FileInfo -> Rep FileInfo x #

to :: Rep FileInfo x -> FileInfo #

Show FileInfo Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

showsPrec :: Int -> FileInfo -> ShowS #

show :: FileInfo -> String #

showList :: [FileInfo] -> ShowS #

NFData FileInfo Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

Methods

rnf :: FileInfo -> () #

type Rep FileInfo Source #

Instance details

Defined in Cryptol.ModuleSystem.Env

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

fileInfo :: Fingerprint -> Map FilePath Fingerprint -> 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