Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Monad.Base.Types
Description
Data structures for the type checker.
Part of Agda.TypeChecking.Monad.Base, extracted to avoid import cycles.
Synopsis
- data HighlightingLevel
- data HighlightingMethod
- data Comparison
- data Polarity
- data NamedMeta = NamedMeta {}
- newtype SourceFile = SourceFile {}
- data ModuleToSource = ModuleToSource {}
- data IPFace' t = IPFace' {}
- data IsBuiltinModule
- type Context = [ContextEntry]
- data ContextEntry = CtxVar {}
- type BuiltinModuleIds = EnumMap FileId IsBuiltinModule
- data FileDictWithBuiltins = FileDictWithBuiltins {}
- type PrimitiveLibDir = AbsolutePath
- type ModuleToSourceId = Map TopLevelModuleName SourceFile
- lensFileDictFileDictBuilder :: Lens' FileDictWithBuiltins FileDictBuilder
- lensFileDictBuiltinModuleIds :: Lens' FileDictWithBuiltins BuiltinModuleIds
- lensFileDictPrimitiveLibDir :: Lens' FileDictWithBuiltins PrimitiveLibDir
- lensPairModuleToSource :: Lens' (FileDictWithBuiltins, ModuleToSourceId) ModuleToSource
- type TopLevelModuleName = TopLevelModuleName' Range
- data AbsolutePath
- data FileId
- data FileDictBuilder
Documentation
data HighlightingLevel Source #
How much highlighting should be sent to the user interface?
Constructors
None | |
NonInteractive | |
Interactive | This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked. |
Instances
Generic HighlightingLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Associated Types
Methods from :: HighlightingLevel -> Rep HighlightingLevel x to :: Rep HighlightingLevel x -> HighlightingLevel | |||||
Read HighlightingLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods readsPrec :: Int -> ReadS HighlightingLevel readList :: ReadS [HighlightingLevel] readPrec :: ReadPrec HighlightingLevel readListPrec :: ReadPrec [HighlightingLevel] | |||||
Show HighlightingLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> HighlightingLevel -> ShowS # show :: HighlightingLevel -> String # showList :: [HighlightingLevel] -> ShowS # | |||||
NFData HighlightingLevel | |||||
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: HighlightingLevel -> () | |||||
Eq HighlightingLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods (==) :: HighlightingLevel -> HighlightingLevel -> Bool (/=) :: HighlightingLevel -> HighlightingLevel -> Bool | |||||
Ord HighlightingLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods compare :: HighlightingLevel -> HighlightingLevel -> Ordering (<) :: HighlightingLevel -> HighlightingLevel -> Bool (<=) :: HighlightingLevel -> HighlightingLevel -> Bool (>) :: HighlightingLevel -> HighlightingLevel -> Bool (>=) :: HighlightingLevel -> HighlightingLevel -> Bool max :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel min :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel | |||||
type Rep HighlightingLevel Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types type Rep HighlightingLevel = D1 ('MetaData "HighlightingLevel" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) (C1 ('MetaCons "None" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonInteractive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Interactive" 'PrefixI 'False) (U1 :: Type -> Type))) |
data HighlightingMethod Source #
How should highlighting be sent to the user interface?
Instances
Generic HighlightingMethod Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Associated Types
Methods from :: HighlightingMethod -> Rep HighlightingMethod x to :: Rep HighlightingMethod x -> HighlightingMethod | |||||
Read HighlightingMethod Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods readsPrec :: Int -> ReadS HighlightingMethod readList :: ReadS [HighlightingMethod] readPrec :: ReadPrec HighlightingMethod readListPrec :: ReadPrec [HighlightingMethod] | |||||
Show HighlightingMethod Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> HighlightingMethod -> ShowS # show :: HighlightingMethod -> String # showList :: [HighlightingMethod] -> ShowS # | |||||
NFData HighlightingMethod | |||||
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: HighlightingMethod -> () | |||||
Eq HighlightingMethod Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods (==) :: HighlightingMethod -> HighlightingMethod -> Bool (/=) :: HighlightingMethod -> HighlightingMethod -> Bool | |||||
type Rep HighlightingMethod Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types type Rep HighlightingMethod = D1 ('MetaData "HighlightingMethod" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) (C1 ('MetaCons "Direct" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Indirect" 'PrefixI 'False) (U1 :: Type -> Type)) |
data Comparison Source #
Instances
Pretty Comparison Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Comparison -> Doc Source # prettyPrec :: Int -> Comparison -> Doc Source # prettyList :: [Comparison] -> Doc Source # | |||||
PrettyTCM Comparison Source # | |||||
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Comparison -> m Doc Source # | |||||
EmbPrj Comparison Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Comparison -> S Word32 Source # icod_ :: Comparison -> S Word32 Source # value :: Word32 -> R Comparison Source # | |||||
Generic Comparison Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Associated Types
| |||||
Show Comparison Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> Comparison -> ShowS # show :: Comparison -> String # showList :: [Comparison] -> ShowS # | |||||
NFData Comparison | |||||
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: Comparison -> () | |||||
Eq Comparison Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types | |||||
type Rep Comparison Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types type Rep Comparison = D1 ('MetaData "Comparison" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) (C1 ('MetaCons "CmpEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CmpLeq" 'PrefixI 'False) (U1 :: Type -> Type)) |
Polarity for equality and subtype checking.
Constructors
Covariant | monotone |
Contravariant | antitone |
Invariant | no information (mixed variance) |
Nonvariant | constant |
Instances
Pretty Polarity Source # | |||||
KillRange Polarity Source # | |||||
Defined in Agda.TypeChecking.Monad.Base Methods | |||||
PrettyTCM Polarity Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
EmbPrj Polarity Source # | |||||
Generic Polarity Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Associated Types
| |||||
Show Polarity Source # | |||||
NFData Polarity | |||||
Defined in Agda.TypeChecking.Monad.Base | |||||
Eq Polarity Source # | |||||
Abstract [Polarity] Source # | |||||
Apply [Polarity] Source # | |||||
type Rep Polarity Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types type Rep Polarity = D1 ('MetaData "Polarity" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) ((C1 ('MetaCons "Covariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Contravariant" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Invariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Nonvariant" 'PrefixI 'False) (U1 :: Type -> Type))) |
For printing, we couple a meta with its name suggestion.
Constructors
NamedMeta | |
Fields |
Instances
EncodeTCM NamedMeta Source # | |||||
Pretty NamedMeta Source # | |||||
ToConcrete NamedMeta Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types
| |||||
PrettyTCM NamedMeta Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
type ConOfAbs NamedMeta Source # | |||||
Defined in Agda.Syntax.Translation.AbstractToConcrete |
newtype SourceFile Source #
SourceFile
s must exist and be registered in our file dictionary.
Constructors
SourceFile | |
Instances
Generic SourceFile Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Associated Types
| |||||
Show SourceFile Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> SourceFile -> ShowS # show :: SourceFile -> String # showList :: [SourceFile] -> ShowS # | |||||
NFData SourceFile Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods rnf :: SourceFile -> () | |||||
Eq SourceFile Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types | |||||
Ord SourceFile Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods compare :: SourceFile -> SourceFile -> Ordering (<) :: SourceFile -> SourceFile -> Bool (<=) :: SourceFile -> SourceFile -> Bool (>) :: SourceFile -> SourceFile -> Bool (>=) :: SourceFile -> SourceFile -> Bool max :: SourceFile -> SourceFile -> SourceFile min :: SourceFile -> SourceFile -> SourceFile | |||||
type Rep SourceFile Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types type Rep SourceFile = D1 ('MetaData "SourceFile" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'True) (C1 ('MetaCons "SourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId))) |
data ModuleToSource Source #
Constructors
ModuleToSource | |
Fields |
Instances
Pretty ModuleToSource Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods pretty :: ModuleToSource -> Doc Source # prettyPrec :: Int -> ModuleToSource -> Doc Source # prettyList :: [ModuleToSource] -> Doc Source # |
Datatype representing a single boundary condition: x_0 = u_0, ... ,x_n = u_n ⊢ t = ?n es
data IsBuiltinModule Source #
Discern Agda's primitive modules from other file modules.
@IsPrimitiveModule implies
IsBuiltinModuleWithSafePostulate implies
isBuiltinModule.
Constructors
IsPrimitiveModule | Very magical module, e.g. |
IsBuiltinModuleWithSafePostulates | Safe module, e.g. |
IsBuiltinModule | Any builtin module. |
Instances
Generic IsBuiltinModule Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Associated Types
Methods from :: IsBuiltinModule -> Rep IsBuiltinModule x to :: Rep IsBuiltinModule x -> IsBuiltinModule | |||||
Show IsBuiltinModule Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> IsBuiltinModule -> ShowS # show :: IsBuiltinModule -> String # showList :: [IsBuiltinModule] -> ShowS # | |||||
NFData IsBuiltinModule Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods rnf :: IsBuiltinModule -> () | |||||
Eq IsBuiltinModule Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods (==) :: IsBuiltinModule -> IsBuiltinModule -> Bool (/=) :: IsBuiltinModule -> IsBuiltinModule -> Bool | |||||
Ord IsBuiltinModule Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods compare :: IsBuiltinModule -> IsBuiltinModule -> Ordering (<) :: IsBuiltinModule -> IsBuiltinModule -> Bool (<=) :: IsBuiltinModule -> IsBuiltinModule -> Bool (>) :: IsBuiltinModule -> IsBuiltinModule -> Bool (>=) :: IsBuiltinModule -> IsBuiltinModule -> Bool max :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule min :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule | |||||
type Rep IsBuiltinModule Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types type Rep IsBuiltinModule = D1 ('MetaData "IsBuiltinModule" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) (C1 ('MetaCons "IsPrimitiveModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "IsBuiltinModuleWithSafePostulates" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsBuiltinModule" 'PrefixI 'False) (U1 :: Type -> Type))) |
type Context = [ContextEntry] Source #
The Context
is a stack of ContextEntry
s.
data ContextEntry Source #
Instances
type BuiltinModuleIds = EnumMap FileId IsBuiltinModule Source #
Collection of FileId
s of primitive modules.
data FileDictWithBuiltins Source #
Translation between AbsolutePath
and FileId
that also knows about Agda's builtin modules.
Constructors
FileDictWithBuiltins | |
Fields
|
Instances
GetFileId FileDictWithBuiltins Source # | |||||
Defined in Agda.TypeChecking.Monad.Base | |||||
GetIdFile FileDictWithBuiltins Source # | |||||
Defined in Agda.TypeChecking.Monad.Base | |||||
Generic FileDictWithBuiltins Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Associated Types
Methods from :: FileDictWithBuiltins -> Rep FileDictWithBuiltins x to :: Rep FileDictWithBuiltins x -> FileDictWithBuiltins | |||||
NFData FileDictWithBuiltins Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types Methods rnf :: FileDictWithBuiltins -> () | |||||
type Rep FileDictWithBuiltins Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Types type Rep FileDictWithBuiltins = D1 ('MetaData "FileDictWithBuiltins" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" '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)))) |
type PrimitiveLibDir = AbsolutePath Source #
type ModuleToSourceId = Map TopLevelModuleName SourceFile Source #
Maps top-level module names to the corresponding source file ids.
type TopLevelModuleName = TopLevelModuleName' Range Source #
Top-level module names (with constant-time comparisons).
data AbsolutePath Source #
Paths which are known to be absolute.
Note that the Eq
and Ord
instances do not check if different
paths point to the same files or directories.
Instances
Pretty AbsolutePath Source # | |
Defined in Agda.Syntax.Common.Pretty Methods pretty :: AbsolutePath -> Doc Source # prettyPrec :: Int -> AbsolutePath -> Doc Source # prettyList :: [AbsolutePath] -> Doc Source # | |
GetFileId FileToId Source # | |
GetIdFile IdToFile Source # | |
ToJSON AbsolutePath Source # | |
Defined in Agda.Interaction.JSON Methods toJSON :: AbsolutePath -> Value # toEncoding :: AbsolutePath -> Encoding # toJSONList :: [AbsolutePath] -> Value # toEncodingList :: [AbsolutePath] -> Encoding # omitField :: AbsolutePath -> Bool # | |
Read AbsolutePath | |
Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS AbsolutePath readList :: ReadS [AbsolutePath] readPrec :: ReadPrec AbsolutePath readListPrec :: ReadPrec [AbsolutePath] | |
Show AbsolutePath Source # | |
Defined in Agda.Utils.FileName Methods showsPrec :: Int -> AbsolutePath -> ShowS # show :: AbsolutePath -> String # showList :: [AbsolutePath] -> ShowS # | |
NFData AbsolutePath Source # | |
Defined in Agda.Utils.FileName Methods rnf :: AbsolutePath -> () | |
Eq AbsolutePath Source # | |
Defined in Agda.Utils.FileName | |
Ord AbsolutePath Source # | |
Defined in Agda.Utils.FileName Methods compare :: AbsolutePath -> AbsolutePath -> Ordering (<) :: AbsolutePath -> AbsolutePath -> Bool (<=) :: AbsolutePath -> AbsolutePath -> Bool (>) :: AbsolutePath -> AbsolutePath -> Bool (>=) :: AbsolutePath -> AbsolutePath -> Bool max :: AbsolutePath -> AbsolutePath -> AbsolutePath min :: AbsolutePath -> AbsolutePath -> AbsolutePath | |
Hashable AbsolutePath Source # | |
Defined in Agda.Utils.FileName |
Unique identifier of a file.
Instances
GetFileId FileToId Source # | |||||
GetIdFile IdToFile Source # | |||||
Enum FileId Source # | |||||
Defined in Agda.Utils.FileId | |||||
Generic FileId Source # | |||||
Defined in Agda.Utils.FileId Associated Types
| |||||
Num FileId Source # | |||||
Show FileId Source # | |||||
NFData FileId Source # | |||||
Defined in Agda.Utils.FileId | |||||
Eq FileId Source # | |||||
Ord FileId Source # | |||||
type Rep FileId Source # | |||||
Defined in Agda.Utils.FileId |
data FileDictBuilder Source #
Instances
GetFileId FileDictBuilder Source # | |||||
Defined in Agda.Utils.FileId | |||||
GetIdFile FileDictBuilder Source # | |||||
Defined in Agda.Utils.FileId | |||||
Null FileDictBuilder Source # | |||||
Defined in Agda.Utils.FileId | |||||
Generic FileDictBuilder Source # | |||||
Defined in Agda.Utils.FileId Associated Types
Methods from :: FileDictBuilder -> Rep FileDictBuilder x to :: Rep FileDictBuilder x -> FileDictBuilder | |||||
NFData FileDictBuilder Source # | |||||
Defined in Agda.Utils.FileId Methods rnf :: FileDictBuilder -> () | |||||
type Rep FileDictBuilder Source # | |||||
Defined in Agda.Utils.FileId type Rep FileDictBuilder = D1 ('MetaData "FileDictBuilder" "Agda.Utils.FileId" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) (C1 ('MetaCons "FileDictBuilder" 'PrefixI 'True) (S1 ('MetaSel ('Just "nextFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just "fileDict") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict))) |