| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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

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

= OptionsPragma [String]
| BuiltinPragma String Expr
| CompiledPragma QName String
| CompiledTypePragma QName String
| CompiledDataPragma QName String [String]

data LetBinding

= LetBind LetInfo 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 Induction [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 Hiding [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 | 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

Instances

Data Expr
Show Expr
Typeable Expr
KillRange Expr
HasRange Expr
DotVars Expr
PrettyTCM Expr
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

data Declaration | Source

Constructors

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

Instances

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

data Pragma | Source

Constructors

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

Instances

Data Pragma
Show Pragma
Typeable Pragma

data LetBinding | Source

Constructors

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

Instances

Data LetBinding
Show LetBinding
Typeable LetBinding
KillRange LetBinding
HasRange LetBinding
ToConcrete LetBinding ([] Declaration)

data Definition | Source

A definition without its type signature.
Constructors

FunDef DefInfo QName [Clause] |
DataDef DefInfo QName Induction [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 | Source

Only `Axiom`s.

type Constructor = TypeSignature | Source

data LamBinding | Source

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

Typed bindings with hiding information.
Constructors

TypedBindings Range Hiding [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

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 |

Instances

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

type Telescope = [TypedBindings] | Source

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

Instances

Data Clause
Show Clause
Typeable Clause
KillRange Clause
HasRange Clause
ToAbstract Clause Clause
Reify NamedClause Clause
ToConcrete Clause ([] 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 `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 | Source

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

Instances

Functor Pattern'
Typeable1 Pattern'
Traversable Pattern'
Foldable 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 | Source

allNames :: Declaration -> Seq QName | Source

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

The name defined by the given axiom. Precondition: The declaration has to be an `Axiom`.
module Agda.Syntax.Abstract.Name
Produced by Haddock version 2.4.2