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

Agda.Syntax.Concrete

Contents

- Expressions
- Bindings
- Declarations

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

- data Expr
  - = Ident QName
  - | Lit Literal
  - | QuestionMark !Range (Maybe Nat)
  - | Underscore !Range (Maybe Nat)
  - | RawApp !Range [Expr]
  - | App !Range Expr (NamedArg Expr)
  - | OpApp !Range Name [Expr]
  - | WithApp !Range Expr [Expr]
  - | HiddenArg !Range (Named String Expr)
  - | Lam !Range [LamBinding] Expr
  - | AbsurdLam !Range Hiding
  - | Fun !Range Expr Expr
  - | Pi Telescope Expr
  - | Set !Range
  - | Prop !Range
  - | SetN !Range Nat
  - | Rec !Range [(Name, Expr)]
  - | Let !Range [Declaration] Expr
  - | Paren !Range Expr
  - | Absurd !Range
  - | As !Range Name Expr
  - | Dot !Range Expr
  - | ETel Telescope
  - | QuoteGoal !Range Name Expr
  - | Quote !Range
- module Agda.Syntax.Concrete.Name
- appView :: Expr -> AppView
- data AppView = AppView Expr [NamedArg Expr]
- data LamBinding
  - = DomainFree Hiding BoundName
  - | DomainFull TypedBindings
- data TypedBindings = TypedBindings !Range (Arg [TypedBinding])
- data TypedBinding
  - = TBind !Range [BoundName] Expr
  - | TNoBind Expr
- data BoundName = BName {
  - boundName :: Name
  - bnameFixity :: Fixity'
  }
- mkBoundName_ :: Name -> BoundName
- type Telescope = [TypedBindings]
- data Declaration
  - = TypeSig Relevance Name Expr
  - | Field Name (Arg Expr)
  - | FunClause LHS RHS WhereClause
  - | Data !Range Induction Name [TypedBindings] Expr [Constructor]
  - | Record !Range Name (Maybe Name) [TypedBindings] Expr [Declaration]
  - | Infix Fixity [Name]
  - | Syntax Name Notation
  - | 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
- type TypeSignature = Declaration
- type Constructor = TypeSignature
- type Field = TypeSignature
- data ImportDirective = ImportDirective {
  - importDirRange :: !Range
  - usingOrHiding :: UsingOrHiding
  - renaming :: [Renaming]
  - publicOpen :: Bool
  }
- data UsingOrHiding
  - = Hiding [ImportedName]
  - | Using [ImportedName]
- data ImportedName
  - = ImportedModule {
    - importedName :: Name
    }
  - | ImportedName {
    - importedName :: Name
    }
- data Renaming = Renaming {
  - renFrom :: ImportedName
  - renTo :: Name
  - renToRange :: Range
  }
- data AsName = AsName {
  - asName :: Name
  - asRange :: Range
  }
- defaultImportDir :: ImportDirective
- data OpenShortHand
  - = DoOpen
  - | DontOpen
- data LHS
  - = LHS Pattern [Pattern] [RewriteEqn] [WithExpr]
  - | Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]
- data Pattern
  - = 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
- data RHS
  - = AbsurdRHS
  - | RHS Expr
- data WhereClause
  - = NoWhere
  - | AnyWhere [Declaration]
  - | SomeWhere Name [Declaration]
- data Pragma
  - = OptionsPragma !Range [String]
  - | BuiltinPragma !Range String Expr
  - | CompiledDataPragma !Range QName String [String]
  - | CompiledTypePragma !Range QName String
  - | CompiledPragma !Range QName String
  - | CompiledEpicPragma !Range QName String
  - | ImportPragma !Range String
  - | ImpossiblePragma !Range
  - | EtaPragma !Range QName
- type Module = ([Pragma], [Declaration])
- topLevelModuleName :: Module -> TopLevelModuleName

# 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 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` (NYI: `{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
QuoteGoal !Range Name Expr | ex: `quoteGoal x in e`
Quote !Range | ex: `quote`, should be applied to a name

Instances

Data Expr |
Show Expr |
Typeable Expr |
Pretty Expr |
HasRange Expr |
Strict Expr |
IsExpr Expr |
LowerMeta Expr |
ToConcrete MetaId Expr |
ToConcrete Expr Expr |
ToConcrete InteractionId Expr |
ToAbstract Expr Expr |
ToAbstract Pattern (Pattern' Expr) |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |

module Agda.Syntax.Concrete.Name

appView :: Expr -> AppView

data AppView

The `Expr` is not an application.

Constructors

AppView Expr [NamedArg Expr] |

# Bindings

data LamBinding

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 LamBinding |
Show LamBinding |
Typeable LamBinding |
Pretty LamBinding |
HasRange LamBinding |
LowerMeta LamBinding |
ToConcrete LamBinding LamBinding |
ToAbstract LamBinding LamBinding |

data TypedBindings

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

Constructors

TypedBindings !Range (Arg [TypedBinding]) | . `(xs:e;..;ys:e')` or `{xs:e;..;ys:e'}`

Instances

Data TypedBindings |
Show TypedBindings |
Typeable TypedBindings |
Pretty TypedBindings |
HasRange TypedBindings |
LowerMeta TypedBindings |
ToConcrete TypedBindings TypedBindings |
ToAbstract TypedBindings TypedBindings |

data TypedBinding

A typed binding.

Constructors

TBind !Range [BoundName] Expr |
TNoBind Expr |

Instances

Data TypedBinding |
Typeable TypedBinding |
Pretty TypedBinding |
HasRange TypedBinding |
LowerMeta TypedBinding |
ToConcrete TypedBinding TypedBinding |
ToAbstract TypedBinding TypedBinding |

data BoundName

Constructors

BName |

Fields

boundName :: Name
bnameFixity :: Fixity'

Instances

Data BoundName |
Typeable BoundName |
Pretty BoundName |
HasRange BoundName |
ToAbstract (NewName BoundName) Name |

mkBoundName_ :: Name -> BoundName

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.

Constructors

TypeSig Relevance Name Expr | Axioms and functions can be irrelevant.
Field Name (Arg Expr) | Record field, can be hidden and/or irrelevant.
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] |
Syntax Name Notation | notation declaration for a 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

Data Declaration |
Show Declaration |
Typeable Declaration |
Pretty Declaration |
HasRange Declaration |
Strict Declaration |
LowerMeta Declaration |
ToConcrete Clause [Declaration] |
ToConcrete LetBinding [Declaration] |
ToConcrete Declaration [Declaration] |
ToConcrete TypeAndDef [Declaration] |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |
Pretty [Declaration] |
ToConcrete (Constr Constructor) Declaration |
ToAbstract (TopLevel [Declaration]) TopLevelInfo |
ToConcrete [Declaration] [Declaration] |
ToAbstract [Declaration] [Declaration] |

type TypeSignature = Declaration

Just type signatures.

type Constructor = TypeSignature

A constructor or field declaration is just a type signature.

type Field = TypeSignature

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

Data ImportDirective |
Show ImportDirective |
Typeable ImportDirective |
Pretty ImportDirective |
HasRange ImportDirective |

data UsingOrHiding

Constructors

Hiding [ImportedName] |
Using [ImportedName] |

Instances

Data UsingOrHiding |
Typeable UsingOrHiding |
Pretty 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 |
Data ImportedName |
Ord ImportedName |
Show ImportedName |
Typeable ImportedName |
Pretty 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

Data Renaming |
Typeable 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

Data AsName |
Typeable AsName |
HasRange AsName |

defaultImportDir :: ImportDirective

data OpenShortHand

Constructors

DoOpen |
DontOpen |

Instances

Data OpenShortHand |
Show OpenShortHand |
Typeable OpenShortHand |
Pretty OpenShortHand |

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 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 LHS |
Typeable LHS |
Pretty LHS |
HasRange LHS |
ToConcrete LHS LHS |

data Pattern

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 Pattern |
Show Pattern |
Typeable Pattern |
Pretty Pattern |
HasRange Pattern |
IsExpr Pattern |
ToConcrete Pattern Pattern |
ToAbstract Pattern (Pattern' Expr) |
Pretty [Pattern] |

data RHS

Constructors

AbsurdRHS |
RHS Expr |

Instances

Data RHS |
Show RHS |
Typeable RHS |
Pretty RHS |
HasRange RHS |
LowerMeta RHS |
ToAbstract RHS AbstractRHS |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |

data WhereClause

Constructors

NoWhere |
AnyWhere [Declaration] |
SomeWhere Name [Declaration] |

Instances

Data WhereClause |
Typeable WhereClause |
Pretty WhereClause |
HasRange WhereClause |
LowerMeta WhereClause |
ToConcrete AsWhereDecls WhereClause |

data Pragma

Constructors

OptionsPragma !Range [String] |
BuiltinPragma !Range String Expr |
CompiledDataPragma !Range QName String [String] |
CompiledTypePragma !Range QName String |
CompiledPragma !Range QName String |
CompiledEpicPragma !Range QName String |
ImportPragma !Range String | Invariant: The string must be a valid Haskell module name.
ImpossiblePragma !Range |
EtaPragma !Range QName |

Instances

Data Pragma |
Show Pragma |
Typeable Pragma |
Pretty Pragma |
HasRange Pragma |
Strict Pragma |
ToConcrete RangeAndPragma Pragma |
ToAbstract Pragma [Pragma] |

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

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

topLevelModuleName :: Module -> TopLevelModuleName

Computes the top-level module name.

Precondition: The `Module` has to be well-formed.