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.

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 Bool) (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

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

Methods

showsPrec :: Int -> NiceDeclaration -> ShowS

show :: NiceDeclaration -> String

showList :: [NiceDeclaration] -> ShowS

HasRange NiceDeclaration

Methods

getRange :: NiceDeclaration -> Range

ToAbstract NiceDeclaration Declaration

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

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

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

ToAbstract Clause Clause

Methods

toAbstract :: Clause -> ScopeM Clause

data DeclarationException

The exception type.

Constructors

MultipleFixityDecls [(Name, [Fixity'])]

MultiplePolarityPragmas [Name]

InvalidName Name

DuplicateDefinition Name

MissingDefinition Name

MissingWithClauses Name

MissingTypeSignature LHS

MissingDataSignature 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

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 {--}.

InvalidCatchallPragma Range

UnquoteDefRequiresSignature [Name]

BadMacroDef NiceDeclaration

InvalidNoPositivityCheckPragma Range

Instances

Data DeclarationException

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

Methods

showsPrec :: Int -> DeclarationException -> ShowS

show :: DeclarationException -> String

showList :: [DeclarationException] -> ShowS

Pretty DeclarationException

Methods

pretty :: DeclarationException -> Doc

prettyPrec :: Int -> DeclarationException -> Doc

prettyList :: [DeclarationException] -> Doc

HasRange DeclarationException

Methods

getRange :: DeclarationException -> Range

MonadError DeclarationException Nice

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]

UnknownNamesInPolarityPragmas [Name]

PolarityPragmasButNotPostulates [Name]

UselessPrivate Range

UselessAbstract Range

UselessInstance Range

Instances

Data DeclarationWarning

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

Methods

showsPrec :: Int -> DeclarationWarning -> ShowS

show :: DeclarationWarning -> String

showList :: [DeclarationWarning] -> ShowS

Pretty DeclarationWarning

Methods

pretty :: DeclarationWarning -> Doc

prettyPrec :: Int -> DeclarationWarning -> Doc

prettyList :: [DeclarationWarning] -> Doc

HasRange DeclarationWarning

Methods

getRange :: DeclarationWarning -> Range

data Nice a

Nicifier monad. Preserve the state when throwing an exception.

Instances

Monad Nice

Methods

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

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

return :: a -> Nice a

fail :: String -> Nice a

Functor Nice

Methods

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

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

Applicative Nice

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

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.