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

Agda.Syntax.Abstract

Description

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).

Synopsis

- data Expr
  - = Var Name
  - | Def QName
  - | Con AmbiguousQName
  - | Lit Literal
  - | QuestionMark MetaInfo
  - | Underscore MetaInfo
  - | App ExprInfo Expr (NamedArg Expr)
  - | WithApp ExprInfo Expr [Expr]
  - | Lam ExprInfo LamBinding Expr
  - | AbsurdLam ExprInfo Hiding
  - | Pi ExprInfo Telescope Expr
  - | Fun ExprInfo (Arg Expr) Expr
  - | Set ExprInfo Nat
  - | Prop ExprInfo
  - | Let ExprInfo [LetBinding] Expr
  - | ETel Telescope
  - | Rec ExprInfo [(Name, Expr)]
  - | ScopedExpr ScopeInfo Expr
  - | QuoteGoal ExprInfo Name Expr
  - | Quote ExprInfo
  - | DontCare
- data Declaration
  - = Axiom DefInfo Relevance QName Expr
  - | Field DefInfo QName (Arg Expr)
  - | Primitive DefInfo QName Expr
  - | Definition DeclInfo [TypeSignature] [Definition]
  - | Section ModuleInfo ModuleName [TypedBindings] [Declaration]
  - | Apply ModuleInfo ModuleName [TypedBindings] ModuleName [NamedArg Expr] (Map QName QName) (Map ModuleName ModuleName)
  - | Import ModuleInfo ModuleName
  - | Pragma Range Pragma
  - | Open ModuleInfo ModuleName
  - | ScopedDecl ScopeInfo [Declaration]
- data Pragma
  - = OptionsPragma [String]
  - | BuiltinPragma String Expr
  - | CompiledPragma QName String
  - | CompiledTypePragma QName String
  - | CompiledDataPragma QName String [String]
  - | CompiledEpicPragma QName String
  - | EtaPragma QName
- data LetBinding
  - = LetBind LetInfo Relevance Name Expr Expr
  - | LetApply ModuleInfo ModuleName [TypedBindings] ModuleName [NamedArg Expr] (Map QName QName) (Map ModuleName ModuleName)
  - | LetOpen ModuleInfo ModuleName
- data Definition
  - = FunDef DefInfo QName [Clause]
  - | DataDef DefInfo QName [LamBinding] [Constructor]
  - | RecDef DefInfo QName (Maybe Constructor) [LamBinding] Expr [Declaration]
  - | ScopedDef ScopeInfo Definition
- type TypeSignature = Declaration
- type Constructor = TypeSignature
- data LamBinding
  - = DomainFree Hiding Name
  - | DomainFull TypedBindings
- data TypedBindings = TypedBindings Range (Arg [TypedBinding])
- data TypedBinding
  - = TBind Range [Name] Expr
  - | TNoBind Expr
- type Telescope = [TypedBindings]
- data Clause = Clause LHS RHS [Declaration]
- data RHS
  - = RHS Expr
  - | AbsurdRHS
  - | WithRHS QName [Expr] [Clause]
  - | RewriteRHS [QName] [Expr] RHS [Declaration]
- data LHS = LHS LHSInfo QName [NamedArg Pattern] [Pattern]
- data Pattern' e
  - = VarP Name
  - | ConP PatInfo AmbiguousQName [NamedArg (Pattern' e)]
  - | DefP PatInfo QName [NamedArg (Pattern' e)]
  - | WildP PatInfo
  - | AsP PatInfo Name (Pattern' e)
  - | DotP PatInfo e
  - | AbsurdP PatInfo
  - | LitP Literal
  - | ImplicitP PatInfo
- type Pattern = Pattern' Expr
- allNames :: Declaration -> Seq QName
- axiomName :: Declaration -> QName
- module Agda.Syntax.Abstract.Name

# Documentation

data Expr

Constructors

Var Name | Bound variables
Def QName | Constants (i.e. axioms, functions, and datatypes)
Con AmbiguousQName | Constructors
Lit Literal | Literals
QuestionMark MetaInfo | meta variable for interaction
Underscore MetaInfo | meta variable for hidden argument (must be inferred locally)
App ExprInfo Expr (NamedArg Expr) |
WithApp ExprInfo Expr [Expr] | with application
Lam ExprInfo LamBinding Expr |
AbsurdLam ExprInfo Hiding |
Pi ExprInfo Telescope Expr |
Fun ExprInfo (Arg Expr) Expr | independent function space
Set ExprInfo Nat |
Prop ExprInfo |
Let ExprInfo [LetBinding] Expr |
ETel Telescope | only used when printing telescopes
Rec ExprInfo [(Name, Expr)] | record construction
ScopedExpr ScopeInfo Expr | scope annotation
QuoteGoal ExprInfo Name Expr |
Quote ExprInfo |
DontCare | for printing DontCare from Syntax.Internal

Instances

Data Expr |
Show Expr |
Typeable Expr |
KillRange Expr |
HasRange Expr |
DotVars Pattern |
DotVars Expr |
PrettyTCM Expr |
ToConcrete Pattern Pattern |
ToConcrete Expr Expr |
ToAbstract Expr Expr |
ToAbstract OldQName Expr |
Reify Literal Expr |
Reify MetaId Expr |
Reify Sort Expr |
Reify Type Expr |
Reify Term Expr |
Reify DisplayTerm Expr |
Reify Constraint (OutputForm Expr Expr) |

data Declaration

Constructors

Axiom DefInfo Relevance QName Expr | postulate
Field DefInfo QName (Arg Expr) | record field
Primitive DefInfo QName Expr | primitive function
Definition DeclInfo [TypeSignature] [Definition] | a bunch of mutually recursive definitions
Section ModuleInfo ModuleName [TypedBindings] [Declaration] |
Apply ModuleInfo ModuleName [TypedBindings] ModuleName [NamedArg Expr] (Map QName QName) (Map ModuleName ModuleName) |
Import ModuleInfo ModuleName |
Pragma Range Pragma |
Open ModuleInfo ModuleName | only retained for highlighting purposes
ScopedDecl ScopeInfo [Declaration] | scope annotation

Instances

Data Declaration |
Show Declaration |
Typeable Declaration |
KillRange Declaration |
HasRange Declaration |
ToAbstract NiceDeclaration Declaration |
ToAbstract ConstrDecl Declaration |
ToConcrete Declaration [Declaration] |
ToConcrete (Constr Constructor) Declaration |
ToConcrete [Declaration] [Declaration] |
ToAbstract [Declaration] [Declaration] |

data Pragma

Constructors

OptionsPragma [String] |
BuiltinPragma String Expr |
CompiledPragma QName String |
CompiledTypePragma QName String |
CompiledDataPragma QName String [String] |
CompiledEpicPragma QName String |
EtaPragma QName |

Instances

Data Pragma |
Show Pragma |
Typeable Pragma |
ToAbstract Pragma [Pragma] |

data LetBinding

Constructors

LetBind LetInfo Relevance Name Expr Expr | LetBind info name type defn
LetApply ModuleInfo ModuleName [TypedBindings] ModuleName [NamedArg Expr] (Map QName QName) (Map ModuleName ModuleName) |
LetOpen ModuleInfo ModuleName | only for highlighting and abstractToConcrete

Instances

Data LetBinding |
Show LetBinding |
Typeable LetBinding |
KillRange LetBinding |
HasRange LetBinding |
ToConcrete LetBinding [Declaration] |
ToAbstract LetDef [LetBinding] |
ToAbstract LetDefs [LetBinding] |

data Definition

A definition without its type signature.

Constructors

FunDef DefInfo QName [Clause] |
DataDef DefInfo QName [LamBinding] [Constructor] | the `LamBinding`s are `DomainFree` and binds the parameters of the datatype.
RecDef DefInfo QName (Maybe Constructor) [LamBinding] Expr [Declaration] | The `Expr` gives the constructor type telescope, `(x1 : A1)..(xn : An) -> Prop`, and the optional name is the constructor's name.
ScopedDef ScopeInfo Definition |

Instances

Data Definition |
Show Definition |
Typeable Definition |
KillRange Definition |
HasRange Definition |
ToAbstract NiceDefinition Definition |

type TypeSignature = Declaration

Only `Axiom`s.

type Constructor = TypeSignature

data LamBinding

A lambda binding is either domain free or typed.

Constructors

DomainFree Hiding Name | . `x` or `{x}`
DomainFull TypedBindings | . `(xs:e)` or `{xs:e}`

Instances

Data LamBinding |
Show LamBinding |
Typeable LamBinding |
KillRange LamBinding |
HasRange LamBinding |
ToConcrete LamBinding LamBinding |
ToAbstract LamBinding LamBinding |

data TypedBindings

Typed bindings with hiding information.

Constructors

TypedBindings Range (Arg [TypedBinding]) | . `(xs:e;..;ys:e')` or `{xs:e;..;ys:e'}`

Instances

Data TypedBindings |
Show TypedBindings |
Typeable TypedBindings |
KillRange TypedBindings |
HasRange TypedBindings |
DotVars TypedBindings |
ToConcrete TypedBindings TypedBindings |
ToAbstract TypedBindings TypedBindings |
Reify Telescope Telescope |

data TypedBinding

A typed binding. Appears in dependent function spaces, typed lambdas, and telescopes. I might be tempting to simplify this to only bind a single name at a time. This would mean that we would have to typecheck the type several times (`x,y:A` vs. `x:A; y:A`). In most cases this wouldn't really be a problem, but it's good principle to not do extra work unless you have to.

Constructors

TBind Range [Name] Expr |
TNoBind Expr |

Instances

Data TypedBinding |
Show TypedBinding |
Typeable TypedBinding |
KillRange TypedBinding |
HasRange TypedBinding |
DotVars TypedBinding |
ToConcrete TypedBinding TypedBinding |
ToAbstract TypedBinding TypedBinding |

type Telescope = [TypedBindings]

data Clause

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

Clause LHS RHS [Declaration] |

Instances

Data Clause |
Show Clause |
Typeable Clause |
KillRange Clause |
HasRange Clause |
ToAbstract Clause Clause |
Reify NamedClause Clause |
ToConcrete Clause [Declaration] |

data RHS

Constructors

RHS Expr |
AbsurdRHS |
WithRHS QName [Expr] [Clause] | The `QName` is the name of the with function.
RewriteRHS [QName] [Expr] RHS [Declaration] | The `QName`s are the names of the generated with functions. One for each `Expr`. The RHS shouldn't be another RewriteRHS

Instances

Data RHS |
Show RHS |
Typeable RHS |
KillRange RHS |
HasRange RHS |
ToAbstract AbstractRHS RHS |
Reify ClauseBody RHS |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |

data LHS

Constructors

LHS LHSInfo QName [NamedArg Pattern] [Pattern] |

Instances

Data LHS |
Show LHS |
Typeable LHS |
KillRange LHS |
HasRange LHS |
ToConcrete LHS LHS |
ToAbstract LeftHandSide LHS |

data Pattern' e

Parameterised over the type of dot patterns.

Constructors

VarP Name |
ConP PatInfo AmbiguousQName [NamedArg (Pattern' e)] |
DefP PatInfo QName [NamedArg (Pattern' e)] | defined pattern
WildP PatInfo |
AsP PatInfo Name (Pattern' e) |
DotP PatInfo e |
AbsurdP PatInfo |
LitP Literal |
ImplicitP PatInfo | generated at type checking for implicit arguments

Instances

Functor Pattern' |
Typeable1 Pattern' |
Foldable Pattern' |
Traversable Pattern' |
DotVars Pattern |
ToConcrete Pattern Pattern |
ToAbstract Pattern (Pattern' Expr) |
Data e => Data (Pattern' e) |
Show e => Show (Pattern' e) |
KillRange e => KillRange (Pattern' e) |
HasRange (Pattern' e) |
ToAbstract c a => ToAbstract (Pattern' c) (Pattern' a) |

type Pattern = Pattern' Expr

allNames :: Declaration -> Seq QName

Extracts all the names which are declared in a `Declaration`. This does not include open public or let expressions, but it does include local modules and where clauses.

axiomName :: Declaration -> QName

The name defined by the given axiom.

Precondition: The declaration has to be an `Axiom`.

module Agda.Syntax.Abstract.Name