Safe Haskell | None |
---|---|
Language | Haskell98 |
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 (Set Name) [NamedArg (OpApp Expr)]
- | WithApp !Range Expr [Expr]
- | HiddenArg !Range (Named_ Expr)
- | InstanceArg !Range (Named_ 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
- | QuoteContext !Range Name Expr
- | Quote !Range
- | QuoteTerm !Range
- | Tactic !Range Expr [Expr]
- | Unquote !Range
- | DontCare Expr
- | Equal !Range Expr 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]
- type LamBinding = LamBinding' TypedBindings
- data LamBinding' a
- type TypedBindings = TypedBindings' TypedBinding
- data TypedBindings' a = TypedBindings !Range (Arg a)
- type TypedBinding = TypedBinding' Expr
- data TypedBinding' e
- = TBind !Range [WithHiding BoundName] e
- | TLet !Range [Declaration]
- data ColoredTypedBinding = WithColors [Color] TypedBinding
- data BoundName = BName {
- boundName :: Name
- boundLabel :: Name
- bnameFixity :: Fixity'
- mkBoundName_ :: Name -> BoundName
- mkBoundName :: Name -> Fixity' -> BoundName
- type Telescope = [TypedBindings]
- countTelVars :: Telescope -> Nat
- data Declaration
- = TypeSig ArgInfo 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 (Ranged Induction)) (Maybe Name) [LamBinding] (Maybe Expr) [Declaration]
- | Infix Fixity [Name]
- | Syntax Name Notation
- | PatternSyn !Range Name [Arg Name] Pattern
- | Mutual !Range [Declaration]
- | Abstract !Range [Declaration]
- | Private !Range [Declaration]
- | InstanceB !Range [Declaration]
- | Postulate !Range [TypeSignatureOrInstanceBlock]
- | 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]
- | UnquoteDecl !Range Name Expr
- | Pragma Pragma
- data ModuleApplication
- type TypeSignature = Declaration
- type TypeSignatureOrInstanceBlock = 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
- | QuoteP !Range
- | AppP Pattern (NamedArg Pattern)
- | RawAppP !Range [Pattern]
- | OpAppP !Range QName (Set Name) [NamedArg Pattern]
- | HiddenP !Range (Named_ Pattern)
- | InstanceP !Range (Named_ Pattern)
- | ParenP !Range Pattern
- | WildP !Range
- | AbsurdP !Range
- | AsP !Range Name Pattern
- | DotP !Range Expr
- | LitP Literal
- data LHSCore
- type RHS = RHS' Expr
- data RHS' e
- type WhereClause = WhereClause' [Declaration]
- data WhereClause' decls
- data Pragma
- = OptionsPragma !Range [String]
- | BuiltinPragma !Range String Expr
- | RewritePragma !Range QName
- | CompiledDataPragma !Range QName String [String]
- | CompiledTypePragma !Range QName String
- | CompiledPragma !Range QName String
- | CompiledExportPragma !Range QName String
- | CompiledEpicPragma !Range QName String
- | CompiledJSPragma !Range QName String
- | StaticPragma !Range QName
- | ImportPragma !Range String
- | ImpossiblePragma !Range
- | EtaPragma !Range QName
- | TerminationCheckPragma !Range (TerminationCheck Name)
- type Module = ([Pragma], [Declaration])
- data ThingWithFixity x = ThingWithFixity x Fixity'
- topLevelModuleName :: Module -> TopLevelModuleName
- patternHead :: Pattern -> Maybe Name
- patternNames :: Pattern -> [Name]
- mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
- type Color = Expr
- type Arg a = Arg Color a
- type NamedArg a = NamedArg Color a
- type ArgInfo = ArgInfo Color
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 (Set Name) [NamedArg (OpApp Expr)] | ex: |
WithApp !Range Expr [Expr] | ex: |
HiddenArg !Range (Named_ Expr) | ex: |
InstanceArg !Range (Named_ 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: |
QuoteContext !Range Name Expr | ex: |
Quote !Range | ex: |
QuoteTerm !Range | ex: |
Tactic !Range Expr [Expr] | tactic solve | subgoal1 | .. | subgoalN |
Unquote !Range | ex: |
DontCare Expr | to print irrelevant things |
Equal !Range Expr Expr | ex: |
SyntaxBindingLambda !Range [LamBinding] e | An abstraction inside a special syntax declaration (see Issue 358 why we introduce this). |
Ordinary e |
fromOrdinary :: e -> OpApp e -> e Source
module Agda.Syntax.Concrete.Name
Bindings
type LamBinding = LamBinding' TypedBindings Source
A lambda binding is either domain free or typed.
data LamBinding' a Source
DomainFree ArgInfo BoundName | . |
DomainFull a | . |
data TypedBindings' a Source
TypedBindings !Range (Arg a) | . |
type TypedBinding = TypedBinding' Expr Source
A typed binding.
data TypedBinding' e Source
TBind !Range [WithHiding BoundName] e | Binding |
TLet !Range [Declaration] | Let binding |
BName | |
|
mkBoundName_ :: Name -> BoundName Source
mkBoundName :: Name -> Fixity' -> BoundName Source
type Telescope = [TypedBindings] Source
A telescope is a sequence of typed bindings. Bound variables are in scope in later types.
countTelVars :: Telescope -> Nat Source
Declarations
data Declaration Source
The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.
KillRange Declaration Source | |
KillRange WhereClause Source | |
HasRange Declaration Source | |
HasRange WhereClause Source | |
ExprLike Declaration Source | |
ToConcrete LetBinding [Declaration] Source | |
ToConcrete Declaration [Declaration] Source | |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source | |
ToConcrete (Constr Constructor) Declaration Source | |
ToAbstract (TopLevel [Declaration]) TopLevelInfo Source | Top-level declarations are always
|
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] Source | |
ToAbstract [Declaration] [Declaration] Source |
data ModuleApplication Source
SectionApp Range [TypedBindings] Expr | tel. M args |
RecordModuleIFS Range QName | M {{...}} |
type TypeSignature = Declaration Source
Just type signatures.
type TypeSignatureOrInstanceBlock = Declaration Source
Just type signatures or instance blocks.
type Constructor = TypeSignature Source
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 :: ImportDirective Source
Default is directive is private
(use everything, but do not export).
type RewriteEqn = Expr 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.
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 |
|
QuoteP !Range | quote |
AppP Pattern (NamedArg Pattern) |
|
RawAppP !Range [Pattern] |
|
OpAppP !Range QName (Set Name) [NamedArg Pattern] | eg: |
HiddenP !Range (Named_ Pattern) |
|
InstanceP !Range (Named_ 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 | |
|
type WhereClause = WhereClause' [Declaration] Source
data WhereClause' decls Source
OptionsPragma !Range [String] | |
BuiltinPragma !Range String Expr | |
RewritePragma !Range QName | |
CompiledDataPragma !Range QName String [String] | |
CompiledTypePragma !Range QName String | |
CompiledPragma !Range QName String | |
CompiledExportPragma !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 | |
TerminationCheckPragma !Range (TerminationCheck Name) |
type Module = ([Pragma], [Declaration]) Source
Modules: Top-level pragmas plus other top-level declarations.
data ThingWithFixity x Source
Decorating something with Fixity'
.
topLevelModuleName :: Module -> TopLevelModuleName Source
Computes the top-level module name.
Precondition: The Module
has to be well-formed.
Pattern tools
patternHead :: Pattern -> Maybe Name Source
Get the leftmost symbol in a pattern.
patternNames :: Pattern -> [Name] Source
Get all the identifiers in a pattern in left-to-right order.