Agda-2.3.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Infered

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
  - | 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
  - = SectionApp [TypedBindings] ModuleName [NamedArg Expr]
  - | RecordModuleIFS ModuleName
- data Pragma
  - = OptionsPragma [String]
  - | BuiltinPragma String Expr
  - | CompiledPragma QName String
  - | CompiledTypePragma QName String
  - | CompiledDataPragma QName String [String]
  - | CompiledEpicPragma QName String
  - | CompiledJSPragma QName String
  - | StaticPragma QName
  - | EtaPragma QName
- data LetBinding
  - = LetBind LetInfo Relevance Name Expr Expr
  - | LetApply ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName)
  - | LetOpen ModuleInfo ModuleName
- type TypeSignature = Declaration
- type Constructor = TypeSignature
- data LamBinding
  - = DomainFree Hiding Relevance Name
  - | DomainFull TypedBindings
- data TypedBindings = TypedBindings Range (Arg 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
- class AnyAbstract a where
  - anyAbstract :: a -> Bool
- module Agda.Syntax.Abstract.Name

# Documentation

data Expr

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

Instances

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

Constructors

Axiom DefInfo Relevance QName Expr | postulate
Field DefInfo QName (Arg Expr) | record field
Primitive DefInfo QName Expr | primitive function
Mutual DeclInfo [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 [Clause] |
DataSig DefInfo QName Telescope Expr | lone data signature ^ the `LamBinding`s are `DomainFree` and binds the parameters of the datatype.
DataDef DefInfo QName [LamBinding] [Constructor] | the `LamBinding`s are `DomainFree` and binds the parameters of the datatype.
RecSig DefInfo QName Telescope Expr | lone record signature
RecDef DefInfo QName (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

Instances

Data Declaration |
Show Declaration |
Typeable Declaration |
KillRange Declaration |
HasRange Declaration |
AnyAbstract Declaration |
GetDefInfo Declaration |
ToAbstract NiceDeclaration Declaration |
ToAbstract ConstrDecl Declaration |
ToConcrete Declaration [Declaration] |
ToConcrete (Constr Constructor) Declaration |
ToAbstract [Declaration] [Declaration] |

class GetDefInfo a where

Methods

getDefInfo :: a -> Maybe DefInfo

Instances

GetDefInfo Declaration |

data ModuleApplication

Constructors

SectionApp [TypedBindings] ModuleName [NamedArg Expr] |
RecordModuleIFS ModuleName |

Instances

Data ModuleApplication |
Show ModuleApplication |
Typeable ModuleApplication |
KillRange ModuleApplication |
ToConcrete ModuleApplication ModuleApplication |

data Pragma

Constructors

OptionsPragma [String] |
BuiltinPragma String Expr |
CompiledPragma QName String |
CompiledTypePragma QName String |
CompiledDataPragma QName String [String] |
CompiledEpicPragma QName String |
CompiledJSPragma QName String |
StaticPragma QName |
EtaPragma QName |

Instances

Data Pragma |
Show Pragma |
Typeable Pragma |
ToAbstract Pragma [Pragma] |

data LetBinding

Constructors

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

Instances

Data LetBinding |
Show LetBinding |
Typeable LetBinding |
KillRange LetBinding |
HasRange LetBinding |
ToConcrete LetBinding [Declaration] |
ToAbstract LetDef [LetBinding] |
ToAbstract LetDefs [LetBinding] |

type TypeSignature = Declaration

Only `Axiom`s.

type Constructor = TypeSignature

data LamBinding

A lambda binding is either domain free or typed.

Constructors

DomainFree Hiding Relevance Name | . `x` or `{x}` or `.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

Typed bindings with hiding information.

Constructors

TypedBindings Range (Arg TypedBinding) | . `(xs : e)` or `{xs : e}`

Instances

Data TypedBindings |
Show TypedBindings |
Typeable TypedBindings |
KillRange TypedBindings |
HasRange TypedBindings |
DotVars TypedBindings |
ToConcrete TypedBindings TypedBindings |
ToAbstract TypedBindings TypedBindings |
Reify Telescope Telescope |

data TypedBinding

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]

data Clause

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 |
DotVars Clause |
ToAbstract Clause Clause |
Reify NamedClause Clause |
ToConcrete Clause [Declaration] |

data RHS

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 |
DotVars RHS |
ToAbstract AbstractRHS RHS |
Reify ClauseBody RHS |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |

data LHS

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

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

type Pattern = Pattern' Expr

allNames :: Declaration -> Seq QName

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

The name defined by the given axiom.

Precondition: The declaration has to be an `Axiom`.

class AnyAbstract a where

Are we in an abstract block?

In that case some definition is abstract.

Methods

anyAbstract :: a -> Bool

Instances

AnyAbstract Declaration |
AnyAbstract a => AnyAbstract [a] |

module Agda.Syntax.Abstract.Name