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

Agda.Syntax.Concrete.Definitions

Synopsis

- data NiceDeclaration
  - = Axiom Range Fixity' Access IsAbstract Relevance Name Expr
  - | NiceField Range Fixity' Access IsAbstract Name (Arg 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 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]
  - | Codata Range
  - | DeclarationPanic String
- type Nice = Either DeclarationException
- runNice :: Nice a -> Either DeclarationException a
- niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]
- notSoNiceDeclarations :: [NiceDeclaration] -> [Declaration]

# Documentation

data NiceDeclaration

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 Relevance Name Expr | Axioms and functions can be declared irrelevant.
NiceField Range Fixity' Access IsAbstract Name (Arg 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

A definition without its type signature.

Constructors

FunDef Range [Declaration] Fixity' Access IsAbstract Name [Clause] |
DataDef Range 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

Only `Axiom`s.

type NiceTypeSignature = NiceDeclaration

Only `Axiom`s.

data Clause

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

The exception type.

Constructors

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

Instances

Show DeclarationException |
Typeable DeclarationException |
Error DeclarationException |
HasRange DeclarationException |

type Nice = Either DeclarationException

runNice :: Nice a -> Either DeclarationException a

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

notSoNiceDeclarations :: [NiceDeclaration] -> [Declaration]