Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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
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).
type NiceConstructor = NiceTypeSignatureSource
Only Axioms.
type NiceTypeSignature = NiceDeclarationSource
Only Axioms.
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]
data DeclarationException Source
The exception type.
Constructors
MultipleFixityDecls [(Name, [Fixity])]
MissingDefinition Name
MissingWithClauses Name
MissingTypeSignature LHS
NotAllowedInMutual NiceDeclaration
UnknownNamesInFixityDecl [Name]
DeclarationPanic String
type Nice = Either DeclarationExceptionSource
runNice :: Nice a -> Either DeclarationException aSource
niceDeclarations :: [Declaration] -> Nice [NiceDeclaration]Source
notSoNiceDeclarations :: [NiceDeclaration] -> [Declaration]Source
Produced by Haddock version 2.6.0