This module contains a compiler pass that processes pragmas.

Specification

Preconditions

There are no special requirements.

Translation

• If there is a pragma of the form {--} or {--} and a declaration f x₁ … xᵢ … xₙ = e, the index i - 1 and identifier xᵢ are inserted into the environment as the decreasing argument of f.

Postconditions

• There is an entry for all explicitly annotated decreasing arguments in the environment.

Error Cases

• If there is a pragma of the form {--} or {--}, but there is no such function declaration or the function does not have an argument with the specified name or at the specified position, a fatal error is reported.