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
- | ExtendedLam ExprInfo DefInfo QName [Clause]
- | Pi ExprInfo Telescope Expr
- | Fun ExprInfo (Arg Expr) Expr
- | Set ExprInfo Nat
- | Prop ExprInfo
- | Let ExprInfo [LetBinding] Expr
- | ETel Telescope
- | Rec ExprInfo [(Name, Expr)]
- | RecUpdate ExprInfo Expr [(Name, Expr)]
- | ScopedExpr ScopeInfo Expr
- | QuoteGoal ExprInfo Name Expr
- | Quote ExprInfo
- | QuoteTerm ExprInfo
- | Unquote ExprInfo
- | DontCare Expr
- data Declaration
- = Axiom DefInfo Relevance QName Expr
- | Field DefInfo QName (Arg Expr)
- | Primitive DefInfo QName Expr
- | Mutual DeclInfo [Declaration]
- | Section ModuleInfo ModuleName [TypedBindings] [Declaration]
- | Apply ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName)
- | Import ModuleInfo ModuleName
- | Pragma Range Pragma
- | Open ModuleInfo ModuleName
- | FunDef DefInfo QName [Clause]
- | DataSig DefInfo QName Telescope Expr
- | DataDef DefInfo QName [LamBinding] [Constructor]
- | RecSig DefInfo QName Telescope Expr
- | RecDef DefInfo QName (Maybe QName) [LamBinding] Expr [Declaration]
- | ScopedDecl ScopeInfo [Declaration]
- class GetDefInfo a where
- getDefInfo :: a -> Maybe DefInfo
- data ModuleApplication
- data Pragma
- data LetBinding
- type TypeSignature = Declaration
- type Constructor = TypeSignature
- data LamBinding
- data TypedBindings = TypedBindings Range (Arg 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
- class AnyAbstract a where
- anyAbstract :: a -> Bool
- 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 | |
ExtendedLam ExprInfo DefInfo QName [Clause] | |
Pi ExprInfo Telescope Expr | |
Fun ExprInfo (Arg Expr) Expr | independent function space |
Set ExprInfo Nat | 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 | |
Quote ExprInfo | |
QuoteTerm ExprInfo | |
Unquote ExprInfo | The splicing construct: unquote ... |
DontCare Expr | for printing DontCare from Syntax.Internal |
Data Expr | |
Show Expr | |
Typeable Expr | |
KillRange Expr | |
HasRange Expr | |
PrettyTCM Expr | |
DotVars Pattern | |
DotVars Expr | Getting all(!) variables of an expression. It should only get free ones, but it does not matter to include the bound ones. |
ToConcrete Pattern Pattern | |
ToConcrete Expr Expr | |
ToAbstract Expr Expr | |
ToAbstract OldQName Expr | |
Reify Literal Expr | |
Reify MetaId Expr | |
Reify Level Expr | |
Reify Sort Expr | |
Reify Elim Expr | |
Reify Type Expr | |
Reify Term Expr | |
Reify DisplayTerm Expr | |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) | |
Reify Constraint (OutputConstraint Expr Expr) |
data Declaration Source
data ModuleApplication Source
data LetBinding Source
LetBind LetInfo Relevance Name Expr Expr | LetBind info rel name type defn |
LetApply ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName) | |
LetOpen ModuleInfo ModuleName | only for highlighting and abstractToConcrete |
type TypeSignature = DeclarationSource
Only Axiom
s.
type Constructor = TypeSignatureSource
data LamBinding Source
A lambda binding is either domain free or typed.
DomainFree Hiding Relevance Name | . |
DomainFull TypedBindings | . |
data TypedBindings Source
Typed bindings with hiding information.
TypedBindings Range (Arg 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 | |
DotVars RHS | |
ToAbstract AbstractRHS RHS | |
Reify ClauseBody RHS | |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |
Parameterised over the type of dot patterns.
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 |
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) |
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
AnyAbstract Declaration | |
AnyAbstract a => AnyAbstract [a] |
module Agda.Syntax.Abstract.Name