| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Syntax.Concrete

Contents

Expressions
Bindings
Declarations

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 Nat)
| RawApp !Range [Expr]
| App !Range Expr (NamedArg Expr)
| OpApp !Range Name [Expr]
| WithApp !Range Expr [Expr]
| HiddenArg !Range (Named String Expr)
| Lam !Range [LamBinding] Expr
| AbsurdLam !Range Hiding
| Fun !Range Expr Expr
| Pi Telescope Expr
| Set !Range
| Prop !Range
| SetN !Range Nat
| Rec !Range [(Name, Expr)]
| Let !Range [Declaration] Expr
| Paren !Range Expr
| Absurd !Range
| As !Range Name Expr
| Dot !Range Expr
| ETel Telescope

module Agda.Syntax.Concrete.Name
appView :: Expr -> AppView
data AppView = AppView Expr [NamedArg Expr]

data LamBinding

= DomainFree Hiding BoundName
| DomainFull TypedBindings

data TypedBindings = TypedBindings !Range Hiding [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 Name Expr
| Field Hiding Name Expr
| FunClause LHS RHS WhereClause
| Data !Range Induction Name [TypedBindings] Expr [Constructor]
| Record !Range Name (Maybe Name) [TypedBindings] Expr [Declaration]
| Infix Fixity [Name]
| 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 [TypedBindings] Expr OpenShortHand ImportDirective
| Module !Range QName [TypedBindings] [Declaration]
| Pragma Pragma

type TypeSignature = Declaration
type Constructor = TypeSignature
type Field = 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

data LHS

= LHS Pattern [Pattern] [RewriteEqn] [WithExpr]
| Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]

data Pattern

= IdentP QName
| AppP Pattern (NamedArg Pattern)
| RawAppP !Range [Pattern]
| OpAppP !Range Name [Pattern]
| HiddenP !Range (Named String Pattern)
| ParenP !Range Pattern
| WildP !Range
| AbsurdP !Range
| AsP !Range Name Pattern
| DotP !Range Expr
| LitP Literal

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
| ImportPragma !Range String
| ImpossiblePragma !Range

type Module = ([Pragma], [Declaration])
topLevelModuleName :: Module -> TopLevelModuleName

Expressions

data Expr | Source

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 Nat) | ex: `_`
RawApp !Range [Expr] | before parsing operators
App !Range Expr (NamedArg Expr) | ex: `e e`, `e {e}`, or `e {x = e}`
OpApp !Range Name [Expr] | ex: `e + e`
WithApp !Range Expr [Expr] | ex: `e | e1 | .. | en`
HiddenArg !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: `\ ()`
Fun !Range Expr Expr | ex: `e -> e` or `{e} -> e`
Pi Telescope Expr | ex: `(xs:e) -> e` or `{xs:e} -> e`
Set !Range | ex: `Set`
Prop !Range | ex: `Prop`
SetN !Range Nat | ex: `Set0, Set1, ..`
Rec !Range [(Name, Expr)] | ex: `record {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

Instances

Eq Expr
Data Expr
Show Expr
Typeable Expr
Pretty Expr
HasRange Expr
IsExpr Expr
Strict Expr
LowerMeta Expr
ToConcrete MetaId Expr
ToConcrete Expr Expr
ToConcrete InteractionId Expr
ToAbstract Expr Expr

module Agda.Syntax.Concrete.Name

appView :: Expr -> AppView | Source

data AppView | Source

The `Expr` is not an application.
Constructors

AppView Expr [NamedArg Expr] |

Bindings

data LamBinding | Source

A lambda binding is either domain free or typed.
Constructors

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

Instances

Eq LamBinding
Data LamBinding
Show LamBinding
Typeable LamBinding
Pretty LamBinding
HasRange LamBinding
LowerMeta LamBinding
ToConcrete LamBinding LamBinding
ToAbstract LamBinding LamBinding

data TypedBindings | Source

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

TypedBindings !Range Hiding [TypedBinding] | . `(xs:e;..;ys:e')` or `{xs:e;..;ys:e'}`

Instances

Eq TypedBindings
Data TypedBindings
Show TypedBindings
Typeable TypedBindings
Pretty TypedBindings
HasRange TypedBindings
LowerMeta TypedBindings
ToConcrete TypedBindings TypedBindings
ToAbstract TypedBindings TypedBindings

data TypedBinding | Source

A typed binding.
Constructors

TBind !Range [BoundName] Expr |
TNoBind Expr |

Instances

Eq TypedBinding
Data TypedBinding
Typeable TypedBinding
Pretty TypedBinding
HasRange TypedBinding
LowerMeta TypedBinding
ToConcrete TypedBinding TypedBinding
ToAbstract TypedBinding TypedBinding

data BoundName | Source

Constructors

BName |

boundName :: Name |
bnameFixity :: Fixity |

Instances

Eq BoundName
Data BoundName
Typeable BoundName
Pretty BoundName
HasRange BoundName

mkBoundName_ :: Name -> BoundName | Source

type Telescope = [TypedBindings] | Source

A telescope is a sequence of typed bindings. Bound variables are in scope in later types. Or it's the mysterious Thierry-function-telescope. Only it's not.
Declarations

data Declaration | Source

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

TypeSig Name Expr |
Field Hiding Name Expr |
FunClause LHS RHS WhereClause |
Data !Range Induction Name [TypedBindings] Expr [Constructor] |
Record !Range Name (Maybe Name) [TypedBindings] Expr [Declaration] | The optional name is a name for the record constructor.
Infix Fixity [Name] |
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 [TypedBindings] Expr OpenShortHand ImportDirective |
Module !Range QName [TypedBindings] [Declaration] |
Pragma Pragma |

Instances

Eq Declaration
Data Declaration
Show Declaration
Typeable Declaration
Pretty Declaration
HasRange Declaration
Strict Declaration
LowerMeta Declaration
ToConcrete (Constr Constructor) Declaration

type TypeSignature = Declaration | Source

Just type signatures.

type Constructor = TypeSignature | Source

A constructor or field declaration is just a type signature.

type Field = TypeSignature | Source

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).
Constructors

ImportDirective |

importDirRange :: !Range |
usingOrHiding :: UsingOrHiding |
renaming :: [Renaming] |
publicOpen :: Bool | Only for `open`. Exports the opened names from the current module.

Instances

Eq ImportDirective
Data ImportDirective
Show ImportDirective
Typeable ImportDirective
Pretty ImportDirective
HasRange ImportDirective

data UsingOrHiding | Source

Constructors

Hiding [ImportedName] |
Using [ImportedName] |

Instances

Eq UsingOrHiding
Data UsingOrHiding
Typeable UsingOrHiding
Pretty UsingOrHiding
HasRange UsingOrHiding

data ImportedName | Source

An imported name can be a module or a defined name
Constructors

ImportedModule |

importedName :: Name |

ImportedName |

importedName :: Name |

Instances

Eq ImportedName
Data ImportedName
Ord ImportedName
Show ImportedName
Typeable ImportedName
Pretty ImportedName
HasRange ImportedName

data Renaming | Source

Constructors

Renaming |

renFrom :: ImportedName | Rename from this name.
renTo :: Name | To this one.
renToRange :: Range | The range of the "to" keyword. Retained for highlighting purposes.

Instances

Eq Renaming
Data Renaming
Typeable Renaming
HasRange Renaming

data AsName | Source

Constructors

AsName |

asName :: Name | The "as" name.
asRange :: Range | The range of the "as" keyword. Retained for highlighting purposes.

Instances

Eq AsName
Data AsName
Typeable AsName
HasRange AsName

defaultImportDir :: ImportDirective | Source

data OpenShortHand | Source

Constructors

DoOpen |
DontOpen |

Instances

Eq OpenShortHand
Data OpenShortHand
Show OpenShortHand
Typeable OpenShortHand
Pretty OpenShortHand

data LHS | 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.

Constructors

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

Instances

Eq LHS
Data LHS
Typeable LHS
Pretty LHS
HasRange LHS
ToConcrete LHS LHS

data Pattern | Source

Concrete patterns. No literals in patterns at the moment.
Constructors

IdentP QName |
AppP Pattern (NamedArg Pattern) |
RawAppP !Range [Pattern] |
OpAppP !Range Name [Pattern] |
HiddenP !Range (Named String Pattern) |
ParenP !Range Pattern |
WildP !Range |
AbsurdP !Range |
AsP !Range Name Pattern |
DotP !Range Expr |
LitP Literal |

Instances

Eq Pattern
Data Pattern
Show Pattern
Typeable Pattern
Pretty Pattern
HasRange Pattern
IsExpr Pattern
ToConcrete Pattern Pattern
ToAbstract Pattern (Pattern' Expr)

data RHS | Source

Constructors

AbsurdRHS |
RHS Expr |

Instances

Eq RHS
Data RHS
Show RHS
Typeable RHS
Pretty RHS
HasRange RHS
LowerMeta RHS
ToAbstract RHS AbstractRHS

data WhereClause | Source

Constructors

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

Instances

Eq WhereClause
Data WhereClause
Typeable WhereClause
Pretty WhereClause
HasRange WhereClause
LowerMeta WhereClause

data Pragma | Source

Constructors

OptionsPragma !Range [String] |
BuiltinPragma !Range String Expr |
CompiledDataPragma !Range QName String [String] |
CompiledTypePragma !Range QName String |
CompiledPragma !Range QName String |
ImportPragma !Range String | Invariant: The string must be a valid Haskell module name.
ImpossiblePragma !Range |

Instances

Eq Pragma
Data Pragma
Show Pragma
Typeable Pragma
Pretty Pragma
HasRange Pragma
Strict Pragma
ToConcrete RangeAndPragma Pragma
ToAbstract Pragma ([] Pragma)

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

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

topLevelModuleName :: Module -> TopLevelModuleName | Source

Computes the top-level module name. Precondition: The `Module` has to be well-formed.
Produced by Haddock version 2.4.2