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

Safe Haskell | None

Agda.Syntax.Concrete.Definitions

Synopsis

- data NiceDeclaration
  - = Axiom Range Fixity' Access Relevance Name Expr
  - | NiceField Range Fixity' Access IsAbstract Name (Arg Expr)
  - | PrimitiveFunction Range Fixity' Access IsAbstract Name Expr
  - | NiceMutual Range TerminationCheck [NiceDeclaration]
  - | NiceModule Range Access IsAbstract QName Telescope [Declaration]
  - | NiceModuleMacro Range Access IsAbstract Name ModuleApplication OpenShortHand ImportDirective
  - | NiceOpen Range QName ImportDirective
  - | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
  - | NicePragma Range Pragma
  - | NiceRecSig Range Fixity' Access Name [LamBinding] Expr
  - | NiceDataSig Range Fixity' Access Name [LamBinding] Expr
  - | NiceFunClause Range Access IsAbstract TerminationCheck Declaration
  - | FunSig Range Fixity' Access Relevance TerminationCheck Name Expr
  - | FunDef Range [Declaration] Fixity' IsAbstract TerminationCheck Name [Clause]
  - | DataDef Range Fixity' IsAbstract Name [LamBinding] [NiceConstructor]
  - | RecDef Range Fixity' IsAbstract Name (Maybe Induction) (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration]
  - | NicePatternSyn Range Fixity' Name [Name] Pattern
- 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
  - | MissingDataSignature Name
  - | WrongDefinition Name DataRecOrFun DataRecOrFun
  - | WrongParameters Name
  - | NotAllowedInMutual NiceDeclaration
  - | UnknownNamesInFixityDecl [Name]
  - | Codata Range
  - | DeclarationPanic String
  - | UselessPrivate Range
  - | UselessAbstract Range
  - | AmbiguousFunClauses LHS [Name]
  - | InvalidNoTerminationCheckPragma Range
- type Nice = StateT NiceEnv (Either DeclarationException)
- runNice :: Nice a -> Either DeclarationException a
- niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]
- notSoNiceDeclaration :: 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 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 |
NiceMutual Range TerminationCheck [NiceDeclaration] |
NiceModule Range Access IsAbstract QName Telescope [Declaration] |
NiceModuleMacro Range Access IsAbstract Name ModuleApplication OpenShortHand ImportDirective |
NiceOpen Range QName ImportDirective |
NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective |
NicePragma Range Pragma |
NiceRecSig Range Fixity' Access Name [LamBinding] Expr |
NiceDataSig Range Fixity' Access Name [LamBinding] Expr |
NiceFunClause Range Access IsAbstract TerminationCheck Declaration | a uncategorized function clause, could be a function clause without type signature or a pattern lhs (e.g. for irrefutable let)x
FunSig Range Fixity' Access Relevance TerminationCheck Name Expr |
FunDef Range [Declaration] Fixity' IsAbstract TerminationCheck Name [Clause] | block of function clauses (we have seen the type signature before)
DataDef Range Fixity' IsAbstract Name [LamBinding] [NiceConstructor] |
RecDef Range Fixity' IsAbstract Name (Maybe Induction) (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration] |
NicePatternSyn Range Fixity' Name [Name] Pattern |

Instances

Show NiceDeclaration |
Typeable NiceDeclaration |
HasRange NiceDeclaration |
ToAbstract NiceDeclaration Declaration |

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

Show Clause |
Typeable Clause |
ToAbstract Clause Clause |

data DeclarationException

The exception type.

Constructors

MultipleFixityDecls [(Name, [Fixity'])] |
MissingDefinition Name |
MissingWithClauses Name |
MissingTypeSignature LHS |
MissingDataSignature Name |
WrongDefinition Name DataRecOrFun DataRecOrFun |
WrongParameters Name |
NotAllowedInMutual NiceDeclaration |
UnknownNamesInFixityDecl [Name] |
Codata Range |
DeclarationPanic String |
UselessPrivate Range |
UselessAbstract Range |
AmbiguousFunClauses LHS [Name] | in a mutual block, a clause could belong to any of the `[Name]` type signatures
InvalidNoTerminationCheckPragma Range |

Instances

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

type Nice = StateT NiceEnv (Either DeclarationException)

runNice :: Nice a -> Either DeclarationException a

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

notSoNiceDeclaration :: NiceDeclaration -> Declaration