Agda.Syntax.Concrete.Definitions

Preprocess Declarations, producing NiceDeclarations.

• Attach fixity and syntax declarations to the definition they refer to.
• Distribute the following attributes to the individual definitions: abstract, instance, postulate, primitive, private, termination pragmas.
• Gather the function clauses belonging to one function definition.
• Expand ellipsis ... in function clauses following with.
• Infer mutual blocks. A block starts when a lone signature is encountered, and ends when all lone signatures have seen their definition.
• Report basic well-formedness error, when one of the above transformation fails.

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, abstract and instance modifiers have been distributed to the individual declarations.

Constructors

Axiom Range Fixity' Access IsInstance ArgInfo Name Expr

Axioms and functions can be declared irrelevant. (Hiding should be NotHidden)

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

An uncategorized function clause, could be a function clause without type signature or a pattern lhs (e.g. for irrefutable let). The Declaration is the actual FunClause.

FunSig Range Fixity' Access IsInstance ArgInfo TerminationCheck Name Expr

FunDef Range [Declaration] Fixity' IsAbstract TerminationCheck Name [Clause]

Block of function clauses (we have seen the type signature before). The Declarations are the original declarations that were processed into this FunDef and are only used in notSoNiceDeclaration.

DataDef Range Fixity' IsAbstract Name [LamBinding] [NiceConstructor]

RecDef Range Fixity' IsAbstract Name (Maybe (Ranged Induction)) (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration]

NicePatternSyn Range Fixity' Name [Arg Name] Pattern

NiceUnquoteDecl Range Fixity' Access IsInstance IsAbstract TerminationCheck Name Expr

Instances

Show NiceDeclaration

HasRange NiceDeclaration

ToAbstract NiceDeclaration Declaration

type NiceConstructor = NiceTypeSignature

Only Axioms.

type NiceTypeSignature = NiceDeclaration

Only Axioms.

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

ToAbstract Clause Clause

data DeclarationException

The exception type.

Constructors

MultipleFixityDecls [(Name, [Fixity'])]

InvalidName Name

DuplicateDefinition Name

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

UselessInstance Range

WrongContentPostulateBlock Range

AmbiguousFunClauses LHS [Name]

in a mutual block, a clause could belong to any of the [Name] type signatures

InvalidTerminationCheckPragma Range

InvalidMeasureMutual Range

In a mutual block, all or none need a MEASURE pragma. Range is of mutual block.

PragmaNoTerminationCheck Range

Pragma {--} has been replaced by {--} and {--}.

Instances

Error DeclarationException

Pretty DeclarationException

HasRange DeclarationException

type Nice = StateT NiceEnv (Either DeclarationException)

Nicifier monad.

runNice :: Nice a -> Either DeclarationException a

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

Main.

notSoNiceDeclaration :: NiceDeclaration -> Declaration

(Approximately) convert a NiceDeclaration back to a Declaration.

type Measure = Name

Termination measure is, for now, a variable name.