Agda.Syntax.Concrete.Definitions

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

FunSig Range Fixity' Access Relevance Name Expr

FunDef Range [Declaration] Fixity' IsAbstract 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 (ThingWithFixity Name)) [LamBinding] [NiceDeclaration]

Instances

Data NiceDeclaration

Show NiceDeclaration

Typeable NiceDeclaration

HasRange NiceDeclaration

Strict 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

Data Clause

Show Clause

Typeable Clause

ToAbstract Clause Clause

data DeclarationException

The exception type.

Constructors

MultipleFixityDecls [(Name, [Fixity'])]

MissingDefinition Name

MissingWithClauses Name

MissingTypeSignature LHS

MissingDataSignature 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

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]

notSoNiceDeclarations :: [NiceDeclaration] -> [Declaration]