Agda.Syntax.Concrete

The concrete syntax is a raw representation of the program text without any desugaring at all. This is what the parser produces. The idea is that if we figure out how to keep the concrete syntax around, it can be printed exactly as the user wrote it.

Expressions

data Expr

Concrete expressions. Should represent exactly what the user wrote.

Constructors

Ident QName

ex: x

Lit Literal

ex: 1 or "foo"

QuestionMark !Range (Maybe Nat)

ex: ? or {! ... !}

Underscore !Range (Maybe String)

ex: _ or _A_5

RawApp !Range [Expr]

before parsing operators

App !Range Expr (NamedArg Expr)

ex: e e, e {e}, or e {x = e}

OpApp !Range QName [NamedArg (OpApp Expr)]

ex: e + e

WithApp !Range Expr [Expr]

ex: e | e1 | .. | en

HiddenArg !Range (Named_ Expr)

ex: {e} or {x=e}

InstanceArg !Range (Named_ Expr)

ex: {{e}} or {{x=e}}

Lam !Range [LamBinding] Expr

ex: \x {y} -> e or \(x:A){y:B} -> e

AbsurdLam !Range Hiding

ex: \ ()

ExtendedLam !Range [(LHS, RHS, WhereClause)]

ex: \ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }

Fun !Range Expr Expr

ex: e -> e or .e -> e (NYI: {e} -> e)

Pi Telescope Expr

ex: (xs:e) -> e or {xs:e} -> e

Set !Range

ex: Set

Prop !Range

ex: Prop

SetN !Range Integer

ex: Set0, Set1, ..

Rec !Range [(Name, Expr)]

ex: record {x = a; y = b}

RecUpdate !Range Expr [(Name, Expr)]

ex: record e {x = a; y = b}

Let !Range [Declaration] Expr

ex: let Ds in e

Paren !Range Expr

ex: (e)

Absurd !Range

ex: () or {}, only in patterns

As !Range Name Expr

ex: x@p, only in patterns

Dot !Range Expr

ex: .p, only in patterns

ETel Telescope

only used for printing telescopes

QuoteGoal !Range Name Expr

ex: quoteGoal x in e

QuoteContext !Range Name Expr

ex: quoteContext ctx in e

Quote !Range

ex: quote, should be applied to a name

QuoteTerm !Range

ex: quoteTerm, should be applied to a term

Tactic !Range Expr [Expr]

tactic solve | subgoal1 | .. | subgoalN

Unquote !Range

ex: unquote, should be applied to a term of type Term

DontCare Expr

to print irrelevant things

Equal !Range Expr Expr

ex: a = b, used internally in the parser

Instances

Show RHS

Show TypedBinding

Show TypedBindings

Show LamBinding

Show Expr

Typeable Expr

NFData Expr

Pretty RHS

Pretty TypedBinding

Pretty TypedBindings

Pretty LamBinding

Pretty Expr

KillRange RHS

KillRange TypedBinding

KillRange TypedBindings

KillRange LamBinding

KillRange Expr

HasRange RHS

HasRange TypedBinding

HasRange TypedBindings

HasRange LamBinding

HasRange Expr

ExprLike TypedBindings

ExprLike LamBinding

ExprLike Expr

IsExpr Expr

ToConcrete InteractionId Expr

ToConcrete TypedBinding TypedBinding

ToConcrete Expr Expr

ToConcrete NamedMeta Expr

ToAbstract RHS AbstractRHS

ToAbstract TypedBinding TypedBinding

ToAbstract TypedBindings TypedBindings

ToAbstract LamBinding LamBinding

ToAbstract Expr Expr

ToAbstract ArgInfo ArgInfo

ToConcrete TypedBindings [TypedBindings]

ToConcrete LamBinding [LamBinding]

ToAbstract LHSCore (LHSCore' Expr)

ToAbstract Pattern (Pattern' Expr)

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

Pretty (OpApp Expr)

Pretty e => Pretty (Arg e)

ExprLike a => ExprLike (Arg a)

ToConcrete (ArgInfo ac) ArgInfo

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

ToAbstract (Pattern' Expr) (Pattern' Expr)

ToAbstract (LHSCore' Expr) (LHSCore' Expr)

ToConcrete a c => ToConcrete (Arg ac a) (Arg c)

data OpApp e

Constructors

SyntaxBindingLambda !Range [LamBinding] e

an abstraction inside a special syntax declaration (see Issue 358 why we introduce this).

Ordinary e

Instances

Functor OpApp

Typeable1 OpApp

Foldable OpApp

Traversable OpApp

Pretty (OpApp Expr)

KillRange e => KillRange (OpApp e)

HasRange e => HasRange (OpApp e)

ExprLike a => ExprLike (OpApp a)

fromOrdinary :: e -> OpApp e -> e

module Agda.Syntax.Concrete.Name

appView :: Expr -> AppView

data AppView

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr]

Bindings

type LamBinding = LamBinding' TypedBindings

A lambda binding is either domain free or typed.

data LamBinding' a

Constructors

DomainFree ArgInfo BoundName

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

DomainFull a

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

Instances

Functor LamBinding'

Show LamBinding

Typeable1 LamBinding'

Foldable LamBinding'

Traversable LamBinding'

Pretty LamBinding

KillRange LamBinding

HasRange LamBinding

ExprLike LamBinding

ToAbstract LamBinding LamBinding

ToConcrete LamBinding [LamBinding]

type TypedBindings = TypedBindings' TypedBinding

A sequence of typed bindings with hiding information. Appears in dependent function spaces, typed lambdas, and telescopes.

data TypedBindings' a

Constructors

TypedBindings !Range (Arg a)

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

Instances

Functor TypedBindings'

Show TypedBindings

Show LamBinding

Typeable1 TypedBindings'

Foldable TypedBindings'

Traversable TypedBindings'

Pretty TypedBindings

Pretty LamBinding

KillRange TypedBindings

KillRange LamBinding

HasRange TypedBindings

HasRange LamBinding

ExprLike TypedBindings

ExprLike LamBinding

ToAbstract TypedBindings TypedBindings

ToAbstract LamBinding LamBinding

ToConcrete TypedBindings [TypedBindings]

ToConcrete LamBinding [LamBinding]

type TypedBinding = TypedBinding' Expr

A typed binding.

data TypedBinding' e

Constructors

TBind !Range [BoundName] e

Binding (x1 ... xn : A).

TLet !Range [Declaration]

Let binding (let Ds) or (open M args).

Instances

Functor TypedBinding'

Show TypedBinding

Show TypedBindings

Show LamBinding

Typeable1 TypedBinding'

Foldable TypedBinding'

Traversable TypedBinding'

Pretty TypedBinding

Pretty TypedBindings

Pretty LamBinding

KillRange TypedBinding

KillRange TypedBindings

KillRange LamBinding

HasRange TypedBinding

HasRange TypedBindings

HasRange LamBinding

ExprLike TypedBindings

ExprLike LamBinding

ToConcrete TypedBinding TypedBinding

ToAbstract TypedBinding TypedBinding

ToAbstract TypedBindings TypedBindings

ToAbstract LamBinding LamBinding

ToConcrete TypedBindings [TypedBindings]

ToConcrete LamBinding [LamBinding]

ExprLike a => ExprLike (TypedBinding' a)

data ColoredTypedBinding

Color a TypeBinding. Used by Pretty.

Constructors

WithColors [Color] TypedBinding

Instances

Pretty ColoredTypedBinding

data BoundName

Constructors

BName

Fields

boundName :: Name

boundLabel :: Name

for implicit function types the label matters and can't be alpha-renamed

bnameFixity :: Fixity'

Instances

Typeable BoundName

Pretty BoundName

KillRange BoundName

HasRange BoundName

ToAbstract (NewName BoundName) Name

mkBoundName_ :: Name -> BoundName

mkBoundName :: Name -> Fixity' -> BoundName

type Telescope = [TypedBindings]

A telescope is a sequence of typed bindings. Bound variables are in scope in later types.

countTelVars :: Telescope -> Nat

Declarations

data Declaration

The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.

Constructors

TypeSig ArgInfo Name Expr

Axioms and functions can be irrelevant. (Hiding should be NotHidden)

Field Name (Arg Expr)

Record field, can be hidden and/or irrelevant.

FunClause LHS RHS WhereClause

DataSig !Range Induction Name [LamBinding] Expr

lone data signature in mutual block

Data !Range Induction Name [LamBinding] (Maybe Expr) [Constructor]

RecordSig !Range Name [LamBinding] Expr

lone record signature in mutual block

Record !Range Name (Maybe (Ranged Induction)) (Maybe Name) [LamBinding] (Maybe Expr) [Declaration]

The optional name is a name for the record constructor.

Infix Fixity [Name]

Syntax Name Notation

notation declaration for a name

PatternSyn !Range Name [Arg Name] Pattern

Mutual !Range [Declaration]

Abstract !Range [Declaration]

Private !Range [Declaration]

InstanceB !Range [Declaration]

Postulate !Range [TypeSignatureOrInstanceBlock]

Primitive !Range [TypeSignature]

Open !Range QName ImportDirective

Import !Range QName (Maybe AsName) OpenShortHand ImportDirective

ModuleMacro !Range Name ModuleApplication OpenShortHand ImportDirective

Module !Range QName [TypedBindings] [Declaration]

UnquoteDecl !Range Name Expr

Pragma Pragma

Instances

Show Declaration

Show WhereClause

Typeable Declaration

Pretty Declaration

Pretty WhereClause

KillRange Declaration

KillRange WhereClause

HasRange Declaration

HasRange WhereClause

ExprLike Declaration

ToConcrete LetBinding [Declaration]

ToConcrete Declaration [Declaration]

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

Pretty [Declaration]

ToConcrete (Constr Constructor) Declaration

ToAbstract (TopLevel [Declaration]) TopLevelInfo

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

ToAbstract [Declaration] [Declaration]

data ModuleApplication

Constructors

SectionApp Range [TypedBindings] Expr

tel. M args

RecordModuleIFS Range QName

M {{...}}

Instances

Show ModuleApplication

Typeable ModuleApplication

Pretty ModuleApplication

KillRange ModuleApplication

HasRange ModuleApplication

ExprLike ModuleApplication

ToConcrete ModuleApplication ModuleApplication

type TypeSignature = Declaration

Just type signatures.

type TypeSignatureOrInstanceBlock = Declaration

Just type signatures or instance blocks.

type Constructor = TypeSignature

A data constructor declaration is just a type signature.

data ImportDirective

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

Constructors

ImportDirective

Fields

importDirRange :: !Range

usingOrHiding :: UsingOrHiding

renaming :: [Renaming]

publicOpen :: Bool

Only for open. Exports the opened names from the current module.

Instances

Show ImportDirective

Typeable ImportDirective

Pretty ImportDirective

KillRange ImportDirective

HasRange ImportDirective

data UsingOrHiding

Constructors

Hiding [ImportedName]

Using [ImportedName]

Instances

Typeable UsingOrHiding

Pretty UsingOrHiding

KillRange UsingOrHiding

HasRange UsingOrHiding

data ImportedName

An imported name can be a module or a defined name

Constructors

ImportedModule

Fields

importedName :: Name

ImportedName

Fields

importedName :: Name

Instances

Eq ImportedName

Ord ImportedName

Show ImportedName

Typeable ImportedName

Pretty ImportedName

KillRange ImportedName

HasRange ImportedName

data Renaming

Constructors

Renaming

Fields

renFrom :: ImportedName

Rename from this name.

renTo :: Name

To this one.

renToRange :: Range

The range of the "to" keyword. Retained for highlighting purposes.

Instances

Typeable Renaming

KillRange Renaming

HasRange Renaming

data AsName

Constructors

AsName

Fields

asName :: Name

The "as" name.

asRange :: Range

The range of the "as" keyword. Retained for highlighting purposes.

Instances

Show AsName

Typeable AsName

KillRange AsName

HasRange AsName

defaultImportDir :: ImportDirective

Default is directive is private (use everything, but do not export).

data OpenShortHand

Constructors

DoOpen

DontOpen

Instances

Eq OpenShortHand

Show OpenShortHand

Typeable OpenShortHand

Pretty OpenShortHand

type RewriteEqn = Expr

type WithExpr = Expr

data LHS

Left hand sides can be written in infix style. For example:

 n + suc m = suc (n + m)
 (f ∘ g) x = f (g x)

We use fixity information to see which name is actually defined.

Constructors

LHS

original pattern, with-patterns, rewrite equations and with-expressions

Fields

lhsOriginalPattern :: Pattern

f ps

lhsWithPattern :: [Pattern]

| p (many)

lhsRewriteEqn :: [RewriteEqn]

rewrite e (many)

lhsWithExpr :: [WithExpr]

with e (many)

Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]

new with-patterns, rewrite equations and with-expressions

Instances

Show LHS

Typeable LHS

Pretty LHS

KillRange LHS

HasRange LHS

ExprLike LHS

ToConcrete LHS LHS

ToConcrete SpineLHS LHS

data Pattern

Concrete patterns. No literals in patterns at the moment.

Constructors

IdentP QName

c or x

QuoteP !Range

quote

AppP Pattern (NamedArg Pattern)

p p' or p {x = p'}

RawAppP !Range [Pattern]

p1..pn before parsing operators

OpAppP !Range QName [NamedArg Pattern]

eg: p => p' for operator _=>_

HiddenP !Range (Named_ Pattern)

{p} or {x = p}

InstanceP !Range (Named_ Pattern)

{{p}} or {{x = p}}

ParenP !Range Pattern

(p)

WildP !Range

_

AbsurdP !Range

()

AsP !Range Name Pattern

x@p unused

DotP !Range Expr

.e

LitP Literal

0, 1, etc.

Instances

Show Pattern

Typeable Pattern

NFData Pattern

Pretty Pattern

KillRange Pattern

HasRange Pattern

IsExpr Pattern

ToConcrete Pattern Pattern

ToConcrete LHSCore Pattern

ToAbstract Pattern (Pattern' Expr)

Pretty [Pattern]

data LHSCore

Processed (scope-checked) intermediate form of the core f ps of LHS. Corresponds to lhsOriginalPattern.

Constructors

LHSHead

Fields

lhsDefName :: Name

f

lhsPats :: [NamedArg Pattern]

ps

LHSProj

Fields

lhsDestructor :: QName

record projection identifier

lhsPatsLeft :: [NamedArg Pattern]

side patterns

lhsFocus :: NamedArg LHSCore

main branch

lhsPatsRight :: [NamedArg Pattern]

side patterns

Instances

Show LHSCore

Typeable LHSCore

NFData LHSCore

Pretty LHSCore

HasRange LHSCore

ToAbstract LHSCore (LHSCore' Expr)

type RHS = RHS' Expr

data RHS' e

Constructors

AbsurdRHS

No right hand side because of absurd match.

RHS e

Instances

Functor RHS'

Show RHS

Typeable1 RHS'

Foldable RHS'

Traversable RHS'

Pretty RHS

KillRange RHS

HasRange RHS

ToAbstract RHS AbstractRHS

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

ExprLike a => ExprLike (RHS' a)

type WhereClause = WhereClause' [Declaration]

data WhereClause' decls

Constructors

NoWhere

No where clauses.

AnyWhere decls

Ordinary where.

SomeWhere Name decls

Named where: module M where.

Instances

Functor WhereClause'

Show WhereClause

Typeable1 WhereClause'

Foldable WhereClause'

Traversable WhereClause'

Pretty WhereClause

KillRange WhereClause

HasRange WhereClause

ExprLike a => ExprLike (WhereClause' a)

data Pragma

Constructors

OptionsPragma !Range [String]

BuiltinPragma !Range String Expr

RewritePragma !Range QName

CompiledDataPragma !Range QName String [String]

CompiledTypePragma !Range QName String

CompiledPragma !Range QName String

CompiledExportPragma !Range QName String

CompiledEpicPragma !Range QName String

CompiledJSPragma !Range QName String

StaticPragma !Range QName

ImportPragma !Range String

Invariant: The string must be a valid Haskell module name.

ImpossiblePragma !Range

EtaPragma !Range QName

TerminationCheckPragma !Range (TerminationCheck Name)

Instances

Show Pragma

Typeable Pragma

Pretty Pragma

KillRange Pragma

HasRange Pragma

ToConcrete RangeAndPragma Pragma

ToAbstract Pragma [Pragma]

type Module = ([Pragma], [Declaration])

Modules: Top-level pragmas plus other top-level declarations.

data ThingWithFixity x

Constructors

ThingWithFixity x Fixity'

Instances

Functor ThingWithFixity

Typeable1 ThingWithFixity

Foldable ThingWithFixity

Traversable ThingWithFixity

Show x => Show (ThingWithFixity x)

Pretty (ThingWithFixity Name)

KillRange x => KillRange (ThingWithFixity x)

topLevelModuleName :: Module -> TopLevelModuleName

Computes the top-level module name.

Precondition: The Module has to be well-formed.

Pattern tools

patternHead :: Pattern -> Maybe Name

Get the leftmost symbol in a pattern.

patternNames :: Pattern -> [Name]

Get all the identifiers in a pattern in left-to-right order.

Concrete instances

type Color = Expr

type Arg a = Arg Color a

type NamedArg a = NamedArg Color a

type ArgInfo = ArgInfo Color