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

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Concrete.Definitions

Description

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.

Synopsis

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

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 IsInstance ArgInfo 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 (Ranged Induction)) (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration] 
NicePatternSyn Range Fixity' Name [Arg Name] Pattern 
NiceUnquoteDecl Range Fixity' Access IsAbstract TerminationCheck Name Expr 

Instances

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] 

Instances

data DeclarationException Source

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

type Nice = StateT NiceEnv (Either DeclarationException) Source

Nicifier monad.

runNice :: Nice a -> Either DeclarationException a Source

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

Main.

notSoNiceDeclaration :: NiceDeclaration -> Declaration Source

(Approximately) convert a NiceDeclaration back to a Declaration.

type Measure = Name Source

Termination measure is, for now, a variable name.