HORIZON HASKELLDocslts/ghc-10.0.x8174fa42026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 8174fa4 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Abstract

The abstract syntax. This is what you get after desugaring and scope analysis of the concrete syntax. The type checker works on abstract syntax, producing internal syntax (Agda.Syntax.Internal).

  • 58 types
  • 3 classes
  • 23 values
  • PackageAgda-2.8.0.2
  • Exports85
  • LanguageHaskell2010
  • LicenceMIT
  • SourceAbstract.hs
newtypenewtype BindName
#

A name in a binding position: we also compare the nameConcrete when comparing the binders for equality.

With --caching on we compare abstract syntax to determine if we can reuse previous typechecking results: during that comparison two names can have the same nameId but be semantically different, e.g. in {_ : A} -> .. vs. {r : A} -> ...

Constructors

Instances18Eq, Ord, Show, NFData, HasRange, Hilite, …
datadata Binder' a
#

Constructors

Instances15Functor, Foldable, Traversable, Eq, Show, Generic, …
datadata Clause' lhs
#

We could throw away where clauses at this point and translate them to let. It's not obvious how to remember that the let was really a where clause though, so for the time being we keep it here.

Constructors

Instances18Functor, Foldable, Traversable, DeclaredNames, BlankVars, LHSToSpine, …
datadata DataDefParams
#

Constructors

Instances8Eq, Show, Generic, NFData, Hilite, KillRange, …
datadata Declaration
#

Constructors

Instances16Eq, Show, Generic, NFData, HasRange, Hilite, …
datadata DeclarationSpine
#

Declaration spines. Used in debugging to make it easy to see where constructors such as ScopedDecl and Mutual are placed.

Constructors

Instances1Show
datadata Expr
#

Expressions after scope checking (operators parsed, names resolved).

Constructors

Instances48Eq, Show, Generic, NFData, IsProjP, HasRange, …
datadata GeneralizeTelescope
#

Constructors

Instances8Eq, Show, Generic, NFData, Hilite, KillRange, …
datadata LHS
#

The lhs of a clause in focused (projection-application) view (outside-in). Projection patters are represented as LHSProjs.

Constructors

Instances18Eq, Show, Generic, NFData, HasRange, ToConcrete, …
datadata LHSCore' e
#

The lhs in projection-application and with-pattern view. Parameterised over the type e of dot patterns.

Constructors

Instances19Functor, Foldable, Traversable, ToConcrete, BlankVars, Binder, …
datadata LamBinding
#

A lambda binding is either domain free or typed.

Constructors

Instances15Eq, Show, Generic, NFData, HasRange, ToConcrete, …
datadata LetBinding
#

Bindings that are valid in a let.

Constructors

Instances13Eq, Show, Generic, NFData, HasRange, ToConcrete, …
datadata ModuleApplication
#

Constructors

Instances11Eq, Show, Generic, NFData, ToConcrete, Hilite, …
datadata Pattern' e
#

Parameterised over the type of dot patterns.

Constructors

Instances42Functor, Foldable, Traversable, PrettyTCM, BlankVars, MapNamedArgPattern, …
datadata Pragma
#

Constructors

Instances8Eq, Show, Generic, NFData, Hilite, DeclaredNames, …
datadata ProblemEq
#

A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.

Constructors

Instances11Eq, Show, Generic, NFData, Subst, PrettyTCM, …
datadata RHS
#

Constructors

Instances14Eq, Show, Generic, NFData, HasRange, ToConcrete, …
datadata RecordConName
#

How did we get our hands on the QName for the constructor of this record?

Constructors

Instances11Eq, Show, Generic, NFData, ToConcrete, Hilite, …
  • Eq RecordConNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
  • Show RecordConNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
  • Generic RecordConNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
  • NFData RecordConNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
  • ToConcrete RecordDirectivesDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
  • Hilite RecordConNameDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract
  • Hilite RecordDirectivesDefined in Agda-2.8.0.2 · Agda.Interaction.Highlighting.FromAbstract

    Reengineered from the old Geniplate-implemented highlighting extraction. This was the old procedure:

    Traversal over declaration in abstract syntax that collects the following hiliting information:

    1. constructorInfo (highest prio)

    2.

    theRest

    (medium prio) 3.

    nameInfo

    (lowest prio)

    nameInfo: "All names mentioned in the syntax tree (not bound variables)." For each possibly ambiguous name (QName and AmbiguousQName) that not isExtendedLambdaName, do hiliteAmbiguous (used to be calledgenerate).

    constructorInfo (only when highlighting level == Full): "After the code has been type checked more information may be available for overloaded constructors, and generateConstructorInfo takes advantage of this information. Note, however, that highlighting for overloaded constructors is included also in nameInfo." This is not computed by recursion over the abstract syntax, but gets the constructor names stDisambiguatedNames that fall within the bounds of the current declaration.

    theRest: Bound variables, dotted patterns, record fields, module names, the "as" and "to" symbols and some other things.

    Here is a table what theRest used to collect:

    • -------------------------------------------------------------------- | A.Expr

    • -------------------------------------------------------------------- | getVarAndField (Expr) | A.Var | bound | getVarAndField | A.Rec(Update) | field | getExpr (Expr) | A.PatternSyn | patsyn | getExpr | A.Macro | macro

    • -------------------------------------------------------------------- | A.LetBinding

    • -------------------------------------------------------------------- | getLet | A.LetBind | bound

    • -------------------------------------------------------------------- | A.LamBinding

    • -------------------------------------------------------------------- | getLam | A.Binder under A.DomainFree | bound | getTyped | A.Binder under A.TBind | bound

    • -------------------------------------------------------------------- | A.Pattern'

    • -------------------------------------------------------------------- | getPattern(Syn) | A.VarP | bound | getPattern(Syn) | A.AsP | bound | getPattern(Syn) | A.DotP (not isProjP) | DottedPattern | getPattern(Syn) | A.RecP | field | getPattern(Syn) | A.PatternSynP | patsyn

    • -------------------------------------------------------------------- | A.Declaration

    • -------------------------------------------------------------------- | getFieldDecl | A.Field under A.RecDef | field | getPatSynArgs | A.PatternSynDef | bound | getPragma | A.BuiltinPragma... | keyword

    • -------------------------------------------------------------------- | A.NamedArg (polymorphism not supported in geniplate)

    • -------------------------------------------------------------------- | getNamedArg | NamedArg a | nameOf | getNamedArgE | NamedArg Exp | nameOf | getNamedArgP | NamedArg Pattern | nameOf | getNamedArgB | NamedArg BindName | nameOf | getNamedArgL | NamedArg LHSCore | nameOf

    | getModuleName | A.MName | mod | getModuleInfo | ModuleInfo | asName, (range of as,to) | getQuantityAttr | Common.Quantity | Symbol (if range)

  • DeclaredNames RecordDirectivesDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract.Views
  • KillRange RecordConNameDefined in Agda-2.8.0.2 · Agda.Syntax.Abstract
  • type Rep RecordConName = D1 ('MetaData "RecordConName" "Agda.Syntax.Abstract" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" 'False) (C1 ('MetaCons "NamedRecCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "recordConName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName)) :+: C1 ('MetaCons "FreshRecCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "recordConName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName)))Defined in Agda-2.8.0.2 · Agda.Syntax.Abstract
  • type ConOfAbs RecordDirectives = [RecordDirective]Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete
datadata ScopeCopyInfo
#

Constructors

Instances7Eq, Show, Generic, NFData, Pretty, KillRange, …
datadata SpineLHS
#

The lhs of a clause in spine view (inside-out). Projection patterns are contained in spLhsPats, represented as ProjP d.

Constructors

Instances12Eq, Show, Generic, NFData, HasRange, ToConcrete, …
classclass SubstExpr a where
#

Methods

Instances11SubstExpr, …
typetype Type = Expr
#

Types are just expressions. Use this type synonym for hinting that an expression should be a type.

datadata TypedBinding
#

A typed binding. Appears in dependent function spaces, typed lambdas, and telescopes. It might be tempting to simplify this to only bind a single name at a time, and translate, say, (x y : A) to (x : A)(y : A) before type-checking. However, this would be slightly problematic:

  1. We would have to typecheck the type A several times.

  2. If A contains a meta variable or hole, it would be duplicated by such a translation.

While 1. is only slightly inefficient, 2. would be an outright bug. Duplicating A could not be done naively, we would have to make sure that the metas of the copy are aliases of the metas of the original.

Constructors

Instances16Eq, Show, Generic, NFData, HasRange, PrettyTCM, …
datadata TypedBindingInfo
#

Extra information that is attached to a typed binding, that plays a role during type checking but strictly speaking is not part of the name : type" relation which a makes up a binding.

Constructors

  • TypedBindingInfo
    • tbTacticAttr :: TacticAttribute

      Does this binding have a tactic annotation?

    • tbFinite :: Bool

      Does this binding correspond to a Partial binder, rather than to a Pi binder? Must be present here to be reflected into abstract syntax later (and to be printed to the user later).

Instances9Eq, Show, Generic, NFData, Null, Hilite, …
datadata WhereDeclarations
#

Constructors

Instances13Eq, Show, Generic, NFData, Null, HasRange, …

module Agda.Syntax.Abstract.Name

Orphan instances

1 instance