Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



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



data Expr Source


Var Name

Bound variables

Def QName

Constants (i.e. axioms, functions, projections, and datatypes)

Con AmbiguousQName


Lit Literal


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 
ExtendedLam ExprInfo DefInfo QName [Clause] 
Pi ExprInfo Telescope Expr 
Fun ExprInfo (Arg Expr) Expr

independent function space

Set ExprInfo Integer

Set, Set1, Set2, ...

Prop ExprInfo 
Let ExprInfo [LetBinding] Expr 
ETel Telescope

only used when printing telescopes

Rec ExprInfo [(Name, Expr)]

record construction

RecUpdate ExprInfo Expr [(Name, Expr)]

record update

ScopedExpr ScopeInfo Expr

scope annotation

QuoteGoal ExprInfo Name Expr

binds Name to current type in Expr

Quote ExprInfo 
QuoteTerm ExprInfo 
Unquote ExprInfo

The splicing construct: unquote ...

DontCare Expr

for printing DontCare from Syntax.Internal

PatternSyn QName 

data Declaration Source


Axiom DefInfo Relevance QName Expr


Field DefInfo QName (Arg Expr)

record field

Primitive DefInfo QName Expr

primitive function

Mutual MutualInfo [Declaration]

a bunch of mutually recursive definitions

Section ModuleInfo ModuleName [TypedBindings] [Declaration] 
Apply ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName) 
Import ModuleInfo ModuleName 
Pragma Range Pragma 
Open ModuleInfo ModuleName

only retained for highlighting purposes

FunDef DefInfo QName Delayed [Clause]

sequence of function clauses

DataSig DefInfo QName Telescope Expr

lone data signature ^ the LamBindings are DomainFree and binds the parameters of the datatype.

DataDef DefInfo QName [LamBinding] [Constructor]

the LamBindings are DomainFree and binds the parameters of the datatype.

RecSig DefInfo QName Telescope Expr

lone record signature

RecDef DefInfo QName (Maybe Induction) (Maybe QName) [LamBinding] Expr [Declaration]

The Expr gives the constructor type telescope, (x1 : A1)..(xn : An) -> Prop, and the optional name is the constructor's name.

ScopedDecl ScopeInfo [Declaration]

scope annotation

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.


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.



data RHS Source


RHS Expr 
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 SpineLHS Source

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




spLhsInfo :: LHSInfo


spLhsDefName :: QName

Name of function we are defining.

spLhsPats :: [NamedArg Pattern]

Function parameters (patterns).

spLhsWithPats :: [Pattern]

with patterns (after |).

data LHS Source

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




lhsInfo :: LHSInfo


lhsCore :: LHSCore


lhsWithPats :: [Pattern]

with patterns (after |).

data LHSCore' e Source

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



The head applied to ordinary patterns.


lhsDefName :: QName

Head f.

lhsPats :: [NamedArg (Pattern' e)]

Applied to patterns ps.




lhsDestructor :: QName

Record projection identifier.

lhsPatsLeft :: [NamedArg (Pattern' e)]

Indices of the projection. Currently none [], since we do not have indexed records.

lhsFocus :: NamedArg (LHSCore' e)

Main branch.

lhsPatsRight :: [NamedArg (Pattern' e)]

Further applied to patterns.

lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]Source

Used for checking pattern linearity.

lhsCoreToPattern :: LHSCore -> PatternSource

Used in AbstractToConcrete.

data Pattern' e Source

Parameterised over the type of dot patterns.


VarP Name 
ConP PatInfo AmbiguousQName [NamedArg (Pattern' e)] 
DefP PatInfo QName [NamedArg (Pattern' e)]

Defined pattern: function definition f ps or destructor pattern d p ps.

WildP PatInfo 
AsP PatInfo Name (Pattern' e) 
DotP PatInfo e 
AbsurdP PatInfo 
LitP Literal 
ImplicitP PatInfo

Generated at type checking for implicit arguments.

PatternSynP PatInfo QName [NamedArg (Pattern' e)] 

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, where clauses and the names of extended lambdas.

axiomName :: Declaration -> QNameSource

The name defined by the given axiom.

Precondition: The declaration has to be an Axiom.

class AnyAbstract a whereSource

Are we in an abstract block?

In that case some definition is abstract.


anyAbstract :: a -> BoolSource