ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Monad.Base.Types
Data structures for the type checker.
Part of Agda.TypeChecking.Monad.Base, extracted to avoid import cycles.
Synopsis
- value lensFileDictBuiltinModuleIds
- value lensFileDictFileDictBuilder
- value lensFileDictPrimitiveLibDir
- value lensPairModuleToSource
- type BuiltinModuleIds
- data Comparison
- type Context
- data ContextEntry
- data FileDictWithBuiltins
- data HighlightingLevel
- data HighlightingMethod
- data IPFace'
- data IsBuiltinModule
- data ModuleToSource
- type ModuleToSourceId
- data NamedMeta
- data Polarity
- type PrimitiveLibDir
- newtype SourceFile
- type TopLevelModuleName
- data FileDictBuilder
- newtype FileId
- newtype AbsolutePath
- PackageAgda-2.8.0.2
- Exports23
- LanguageHaskell2010
- LicenceMIT
- SourceTypes.hs
Collection of FileIds of primitive modules.
Instances8Eq, Show, Generic, NFData, Pretty, PrettyTCM, …
Eq ComparisonDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesShow ComparisonDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesGeneric ComparisonDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesNFData ComparisonDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphanPretty ComparisonDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphanPrettyTCM ComparisonDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyEmbPrj ComparisonDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Internal · orphantype Rep Comparison = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types"Comparison"
"Agda.TypeChecking.Monad.Base.Types"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"CmpEq"
'PrefixI 'False) U1 :+: C1 ('MetaCons"CmpLeq"
'PrefixI 'False) U1)
The Context is a stack of ContextEntrys.
Instances19Show, Generic, NFData, AddContext, Subst, PrettyTCM, …
Show ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesGeneric ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesNFData ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesAddContext ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.ContextSubst ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphanPrettyTCM ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyReify ContextEntryDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstractLensHiding ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesLensOrigin ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesLensArgInfo ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesLensCohesion ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesLensModalPolarity ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesLensModality ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesLensQuantity ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesLensRelevance ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesInstantiateFull ContextEntryDefined in Agda-2.8.0.2 · Agda.TypeChecking.Reducetype Rep ContextEntry = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types"ContextEntry"
"Agda.TypeChecking.Monad.Base.Types"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"CtxVar"
'PrefixI 'True) (S1 ('MetaSel ('Just"ceName"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just"ceType"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type))))type SubstArg ContextEntry = TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphantype ReifiesTo ContextEntry = TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstract
Translation between AbsolutePath and FileId that also knows about Agda's builtin modules.
Constructors
FileDictWithBuiltinsfileDictBuilder :: !FileDictBuilder(Building a) translation between AbsolutePath and FileId.
builtinModuleIds :: !BuiltinModuleIdsFor the known FileIds, remember whether they refer to Agda's builtin modules.
primitiveLibDir :: !PrimitiveLibDirThe absolute path to the directory with the builtin modules. Needs to be set upon initialization.
Instances5Generic, NFData, GetFileId, GetIdFile, Rep
Generic FileDictWithBuiltinsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesNFData FileDictWithBuiltinsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesGetFileId FileDictWithBuiltinsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphanGetIdFile FileDictWithBuiltinsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphantype Rep FileDictWithBuiltins = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types"FileDictWithBuiltins"
"Agda.TypeChecking.Monad.Base.Types"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"FileDictWithBuiltins"
'PrefixI 'True) (S1 ('MetaSel ('Just"fileDictBuilder"
) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FileDictBuilder) :*: (S1 ('MetaSel ('Just"builtinModuleIds"
) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BuiltinModuleIds) :*: S1 ('MetaSel ('Just"primitiveLibDir"
) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PrimitiveLibDir))))
How much highlighting should be sent to the user interface?
Constructors
NoneNonInteractiveInteractiveThis includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked.
Instances7Eq, Ord, Read, Show, Generic, NFData, …
Eq HighlightingLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesOrd HighlightingLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesRead HighlightingLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesShow HighlightingLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesGeneric HighlightingLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesNFData HighlightingLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphantype Rep HighlightingLevel = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types"HighlightingLevel"
"Agda.TypeChecking.Monad.Base.Types"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"None"
'PrefixI 'False) U1 :+: (C1 ('MetaCons"NonInteractive"
'PrefixI 'False) U1 :+: C1 ('MetaCons"Interactive"
'PrefixI 'False) U1))
How should highlighting be sent to the user interface?
Instances6Eq, Read, Show, Generic, NFData, Rep
Eq HighlightingMethodDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesRead HighlightingMethodDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesShow HighlightingMethodDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesGeneric HighlightingMethodDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesNFData HighlightingMethodDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphantype Rep HighlightingMethod = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types"HighlightingMethod"
"Agda.TypeChecking.Monad.Base.Types"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"Direct"
'PrefixI 'False) U1 :+: C1 ('MetaCons"Indirect"
'PrefixI 'False) U1)
Datatype representing a single boundary condition: x_0 = u_0, ... ,x_n = u_n ⊢ t = ?n es
Discern Agda's primitive modules from other file modules.
@IsPrimitiveModule implies IsBuiltinModuleWithSafePostulate implies isBuiltinModule.
Constructors
IsPrimitiveModuleVery magical module, e.g.
Agda.Primitive.IsBuiltinModuleWithSafePostulatesSafe module, e.g.
Agda.Builtin.Equality.IsBuiltinModuleAny builtin module.
Instances6Eq, Ord, Show, Generic, NFData, Rep
Eq IsBuiltinModuleDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesOrd IsBuiltinModuleDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesShow IsBuiltinModuleDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesGeneric IsBuiltinModuleDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesNFData IsBuiltinModuleDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Typestype Rep IsBuiltinModule = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types"IsBuiltinModule"
"Agda.TypeChecking.Monad.Base.Types"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"IsPrimitiveModule"
'PrefixI 'False) U1 :+: (C1 ('MetaCons"IsBuiltinModuleWithSafePostulates"
'PrefixI 'False) U1 :+: C1 ('MetaCons"IsBuiltinModule"
'PrefixI 'False) U1))
Constructors
Instances1Pretty
Pretty ModuleToSourceDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphan
Maps top-level module names to the corresponding source file ids.
For printing, we couple a meta with its name suggestion.
Constructors
Instances5Pretty, PrettyTCM, ToConcrete, EncodeTCM, ConOfAbs
Pretty NamedMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphanPrettyTCM NamedMetaDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyToConcrete NamedMetaDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcreteEncodeTCM NamedMetaDefined in Agda-2.8.0.2 · Agda.Interaction.JSONTop · orphantype ConOfAbs NamedMeta = ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
Polarity for equality and subtype checking.
Constructors
Covariantmonotone
Contravariantantitone
Invariantno information (mixed variance)
Nonvariantconstant
Instances12Eq, Show, Generic, NFData, Pretty, PrettyTCM, …
Eq PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesShow PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesGeneric PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesNFData PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphanPretty PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphanPrettyTCM PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyKillRange PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphanEmbPrj PolarityDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Internal · orphanMonad m => Singleton Polarity (LeastPolarity m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PolarityApply [Polarity]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphanAbstract [Polarity]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphantype Rep Polarity = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types"Polarity"
"Agda.TypeChecking.Monad.Base.Types"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) ((C1 ('MetaCons"Covariant"
'PrefixI 'False) U1 :+: C1 ('MetaCons"Contravariant"
'PrefixI 'False) U1) :+: (C1 ('MetaCons"Invariant"
'PrefixI 'False) U1 :+: C1 ('MetaCons"Nonvariant"
'PrefixI 'False) U1))
SourceFiles must exist and be registered in our file dictionary.
Constructors
Instances6Eq, Ord, Show, Generic, NFData, Rep
Eq SourceFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesOrd SourceFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesShow SourceFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesGeneric SourceFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.TypesNFData SourceFileDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Typestype Rep SourceFile = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base.Types"SourceFile"
"Agda.TypeChecking.Monad.Base.Types"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'True) (C1 ('MetaCons"SourceFile"
'PrefixI 'True) (S1 ('MetaSel ('Just"srcFileId"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId)))
Top-level module names (with constant-time comparisons).
Instances6Generic, NFData, Null, GetFileId, GetIdFile, Rep
Generic FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdNFData FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdNull FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetFileId FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetIdFile FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdtype Rep FileDictBuilder = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.Utils.FileId"FileDictBuilder"
"Agda.Utils.FileId"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"FileDictBuilder"
'PrefixI 'True) (S1 ('MetaSel ('Just"nextFileId"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just"fileDict"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict)))
Unique identifier of a file.
Instances10Enum, Eq, Num, Ord, Show, Generic, …
Enum FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdEq FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdNum FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdOrd FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdShow FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGeneric FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdNFData FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetFileId FileToIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetIdFile IdToFileDefined in Agda-2.8.0.2 · Agda.Utils.FileIdtype Rep FileId = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.Utils.FileId"FileId"
"Agda.Utils.FileId"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'True) (C1 ('MetaCons"FileId"
'PrefixI 'True) (S1 ('MetaSel ('Just"theFileId"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))
Instances11Eq, Ord, Read, Show, NFData, Hashable, …
Eq AbsolutePathDefined in Agda-2.8.0.2 · Agda.Utils.FileNameOrd AbsolutePathDefined in Agda-2.8.0.2 · Agda.Utils.FileNameRead AbsolutePathDefined in Agda-2.8.0.2 · Agda.Interaction.Base · orphanShow AbsolutePathDefined in Agda-2.8.0.2 · Agda.Utils.FileNameNFData AbsolutePathDefined in Agda-2.8.0.2 · Agda.Utils.FileNameHashable AbsolutePathDefined in Agda-2.8.0.2 · Agda.Utils.FileNameToJSON AbsolutePathDefined in Agda-2.8.0.2 · Agda.Interaction.JSON · orphanPretty AbsolutePathDefined in Agda-2.8.0.2 · Agda.Syntax.Common.PrettyBeginningOfFile AbsolutePathDefined in Agda-2.8.0.2 · Agda.Syntax.PositionGetFileId FileToIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetIdFile IdToFileDefined in Agda-2.8.0.2 · Agda.Utils.FileId