Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 QNameex: x
Lit Literalex: 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] Exprex: \x {y} -> e or \(x:A){y:B} -> e
AbsurdLam !Range Hidingex: \ ()
Fun !Range Expr Exprex: e -> e or {e} -> e
Pi Telescope Exprex: (xs:e) -> e or {xs:e} -> e
Set !Rangeex: Set
Prop !Rangeex: Prop
SetN !Range Natex: Set0, Set1, ..
Rec !Range [(Name, Expr)]ex: record {x = a; y = b}
Let !Range [Declaration] Exprex: let Ds in e
Paren !Range Exprex: (e)
Absurd !Rangeex: () or {}, only in patterns
As !Range Name Exprex: x@p, only in patterns
Dot !Range Exprex: .p, only in patterns
ETel Telescopeonly used for printing telescopes
module Agda.Syntax.Concrete.Name
appView :: Expr -> AppViewSource
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'}
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'}
data TypedBinding Source
A typed binding.
Constructors
TBind !Range [BoundName] Expr
TNoBind Expr
data BoundName Source
Constructors
BName
boundName :: Name
bnameFixity :: Fixity
mkBoundName_ :: Name -> BoundNameSource
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
type TypeSignature = DeclarationSource
Just type signatures.
type Constructor = TypeSignatureSource
A constructor or field declaration is just a type signature.
type Field = TypeSignatureSource
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 :: BoolOnly for open. Exports the opened names from the current module.
data UsingOrHiding Source
Constructors
Hiding [ImportedName]
Using [ImportedName]
data ImportedName Source
An imported name can be a module or a defined name
Constructors
ImportedModule
importedName :: Name
ImportedName
importedName :: Name
data Renaming Source
Constructors
Renaming
renFrom :: ImportedNameRename from this name.
renTo :: NameTo this one.
renToRange :: RangeThe range of the "to" keyword. Retained for highlighting purposes.
data AsName Source
Constructors
AsName
asName :: NameThe "as" name.
asRange :: RangeThe range of the "as" keyword. Retained for highlighting purposes.
defaultImportDir :: ImportDirectiveSource
data OpenShortHand Source
Constructors
DoOpen
DontOpen
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
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
data RHS Source
Constructors
AbsurdRHS
RHS Expr
data WhereClause Source
Constructors
NoWhere
AnyWhere [Declaration]
SomeWhere Name [Declaration]
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 StringInvariant: The string must be a valid Haskell module name.
ImpossiblePragma !Range
type Module = ([Pragma], [Declaration])Source
Modules: Top-level pragmas plus other top-level declarations.
topLevelModuleName :: Module -> TopLevelModuleNameSource

Computes the top-level module name.

Precondition: The Module has to be well-formed.

Produced by Haddock version 2.6.0