Safe Haskell | None |
---|
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 String)
- | RawApp !Range [Expr]
- | App !Range Expr (NamedArg Expr)
- | OpApp !Range QName [OpApp Expr]
- | WithApp !Range Expr [Expr]
- | HiddenArg !Range (Named String Expr)
- | InstanceArg !Range (Named String Expr)
- | Lam !Range [LamBinding] Expr
- | AbsurdLam !Range Hiding
- | ExtendedLam !Range [(LHS, RHS, WhereClause)]
- | Fun !Range Expr Expr
- | Pi Telescope Expr
- | Set !Range
- | Prop !Range
- | SetN !Range Integer
- | Rec !Range [(Name, Expr)]
- | RecUpdate !Range Expr [(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
- | QuoteTerm !Range
- | Unquote !Range
- | DontCare Expr
- data OpApp e
- = SyntaxBindingLambda !Range [LamBinding] e
- | Ordinary e
- fromOrdinary :: e -> OpApp e -> e
- module Agda.Syntax.Concrete.Name
- appView :: Expr -> AppView
- data AppView = AppView Expr [NamedArg Expr]
- data LamBinding
- data TypedBindings = TypedBindings !Range (Arg TypedBinding)
- data TypedBinding
- 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
- | DataSig !Range Induction Name [LamBinding] Expr
- | Data !Range Induction Name [LamBinding] (Maybe Expr) [Constructor]
- | RecordSig !Range Name [LamBinding] Expr
- | Record !Range Name (Maybe Induction) (Maybe Name) [LamBinding] (Maybe Expr) [Declaration]
- | Infix Fixity [Name]
- | Syntax Name Notation
- | PatternSyn !Range Name [Name] Pattern
- | 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 ModuleApplication OpenShortHand ImportDirective
- | Module !Range QName [TypedBindings] [Declaration]
- | Pragma Pragma
- data ModuleApplication
- type TypeSignature = Declaration
- type Constructor = 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
- type RewriteEqn = Expr
- type WithExpr = Expr
- data LHS
- = LHS {
- lhsOriginalPattern :: Pattern
- lhsWithPattern :: [Pattern]
- lhsRewriteEqn :: [RewriteEqn]
- lhsWithExpr :: [WithExpr]
- | Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]
- = LHS {
- data Pattern
- = IdentP QName
- | AppP Pattern (NamedArg Pattern)
- | RawAppP !Range [Pattern]
- | OpAppP !Range QName [Pattern]
- | HiddenP !Range (Named String Pattern)
- | InstanceP !Range (Named String Pattern)
- | ParenP !Range Pattern
- | WildP !Range
- | AbsurdP !Range
- | AsP !Range Name Pattern
- | DotP !Range Expr
- | LitP Literal
- data LHSCore
- data RHS
- 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
- | CompiledJSPragma !Range QName String
- | StaticPragma !Range QName
- | ImportPragma !Range String
- | ImpossiblePragma !Range
- | EtaPragma !Range QName
- | NoTerminationCheckPragma !Range
- type Module = ([Pragma], [Declaration])
- data ThingWithFixity x = ThingWithFixity x Fixity'
- topLevelModuleName :: Module -> TopLevelModuleName
- patternHead :: Pattern -> Maybe Name
- patternNames :: Pattern -> [Name]
Expressions
Concrete expressions. Should represent exactly what the user wrote.
Ident QName | ex: |
Lit Literal | ex: |
QuestionMark !Range (Maybe Nat) | ex: |
Underscore !Range (Maybe String) | ex: |
RawApp !Range [Expr] | before parsing operators |
App !Range Expr (NamedArg Expr) | ex: |
OpApp !Range QName [OpApp Expr] | ex: |
WithApp !Range Expr [Expr] | ex: |
HiddenArg !Range (Named String Expr) | ex: |
InstanceArg !Range (Named String Expr) | ex: |
Lam !Range [LamBinding] Expr | ex: |
AbsurdLam !Range Hiding | ex: |
ExtendedLam !Range [(LHS, RHS, WhereClause)] | ex: |
Fun !Range Expr Expr | ex: |
Pi Telescope Expr | ex: |
Set !Range | ex: |
Prop !Range | ex: |
SetN !Range Integer | ex: |
Rec !Range [(Name, Expr)] | ex: |
RecUpdate !Range Expr [(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 |
QuoteGoal !Range Name Expr | ex: |
Quote !Range | ex: |
QuoteTerm !Range | ex: |
Unquote !Range | ex: |
DontCare Expr | to print irrelevant things |
SyntaxBindingLambda !Range [LamBinding] e | an abstraction inside a special syntax declaration (see Issue 358 why we introduce this). |
Ordinary e |
fromOrdinary :: e -> OpApp e -> eSource
module Agda.Syntax.Concrete.Name
Bindings
data LamBinding Source
A lambda binding is either domain free or typed.
DomainFree Hiding Relevance 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 (Arg 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.
Declarations
data Declaration Source
The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.
data ModuleApplication Source
type TypeSignature = DeclarationSource
Just type signatures.
type Constructor = TypeSignatureSource
A data constructor declaration is just a type signature.
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 | |
|
defaultImportDir :: ImportDirectiveSource
Default is directive is private
(use everything, but do not export).
data OpenShortHand Source
type RewriteEqn = ExprSource
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.
LHS | 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.
IdentP QName |
|
AppP Pattern (NamedArg Pattern) |
|
RawAppP !Range [Pattern] |
|
OpAppP !Range QName [Pattern] | eg: |
HiddenP !Range (Named String Pattern) |
|
InstanceP !Range (Named String Pattern) |
|
ParenP !Range Pattern | (p) |
WildP !Range | _ |
AbsurdP !Range | () |
AsP !Range Name Pattern |
|
DotP !Range Expr | .e |
LitP Literal |
|
Processed (scope-checked) intermediate form of the core f ps
of LHS
.
Corresponds to lhsOriginalPattern
.
LHSHead | |
| |
LHSProj | |
|
data WhereClause Source
OptionsPragma !Range [String] | |
BuiltinPragma !Range String Expr | |
CompiledDataPragma !Range QName String [String] | |
CompiledTypePragma !Range QName String | |
CompiledPragma !Range QName String | |
CompiledEpicPragma !Range QName String | |
CompiledJSPragma !Range QName String | |
StaticPragma !Range QName | |
ImportPragma !Range String | Invariant: The string must be a valid Haskell module name. |
ImpossiblePragma !Range | |
EtaPragma !Range QName | |
NoTerminationCheckPragma !Range |
type Module = ([Pragma], [Declaration])Source
Modules: Top-level pragmas plus other top-level declarations.
data ThingWithFixity x Source
topLevelModuleName :: Module -> TopLevelModuleNameSource
Computes the top-level module name.
Precondition: The Module
has to be well-formed.
Pattern tools
patternHead :: Pattern -> Maybe NameSource
Get the leftmost symbol in a pattern.
patternNames :: Pattern -> [Name]Source
Get all the identifiers in a pattern in left-to-right order.