Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.Syntax.Concrete
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.
- 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
data Expr
Concrete expressions. Should represent exactly what the user wrote.
Constructors
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: |
Instances
data OpApp e
Constructors
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
module Agda.Syntax.Concrete.Name
Bindings
type LamBinding = LamBinding' TypedBindings
A lambda binding is either domain free or typed.
data LamBinding' a
Constructors
DomainFree ArgInfo BoundName | . |
DomainFull a | . |
data TypedBindings' a
Constructors
TypedBindings !Range (Arg a) | . |
Instances
type TypedBinding = TypedBinding' Expr
A typed binding.
data TypedBinding' e
Constructors
TBind !Range [WithHiding BoundName] e | Binding |
TLet !Range [Declaration] | Let binding |
Instances
data ColoredTypedBinding
Color a TypeBinding. Used by Pretty.
Constructors
WithColors [Color] TypedBinding |
data BoundName
Constructors
BName | |
Fields
|
mkBoundName_ :: Name -> BoundName
mkBoundName :: Name -> Fixity' -> BoundName
type Telescope = [TypedBindings]
A telescope is a sequence of typed bindings. Bound variables are in scope in later types.
countTelVars :: Telescope -> Nat
Declarations
data Declaration
The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.
Constructors
Instances
KillRange Declaration | |
KillRange WhereClause | |
HasRange Declaration | |
HasRange WhereClause | |
ExprLike Declaration | |
ToConcrete LetBinding [Declaration] | |
ToConcrete Declaration [Declaration] | |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) | |
ToConcrete (Constr Constructor) Declaration | |
ToAbstract (TopLevel [Declaration]) TopLevelInfo | Top-level declarations are always
|
ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] | |
ToAbstract [Declaration] [Declaration] |
data ModuleApplication
Constructors
SectionApp Range [TypedBindings] Expr | tel. M args |
RecordModuleIFS Range QName | M {{...}} |
type TypeSignature = Declaration
Just type signatures.
type TypeSignatureOrInstanceBlock = Declaration
Just type signatures or instance blocks.
type Constructor = TypeSignature
A data constructor declaration is just a type signature.
data ImportDirective
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import
, namespace
, or open
declarations).
Constructors
ImportDirective | |
Fields
|
Instances
data ImportedName
An imported name can be a module or a defined name
Constructors
ImportedModule | |
Fields
| |
ImportedName | |
Fields
|
data Renaming
Constructors
Renaming | |
Fields
|
defaultImportDir :: ImportDirective
Default is directive is private
(use everything, but do not export).
type RewriteEqn = Expr
data LHS
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 | original pattern, with-patterns, rewrite equations and with-expressions |
Fields
| |
Ellipsis Range [Pattern] [RewriteEqn] [WithExpr] | new with-patterns, rewrite equations and with-expressions |
data Pattern
Concrete patterns. No literals in patterns at the moment.
Constructors
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 |
|
data LHSCore
Processed (scope-checked) intermediate form of the core f ps
of LHS
.
Corresponds to lhsOriginalPattern
.
Constructors
LHSHead | |
Fields
| |
LHSProj | |
Fields
|
data RHS' e
Instances
Functor RHS' | |
Foldable RHS' | |
Traversable RHS' | |
KillRange RHS | |
HasRange RHS | |
ToAbstract RHS AbstractRHS | |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) | |
ExprLike a => ExprLike (RHS' a) |
type WhereClause = WhereClause' [Declaration]
data WhereClause' decls
data Pragma
Constructors
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])
Modules: Top-level pragmas plus other top-level declarations.
data ThingWithFixity x
Decorating something with Fixity'
.
Constructors
ThingWithFixity x Fixity' |
Instances
topLevelModuleName :: Module -> TopLevelModuleName
Computes the top-level module name.
Precondition: The Module
has to be well-formed.
Pattern tools
patternHead :: Pattern -> Maybe Name
Get the leftmost symbol in a pattern.
patternNames :: Pattern -> [Name]
Get all the identifiers in a pattern in left-to-right order.
Lenses
mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS