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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Concrete

Contents

Description

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.

Synopsis

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

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

data OpApp e

Constructors

SyntaxBindingLambda !Range [LamBinding] e

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

Ordinary e 

fromOrdinary :: e -> OpApp e -> e

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.

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.

type TypedBinding = TypedBinding' Expr

A typed binding.

data ColoredTypedBinding

Color a TypeBinding. Used by Pretty.

Constructors

WithColors [Color] TypedBinding 

data BoundName

Constructors

BName 

Fields

boundName :: Name
 
boundLabel :: Name

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

bnameFixity :: Fixity'
 

type Telescope = [TypedBindings]

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

Declarations

data Declaration

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

Instances

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.

data ImportedName

An imported name can be a module or a defined name

Constructors

ImportedModule 

Fields

importedName :: Name
 
ImportedName 

Fields

importedName :: Name
 

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.

data AsName

Constructors

AsName 

Fields

asName :: Name

The "as" name.

asRange :: Range

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

defaultImportDir :: ImportDirective

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

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

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.

data LHSCore

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

Constructors

LHSHead 
LHSProj 

Fields

lhsDestructor :: QName

record projection identifier

lhsPatsLeft :: [NamedArg Pattern]

side patterns

lhsFocus :: NamedArg LHSCore

main branch

lhsPatsRight :: [NamedArg Pattern]

side patterns

type RHS = RHS' Expr

data RHS' e

Constructors

AbsurdRHS

No right hand side because of absurd match.

RHS e 

data WhereClause' decls

Constructors

NoWhere

No where clauses.

AnyWhere decls

Ordinary where.

SomeWhere Name decls

Named where: module M where.

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

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

data ThingWithFixity x

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity' 

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.

Lenses

Concrete instances

type Color = Expr

type Arg a = Arg Color a