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 Fixity' Access IsAbstract IsInstance ArgInfo (Maybe [Occurrence]) 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.)

Maybe [Occurrence] argument: Polarities can be assigned to identifiers.

NiceField Range Fixity' Access IsAbstract IsInstance Name (Arg Expr)

PrimitiveFunction Range Fixity' Access IsAbstract Name Expr

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

NiceDataSig Range Fixity' Access IsAbstract PositivityCheck Name [LamBinding] Expr

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

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

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

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

NicePatternSyn Range Fixity' Name [Arg Name] Pattern

NiceUnquoteDecl Range [Fixity'] Access IsAbstract IsInstance TerminationCheck [Name] Expr

NiceUnquoteDef Range [Fixity'] Access IsAbstract TerminationCheck [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 :: (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

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

MultipleFixityDecls [(Name, [Fixity'])]

MultiplePolarityPragmas [Name]

MultipleEllipses Pattern

InvalidName Name

DuplicateDefinition Name

MissingDefinition Name

MissingWithClauses Name

WrongDefinition Name DataRecOrFun DataRecOrFun

WrongParameters Name Params Params

Name of symbol, Params of signature, Params of definition.

NotAllowedInMutual NiceDeclaration

Codata Range

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.

PragmaNoTerminationCheck Range

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

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

UnknownNamesInFixityDecl [Name]

UnknownFixityInMixfixDecl [Name]

UnknownNamesInPolarityPragmas [Name]

PolarityPragmasButNotPostulates [Name]

UselessPrivate Range

UselessAbstract Range

UselessInstance Range

EmptyMutual Range

Empty mutual block.

EmptyAbstract Range

Empty abstract block.

EmptyPrivate Range

Empty private block.

EmptyInstance Range

Empty instance block

EmptyMacro Range

Empty macro block.

EmptyPostulate Range

Empty postulate block.

InvalidTerminationCheckPragma Range

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

InvalidNoPositivityCheckPragma Range

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

InvalidCatchallPragma Range

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

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

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

fail :: String -> 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 :: [Declaration] -> Nice [NiceDeclaration]

Main.

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