|
|
|
|
|
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
|
|
|
Concrete expressions. Should represent exactly what the user wrote.
| Constructors | |
|
|
module Agda.Syntax.Concrete.Name |
|
|
|
|
The Expr is not an application.
| Constructors | |
|
|
Bindings
|
|
|
A lambda binding is either domain free or typed.
| Constructors | |
|
|
|
A sequence of typed bindings with hiding information. Appears in dependent
function spaces, typed lambdas, and telescopes.
| Constructors | |
|
|
|
A typed binding.
| Constructors | |
|
|
|
|
|
|
|
|
A telescope is a sequence of typed bindings. Bound variables are in scope
in later types.
|
|
Declarations
|
|
|
The representation type of a declaration. The comments indicate
which type in the intended family the constructor targets.
| Constructors | |
|
|
|
Just type signatures.
|
|
|
A constructor or field declaration is just a type signature.
|
|
|
|
|
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import, namespace, or open declarations).
| Constructors | ImportDirective | | importDirRange :: !Range | | usingOrHiding :: UsingOrHiding | | renaming :: [Renaming] | | publicOpen :: Bool | Only for open. Exports the opened names from the current module.
|
|
|
|
|
|
|
|
|
An imported name can be a module or a defined name
| Constructors | ImportedModule | | | ImportedName | | |
|
|
|
|
Constructors | Renaming | | renFrom :: ImportedName | Rename from this name.
| renTo :: Name | To this one.
| renToRange :: Range | The range of the "to" keyword. Retained
for highlighting purposes.
|
|
|
|
|
|
Constructors | AsName | | asName :: Name | The "as" name.
| asRange :: Range | The range of the "as" keyword. Retained
for highlighting purposes.
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
Concrete patterns. No literals in patterns at the moment.
| Constructors | |
|
|
|
|
|
|
|
|
|
|
|
|
Modules: Top-level pragmas plus other top-level declarations.
|
|
|
Computes the top-level module name.
Precondition: The Module has to be well-formed.
|
|
Produced by Haddock version 2.6.1 |