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. When possible, errors should be deferred to the scope checking phase (ConcreteToAbstract), where we are in the TCM and can produce more informative error messages.

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.

Observe the order of components:

Range Fixity' Access IsAbstract IsInstance TerminationCheck PositivityCheck

further attributes

(Q)Name

content (Expr, Declaration ...)

Constructors

Axiom Range Access IsAbstract IsInstance ArgInfo Name Expr

IsAbstract argument: We record whether a declaration was made in an abstract block.

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

NiceField Range Access IsAbstract IsInstance TacticAttribute Name (Arg Expr)

PrimitiveFunction Range Access IsAbstract Name Expr

NiceMutual Range TerminationCheck CoverageCheck PositivityCheck [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 Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr

NiceDataSig Range Access IsAbstract PositivityCheck UniverseCheck Name [LamBinding] Expr

NiceFunClause Range Access IsAbstract TerminationCheck CoverageCheck Catchall 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 Access IsAbstract IsInstance IsMacro ArgInfo TerminationCheck CoverageCheck Name Expr

FunDef Range [Declaration] IsAbstract IsInstance TerminationCheck CoverageCheck 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. Andreas, 2017-01-01: Because of issue #2372, we add IsInstance here. An alias should know that it is an instance.

NiceDataDef Range Origin IsAbstract PositivityCheck UniverseCheck Name [LamBinding] [NiceConstructor]

NiceRecDef Range Origin IsAbstract PositivityCheck UniverseCheck Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] [Declaration]

NicePatternSyn Range Access Name [Arg Name] Pattern

NiceGeneralize Range Access ArgInfo TacticAttribute Name Expr

NiceUnquoteDecl Range Access IsAbstract IsInstance TerminationCheck CoverageCheck [Name] Expr

NiceUnquoteDef Range Access IsAbstract TerminationCheck CoverageCheck [Name] Expr

Instances

Data NiceDeclaration

Defined in Agda.Syntax.Concrete.Definitions

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NiceDeclaration -> c NiceDeclaration

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NiceDeclaration

toConstr :: NiceDeclaration -> Constr

dataTypeOf :: NiceDeclaration -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NiceDeclaration)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NiceDeclaration)

gmapT :: (forall b. Data b => b -> b) -> NiceDeclaration -> NiceDeclaration

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NiceDeclaration -> r

gmapQ :: (forall d. Data d => d -> u) -> NiceDeclaration -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NiceDeclaration -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NiceDeclaration -> m NiceDeclaration

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NiceDeclaration -> m NiceDeclaration

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NiceDeclaration -> m NiceDeclaration

Show NiceDeclaration

Defined in Agda.Syntax.Concrete.Definitions

Methods

showsPrec :: Int -> NiceDeclaration -> ShowS

show :: NiceDeclaration -> String

showList :: [NiceDeclaration] -> ShowS

Pretty NiceDeclaration

Defined in Agda.Syntax.Concrete.Definitions

Methods

pretty :: NiceDeclaration -> Doc

prettyPrec :: Int -> NiceDeclaration -> Doc

prettyList :: [NiceDeclaration] -> Doc

HasRange NiceDeclaration

Defined in Agda.Syntax.Concrete.Definitions

Methods

getRange :: NiceDeclaration -> Range

ToAbstract NiceDeclaration Declaration

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: NiceDeclaration -> ScopeM 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 Catchall LHS RHS WhereClause [Clause]

Instances

Data Clause

Defined in Agda.Syntax.Concrete.Definitions

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause -> c Clause

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Clause

toConstr :: Clause -> Constr

dataTypeOf :: Clause -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Clause)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause)

gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r

gmapQ :: (forall d. Data d => d -> u) -> Clause -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause -> m Clause

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause

Show Clause

Defined in Agda.Syntax.Concrete.Definitions

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

ToAbstract Clause Clause

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

toAbstract :: Clause -> ScopeM Clause0

data DeclarationException

The exception type.

Constructors

MultipleEllipses Pattern

InvalidName Name

DuplicateDefinition Name

MissingWithClauses Name LHS

WrongDefinition Name DataRecOrFun DataRecOrFun

DeclarationPanic String

WrongContentBlock KindOfBlock Range

AmbiguousFunClauses LHS [Name]

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

InvalidMeasureMutual Range

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

UnquoteDefRequiresSignature [Name]

BadMacroDef NiceDeclaration

Instances

Data DeclarationException

Defined in Agda.Syntax.Concrete.Definitions

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DeclarationException -> c DeclarationException

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DeclarationException

toConstr :: DeclarationException -> Constr

dataTypeOf :: DeclarationException -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DeclarationException)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DeclarationException)

gmapT :: (forall b. Data b => b -> b) -> DeclarationException -> DeclarationException

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DeclarationException -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DeclarationException -> r

gmapQ :: (forall d. Data d => d -> u) -> DeclarationException -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DeclarationException -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DeclarationException -> m DeclarationException

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclarationException -> m DeclarationException

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclarationException -> m DeclarationException

Show DeclarationException

Defined in Agda.Syntax.Concrete.Definitions

Methods

showsPrec :: Int -> DeclarationException -> ShowS

show :: DeclarationException -> String

showList :: [DeclarationException] -> ShowS

Pretty DeclarationException

Defined in Agda.Syntax.Concrete.Definitions

Methods

pretty :: DeclarationException -> Doc

prettyPrec :: Int -> DeclarationException -> Doc

prettyList :: [DeclarationException] -> Doc

HasRange DeclarationException

Defined in Agda.Syntax.Concrete.Definitions

Methods

getRange :: DeclarationException -> Range

MonadError DeclarationException Nice

Defined in Agda.Syntax.Concrete.Definitions

Methods

throwError :: DeclarationException -> Nice a

catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a

data DeclarationWarning

Non-fatal errors encountered in the Nicifier.

Constructors

EmptyAbstract Range

Empty abstract block.

EmptyField Range

Empty field block.

EmptyGeneralize Range

Empty variable block.

EmptyInstance Range

Empty instance block

EmptyMacro Range

Empty macro block.

EmptyMutual Range

Empty mutual block.

EmptyPostulate Range

Empty postulate block.

EmptyPrivate Range

Empty private block.

EmptyPrimitive Range

Empty primitive block.

InvalidCatchallPragma Range

A {-# CATCHALL #-} pragma that does not precede a function clause.

InvalidCoverageCheckPragma Range

A {-# NON_COVERING #-} pragma that does not apply to any function.

InvalidNoPositivityCheckPragma Range

A {-# NO_POSITIVITY_CHECK #-} pragma that does not apply to any data or record type.

InvalidNoUniverseCheckPragma Range

A {-# NO_UNIVERSE_CHECK #-} pragma that does not apply to a data or record type.

InvalidTerminationCheckPragma Range

A {-# TERMINATING #-} and {-# NON_TERMINATING #-} pragma that does not apply to any function.

MissingDefinitions [(Name, Range)]

Declarations (e.g. type signatures) without a definition.

NotAllowedInMutual Range String

OpenPublicPrivate Range

private has no effect on open public. (But the user might think so.)

OpenPublicAbstract Range

abstract has no effect on open public. (But the user might think so.)

PolarityPragmasButNotPostulates [Name]

PragmaNoTerminationCheck Range

Pragma {-# NO_TERMINATION_CHECK #-} has been replaced by {-# TERMINATING #-} and {-# NON_TERMINATING #-}.

PragmaCompiled Range

COMPILE pragmas are not allowed in safe mode

ShadowingInTelescope [(Name, [Range])]

UnknownFixityInMixfixDecl [Name]

UnknownNamesInFixityDecl [Name]

UnknownNamesInPolarityPragmas [Name]

UselessAbstract Range

abstract block with nothing that can (newly) be made abstract.

UselessInstance Range

instance block with nothing that can (newly) become an instance.

UselessPrivate Range

private block with nothing that can (newly) be made private.

Instances

Data DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DeclarationWarning -> c DeclarationWarning

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DeclarationWarning

toConstr :: DeclarationWarning -> Constr

dataTypeOf :: DeclarationWarning -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DeclarationWarning)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DeclarationWarning)

gmapT :: (forall b. Data b => b -> b) -> DeclarationWarning -> DeclarationWarning

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DeclarationWarning -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DeclarationWarning -> r

gmapQ :: (forall d. Data d => d -> u) -> DeclarationWarning -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DeclarationWarning -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DeclarationWarning -> m DeclarationWarning

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclarationWarning -> m DeclarationWarning

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclarationWarning -> m DeclarationWarning

Show DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions

Methods

showsPrec :: Int -> DeclarationWarning -> ShowS

show :: DeclarationWarning -> String

showList :: [DeclarationWarning] -> ShowS

Pretty DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions

Methods

pretty :: DeclarationWarning -> Doc

prettyPrec :: Int -> DeclarationWarning -> Doc

prettyList :: [DeclarationWarning] -> Doc

HasRange DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions

Methods

getRange :: DeclarationWarning -> Range

EmbPrj DeclarationWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: DeclarationWarning -> S Int32

icod_ :: DeclarationWarning -> S Int32

value :: Int32 -> R DeclarationWarning

unsafeDeclarationWarning :: DeclarationWarning -> Bool

Nicifier warnings turned into errors in --safe mode.

data Nice a

Nicifier monad. Preserve the state when throwing an exception.

Instances

Monad Nice

Defined in Agda.Syntax.Concrete.Definitions

Methods

(>>=) :: Nice a -> (a -> Nice b) -> Nice b

(>>) :: Nice a -> Nice b -> Nice b

return :: a -> Nice a

Functor Nice

Defined in Agda.Syntax.Concrete.Definitions

Methods

fmap :: (a -> b) -> Nice a -> Nice b

(<$) :: a -> Nice b -> Nice a

Applicative Nice

Defined in Agda.Syntax.Concrete.Definitions

Methods

pure :: a -> Nice a

(<*>) :: Nice (a -> b) -> Nice a -> Nice b

liftA2 :: (a -> b -> c) -> Nice a -> Nice b -> Nice c

(*>) :: Nice a -> Nice b -> Nice b

(<*) :: Nice a -> Nice b -> Nice a

MonadError DeclarationException Nice

Defined in Agda.Syntax.Concrete.Definitions

Methods

throwError :: DeclarationException -> Nice a

catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a

runNice :: Nice a -> (Either DeclarationException a, NiceWarnings)

Run a Nicifier computation, return result and warnings (in chronological order).

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

Main. Fixities (or more precisely syntax declarations) are needed when grouping function clauses.

notSoNiceDeclarations :: NiceDeclaration -> [Declaration]

(Approximately) convert a NiceDeclaration back to a list of Declarations.

niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract

Has the NiceDeclaration a field of type IsAbstract?

type Measure = Name

Termination measure is, for now, a variable name.

declarationWarningName :: DeclarationWarning -> WarningName