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
- = 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
- data Declaration
- = Axiom DefInfo QName Expr
- | Field DefInfo Hiding QName 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
- data LetBinding
- data Definition
- = FunDef DefInfo QName [Clause]
- | DataDef DefInfo QName Induction [LamBinding] [Constructor]
- | RecDef DefInfo QName (Maybe Constructor) [LamBinding] Expr [Declaration]
- | ScopedDef ScopeInfo Definition
- type TypeSignature = Declaration
- type Constructor = TypeSignature
- data LamBinding
- data TypedBindings = TypedBindings Range Hiding [TypedBinding]
- data TypedBinding
- type Telescope = [TypedBindings]
- data Clause = Clause LHS RHS [Declaration]
- data RHS
- data LHS = LHS LHSInfo QName [NamedArg Pattern] [Pattern]
- data Pattern' e
- type Pattern = Pattern' Expr
- allNames :: Declaration -> Seq QName
- axiomName :: Declaration -> QName
- module Agda.Syntax.Abstract.Name
Documentation
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 |
data Declaration Source
Axiom DefInfo QName Expr | postulate |
Field DefInfo Hiding QName 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 |
data LetBinding Source
LetBind LetInfo 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 |
data Definition Source
A definition without its type signature.
FunDef DefInfo QName [Clause] | |
DataDef DefInfo QName Induction [LamBinding] [Constructor] | the |
RecDef DefInfo QName (Maybe Constructor) [LamBinding] Expr [Declaration] | The |
ScopedDef ScopeInfo Definition |
type TypeSignature = DeclarationSource
Only Axiom
s.
type Constructor = TypeSignatureSource
data LamBinding Source
A lambda binding is either domain free or typed.
DomainFree Hiding Name | . |
DomainFull TypedBindings | . |
data TypedBindings Source
Typed bindings with hiding information.
TypedBindings Range Hiding [TypedBinding] | . |
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.
type Telescope = [TypedBindings]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.
RHS Expr | |
AbsurdRHS | |
WithRHS QName [Expr] [Clause] | The |
RewriteRHS [QName] [Expr] RHS [Declaration] | The |
Data RHS | |
Show RHS | |
Typeable RHS | |
KillRange RHS | |
HasRange RHS | |
ToAbstract AbstractRHS RHS | |
Reify ClauseBody RHS | |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |
Parameterised over the type of dot patterns.
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
.
module Agda.Syntax.Abstract.Name