Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 NameBound variables
Def QNameConstants (i.e. axioms, functions, and datatypes)
Con AmbiguousQNameConstructors
Lit LiteralLiterals
QuestionMark MetaInfometa variable for interaction
Underscore MetaInfometa 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) Exprindependent function space
Set ExprInfo Nat
Prop ExprInfo
Let ExprInfo [LetBinding] Expr
ETel Telescopeonly used when printing telescopes
Rec ExprInfo [(Name, Expr)]record construction
ScopedExpr ScopeInfo Exprscope annotation
data Declaration Source
Constructors
Axiom DefInfo QName Exprpostulate
Field DefInfo Hiding QName Exprrecord field
Primitive DefInfo QName Exprprimitive 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 ModuleNameonly retained for highlighting purposes
ScopedDecl ScopeInfo [Declaration]scope annotation
data Pragma Source
Constructors
OptionsPragma [String]
BuiltinPragma String Expr
CompiledPragma QName String
CompiledTypePragma QName String
CompiledDataPragma QName String [String]
data LetBinding Source
Constructors
LetBind LetInfo Name Expr ExprLetBind info name type defn
LetApply ModuleInfo ModuleName [TypedBindings] ModuleName [NamedArg Expr] (Map QName QName) (Map ModuleName ModuleName)
LetOpen ModuleInfo ModuleNameonly for highlighting
data Definition Source
A definition without its type signature.
Constructors
FunDef DefInfo QName [Clause]
DataDef DefInfo QName Induction [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
type TypeSignature = DeclarationSource
Only Axioms.
type Constructor = TypeSignatureSource
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}
data TypedBindings Source
Typed bindings with hiding information.
Constructors
TypedBindings Range Hiding [TypedBinding]. (xs:e;..;ys:e') or {xs:e;..;ys:e'}
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
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]
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 LHS Source
Constructors
LHS LHSInfo QName [NamedArg Pattern] [Pattern]
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 PatInfogenerated at type checking for implicit arguments
type Pattern = Pattern' ExprSource
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
Produced by Haddock version 2.6.0