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

Safe Haskell | None

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 Integer
  - | 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
  - | PatternSyn QName
- data Declaration
  - = Axiom DefInfo Relevance QName Expr
  - | Field DefInfo QName (Arg Expr)
  - | Primitive DefInfo QName Expr
  - | Mutual MutualInfo [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 Delayed [Clause]
  - | DataSig DefInfo QName Telescope Expr
  - | DataDef DefInfo QName [LamBinding] [Constructor]
  - | RecSig DefInfo QName Telescope Expr
  - | RecDef DefInfo QName (Maybe Induction) (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
  - | LetPatBind LetInfo Pattern Expr
  - | LetApply ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName)
  - | LetOpen ModuleInfo ModuleName
- type TypeSignature = Declaration
- type Constructor = TypeSignature
- type Field = 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 {
  - clauseLHS :: LHS
  - clauseRHS :: RHS
  - clauseWhereDecls :: [Declaration]
  }
- data RHS
  - = RHS Expr
  - | AbsurdRHS
  - | WithRHS QName [Expr] [Clause]
  - | RewriteRHS [QName] [Expr] RHS [Declaration]
- data SpineLHS = SpineLHS {
  - spLhsInfo :: LHSInfo
  - spLhsDefName :: QName
  - spLhsPats :: [NamedArg Pattern]
  - spLhsWithPats :: [Pattern]
  }
- data LHS = LHS {
  - lhsInfo :: LHSInfo
  - lhsCore :: LHSCore
  - lhsWithPats :: [Pattern]
  }
- data LHSCore' e
  - = LHSHead {
    - lhsDefName :: QName
    - lhsPats :: [NamedArg (Pattern' e)]
    }
  - | LHSProj {
    - lhsDestructor :: QName
    - lhsPatsLeft :: [NamedArg (Pattern' e)]
    - lhsFocus :: NamedArg (LHSCore' e)
    - lhsPatsRight :: [NamedArg (Pattern' e)]
    }
- type LHSCore = LHSCore' Expr
- lhsToSpine :: LHS -> SpineLHS
- lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)]
- lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]
- lhsCoreToPattern :: LHSCore -> Pattern
- mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore
- 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
  - | PatternSynP PatInfo QName [NamedArg (Pattern' e)]
- type Pattern = Pattern' Expr
- type Patterns = [NamedArg Pattern]
- allNames :: Declaration -> Seq QName
- axiomName :: Declaration -> QName
- class AnyAbstract a where
  - anyAbstract :: a -> Bool
- app :: Expr -> [NamedArg Expr] -> Expr
- patternToExpr :: Pattern -> Expr
- type PatternSynDefn = ([Name], Pattern)
- type PatternSynDefns = Map QName PatternSynDefn
- lambdaLiftExpr :: [Name] -> Expr -> Expr
- substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
- substExpr :: [(Name, Expr)] -> Expr -> Expr
- substLetBinding :: [(Name, Expr)] -> LetBinding -> LetBinding
- substTypedBindings :: [(Name, Expr)] -> TypedBindings -> TypedBindings
- substTypedBinding :: [(Name, Expr)] -> TypedBinding -> TypedBinding
- module Agda.Syntax.Abstract.Name

# Documentation

data Expr

Constructors

Var Name | Bound variables
Def QName | Constants (i.e. axioms, functions, projections, 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 Integer | 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 | binds `Name` to current type in `Expr`
Quote ExprInfo |
QuoteTerm ExprInfo |
Unquote ExprInfo | The splicing construct: unquote ...
DontCare Expr | for printing DontCare from Syntax.Internal
PatternSyn QName |

Instances

Show Expr |
Typeable Expr |
KillRange Expr |
HasRange Expr |
Rename Pattern |
Rename LHSCore |
Rename 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.
EmbPrj Pattern |
EmbPrj Expr |
UniverseBi Declaration Pattern |
UniverseBi Declaration Expr |
ToConcrete Pattern Pattern |
ToConcrete LHSCore Pattern |
ToConcrete Expr Expr |
ToAbstract Expr Expr |
ToAbstract OldQName Expr |
Reify Literal Expr |
Reify MetaId Expr |
Reify Level Expr |
Reify Sort Expr |
Reify Type Expr |
Reify Elim Expr |
Reify Term Expr |
Reify Expr Expr |
Reify DisplayTerm Expr |
Reify i Expr => ReifyWhen i Expr |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) |
Reify Constraint (OutputConstraint Expr Expr) |
ToAbstract (Pattern' Expr) (Pattern' Expr) |
ToAbstract (LHSCore' Expr) (LHSCore' Expr) |

data Declaration

Constructors

Axiom DefInfo Relevance QName Expr | postulate
Field DefInfo QName (Arg Expr) | record field
Primitive DefInfo QName Expr | primitive function
Mutual MutualInfo [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 Delayed [Clause] | sequence of function clauses
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 Induction) (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

Show Declaration |
Typeable Declaration |
KillRange Declaration |
HasRange Declaration |
GetDefInfo Declaration |
AnyAbstract Declaration |
Rename Declaration |
UniverseBi Declaration AmbiguousQName |
UniverseBi Declaration ModuleName |
UniverseBi Declaration QName |
UniverseBi Declaration ModuleInfo |
UniverseBi Declaration Pattern |
UniverseBi Declaration TypedBinding |
UniverseBi Declaration LamBinding |
UniverseBi Declaration LetBinding |
UniverseBi Declaration Declaration |
UniverseBi Declaration Expr |
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

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

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

data LetBinding

Constructors

LetBind LetInfo Relevance Name Expr Expr | LetBind info rel name type defn
LetPatBind LetInfo Pattern Expr | irrefutable pattern binding
LetApply ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName) |
LetOpen ModuleInfo ModuleName | only for highlighting and abstractToConcrete

Instances

Show LetBinding |
Typeable LetBinding |
KillRange LetBinding |
HasRange LetBinding |
Rename LetBinding |
EmbPrj LetBinding |
UniverseBi Declaration LetBinding |
ToConcrete LetBinding [Declaration] |
ToAbstract LetDef [LetBinding] |
ToAbstract LetDefs [LetBinding] |

type TypeSignature = Declaration

Only `Axiom`s.

type Constructor = TypeSignature

type Field = 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

Show LamBinding |
Typeable LamBinding |
KillRange LamBinding |
HasRange LamBinding |
Rename LamBinding |
EmbPrj LamBinding |
UniverseBi Declaration 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

Show TypedBindings |
Typeable TypedBindings |
KillRange TypedBindings |
HasRange TypedBindings |
Rename TypedBindings |
DotVars TypedBindings |
EmbPrj 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

Show TypedBinding |
Typeable TypedBinding |
KillRange TypedBinding |
HasRange TypedBinding |
Rename TypedBinding |
DotVars TypedBinding |
EmbPrj TypedBinding |
UniverseBi Declaration 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 |
Fields clauseLHS :: LHS clauseRHS :: RHS clauseWhereDecls :: [Declaration]

Instances

Show Clause |
Typeable Clause |
KillRange Clause |
HasRange Clause |
Rename 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

Show RHS |
Typeable RHS |
KillRange RHS |
HasRange RHS |
Rename RHS |
DotVars RHS |
ToAbstract AbstractRHS RHS |
Reify ClauseBody RHS |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |

data SpineLHS

The lhs of a clause in spine view (inside-out). Projection patterns are contained in `spLhsPats`, represented as `DefP d []`.

Constructors

SpineLHS |
Fields spLhsInfo :: LHSInfo Range. spLhsDefName :: QName Name of function we are defining. spLhsPats :: [NamedArg Pattern] Function parameters (patterns). spLhsWithPats :: [Pattern] `with` patterns (after `|`).

Instances

Show SpineLHS |
Typeable SpineLHS |

data LHS

The lhs of a clause in projection-application view (outside-in). Projection patters are represented as `LHSProj`s.

Constructors

LHS |
Fields lhsInfo :: LHSInfo Range. lhsCore :: LHSCore Copatterns. lhsWithPats :: [Pattern] `with` patterns (after `|`).

Instances

Eq LHS |
Show LHS |
Typeable LHS |
KillRange LHS |
HasRange LHS |
Alpha LHS |
Rename LHS |
ToConcrete LHS LHS |
ToAbstract LeftHandSide LHS |

data LHSCore' e

The lhs minus `with`-patterns in projection-application view. Parameterised over the type `e` of dot patterns.

Constructors

LHSHead | The head applied to ordinary patterns.
Fields lhsDefName :: QName Head `f`. lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.
LHSProj | Projection
Fields lhsDestructor :: QName Record projection identifier. lhsPatsLeft :: [NamedArg (Pattern' e)] Indices of the projection. Currently none `[]`, since we do not have indexed records. lhsFocus :: NamedArg (LHSCore' e) Main branch. lhsPatsRight :: [NamedArg (Pattern' e)] Further applied to patterns.

Instances

Functor LHSCore' |
Typeable1 LHSCore' |
Foldable LHSCore' |
Traversable LHSCore' |
Rename LHSCore |
ToConcrete LHSCore Pattern |
ToAbstract LHSCore (LHSCore' Expr) |
Eq (LHSCore' e) |
Show e => Show (LHSCore' e) |
KillRange e => KillRange (LHSCore' e) |
HasRange (LHSCore' e) |
Alpha (LHSCore' e) |
ToAbstract (LHSCore' Expr) (LHSCore' Expr) |

type LHSCore = LHSCore' Expr

lhsToSpine :: LHS -> SpineLHS

lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)]

lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]

Used for checking pattern linearity.

lhsCoreToPattern :: LHSCore -> Pattern

Used in AbstractToConcrete.

mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore

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: function definition `f ps` or destructor pattern `d p ps`.
WildP PatInfo |
AsP PatInfo Name (Pattern' e) |
DotP PatInfo e |
AbsurdP PatInfo |
LitP Literal |
ImplicitP PatInfo | Generated at type checking for implicit arguments.
PatternSynP PatInfo QName [NamedArg (Pattern' e)] |

Instances

Functor Pattern' |
Typeable1 Pattern' |
Foldable Pattern' |
Traversable Pattern' |
Rename Pattern |
DotVars Pattern |
EmbPrj Pattern |
UniverseBi Declaration Pattern |
ToConcrete Pattern Pattern |
ToAbstract Pattern (Pattern' Expr) |
Eq (Pattern' e) | Literal equality of patterns, ignoring dot patterns
Show e => Show (Pattern' e) |
KillRange e => KillRange (Pattern' e) |
SetRange (Pattern' a) |
HasRange (Pattern' e) |
Alpha (Pattern' e) |
ToAbstract (Pattern' Expr) (Pattern' Expr) |

type Pattern = Pattern' Expr

type Patterns = [NamedArg Pattern]

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

app :: Expr -> [NamedArg Expr] -> Expr

patternToExpr :: Pattern -> Expr

type PatternSynDefn = ([Name], Pattern)

type PatternSynDefns = Map QName PatternSynDefn

lambdaLiftExpr :: [Name] -> Expr -> Expr

substPattern :: [(Name, Pattern)] -> Pattern -> Pattern

substExpr :: [(Name, Expr)] -> Expr -> Expr

substLetBinding :: [(Name, Expr)] -> LetBinding -> LetBinding

substTypedBindings :: [(Name, Expr)] -> TypedBindings -> TypedBindings

substTypedBinding :: [(Name, Expr)] -> TypedBinding -> TypedBinding

module Agda.Syntax.Abstract.Name