Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 Comparison
  - = CmpEq
  - | CmpLeq
- data Polarity
  - = Covariant
  - | Contravariant
  - | Invariant
  - | Nonvariant
- data HighlightingLevel
  - = None
  - | NonInteractive
  - | Interactive
- data HighlightingMethod
  - = Direct
  - | Indirect
- data NamedMeta = NamedMeta {
  - nmSuggestion :: MetaNameSuggestion
  - nmid :: MetaId
  }
- newtype SourceFile = SourceFile {
  - srcFileId :: FileId
  }
- data ModuleToSource = ModuleToSource {
  - fileDict :: !FileDictWithBuiltins
  - moduleToSourceId :: !ModuleToSourceId
  }
- data IPFace' t = IPFace' {
  - faceEqns :: [(t, t)]
  - faceRHS :: t
  }
- data IsBuiltinModule
  - = IsPrimitiveModule
  - | IsBuiltinModuleWithSafePostulates
  - | IsBuiltinModule
- type Context = [ContextEntry]
- data ContextEntry = CtxVar {
  - ceName :: Name
  - ceType :: Dom Type
  }
- type BuiltinModuleIds = EnumMap FileId IsBuiltinModule
- data FileDictWithBuiltins = FileDictWithBuiltins {
  - fileDictBuilder :: !FileDictBuilder
  - builtinModuleIds :: !BuiltinModuleIds
  - primitiveLibDir :: !PrimitiveLibDir
  }
- 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 Comparison Source #

Constructors

CmpEq |
CmpLeq |

#### Instances

Instances details

Pretty Comparison Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Comparison -> Doc Source # prettyPrec :: Int -> Comparison -> Doc Source # prettyList :: [Comparison] -> Doc Source #
PrettyTCM Comparison Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Comparison -> m Doc Source #
EmbPrj Comparison Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Comparison -> S Word32 Source # icod_ :: Comparison -> S Word32 Source # value :: Word32 -> R Comparison Source #
NFData Comparison Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: Comparison -> () Source #
Generic Comparison Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep Comparison |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types type Rep Comparison = D1 ('MetaData "Comparison" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "CmpEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CmpLeq" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: Comparison -> Rep Comparison x Source #

to :: Rep Comparison x -> Comparison Source #

Show Comparison Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> Comparison -> ShowS Source # show :: Comparison -> String Source # showList :: [Comparison] -> ShowS Source #
Eq Comparison Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods (==) :: Comparison -> Comparison -> Bool Source # (/=) :: Comparison -> Comparison -> Bool Source #
type Rep Comparison Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types type Rep Comparison = D1 ('MetaData "Comparison" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "CmpEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CmpLeq" 'PrefixI 'False) (U1 :: Type -> Type))

data Polarity Source #

Polarity for equality and subtype checking.

Constructors

Covariant | monotone
Contravariant | antitone
Invariant | no information (mixed variance)
Nonvariant | constant

#### Instances

Instances details

Pretty Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Polarity -> Doc Source # prettyPrec :: Int -> Polarity -> Doc Source # prettyList :: [Polarity] -> Doc Source #
KillRange Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Polarity Source #
PrettyTCM Polarity Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Polarity -> m Doc Source #
EmbPrj Polarity Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Polarity -> S Word32 Source # icod_ :: Polarity -> S Word32 Source # value :: Word32 -> R Polarity Source #
NFData Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: Polarity -> () Source #
Generic Polarity Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep Polarity |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep Polarity = D1 ('MetaData "Polarity" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

Methods

from :: Polarity -> Rep Polarity x Source #

to :: Rep Polarity x -> Polarity Source #

Show Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> Polarity -> ShowS Source # show :: Polarity -> String Source # showList :: [Polarity] -> ShowS Source #
Eq Polarity Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods (==) :: Polarity -> Polarity -> Bool Source # (/=) :: Polarity -> Polarity -> Bool Source #
Abstract [Polarity] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [Polarity] -> [Polarity] Source #
Apply [Polarity] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [Polarity] -> Args -> [Polarity] Source # applyE :: [Polarity] -> Elims -> [Polarity] Source #
type Rep Polarity Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep Polarity = D1 ('MetaData "Polarity" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

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

Instances details

NFData HighlightingLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: HighlightingLevel -> () Source #
Generic HighlightingLevel Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep HighlightingLevel |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep HighlightingLevel = D1 ('MetaData "HighlightingLevel" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

Methods

from :: HighlightingLevel -> Rep HighlightingLevel x Source #

to :: Rep HighlightingLevel x -> HighlightingLevel Source #

Read HighlightingLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods readsPrec :: Int -> ReadS HighlightingLevel Source # readList :: ReadS [HighlightingLevel] Source # readPrec :: ReadPrec HighlightingLevel Source # readListPrec :: ReadPrec [HighlightingLevel] Source #
Show HighlightingLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> HighlightingLevel -> ShowS Source # show :: HighlightingLevel -> String Source # showList :: [HighlightingLevel] -> ShowS Source #
Eq HighlightingLevel Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods (==) :: HighlightingLevel -> HighlightingLevel -> Bool Source # (/=) :: HighlightingLevel -> HighlightingLevel -> Bool Source #
Ord HighlightingLevel Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

compare :: HighlightingLevel -> HighlightingLevel -> Ordering Source #

(<) :: HighlightingLevel -> HighlightingLevel -> Bool Source #

(<=) :: HighlightingLevel -> HighlightingLevel -> Bool Source #

(>) :: HighlightingLevel -> HighlightingLevel -> Bool Source #

(>=) :: HighlightingLevel -> HighlightingLevel -> Bool Source #

max :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel Source #

min :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel Source #

type Rep HighlightingLevel Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep HighlightingLevel = D1 ('MetaData "HighlightingLevel" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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?

Constructors

Direct | Via stdout.
Indirect | Both via files and via stdout.

#### Instances

Instances details

NFData HighlightingMethod Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: HighlightingMethod -> () Source #
Generic HighlightingMethod Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep HighlightingMethod |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types type Rep HighlightingMethod = D1 ('MetaData "HighlightingMethod" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Direct" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Indirect" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: HighlightingMethod -> Rep HighlightingMethod x Source #

to :: Rep HighlightingMethod x -> HighlightingMethod Source #

Read HighlightingMethod Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods readsPrec :: Int -> ReadS HighlightingMethod Source # readList :: ReadS [HighlightingMethod] Source # readPrec :: ReadPrec HighlightingMethod Source # readListPrec :: ReadPrec [HighlightingMethod] Source #
Show HighlightingMethod Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> HighlightingMethod -> ShowS Source # show :: HighlightingMethod -> String Source # showList :: [HighlightingMethod] -> ShowS Source #
Eq HighlightingMethod Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods (==) :: HighlightingMethod -> HighlightingMethod -> Bool Source # (/=) :: HighlightingMethod -> HighlightingMethod -> Bool Source #
type Rep HighlightingMethod Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types type Rep HighlightingMethod = D1 ('MetaData "HighlightingMethod" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Direct" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Indirect" 'PrefixI 'False) (U1 :: Type -> Type))

data NamedMeta Source #

For printing, we couple a meta with its name suggestion.

Constructors

NamedMeta |

Fields

- nmSuggestion :: MetaNameSuggestion
- nmid :: MetaId

#### Instances

Instances details

EncodeTCM NamedMeta Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: NamedMeta -> TCM Value Source #
Pretty NamedMeta Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: NamedMeta -> Doc Source # prettyPrec :: Int -> NamedMeta -> Doc Source # prettyList :: [NamedMeta] -> Doc Source #
ToConcrete NamedMeta Source # |

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs NamedMeta |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs NamedMeta = Expr

Methods

toConcrete :: MonadToConcrete m => NamedMeta -> m (ConOfAbs NamedMeta) Source #

bindToConcrete :: MonadToConcrete m => NamedMeta -> (ConOfAbs NamedMeta -> m b) -> m b Source #

PrettyTCM NamedMeta Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedMeta -> m Doc Source #
type ConOfAbs NamedMeta Source # |
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs NamedMeta = Expr

newtype SourceFile Source #

`SourceFile`s must exist and be registered in our file dictionary.

Constructors

SourceFile |

Fields

- srcFileId :: FileId

#### Instances

Instances details

NFData SourceFile Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods rnf :: SourceFile -> () Source #
Generic SourceFile Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep SourceFile |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types type Rep SourceFile = D1 ('MetaData "SourceFile" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "SourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId)))

Methods

from :: SourceFile -> Rep SourceFile x Source #

to :: Rep SourceFile x -> SourceFile Source #

Show SourceFile Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> SourceFile -> ShowS Source # show :: SourceFile -> String Source # showList :: [SourceFile] -> ShowS Source #
Eq SourceFile Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods (==) :: SourceFile -> SourceFile -> Bool Source # (/=) :: SourceFile -> SourceFile -> Bool Source #
Ord SourceFile Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

compare :: SourceFile -> SourceFile -> Ordering Source #

(<) :: SourceFile -> SourceFile -> Bool Source #

(<=) :: SourceFile -> SourceFile -> Bool Source #

(>) :: SourceFile -> SourceFile -> Bool Source #

(>=) :: SourceFile -> SourceFile -> Bool Source #

max :: SourceFile -> SourceFile -> SourceFile Source #

min :: SourceFile -> SourceFile -> SourceFile Source #

type Rep SourceFile Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types type Rep SourceFile = D1 ('MetaData "SourceFile" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "SourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId)))

data ModuleToSource Source #

Constructors

ModuleToSource |

Fields

- fileDict :: !FileDictWithBuiltins
- moduleToSourceId :: !ModuleToSourceId

#### Instances

Instances details

Pretty ModuleToSource Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: ModuleToSource -> Doc Source # prettyPrec :: Int -> ModuleToSource -> Doc Source # prettyList :: [ModuleToSource] -> Doc Source #

data IPFace' t Source #

Datatype representing a single boundary condition: x_0 = u_0, ... ,x_n = u_n ⊢ t = ?n es

Constructors

IPFace' |

Fields

- faceEqns :: [(t, t)]
- faceRHS :: t

#### Instances

Instances details

Pretty c => Pretty (IPFace' c) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: IPFace' c -> Doc Source # prettyPrec :: Int -> IPFace' c -> Doc Source # prettyList :: [IPFace' c] -> Doc Source #

data IsBuiltinModule Source #

Discern Agda's primitive modules from other file modules. @IsPrimitiveModule `implies` IsBuiltinModuleWithSafePostulate `implies` isBuiltinModule.

Constructors

IsPrimitiveModule | Very magical module, e.g. `Agda.Primitive`.
IsBuiltinModuleWithSafePostulates | Safe module, e.g. `Agda.Builtin.Equality`.
IsBuiltinModule | Any builtin module.

#### Instances

Instances details

NFData IsBuiltinModule Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods rnf :: IsBuiltinModule -> () Source #
Generic IsBuiltinModule Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep IsBuiltinModule |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep IsBuiltinModule = D1 ('MetaData "IsBuiltinModule" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

Methods

from :: IsBuiltinModule -> Rep IsBuiltinModule x Source #

to :: Rep IsBuiltinModule x -> IsBuiltinModule Source #

Show IsBuiltinModule Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> IsBuiltinModule -> ShowS Source # show :: IsBuiltinModule -> String Source # showList :: [IsBuiltinModule] -> ShowS Source #
Eq IsBuiltinModule Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods (==) :: IsBuiltinModule -> IsBuiltinModule -> Bool Source # (/=) :: IsBuiltinModule -> IsBuiltinModule -> Bool Source #
Ord IsBuiltinModule Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

compare :: IsBuiltinModule -> IsBuiltinModule -> Ordering Source #

(<) :: IsBuiltinModule -> IsBuiltinModule -> Bool Source #

(<=) :: IsBuiltinModule -> IsBuiltinModule -> Bool Source #

(>) :: IsBuiltinModule -> IsBuiltinModule -> Bool Source #

(>=) :: IsBuiltinModule -> IsBuiltinModule -> Bool Source #

max :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule Source #

min :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule Source #

type Rep IsBuiltinModule Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep IsBuiltinModule = D1 ('MetaData "IsBuiltinModule" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 #

Constructors

CtxVar |

Fields

- ceName :: Name
- ceType :: Dom Type

#### Instances

Instances details

LensArgInfo ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods getArgInfo :: ContextEntry -> ArgInfo Source # setArgInfo :: ArgInfo -> ContextEntry -> ContextEntry Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> ContextEntry -> ContextEntry Source #
LensCohesion ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods getCohesion :: ContextEntry -> Cohesion Source # setCohesion :: Cohesion -> ContextEntry -> ContextEntry Source # mapCohesion :: (Cohesion -> Cohesion) -> ContextEntry -> ContextEntry Source #
LensHiding ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods getHiding :: ContextEntry -> Hiding Source # setHiding :: Hiding -> ContextEntry -> ContextEntry Source # mapHiding :: (Hiding -> Hiding) -> ContextEntry -> ContextEntry Source #
LensModalPolarity ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods getModalPolarity :: ContextEntry -> PolarityModality Source # setModalPolarity :: PolarityModality -> ContextEntry -> ContextEntry Source # mapModalPolarity :: (PolarityModality -> PolarityModality) -> ContextEntry -> ContextEntry Source #
LensModality ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods getModality :: ContextEntry -> Modality Source # setModality :: Modality -> ContextEntry -> ContextEntry Source # mapModality :: (Modality -> Modality) -> ContextEntry -> ContextEntry Source #
LensOrigin ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods getOrigin :: ContextEntry -> Origin Source # setOrigin :: Origin -> ContextEntry -> ContextEntry Source # mapOrigin :: (Origin -> Origin) -> ContextEntry -> ContextEntry Source #
LensQuantity ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods getQuantity :: ContextEntry -> Quantity Source # setQuantity :: Quantity -> ContextEntry -> ContextEntry Source # mapQuantity :: (Quantity -> Quantity) -> ContextEntry -> ContextEntry Source #
LensRelevance ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods getRelevance :: ContextEntry -> Relevance Source # setRelevance :: Relevance -> ContextEntry -> ContextEntry Source # mapRelevance :: (Relevance -> Relevance) -> ContextEntry -> ContextEntry Source #
Reify ContextEntry Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo ContextEntry |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo ContextEntry = TypedBinding

Methods

reify :: MonadReify m => ContextEntry -> m (ReifiesTo ContextEntry) Source #

reifyWhen :: MonadReify m => Bool -> ContextEntry -> m (ReifiesTo ContextEntry) Source #

AddContext ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ContextEntry -> m a -> m a Source # contextSize :: ContextEntry -> Nat Source #
PrettyTCM ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ContextEntry -> m Doc Source #
InstantiateFull ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ContextEntry -> ReduceM ContextEntry Source #
Subst ContextEntry Source # |

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ContextEntry |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ContextEntry = Term

Methods

applySubst :: Substitution' (SubstArg ContextEntry) -> ContextEntry -> ContextEntry Source #

NFData ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods rnf :: ContextEntry -> () Source #
Generic ContextEntry Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep ContextEntry |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep ContextEntry = D1 ('MetaData "ContextEntry" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

from :: ContextEntry -> Rep ContextEntry x Source #

to :: Rep ContextEntry x -> ContextEntry Source #

Show ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods showsPrec :: Int -> ContextEntry -> ShowS Source # show :: ContextEntry -> String Source # showList :: [ContextEntry] -> ShowS Source #
type ReifiesTo ContextEntry Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo ContextEntry = TypedBinding
type SubstArg ContextEntry Source # |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ContextEntry = Term
type Rep ContextEntry Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep ContextEntry = D1 ('MetaData "ContextEntry" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 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

- fileDictBuilder :: !FileDictBuilder

  (Building a) translation between `AbsolutePath` and `FileId`.

- builtinModuleIds :: !BuiltinModuleIds

  For the known `FileId`s, remember whether they refer to Agda's builtin modules.

- primitiveLibDir :: !PrimitiveLibDir

  The absolute path to the directory with the builtin modules. Needs to be set upon initialization.

#### Instances

Instances details

GetFileId FileDictWithBuiltins Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getFileId :: FileDictWithBuiltins -> File -> FileId Source #
GetIdFile FileDictWithBuiltins Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getIdFile :: FileDictWithBuiltins -> FileId -> File Source #
NFData FileDictWithBuiltins Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Types Methods rnf :: FileDictWithBuiltins -> () Source #
Generic FileDictWithBuiltins Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep FileDictWithBuiltins |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep FileDictWithBuiltins = D1 ('MetaData "FileDictWithBuiltins" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

from :: FileDictWithBuiltins -> Rep FileDictWithBuiltins x Source #

to :: Rep FileDictWithBuiltins x -> FileDictWithBuiltins Source #

type Rep FileDictWithBuiltins Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep FileDictWithBuiltins = D1 ('MetaData "FileDictWithBuiltins" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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.

lensFileDictFileDictBuilder :: Lens' FileDictWithBuiltins FileDictBuilder Source #

lensFileDictBuiltinModuleIds :: Lens' FileDictWithBuiltins BuiltinModuleIds Source #

lensFileDictPrimitiveLibDir :: Lens' FileDictWithBuiltins PrimitiveLibDir Source #

lensPairModuleToSource :: Lens' (FileDictWithBuiltins, ModuleToSourceId) ModuleToSource Source #

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

Instances details

Pretty AbsolutePath Source # |
Instance details Defined in Agda.Syntax.Common.Pretty Methods pretty :: AbsolutePath -> Doc Source # prettyPrec :: Int -> AbsolutePath -> Doc Source # prettyList :: [AbsolutePath] -> Doc Source #
GetFileId FileToId Source # |
Instance details Defined in Agda.Utils.FileId Methods getFileId :: FileToId -> File -> FileId Source #
GetIdFile IdToFile Source # |
Instance details Defined in Agda.Utils.FileId Methods getIdFile :: IdToFile -> FileId -> File Source #
ToJSON AbsolutePath Source # |
Instance details Defined in Agda.Interaction.JSON Methods toJSON :: AbsolutePath -> Value Source # toEncoding :: AbsolutePath -> Encoding Source # toJSONList :: [AbsolutePath] -> Value Source # toEncodingList :: [AbsolutePath] -> Encoding Source # omitField :: AbsolutePath -> Bool Source #
NFData AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods rnf :: AbsolutePath -> () Source #
Read AbsolutePath Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS AbsolutePath Source # readList :: ReadS [AbsolutePath] Source # readPrec :: ReadPrec AbsolutePath Source # readListPrec :: ReadPrec [AbsolutePath] Source #
Show AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods showsPrec :: Int -> AbsolutePath -> ShowS Source # show :: AbsolutePath -> String Source # showList :: [AbsolutePath] -> ShowS Source #
Eq AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods (==) :: AbsolutePath -> AbsolutePath -> Bool Source # (/=) :: AbsolutePath -> AbsolutePath -> Bool Source #
Ord AbsolutePath Source # |

Instance details

Defined in Agda.Utils.FileName

Methods

compare :: AbsolutePath -> AbsolutePath -> Ordering Source #

(<) :: AbsolutePath -> AbsolutePath -> Bool Source #

(<=) :: AbsolutePath -> AbsolutePath -> Bool Source #

(>) :: AbsolutePath -> AbsolutePath -> Bool Source #

(>=) :: AbsolutePath -> AbsolutePath -> Bool Source #

max :: AbsolutePath -> AbsolutePath -> AbsolutePath Source #

min :: AbsolutePath -> AbsolutePath -> AbsolutePath Source #

Hashable AbsolutePath Source # |
Instance details Defined in Agda.Utils.FileName Methods hashWithSalt :: Int -> AbsolutePath -> Int Source # hash :: AbsolutePath -> Int Source #

data FileId Source #

Unique identifier of a file.

#### Instances

Instances details

GetFileId FileToId Source # |
Instance details Defined in Agda.Utils.FileId Methods getFileId :: FileToId -> File -> FileId Source #
GetIdFile IdToFile Source # |
Instance details Defined in Agda.Utils.FileId Methods getIdFile :: IdToFile -> FileId -> File Source #
NFData FileId Source # |
Instance details Defined in Agda.Utils.FileId Methods rnf :: FileId -> () Source #
Enum FileId Source # |

Instance details

Defined in Agda.Utils.FileId

Methods

succ :: FileId -> FileId Source #

pred :: FileId -> FileId Source #

toEnum :: Int -> FileId Source #

fromEnum :: FileId -> Int Source #

enumFrom :: FileId -> [FileId] Source #

enumFromThen :: FileId -> FileId -> [FileId] Source #

enumFromTo :: FileId -> FileId -> [FileId] Source #

enumFromThenTo :: FileId -> FileId -> FileId -> [FileId] Source #

Generic FileId Source # |

Instance details

Defined in Agda.Utils.FileId

Associated Types

type Rep FileId |
Instance details Defined in Agda.Utils.FileId type Rep FileId = D1 ('MetaData "FileId" "Agda.Utils.FileId" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "FileId" 'PrefixI 'True) (S1 ('MetaSel ('Just "theFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))

Methods

from :: FileId -> Rep FileId x Source #

to :: Rep FileId x -> FileId Source #

Num FileId Source # |
Instance details Defined in Agda.Utils.FileId Methods (+) :: FileId -> FileId -> FileId Source # (-) :: FileId -> FileId -> FileId Source # (*) :: FileId -> FileId -> FileId Source # negate :: FileId -> FileId Source # abs :: FileId -> FileId Source # signum :: FileId -> FileId Source # fromInteger :: Integer -> FileId Source #
Show FileId Source # |
Instance details Defined in Agda.Utils.FileId Methods showsPrec :: Int -> FileId -> ShowS Source # show :: FileId -> String Source # showList :: [FileId] -> ShowS Source #
Eq FileId Source # |
Instance details Defined in Agda.Utils.FileId Methods (==) :: FileId -> FileId -> Bool Source # (/=) :: FileId -> FileId -> Bool Source #
Ord FileId Source # |
Instance details Defined in Agda.Utils.FileId Methods compare :: FileId -> FileId -> Ordering Source # (<) :: FileId -> FileId -> Bool Source # (<=) :: FileId -> FileId -> Bool Source # (>) :: FileId -> FileId -> Bool Source # (>=) :: FileId -> FileId -> Bool Source # max :: FileId -> FileId -> FileId Source # min :: FileId -> FileId -> FileId Source #
type Rep FileId Source # |
Instance details Defined in Agda.Utils.FileId type Rep FileId = D1 ('MetaData "FileId" "Agda.Utils.FileId" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "FileId" 'PrefixI 'True) (S1 ('MetaSel ('Just "theFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))

data FileDictBuilder Source #

#### Instances

Instances details

GetFileId FileDictBuilder Source # |
Instance details Defined in Agda.Utils.FileId Methods getFileId :: FileDictBuilder -> File -> FileId Source #
GetIdFile FileDictBuilder Source # |
Instance details Defined in Agda.Utils.FileId Methods getIdFile :: FileDictBuilder -> FileId -> File Source #
Null FileDictBuilder Source # |
Instance details Defined in Agda.Utils.FileId Methods empty :: FileDictBuilder Source # null :: FileDictBuilder -> Bool Source #
NFData FileDictBuilder Source # |
Instance details Defined in Agda.Utils.FileId Methods rnf :: FileDictBuilder -> () Source #
Generic FileDictBuilder Source # |

Instance details

Defined in Agda.Utils.FileId

Associated Types

type Rep FileDictBuilder |

Instance details

Defined in Agda.Utils.FileId

type Rep FileDictBuilder = D1 ('MetaData "FileDictBuilder" "Agda.Utils.FileId" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "FileDictBuilder" 'PrefixI 'True) (S1 ('MetaSel ('Just "nextFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just "fileDict") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict)))

Methods

from :: FileDictBuilder -> Rep FileDictBuilder x Source #

to :: Rep FileDictBuilder x -> FileDictBuilder Source #

type Rep FileDictBuilder Source # |

Instance details

Defined in Agda.Utils.FileId

type Rep FileDictBuilder = D1 ('MetaData "FileDictBuilder" "Agda.Utils.FileId" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "FileDictBuilder" 'PrefixI 'True) (S1 ('MetaSel ('Just "nextFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just "fileDict") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict)))