Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 (MaybePlaceholder (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, Bool)]
- | Fun Range Expr Expr
- | Pi Telescope Expr
- | Set Range
- | Prop Range
- | SetN Range Integer
- | Rec Range RecordAssignments
- | RecUpdate Range Expr [FieldAssignment]
- | Let Range [Declaration] Expr
- | Paren Range Expr
- | IdiomBrackets Range Expr
- | Absurd Range
- | As Range Name Expr
- | Dot Range Expr
- | ETel Telescope
- | QuoteGoal Range Name Expr
- | QuoteContext Range
- | 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]
- type RecordAssignment = Either FieldAssignment ModuleAssignment
- type RecordAssignments = [RecordAssignment]
- type FieldAssignment = FieldAssignment' Expr
- data FieldAssignment' a = FieldAssignment {
- _nameFieldA :: Name
- _exprFieldA :: a
- nameFieldA :: Lens' Name (FieldAssignment' a)
- exprFieldA :: Lens' a (FieldAssignment' a)
- data ModuleAssignment = ModuleAssignment {}
- 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 IsInstance Name (Arg Expr)
- | FunClause LHS RHS WhereClause Bool
- | DataSig Range Induction Name [LamBinding] Expr
- | Data Range Induction Name [LamBinding] (Maybe Expr) [TypeSignatureOrInstanceBlock]
- | RecordSig Range Name [LamBinding] Expr
- | Record Range Name (Maybe (Ranged Induction)) (Maybe Bool) (Maybe (Name, IsInstance)) [LamBinding] (Maybe Expr) [Declaration]
- | Infix Fixity [Name]
- | Syntax Name Notation
- | PatternSyn Range Name [Arg Name] Pattern
- | Mutual Range [Declaration]
- | Abstract Range [Declaration]
- | Private Range Origin [Declaration]
- | InstanceB Range [Declaration]
- | Macro 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
- | UnquoteDef Range [Name] Expr
- | Pragma Pragma
- data ModuleApplication
- type TypeSignature = Declaration
- type TypeSignatureOrInstanceBlock = Declaration
- type ImportDirective = ImportDirective' Name Name
- type Using = Using' Name Name
- type ImportedName = ImportedName' Name Name
- type Renaming = Renaming' Name Name
- data AsName = AsName {}
- 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 Origin Expr
- | LitP Literal
- | RecP Range [FieldAssignment' Pattern]
- data LHSCore
- type RHS = RHS' Expr
- data RHS' e
- type WhereClause = WhereClause' [Declaration]
- data WhereClause' decls
- data ExprWhere = ExprWhere Expr WhereClause
- 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
- | CompiledJSPragma Range QName String
- | CompiledUHCPragma Range QName String
- | CompiledDataUHCPragma Range QName String [String]
- | HaskellCodePragma Range String
- | ForeignPragma Range String String
- | CompilePragma Range String QName String
- | StaticPragma Range QName
- | InjectivePragma Range QName
- | InlinePragma Range QName
- | ImportPragma Range String
- | ImportUHCPragma Range String
- | ImpossiblePragma Range
- | EtaPragma Range QName
- | TerminationCheckPragma Range (TerminationCheck Name)
- | CatchallPragma Range
- | DisplayPragma Range Pattern Expr
- | NoPositivityCheckPragma Range
- | PolarityPragma Range Name [Occurrence]
- type Module = ([Pragma], [Declaration])
- data ThingWithFixity x = ThingWithFixity x Fixity'
- topLevelModuleName :: Module -> TopLevelModuleName
- spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
- patternNames :: Pattern -> [Name]
- patternQNames :: Pattern -> [QName]
- mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS
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 (MaybePlaceholder (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, Bool)] | ex: |
Fun Range Expr Expr | ex: |
Pi Telescope Expr | ex: |
Set Range | ex: |
Prop Range | ex: |
SetN Range Integer | ex: |
Rec Range RecordAssignments | ex: |
RecUpdate Range Expr [FieldAssignment] | ex: |
Let Range [Declaration] Expr | ex: |
Paren Range Expr | ex: |
IdiomBrackets 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 | 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 |
type RecordAssignments = [RecordAssignment] Source #
type FieldAssignment = FieldAssignment' Expr Source #
data FieldAssignment' a Source #
FieldAssignment | |
|
Functor FieldAssignment' Source # | |
Foldable FieldAssignment' Source # | |
Traversable FieldAssignment' Source # | |
ExprLike FieldAssignment Source # | |
SubstExpr Assign Source # | |
APatternLike a b => APatternLike a (FieldAssignment' b) Source # | |
Eq a => Eq (FieldAssignment' a) Source # | |
Data a => Data (FieldAssignment' a) Source # | |
Show a => Show (FieldAssignment' a) Source # | |
NFData a => NFData (FieldAssignment' a) Source # | |
KillRange a => KillRange (FieldAssignment' a) Source # | |
HasRange a => HasRange (FieldAssignment' a) Source # | |
ExprLike a => ExprLike (FieldAssignment' a) Source # | |
MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) Source # | |
NamesIn a => NamesIn (FieldAssignment' a) Source # | |
ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) Source # | |
ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c) Source # | |
ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a) Source # | |
nameFieldA :: Lens' Name (FieldAssignment' a) Source #
exprFieldA :: Lens' a (FieldAssignment' a) Source #
data ModuleAssignment Source #
BName | |
|
mkBoundName_ :: Name -> 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.
Data Declaration Source # | |
NFData Declaration Source # | Ranges are not forced. |
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 ImportDirective = ImportDirective' Name Name Source #
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import
, namespace
, or open
declarations).
type ImportedName = ImportedName' Name Name Source #
An imported name can be a module or a defined name.
data OpenShortHand Source #
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 Origin Expr |
|
LitP Literal |
|
RecP Range [FieldAssignment' Pattern] | record {x = p; y = q} |
Processed (scope-checked) intermediate form of the core f ps
of LHS
.
Corresponds to lhsOriginalPattern
.
LHSHead | |
| |
LHSProj | |
|
Functor RHS' Source # | |
Foldable RHS' Source # | |
Traversable RHS' Source # | |
KillRange RHS Source # | |
HasRange RHS Source # | |
ToAbstract RHS AbstractRHS Source # | |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) Source # | |
Data e => Data (RHS' e) Source # | |
NFData a => NFData (RHS' a) Source # | |
ExprLike a => ExprLike (RHS' a) Source # | |
type WhereClause = WhereClause' [Declaration] Source #
data WhereClause' decls Source #
NoWhere | No |
AnyWhere decls | Ordinary |
SomeWhere Name Access decls | Named where: |
Functor WhereClause' Source # | |
Foldable WhereClause' Source # | |
Traversable WhereClause' Source # | |
KillRange WhereClause Source # | |
HasRange WhereClause Source # | |
Data decls => Data (WhereClause' decls) Source # | |
NFData a => NFData (WhereClause' a) Source # | |
Null (WhereClause' a) Source # | A |
ExprLike a => ExprLike (WhereClause' a) Source # | |
An expression followed by a where clause. Currently only used to give better a better error message in interaction.
type Module = ([Pragma], [Declaration]) Source #
Modules: Top-level pragmas plus other top-level declarations.
data ThingWithFixity x Source #
Decorating something with Fixity'
.
Functor ThingWithFixity Source # | |
Foldable ThingWithFixity Source # | |
Traversable ThingWithFixity Source # | |
Data x => Data (ThingWithFixity x) Source # | |
Show x => Show (ThingWithFixity x) Source # | |
KillRange x => KillRange (ThingWithFixity x) Source # | |
topLevelModuleName :: Module -> TopLevelModuleName Source #
Computes the top-level module name.
Precondition: The Module
has to be well-formed.
This means that there are only allowed declarations before the
first module declaration, typically import declarations.
See spanAllowedBeforeModule
.
spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration]) Source #
Splits off allowed (= import) declarations before the first non-allowed declaration. After successful parsing, the first non-allowed declaration should be a module declaration.
Pattern tools
patternNames :: Pattern -> [Name] Source #
Get all the identifiers in a pattern in left-to-right order.
patternQNames :: Pattern -> [QName] Source #
Get all the identifiers in a pattern in left-to-right order.