Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Syntax.Concrete

Contents

- Expressions
- Bindings
- Declarations
- Pattern tools

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.

Synopsis

- 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
  - = DomainFree Hiding Relevance BoundName
  - | DomainFull TypedBindings
- data TypedBindings = TypedBindings !Range (Arg TypedBinding)
- data TypedBinding
  - = TBind !Range [BoundName] Expr
  - | TNoBind Expr
- 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
  - = SectionApp Range [TypedBindings] Expr
  - | RecordModuleIFS Range QName
- 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
    }
- data Renaming = Renaming {
  - renFrom :: ImportedName
  - renTo :: Name
  - renToRange :: Range
  }
- data AsName = AsName {
  - asName :: Name
  - asRange :: Range
  }
- defaultImportDir :: ImportDirective
- data OpenShortHand
  - = DoOpen
  - | DontOpen
- type RewriteEqn = Expr
- type WithExpr = Expr
- data LHS
  - = LHS {
    - lhsOriginalPattern :: Pattern
    - lhsWithPattern :: [Pattern]
    - lhsRewriteEqn :: [RewriteEqn]
    - lhsWithExpr :: [WithExpr]
    }
  - | Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]
- 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
  - = LHSHead {
    - lhsDefName :: Name
    - lhsPats :: [NamedArg Pattern]
    }
  - | LHSProj {
    - lhsDestructor :: QName
    - lhsPatsLeft :: [NamedArg Pattern]
    - lhsFocus :: NamedArg LHSCore
    - lhsPatsRight :: [NamedArg Pattern]
    }
- data RHS
  - = AbsurdRHS
  - | RHS Expr
- 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

data Expr

Concrete expressions. Should represent exactly what the user wrote.

Constructors

Ident QName | ex: `x`
Lit Literal | ex: `1` or `"foo"`
QuestionMark !Range (Maybe Nat) | ex: `?` or `{! ... !}`
Underscore !Range (Maybe String) | ex: `_` or `_A_5`
RawApp !Range [Expr] | before parsing operators
App !Range Expr (NamedArg Expr) | ex: `e e`, `e {e}`, or `e {x = e}`
OpApp !Range QName [OpApp Expr] | ex: `e + e`
WithApp !Range Expr [Expr] | ex: `e | e1 | .. | en`
HiddenArg !Range (Named String Expr) | ex: `{e}` or `{x=e}`
InstanceArg !Range (Named String Expr) | ex: `{{e}}` or `{{x=e}}`
Lam !Range [LamBinding] Expr | ex: `\x {y} -> e` or `\(x:A){y:B} -> e`
AbsurdLam !Range Hiding | ex: `\ ()`
ExtendedLam !Range [(LHS, RHS, WhereClause)] | ex: `\ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }`
Fun !Range Expr Expr | ex: `e -> e` or `.e -> e` (NYI: `{e} -> e`)
Pi Telescope Expr | ex: `(xs:e) -> e` or `{xs:e} -> e`
Set !Range | ex: `Set`
Prop !Range | ex: `Prop`
SetN !Range Integer | ex: `Set0, Set1, ..`
Rec !Range [(Name, Expr)] | ex: `record {x = a; y = b}`
RecUpdate !Range Expr [(Name, Expr)] | ex: `record e {x = a; y = b}`
Let !Range [Declaration] Expr | ex: `let Ds in e`
Paren !Range Expr | ex: `(e)`
Absurd !Range | ex: `()` or `{}`, only in patterns
As !Range Name Expr | ex: `x@p`, only in patterns
Dot !Range Expr | ex: `.p`, only in patterns
ETel Telescope | only used for printing telescopes
QuoteGoal !Range Name Expr | ex: `quoteGoal x in e`
Quote !Range | ex: `quote`, should be applied to a name
QuoteTerm !Range | ex: `quoteTerm`, should be applied to a term
Unquote !Range | ex: `unquote`, should be applied to a term of type `Term`
DontCare Expr | to print irrelevant things

Instances

Show Expr |
Typeable Expr |
Pretty Expr |
KillRange Expr |
HasRange Expr |
IsExpr Expr |
LowerMeta Expr |
ToConcrete Expr Expr |
ToConcrete InteractionId Expr |
ToConcrete NamedMeta Expr |
ToAbstract Expr Expr |
ToAbstract LHSCore (LHSCore' Expr) |
ToAbstract Pattern (Pattern' Expr) |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |
Pretty (OpApp Expr) |
LowerMeta (Maybe Expr) |
LowerMeta (OpApp Expr) |
ToAbstract (Pattern' Expr) (Pattern' Expr) |
ToAbstract (LHSCore' Expr) (LHSCore' Expr) |

data OpApp e

Constructors

SyntaxBindingLambda !Range [LamBinding] e | an abstraction inside a special syntax declaration (see Issue 358 why we introduce this).
Ordinary e |

Instances

Functor OpApp |
Typeable1 OpApp |
Pretty (OpApp Expr) |
KillRange e => KillRange (OpApp e) |
HasRange e => HasRange (OpApp e) |
LowerMeta (OpApp Expr) |

fromOrdinary :: e -> OpApp e -> e

module Agda.Syntax.Concrete.Name

appView :: Expr -> AppView

data AppView

The `Expr` is not an application.

Constructors

AppView Expr [NamedArg Expr] |

# Bindings

data LamBinding

A lambda binding is either domain free or typed.

Constructors

DomainFree Hiding Relevance BoundName | . `x` or `{x}` or `.x` or `.{x}` or `{.x}`
DomainFull TypedBindings | . `(xs : e)` or `{xs : e}`

Instances

Show LamBinding |
Typeable LamBinding |
Pretty LamBinding |
KillRange LamBinding |
HasRange LamBinding |
LowerMeta LamBinding |
ToConcrete LamBinding LamBinding |
ToAbstract LamBinding LamBinding |

data TypedBindings

A sequence of typed bindings with hiding information. Appears in dependent function spaces, typed lambdas, and telescopes.

Constructors

TypedBindings !Range (Arg TypedBinding) | . `(xs : e)` or `{xs : e}`

Instances

Show TypedBindings |
Typeable TypedBindings |
Pretty TypedBindings |
KillRange TypedBindings |
HasRange TypedBindings |
LowerMeta TypedBindings |
ToConcrete TypedBindings TypedBindings |
ToAbstract TypedBindings TypedBindings |

data TypedBinding

A typed binding.

Constructors

TBind !Range [BoundName] Expr |
TNoBind Expr |

Instances

Typeable TypedBinding |
Pretty TypedBinding |
KillRange TypedBinding |
HasRange TypedBinding |
LowerMeta TypedBinding |
ToConcrete TypedBinding TypedBinding |
ToAbstract TypedBinding TypedBinding |

data BoundName

Constructors

BName |

Fields

boundName :: Name
bnameFixity :: Fixity'

Instances

Typeable BoundName |
Pretty BoundName |
KillRange BoundName |
HasRange BoundName |
ToAbstract (NewName BoundName) Name |

mkBoundName_ :: Name -> BoundName

type Telescope = [TypedBindings]

A telescope is a sequence of typed bindings. Bound variables are in scope in later types.

# Declarations

data Declaration

The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.

Constructors

TypeSig Relevance Name Expr | Axioms and functions can be irrelevant.
Field Name (Arg Expr) | Record field, can be hidden and/or irrelevant.
FunClause LHS RHS WhereClause |
DataSig !Range Induction Name [LamBinding] Expr | lone data signature in mutual block
Data !Range Induction Name [LamBinding] (Maybe Expr) [Constructor] |
RecordSig !Range Name [LamBinding] Expr | lone record signature in mutual block
Record !Range Name (Maybe Induction) (Maybe Name) [LamBinding] (Maybe Expr) [Declaration] | The optional name is a name for the record constructor.
Infix Fixity [Name] |
Syntax Name Notation | notation declaration for a name
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 |

Instances

Show Declaration |
Typeable Declaration |
Pretty Declaration |
KillRange Declaration |
HasRange Declaration |
LowerMeta Declaration |
ToConcrete Clause [Declaration] |
ToConcrete LetBinding [Declaration] |
ToConcrete Declaration [Declaration] |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |
Pretty [Declaration] |
ToConcrete (Constr Constructor) Declaration |
ToAbstract (TopLevel [Declaration]) TopLevelInfo |
ToAbstract [Declaration] [Declaration] |

data ModuleApplication

Constructors

SectionApp Range [TypedBindings] Expr |
RecordModuleIFS Range QName |

Instances

Show ModuleApplication |
Typeable ModuleApplication |
Pretty ModuleApplication |
KillRange ModuleApplication |
HasRange ModuleApplication |
LowerMeta ModuleApplication |
ToConcrete ModuleApplication ModuleApplication |

type TypeSignature = Declaration

Just type signatures.

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

importDirRange :: !Range
usingOrHiding :: UsingOrHiding
renaming :: [Renaming]
publicOpen :: Bool

  Only for `open`. Exports the opened names from the current module.

Instances

Show ImportDirective |
Typeable ImportDirective |
Pretty ImportDirective |
KillRange ImportDirective |
HasRange ImportDirective |

data UsingOrHiding

Constructors

Hiding [ImportedName] |
Using [ImportedName] |

Instances

Typeable UsingOrHiding |
Pretty UsingOrHiding |
KillRange UsingOrHiding |
HasRange UsingOrHiding |

data ImportedName

An imported name can be a module or a defined name

Constructors

ImportedModule |

Fields

importedName :: Name

ImportedName |

Fields

importedName :: Name

Instances

Eq ImportedName |
Ord ImportedName |
Show ImportedName |
Typeable ImportedName |
Pretty ImportedName |
KillRange ImportedName |
HasRange ImportedName |

data Renaming

Constructors

Renaming |

Fields

renFrom :: ImportedName

  Rename from this name.

renTo :: Name

  To this one.

renToRange :: Range

  The range of the "to" keyword. Retained for highlighting purposes.

Instances

Typeable Renaming |
KillRange Renaming |
HasRange Renaming |

data AsName

Constructors

AsName |

Fields

asName :: Name

  The "as" name.

asRange :: Range

  The range of the "as" keyword. Retained for highlighting purposes.

Instances

Show AsName |
Typeable AsName |
KillRange AsName |
HasRange AsName |

defaultImportDir :: ImportDirective

Default is directive is `private` (use everything, but do not export).

data OpenShortHand

Constructors

DoOpen |
DontOpen |

Instances

Show OpenShortHand |
Typeable OpenShortHand |
Pretty OpenShortHand |

type RewriteEqn = Expr

type WithExpr = 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

lhsOriginalPattern :: Pattern

      f ps

lhsWithPattern :: [Pattern]

  `| p` (many)

lhsRewriteEqn :: [RewriteEqn]

  `rewrite e` (many)

lhsWithExpr :: [WithExpr]

  `with e` (many)

Ellipsis Range [Pattern] [RewriteEqn] [WithExpr] | new with-patterns, rewrite equations and with-expressions

Instances

Show LHS |
Typeable LHS |
Pretty LHS |
KillRange LHS |
HasRange LHS |
ToConcrete LHS LHS |

data Pattern

Concrete patterns. No literals in patterns at the moment.

Constructors

IdentP QName | `c` or `x`
AppP Pattern (NamedArg Pattern) | `p p'` or `p {x = p'}`
RawAppP !Range [Pattern] | `p1..pn` before parsing operators
OpAppP !Range QName [Pattern] | eg: `p => p'` for operator `_=>_`
HiddenP !Range (Named String Pattern) | `{p}` or `{x = p}`
InstanceP !Range (Named String Pattern) | `{{p}}` or `{{x = p}}`

ParenP !Range Pattern

    (p)

WildP !Range

    _

AbsurdP !Range

    ()

AsP !Range Name Pattern | `x@p` unused

DotP !Range Expr

    .e

LitP Literal | `0`, `1`, etc.

Instances

Show Pattern |
Typeable Pattern |
Pretty Pattern |
KillRange Pattern |
HasRange Pattern |
IsExpr Pattern |
ToConcrete Pattern Pattern |
ToConcrete LHSCore Pattern |
ToAbstract Pattern (Pattern' Expr) |
Pretty [Pattern] |

data LHSCore

Processed (scope-checked) intermediate form of the core `f ps` of `LHS`. Corresponds to `lhsOriginalPattern`.

Constructors

LHSHead |

Fields

lhsDefName :: Name

      f

lhsPats :: [NamedArg Pattern]

      ps

LHSProj |

Fields

lhsDestructor :: QName

  record projection identifier

lhsPatsLeft :: [NamedArg Pattern]

  side patterns

lhsFocus :: NamedArg LHSCore

  main branch

lhsPatsRight :: [NamedArg Pattern]

  side patterns

Instances

Show LHSCore |
Typeable LHSCore |
Pretty LHSCore |
HasRange LHSCore |
ToAbstract LHSCore (LHSCore' Expr) |

data RHS

Constructors

AbsurdRHS |
RHS Expr |

Instances

Show RHS |
Typeable RHS |
Pretty RHS |
KillRange RHS |
HasRange RHS |
LowerMeta RHS |
ToAbstract RHS AbstractRHS |
ToConcrete RHS (RHS, [Expr], [Expr], [Declaration]) |

data WhereClause

Constructors

NoWhere |
AnyWhere [Declaration] |
SomeWhere Name [Declaration] |

Instances

Show WhereClause |
Typeable WhereClause |
Pretty WhereClause |
KillRange WhereClause |
HasRange WhereClause |
LowerMeta WhereClause |
ToConcrete AsWhereDecls WhereClause |

data Pragma

Constructors

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 |

Instances

Show Pragma |
Typeable Pragma |
Pretty Pragma |
KillRange Pragma |
HasRange Pragma |
ToConcrete RangeAndPragma Pragma |
ToAbstract Pragma [Pragma] |

type Module = ([Pragma], [Declaration])

Modules: Top-level pragmas plus other top-level declarations.

data ThingWithFixity x

Constructors

ThingWithFixity x Fixity' |

Instances

Functor ThingWithFixity |
Typeable1 ThingWithFixity |
Foldable ThingWithFixity |
Traversable ThingWithFixity |
Show x => Show (ThingWithFixity x) |
Pretty (ThingWithFixity Name) |
KillRange x => KillRange (ThingWithFixity x) |

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.