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.
- 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
- module Agda.Syntax.Concrete.Name
- appView :: Expr -> AppView
- data AppView = AppView Expr [NamedArg Expr]
- data LamBinding
- data TypedBindings = TypedBindings !Range Hiding [TypedBinding]
- data TypedBinding
- data BoundName = BName {
- boundName :: Name
- bnameFixity :: Fixity
- mkBoundName_ :: Name -> BoundName
- type Telescope = [TypedBindings]
- data Declaration
- = 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]
- | 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
- 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
- = ImportedModule {
- data Renaming = Renaming {
- renFrom :: ImportedName
- renTo :: Name
- renToRange :: Range
- data AsName = AsName {}
- defaultImportDir :: ImportDirective
- data OpenShortHand
- data LHS
- data Pattern
- data RHS
- data WhereClause
- = NoWhere
- | AnyWhere [Declaration]
- | SomeWhere Name [Declaration]
- data Pragma
- type Module = ([Pragma], [Declaration])
- topLevelModuleName :: Module -> TopLevelModuleName
Expressions
Concrete expressions. Should represent exactly what the user wrote.
Ident QName | ex: |
Lit Literal | ex: |
QuestionMark !Range (Maybe Nat) | ex: |
Underscore !Range (Maybe Nat) | ex: |
RawApp !Range [Expr] | before parsing operators |
App !Range Expr (NamedArg Expr) | ex: |
OpApp !Range Name [Expr] | ex: |
WithApp !Range Expr [Expr] | ex: |
HiddenArg !Range (Named String Expr) | ex: |
Lam !Range [LamBinding] Expr | ex: |
AbsurdLam !Range Hiding | ex: |
Fun !Range Expr Expr | ex: |
Pi Telescope Expr | ex: |
Set !Range | ex: |
Prop !Range | ex: |
SetN !Range Nat | ex: |
Rec !Range [(Name, Expr)] | ex: |
Let !Range [Declaration] Expr | ex: |
Paren !Range Expr | ex: |
Absurd !Range | ex: |
As !Range Name Expr | ex: |
Dot !Range Expr | ex: |
ETel Telescope | only used for printing telescopes |
module Agda.Syntax.Concrete.Name
Bindings
data LamBinding Source
A lambda binding is either domain free or typed.
DomainFree Hiding BoundName | . |
DomainFull TypedBindings | . |
data TypedBindings Source
A sequence of typed bindings with hiding information. Appears in dependent function spaces, typed lambdas, and telescopes.
TypedBindings !Range Hiding [TypedBinding] | . |
data TypedBinding Source
A typed binding.
BName | |
|
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.
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 |
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).
ImportDirective | |
|
data UsingOrHiding Source
data ImportedName Source
An imported name can be a module or a defined name
Renaming | |
|
data OpenShortHand 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.
Concrete patterns. No literals in patterns at the moment.
data WhereClause Source
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 |
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.