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

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 = NiceTypeSignature Source

Only Axioms.

type NiceTypeSignature = NiceDeclaration Source

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 DeclarationException Source

runNice :: Nice a -> Either DeclarationException a Source

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

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

Produced by Haddock version 2.6.0