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

Documentation

data Expr Source

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

data Definition Source

A definition without its type signature.

Constructors

FunDef DefInfo QName [Clause] 
DataDef DefInfo QName [LamBinding] [Constructor]

the LamBindings 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 

data TypedBinding Source

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 

data Clause Source

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] 

data RHS Source

Constructors

RHS Expr 
AbsurdRHS 
WithRHS QName [Expr] [Clause]

The QName is the name of the with function.

RewriteRHS [QName] [Expr] RHS [Declaration]

The QNames are the names of the generated with functions. One for each Expr. The RHS shouldn't be another RewriteRHS

data Pattern' e Source

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

allNames :: Declaration -> Seq QNameSource

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 -> QNameSource

The name defined by the given axiom.

Precondition: The declaration has to be an Axiom.