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

Agda.Syntax.Concrete.Definitions

Synopsis

data NiceDeclaration

= Axiom Range Fixity Access IsAbstract Name Expr
| NiceField Range Fixity Access IsAbstract Hiding Name Expr
| PrimitiveFunction Range Fixity Access IsAbstract Name Expr
| NiceDef Range [Declaration] [NiceTypeSignature] [NiceDefinition]
| NiceModule Range Access IsAbstract QName Telescope [Declaration]
| NiceModuleMacro Range Access IsAbstract Name Telescope Expr OpenShortHand ImportDirective
| NiceOpen Range QName ImportDirective
| NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
| NicePragma Range Pragma

data NiceDefinition

= FunDef Range [Declaration] Fixity Access IsAbstract Name [Clause]
| DataDef Range Induction Fixity Access IsAbstract Name [LamBinding] [NiceConstructor]
| RecDef Range Fixity Access IsAbstract Name (Maybe NiceConstructor) [LamBinding] [NiceDeclaration]

type NiceConstructor = NiceTypeSignature
type NiceTypeSignature = NiceDeclaration
data Clause = Clause Name LHS RHS WhereClause [Clause]

data DeclarationException

= MultipleFixityDecls [(Name, [Fixity])]
| MissingDefinition Name
| MissingWithClauses Name
| MissingTypeSignature LHS
| NotAllowedInMutual NiceDeclaration
| UnknownNamesInFixityDecl [Name]
| DeclarationPanic String

type Nice = Either DeclarationException
runNice :: Nice a -> Either DeclarationException a
niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]
notSoNiceDeclarations :: [NiceDeclaration] -> [Declaration]

Documentation

data NiceDeclaration | Source

The nice declarations. No fixity declarations and function definitions are contained in a single constructor instead of spread out between type signatures and clauses. The `private`, `postulate`, and `abstract` modifiers have been distributed to the individual declarations.
Constructors

Axiom Range Fixity Access IsAbstract Name Expr |
NiceField Range Fixity Access IsAbstract Hiding Name Expr |
PrimitiveFunction Range Fixity Access IsAbstract Name Expr |
NiceDef Range [Declaration] [NiceTypeSignature] [NiceDefinition] | A bunch of mutually recursive functions/datatypes. The last two lists have the same length. The first list is the concrete declarations these definitions came from.
NiceModule Range Access IsAbstract QName Telescope [Declaration] |
NiceModuleMacro Range Access IsAbstract Name Telescope Expr OpenShortHand ImportDirective |
NiceOpen Range QName ImportDirective |
NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective |
NicePragma Range Pragma |

Instances

Data NiceDeclaration
Typeable NiceDeclaration
HasRange NiceDeclaration
Strict NiceDeclaration
ToAbstract NiceDeclaration Declaration

data NiceDefinition | Source

A definition without its type signature.
Constructors

FunDef Range [Declaration] Fixity Access IsAbstract Name [Clause] |
DataDef Range Induction Fixity Access IsAbstract Name [LamBinding] [NiceConstructor] |
RecDef Range Fixity Access IsAbstract Name (Maybe NiceConstructor) [LamBinding] [NiceDeclaration] | The `NiceConstructor` has a dummy type field (the record constructor type has not been computed yet).

Instances

Data NiceDefinition
Typeable NiceDefinition
HasRange NiceDefinition
ToAbstract NiceDefinition Definition

type NiceConstructor = NiceTypeSignature | Source

Only `Axiom`s.

type NiceTypeSignature = NiceDeclaration | Source

Only `Axiom`s.

data Clause | Source

One clause in a function definition. There is no guarantee that the `LHS` actually declares the `Name`. We will have to check that later.
Constructors

Clause Name LHS RHS WhereClause [Clause] |

Instances

Data Clause
Typeable Clause
ToAbstract Clause Clause

data DeclarationException | Source

The exception type.
Constructors

MultipleFixityDecls [(Name, [Fixity])] |
MissingDefinition Name |
MissingWithClauses Name |
MissingTypeSignature LHS |
NotAllowedInMutual NiceDeclaration |
UnknownNamesInFixityDecl [Name] |
DeclarationPanic String |

Instances

Show DeclarationException
Typeable DeclarationException
Error DeclarationException
HasRange DeclarationException

type Nice = Either DeclarationException | Source

runNice :: Nice a -> Either DeclarationException a | Source

niceDeclarations :: [Declaration] -> Nice [NiceDeclaration] | Source

notSoNiceDeclarations :: [NiceDeclaration] -> [Declaration] | Source

Produced by Haddock version 2.4.2