Agda.Syntax.Abstract

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

Documentation

type Color = Expr

type Arg a = Arg Color a

type Dom a = Dom Color a

type NamedArg a = NamedArg Color a

type ArgInfo = ArgInfo Color

type Args = [NamedArg Expr]

data Expr

Expressions after scope checking (operators parsed, names resolved).

Constructors

Var Name

Bound variable.

Def QName

Constant: axiom, function, data or record type.

Proj QName

Projection.

Con AmbiguousQName

Constructor.

PatternSyn QName

Pattern synonym.

Lit Literal

Literal.

QuestionMark MetaInfo InteractionId

Meta variable for interaction. The InteractionId is usually identical with the metaNumber of MetaInfo. However, if you want to print an interaction meta as just ? instead of ?n, you should set the metaNumber to Nothing while keeping the InteractionId.

Underscore MetaInfo

Meta variable for hidden argument (must be inferred locally).

App ExprInfo Expr (NamedArg Expr)

Ordinary (binary) application.

WithApp ExprInfo Expr [Expr]

With application.

Lam ExprInfo LamBinding Expr

λ bs → e.

AbsurdLam ExprInfo Hiding

λ() or λ{}.

ExtendedLam ExprInfo DefInfo QName [Clause]

Pi ExprInfo Telescope Expr

Dependent function space Γ → A.

Fun ExprInfo (Arg Expr) Expr

Non-dependent function space.

Set ExprInfo Integer

Set, Set1, Set2, ...

Prop ExprInfo

Prop (no longer supported, used as dummy type).

Let ExprInfo [LetBinding] Expr

let bs in e.

ETel Telescope

Only used when printing telescopes.

Rec ExprInfo Assigns

Record construction.

RecUpdate ExprInfo Expr Assigns

Record update.

ScopedExpr ScopeInfo Expr

Scope annotation.

QuoteGoal ExprInfo Name Expr

Binds Name to current type in Expr.

QuoteContext ExprInfo Name Expr

Binds Name to current context in Expr.

Quote ExprInfo

Quote an identifier QName.

QuoteTerm ExprInfo

Quote a term.

Unquote ExprInfo

The splicing construct: unquote ...

DontCare Expr

For printing DontCare from Syntax.Internal.

Instances

Eq Color

Ord Color

Show Expr

KillRange Expr

HasRange Expr

Underscore Expr

SubstExpr Expr

AllNames Expr

ExprLike Expr

PrettyTCM Expr

ExpandPatternSynonyms Pattern

IsFlexiblePattern Pattern

UniverseBi Declaration Pattern

UniverseBi Declaration Expr

ToConcrete Pattern Pattern

ToConcrete LHSCore Pattern

ToConcrete Expr Expr

Reify MetaId Expr

Reify Literal Expr

Reify Expr Expr

Reify Level Expr

Reify Sort Expr

Reify Type Expr

Reify Elim Expr

Reify Term Expr

Reify ArgInfo ArgInfo

Reify DisplayTerm Expr

ToAbstract Expr Expr

ToAbstract ArgInfo ArgInfo

ToAbstract OldQName Expr

ConvColor ArgInfo ArgInfo

SubstExpr a => SubstExpr (Arg a)

AllNames a => AllNames (Arg a)

Reify i a => Reify (Dom i) (Arg a)

Reify i a => Reify (Arg i) (Arg a)

Skip reification of implicit and irrelevant args if option is off.

ToAbstract c a => ToAbstract (Arg c) (Arg a)

ToAbstract (Pattern' Expr) (Pattern' Expr)

ToAbstract (LHSCore' Expr) (LHSCore' Expr)

ToAbstract c a => ToAbstract (NamedArg c) (NamedArg a)

ConvColor (Dom e) (Dom e)

ConvColor (Arg e) (Arg e)

type Assign = (Name, Expr)

Record field assignment f = e.

type Assigns = [Assign]

data Axiom

Is a type signature a postulate or a function signature?

Constructors

FunSig

A function signature.

NoFunSig

Not a function signature, i.e., a postulate (in user input) or another (e.g. data/record) type signature (internally).

Instances

Eq Axiom

Ord Axiom

Show Axiom

type Ren a = [(a, a)]

Renaming (generic).

data Declaration

Constructors

Axiom Axiom DefInfo ArgInfo QName Expr

type signature (can be irrelevant and colored, but not hidden)

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 (Ren QName) (Ren 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 LamBindings are DomainFree and binds the parameters of the datatype.

DataDef DefInfo QName [LamBinding] [Constructor]

the LamBindings are DomainFree and binds the parameters of the datatype.

RecSig DefInfo QName Telescope Expr

lone record signature

RecDef DefInfo QName (Maybe (Ranged 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.

PatternSynDef QName [Arg Name] Pattern

Only for highlighting purposes

UnquoteDecl MutualInfo DefInfo QName Expr

ScopedDecl ScopeInfo [Declaration]

scope annotation

Instances

Show Declaration

KillRange Declaration

HasRange Declaration

GetDefInfo Declaration

AnyAbstract Declaration

AllNames Declaration

ShowHead Declaration

UniverseBi Declaration RString

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

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 Telescope ModuleName [NamedArg Expr]

tel. M args: applies M to args and abstracts tel.

RecordModuleIFS ModuleName

M {{...}}

Instances

Show ModuleApplication

KillRange ModuleApplication

AllNames ModuleApplication

ToConcrete ModuleApplication ModuleApplication

data Pragma

Constructors

OptionsPragma [String]

BuiltinPragma String Expr

BuiltinNoDefPragma String QName

Builtins that do not come with a definition, but declare a name for an Agda concept.

RewritePragma QName

CompiledPragma QName String

CompiledExportPragma QName String

CompiledTypePragma QName String

CompiledDataPragma QName String [String]

CompiledEpicPragma QName String

CompiledJSPragma QName String

StaticPragma QName

EtaPragma QName

Instances

Show Pragma

ToAbstract Pragma [Pragma]

data LetBinding

Bindings that are valid in a let.

Constructors

LetBind LetInfo ArgInfo Name Expr Expr

LetBind info rel name type defn

LetPatBind LetInfo Pattern Expr

Irrefutable pattern binding.

LetApply ModuleInfo ModuleName ModuleApplication (Ren QName) (Ren ModuleName)

LetApply mi newM (oldM args) renaming moduleRenaming.

LetOpen ModuleInfo ModuleName

only for highlighting and abstractToConcrete

Instances

Show LetBinding

KillRange LetBinding

HasRange LetBinding

SubstExpr LetBinding

AllNames LetBinding

ExprLike LetBinding

UniverseBi Declaration LetBinding

ToConcrete LetBinding [Declaration]

ToAbstract LetDef [LetBinding]

ToAbstract LetDefs [LetBinding]

type TypeSignature = Declaration

Only Axioms.

type Constructor = TypeSignature

type Field = TypeSignature

data LamBinding

A lambda binding is either domain free or typed.

Constructors

DomainFree ArgInfo Name

. x or {x} or .x or .{x}

DomainFull TypedBindings

. (xs:e) or {xs:e} or (let Ds)

Instances

Show LamBinding

KillRange LamBinding

HasRange LamBinding

LensHiding LamBinding

AllNames LamBinding

ExprLike LamBinding

UniverseBi Declaration LamBinding

ToAbstract LamBinding LamBinding

ToConcrete LamBinding [LamBinding]

data TypedBindings

Typed bindings with hiding information.

Constructors

TypedBindings Range (Arg TypedBinding)

. (xs : e) or {xs : e}

Instances

Show TypedBindings

KillRange TypedBindings

HasRange TypedBindings

LensHiding TypedBindings

SubstExpr TypedBindings

AllNames TypedBindings

ExprLike TypedBindings

Reify Telescope Telescope

ToAbstract TypedBindings TypedBindings

ToConcrete TypedBindings [TypedBindings]

data TypedBinding

A typed binding. Appears in dependent function spaces, typed lambdas, and telescopes. It might be tempting to simplify this to only bind a single name at a time, and translate, say, (x y : A) to (x : A)(y : A) before type-checking. However, this would be slightly problematic:

1. We would have to typecheck the type A several times.
2. If A contains a meta variable or hole, it would be duplicated by such a translation.

While 1. is only slightly inefficient, 2. would be an outright bug. Duplicating A could not be done naively, we would have to make sure that the metas of the copy are aliases of the metas of the original.

Constructors

TBind Range [WithHiding Name] Expr

As in telescope (x y z : A) or type (x y z : A) -> B.

TLet Range [LetBinding]

E.g. (let x = e) or (let open M).

Instances

Show TypedBinding

KillRange TypedBinding

HasRange TypedBinding

SubstExpr TypedBinding

AllNames TypedBinding

ExprLike TypedBinding

UniverseBi Declaration TypedBinding

ToConcrete TypedBinding TypedBinding

ToAbstract TypedBinding TypedBinding

type Telescope = [TypedBindings]

data Clause' lhs

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

Functor Clause'

Foldable Clause'

Traversable Clause'

AllNames Clause

LHSToSpine Clause SpineClause

Clause instance.

Reify NamedClause Clause

ToAbstract Clause Clause

Show lhs => Show (Clause' lhs)

KillRange a => KillRange (Clause' a)

HasRange a => HasRange (Clause' a)

ExprLike (Clause' a)

TODO: currently does not go into clauses.

ToConcrete a LHS => ToConcrete (Clause' a) [Declaration]

type Clause = Clause' LHS

type SpineClause = Clause' SpineLHS

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 QNames are the names of the generated with functions. One for each Expr. The RHS shouldn't be another RewriteRHS.

Instances

Show RHS

KillRange RHS

HasRange RHS

AllNames RHS

Reify ClauseBody RHS

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

KillRange SpineLHS

HasRange SpineLHS

LHSToSpine LHS SpineLHS

LHS instance.

LHSToSpine Clause SpineClause

Clause instance.

ToConcrete SpineLHS LHS

data LHS

The lhs of a clause in focused (projection-application) view (outside-in). Projection patters are represented as LHSProjs.

Constructors

LHS

Fields

lhsInfo :: LHSInfo

Range.

lhsCore :: LHSCore

Copatterns.

lhsWithPats :: [Pattern]

with patterns (after |).

Instances

Eq LHS

Show LHS

KillRange LHS

HasRange LHS

AllNames Clause

LHSToSpine LHS SpineLHS

LHS instance.

LHSToSpine Clause SpineClause

Clause instance.

ToConcrete LHS LHS

Reify NamedClause Clause

ToAbstract Clause Clause

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'

Foldable LHSCore'

Traversable LHSCore'

ToConcrete LHSCore Pattern

ToAbstract LHSCore (LHSCore' Expr)

Eq (LHSCore' e)

Show e => Show (LHSCore' e)

KillRange e => KillRange (LHSCore' e)

HasRange (LHSCore' e)

ToAbstract (LHSCore' Expr) (LHSCore' Expr)

type LHSCore = LHSCore' Expr

class LHSToSpine a b where

Convert a focused lhs to spine view and back.

Methods

lhsToSpine :: a -> b

spineToLhs :: b -> a

Instances

LHSToSpine LHS SpineLHS

LHS instance.

LHSToSpine Clause SpineClause

Clause instance.

LHSToSpine a b => LHSToSpine [a] [b]

List instance (for clauses).

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

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

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

Add applicative patterns (non-projection patterns) to the right.

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

Add projection and applicative patterns to the right.

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

Used for checking pattern linearity.

lhsCoreToPattern :: LHSCore -> Pattern

Used in AbstractToConcrete.

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

Patterns

data Pattern' e

Parameterised over the type of dot patterns.

Constructors

VarP Name

ConP ConPatInfo AmbiguousQName [NamedArg (Pattern' e)]

DefP PatInfo QName [NamedArg (Pattern' e)]

Defined pattern: function definition f ps or destructor pattern d p ps.

WildP PatInfo

Underscore pattern entered by user. Or generated at type checking for implicit arguments.

AsP PatInfo Name (Pattern' e)

DotP PatInfo e

AbsurdP PatInfo

LitP Literal

PatternSynP PatInfo QName [NamedArg (Pattern' e)]

Instances

Functor Pattern'

Foldable Pattern'

Traversable Pattern'

ExpandPatternSynonyms Pattern

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

IsProjP (Pattern' e)

ExprLike a => ExprLike (Pattern' a)

ToAbstract (Pattern' Expr) (Pattern' Expr)

type Pattern = Pattern' Expr

type Patterns = [NamedArg Pattern]

class IsProjP a where

Check whether we are a projection pattern.

Methods

isProjP :: a -> Maybe QName

Instances

IsProjP Pattern

IsProjP (Pattern' e)

IsProjP (DeBruijnPat' a)

IsProjP a => IsProjP (Named n a)

IsProjP a => IsProjP (Arg c a)

class AllNames a where

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.

Methods

allNames :: a -> Seq QName

Instances

AllNames QName

AllNames RHS

AllNames Clause

AllNames TypedBinding

AllNames TypedBindings

AllNames LamBinding

AllNames LetBinding

AllNames ModuleApplication

AllNames Declaration

AllNames Expr

AllNames CallInfo

AllNames CallPath

AllNames a => AllNames [a]

AllNames a => AllNames (Maybe a)

AllNames a => AllNames (Arg a)

(AllNames a, AllNames b) => AllNames (a, b)

AllNames a => AllNames (Named name a)

axiomName :: Declaration -> QName

The name defined by the given axiom.

Precondition: The declaration has to be a (scoped) 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 = ([Arg Name], Pattern)

type PatternSynDefns = Map QName PatternSynDefn

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

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

class SubstExpr a where

Methods

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

Instances

SubstExpr Name

SubstExpr TypedBinding

SubstExpr TypedBindings

SubstExpr LetBinding

SubstExpr Expr

SubstExpr a => SubstExpr [a]

SubstExpr a => SubstExpr (Arg a)

(SubstExpr a, SubstExpr b) => SubstExpr (a, b)

SubstExpr a => SubstExpr (Named name a)

insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])

module Agda.Syntax.Abstract.Name