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

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 Source

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

ex: _

RawApp !Range [Expr]

before parsing operators

App !Range Expr (NamedArg Expr)

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

OpApp !Range Name [Expr]

ex: e + e

WithApp !Range Expr [Expr]

ex: e | e1 | .. | en

HiddenArg !Range (Named String Expr)

ex: {e} or {x=e}

Lam !Range [LamBinding] Expr

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

AbsurdLam !Range Hiding

ex: \ ()

Fun !Range Expr Expr

ex: e -> e or {e} -> e

Pi Telescope Expr

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

Set !Range

ex: Set

Prop !Range

ex: Prop

SetN !Range Nat

ex: Set0, Set1, ..

Rec !Range [(Name, Expr)]

ex: record {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

Instances

module Agda.Syntax.Concrete.Name

appView :: Expr -> AppViewSource

data AppView Source

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr] 

Bindings

data LamBinding Source

A lambda binding is either domain free or typed.

Constructors

DomainFree Hiding BoundName

. x or {x}

DomainFull TypedBindings

. (xs:e,..,ys:e') or {xs:e,..,ys:e'}

Instances

data TypedBindings Source

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

Constructors

TypedBindings !Range Hiding [TypedBinding]

. (xs:e;..;ys:e') or {xs:e;..;ys:e'}

Instances

data TypedBinding Source

A typed binding.

Constructors

TBind !Range [BoundName] Expr 
TNoBind Expr 

Instances

data BoundName Source

Constructors

BName 

Fields

boundName :: Name
 
bnameFixity :: Fixity
 

Instances

mkBoundName_ :: Name -> BoundNameSource

type Telescope = [TypedBindings]Source

A telescope is a sequence of typed bindings. Bound variables are in scope in later types. Or it's the mysterious Thierry-function-telescope. Only it's not.

Declarations

data Declaration Source

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

Constructors

TypeSig Name Expr 
Field Hiding Name Expr 
FunClause LHS RHS WhereClause 
Data !Range Induction Name [TypedBindings] Expr [Constructor] 
Record !Range Name (Maybe Name) [TypedBindings] Expr [Declaration]

The optional name is a name for the record constructor.

Infix Fixity [Name] 
Mutual !Range [Declaration] 
Abstract !Range [Declaration] 
Private !Range [Declaration] 
Postulate !Range [TypeSignature] 
Primitive !Range [TypeSignature] 
Open !Range QName ImportDirective 
Import !Range QName (Maybe AsName) OpenShortHand ImportDirective 
ModuleMacro !Range Name [TypedBindings] Expr OpenShortHand ImportDirective 
Module !Range QName [TypedBindings] [Declaration] 
Pragma Pragma 

Instances

type TypeSignature = DeclarationSource

Just type signatures.

type Constructor = TypeSignatureSource

A constructor or field declaration is just a type signature.

type Field = TypeSignatureSource

data ImportDirective Source

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

data UsingOrHiding Source

Constructors

Hiding [ImportedName] 
Using [ImportedName] 

Instances

data ImportedName Source

An imported name can be a module or a defined name

Constructors

ImportedModule 

Fields

importedName :: Name
 
ImportedName 

Fields

importedName :: Name
 

Instances

data Renaming Source

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

data AsName Source

Constructors

AsName 

Fields

asName :: Name

The "as" name.

asRange :: Range

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

Instances

defaultImportDir :: ImportDirectiveSource

data OpenShortHand Source

Constructors

DoOpen 
DontOpen 

Instances

data LHS Source

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 Pattern [Pattern] [RewriteEqn] [WithExpr]

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

Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]

new with-patterns, rewrite equations and with-expressions

Instances

data Pattern Source

Concrete patterns. No literals in patterns at the moment.

Constructors

IdentP QName 
AppP Pattern (NamedArg Pattern) 
RawAppP !Range [Pattern] 
OpAppP !Range Name [Pattern] 
HiddenP !Range (Named String Pattern) 
ParenP !Range Pattern 
WildP !Range 
AbsurdP !Range 
AsP !Range Name Pattern 
DotP !Range Expr 
LitP Literal 

Instances

data RHS Source

Constructors

AbsurdRHS 
RHS Expr 

Instances

data WhereClause Source

Constructors

NoWhere 
AnyWhere [Declaration] 
SomeWhere Name [Declaration] 

Instances

data Pragma Source

Constructors

OptionsPragma !Range [String] 
BuiltinPragma !Range String Expr 
CompiledDataPragma !Range QName String [String] 
CompiledTypePragma !Range QName String 
CompiledPragma !Range QName String 
ImportPragma !Range String

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

ImpossiblePragma !Range 

Instances

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

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

topLevelModuleName :: Module -> TopLevelModuleNameSource

Computes the top-level module name.

Precondition: The Module has to be well-formed.