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 (Set Name) [NamedArg (MaybePlaceholder (OpApp Expr))]

ex: e + e The QName is possibly ambiguous, but it must correspond to one of the names in the set.

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, Bool)]

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 RecordAssignments

ex: record {x = a; y = b}, or record { x = a; M1; M2 }

RecUpdate Range Expr [FieldAssignment]

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

ex: quoteContext

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

NFData Expr

Ranges are not forced.

KillRange RHS

KillRange TypedBinding

KillRange TypedBindings

KillRange LamBinding

KillRange Expr

SetRange TypedBindings

HasRange RHS

HasRange TypedBinding

HasRange TypedBindings

HasRange LamBinding

HasRange Expr

LensRelevance TypedBindings

LensHiding TypedBindings

LensHiding LamBinding

ExprLike TypedBindings

ExprLike LamBinding

ExprLike Expr

ExprLike FieldAssignment

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

ToConcrete TypedBindings [TypedBindings]

ToConcrete LamBinding [LamBinding]

ToAbstract LHSCore (LHSCore' Expr)

ToAbstract Pattern (Pattern' Expr)

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

ToAbstract (Pattern' Expr) (Pattern' Expr)

ToAbstract (LHSCore' Expr) (LHSCore' Expr)

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

Foldable OpApp

Traversable OpApp

NFData a => NFData (OpApp a)

Ranges are not forced.

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'

Foldable LamBinding'

Traversable LamBinding'

KillRange LamBinding

HasRange LamBinding

LensHiding LamBinding

ExprLike LamBinding

ToAbstract LamBinding LamBinding

ToConcrete LamBinding [LamBinding]

NFData a => NFData (LamBinding' a)

type TypedBindings = TypedBindings' TypedBinding

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

If the individual binding contains hiding information as well, the Hiding in TypedBindings must be the unit NotHidden.

data TypedBindings' a

Constructors

TypedBindings Range (Arg a)

. (xs : e) or {xs : e} or something like (x {y} _ : e).

Instances

Functor TypedBindings'

Foldable TypedBindings'

Traversable TypedBindings'

KillRange TypedBindings

KillRange LamBinding

SetRange TypedBindings

HasRange TypedBindings

HasRange LamBinding

LensRelevance TypedBindings

LensHiding TypedBindings

LensHiding LamBinding

ExprLike TypedBindings

ExprLike LamBinding

ToAbstract TypedBindings TypedBindings

ToAbstract LamBinding LamBinding

ToConcrete TypedBindings [TypedBindings]

ToConcrete LamBinding [LamBinding]

NFData a => NFData (TypedBindings' a)

Ranges are not forced.

type TypedBinding = TypedBinding' Expr

A typed binding.

data TypedBinding' e

Constructors

TBind Range [WithHiding BoundName] e

Binding (x1 ... xn : A).

TLet Range [Declaration]

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

Instances

Functor TypedBinding'

Foldable TypedBinding'

Traversable TypedBinding'

KillRange TypedBinding

KillRange TypedBindings

KillRange LamBinding

SetRange TypedBindings

HasRange TypedBinding

HasRange TypedBindings

HasRange LamBinding

LensRelevance TypedBindings

LensHiding TypedBindings

LensHiding LamBinding

ExprLike TypedBindings

ExprLike LamBinding

ToConcrete TypedBinding TypedBinding

ToAbstract TypedBinding TypedBinding

ToAbstract TypedBindings TypedBindings

ToAbstract LamBinding LamBinding

ToConcrete TypedBindings [TypedBindings]

ToConcrete LamBinding [LamBinding]

NFData a => NFData (TypedBinding' a)

Ranges are not forced.

ExprLike a => ExprLike (TypedBinding' a)

type RecordAssignment = Either FieldAssignment ModuleAssignment

type RecordAssignments = [RecordAssignment]

type FieldAssignment = FieldAssignment' Expr

data FieldAssignment' a

Constructors

FieldAssignment

Fields

_nameFieldA :: Name

_exprFieldA :: a

Instances

Functor FieldAssignment'

Foldable FieldAssignment'

Traversable FieldAssignment'

ExprLike FieldAssignment

SubstExpr Assign

Eq a => Eq (FieldAssignment' a)

Show a => Show (FieldAssignment' a)

NFData a => NFData (FieldAssignment' a)

KillRange a => KillRange (FieldAssignment' a)

HasRange a => HasRange (FieldAssignment' a)

ExprLike a => ExprLike (FieldAssignment' a)

NamesIn a => NamesIn (FieldAssignment' a)

ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a)

ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c)

ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a)

nameFieldA :: Lens' Name (FieldAssignment' a)

exprFieldA :: Lens' a (FieldAssignment' a)

data ModuleAssignment

Constructors

ModuleAssignment

Fields

_qnameModA :: QName

_exprModA :: [Expr]

_importDirModA :: ImportDirective

Instances

NFData ModuleAssignment

KillRange ModuleAssignment

HasRange ModuleAssignment

ExprLike ModuleAssignment

ToAbstract ModuleAssignment (ModuleName, [LetBinding])

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

NFData 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 IsInstance Name (Arg Expr)

Record field, can be hidden and/or irrelevant.

FunClause LHS RHS WhereClause Bool

DataSig Range Induction Name [LamBinding] Expr

lone data signature in mutual block

Data Range Induction Name [LamBinding] (Maybe Expr) [TypeSignatureOrInstanceBlock]

RecordSig Range Name [LamBinding] Expr

lone record signature in mutual block

Record Range Name (Maybe (Ranged Induction)) (Maybe Bool) (Maybe (Name, IsInstance)) [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]

Macro 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

UnquoteDef Range [Name] Expr

Pragma Pragma

Instances

NFData Declaration

Ranges are not forced.

KillRange Declaration

KillRange WhereClause

HasRange Declaration

HasRange WhereClause

ExprLike Declaration

ToConcrete LetBinding [Declaration]

ToConcrete Declaration [Declaration]

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

ToConcrete (Constr Constructor) Declaration

ToAbstract (TopLevel [Declaration]) TopLevelInfo

Top-level declarations are always (import|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file

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

NFData ModuleApplication

Ranges are not forced.

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 ImportDirective = ImportDirective' Name Name

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

type Using = Using' Name Name

type ImportedName = ImportedName' Name Name

An imported name can be a module or a defined name.

type Renaming = Renaming' Name Name

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

NFData AsName

Ranges are not forced.

KillRange AsName

HasRange AsName

data OpenShortHand

Constructors

DoOpen

DontOpen

Instances

Eq OpenShortHand

Show 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

NFData LHS

Ranges are not forced.

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 (Set Name) [NamedArg Pattern]

eg: p => p' for operator _=>_ The QName is possibly ambiguous, but it must correspond to one of the names in the set.

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.

RecP Range [FieldAssignment' Pattern]

record {x = p; y = q}

Instances

NFData Pattern

Ranges are not forced.

KillRange Pattern

SetRange Pattern

HasRange Pattern

IsExpr Pattern

ToConcrete Pattern Pattern

ToConcrete LHSCore Pattern

ToAbstract Pattern (Pattern' Expr)

data LHSCore

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

Constructors

LHSHead

Fields

lhsDefName :: QName

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

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'

Foldable RHS'

Traversable RHS'

KillRange RHS

HasRange RHS

ToAbstract RHS AbstractRHS

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

NFData a => NFData (RHS' a)

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'

Foldable WhereClause'

Traversable WhereClause'

KillRange WhereClause

HasRange WhereClause

NFData a => NFData (WhereClause' a)

Null (WhereClause' a)

A WhereClause is null when the where keyword is absent. An empty list of declarations does not count as null here.

ExprLike a => ExprLike (WhereClause' a)

data ExprWhere

An expression followed by a where clause. Currently only used to give better a better error message in interaction.

Constructors

ExprWhere Expr WhereClause

data Pragma

Constructors

OptionsPragma Range [String]

BuiltinPragma Range String Expr

RewritePragma Range QName

CompiledDataPragma Range QName String [String]

CompiledDeclareDataPragma Range QName String

CompiledTypePragma Range QName String

CompiledPragma Range QName String

CompiledExportPragma Range QName String

CompiledEpicPragma Range QName String

CompiledJSPragma Range QName String

CompiledUHCPragma Range QName String

CompiledDataUHCPragma Range QName String [String]

HaskellCodePragma Range String

NoSmashingPragma Range QName

StaticPragma Range QName

InlinePragma Range QName

ImportPragma Range String

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

ImportUHCPragma Range String

same as above, but for the UHC backend

ImpossiblePragma Range

TerminationCheckPragma Range (TerminationCheck Name)

CatchallPragma Range

DisplayPragma Range Pattern Expr

NoPositivityCheckPragma Range

Instances

NFData Pragma

Ranges are not forced.

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

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Functor ThingWithFixity

Foldable ThingWithFixity

Traversable ThingWithFixity

Show x => Show (ThingWithFixity x)

KillRange x => KillRange (ThingWithFixity x)

topLevelModuleName :: Module -> TopLevelModuleName

Computes the top-level module name.

Precondition: The Module has to be well-formed. This means that there are only allowed declarations before the first module declaration, typically import declarations. See spanAllowedBeforeModule.

spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])

Splits off allowed (= import) declarations before the first non-allowed declaration. After successful parsing, the first non-allowed declaration should be a module declaration.

Pattern tools

patternNames :: Pattern -> [Name]

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

patternQNames :: Pattern -> [QName]

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

Lenses

mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS