[m-rev.] for review: document require_tail_recursion pragmas

[Julien Fischer]

On Wed, 10 Jun 2026 at 15:42, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:

> diff --git a/doc/mercury_reference_manual.texi b/doc/mercury_reference_manual.texi
> index f01d8e52d..b98fcda7a 100644
> --- a/doc/mercury_reference_manual.texi
> +++ b/doc/mercury_reference_manual.texi
> @@ -13019,7 +13019,7 @@ the following extensions to the Mercury language:
>                                  calculated results and detecting or avoiding
>                                  certain kinds of infinite loops.
>  * Termination analysis::        Support for automatic proofs of termination.
> - at c * Tail recursion check::        Require that a predicate is tail recursive.
> +* Ensuring tail recursion::     Require recursion to be tail recursive.
>  * Feature sets::                Support for checking that optional features of
>                                  the implementation are supported at compile
>                                  time.
> @@ -13628,103 +13628,249 @@ and if it fails, then it should quit with an error message.
>  @c The compiler includes a structure reuse analysis system.
>  @c

....


> + at c The @samp{require_tail_recursion} pragma
> + at c allows programmers to ask the compiler's help in ensuring that
> + at c recursive predicates can recurse arbitrarily deeply
> + at c while using a bounded amount of stack space.
> + at c This is sometimes critical for avoiding crashes from stack exhaustion
> + at c when handling large amounts of data.
> + at c Even in situations where this is not an issue,
> + at c tail recursion can still be critical for good performance
> + at c (because it leads to much better locality,
> + at c and therefore makes better use of caches).
> +
> +In declarative languages such as Mercury,
> +iterations have to implemented by recursive code,

have to *be*

That said, since we are only concerned with Mercury here, that
can be simplified to:

   In Mercury, iteration must be implemented by recursive code,


> +in which a predicate or function calls itself,
> +with (hopefully) changed input arguments,
> +either directly (@emph{self} recursion),
> +or indirectly through other predicates or functions (@emph{mutual} recursion).
> +In general, each call consumes some stack space,
> +which means that without special treatment,
> +the amount of stack space consumed by an iteration
> +is proportional to the number of iterations.
> +If the number of iterations is large enough,
> +the amount of stack space required can exceed the amount available,
> +and this @emph{stack exhaustion} will lead to a crash.
> +
> +The standard technique for avoiding this
> +is @emph{tail call optimization},
> +which, when applied to recursive calls, is also called @emph{tail recursion}.
> +This technique is applicable whenever a call
> +is the very last thing that a predicate or function does.

You at least need to say "whenever a *recursive* call" there.
It can't just be any old call.

> +This means not just that it is not followed by any computation,
> +but also that it is not followed by any argument shuffling,
> +because the vector of the output arguments of the call
> +matches exactly the vector of the output arguments
> +of the procedure containing the call.
> +Tail call optimization exploits this
> +by freeing the stack space of the caller just before the call,
> +allowing the callee to reuse its stack space.
> +When all the recursive calls in an iteration are tail recursive,
> +they can handle an unbounded number of iterations
> +using constant (and therefore bounded) stack space.
> +Tail recursion is therefore often very important for robostness.

s/robostness/robustness/

> +Even in situations where stack exhaustion is not an issue,
> +tail recursion can still be critical for good performance,
> +because it leads to much better memory locality for references to the stack,
> +and therefore makes better use of caches.
> +
> +The @samp{require_tail_recursion} pragma
> +asks the compiler to generate a diagnostic
> +when any recursive call in a named predicate or function
> +(with the exception mentioned below)
> +is not @emph{tail} recursive.
> +This can useful both

This can *be* useful

> + at itemize @bullet
> + at item
> +when initially writing the predicate or function,
> +to verify that its recursive calls are tail recursive, and
> + at item
> +when maintaining the predicate or function,
> +to verify that changes to its code have not destroyed this property.
> + at end itemize
> +
> +The exception applies to conjunctions that contain two or more recursive calls,
> +as in the recursive clause of quicksort.
> +Since obviously only the last of these calls can be a tail call,

Delete "obviously".

> + at c Since it is obviously impossible
> + at c for any of those calls except the last one to be tail calls,
> +generating a diagnostic for each non-last call would be just a nuisance.
> +Therefore this pragma applies
> +only to the last recursive call in each conjunction.
> +
> +Note that when compiling a module, the compiler cannot see
> +
> + at itemize @bullet
> + at item
> +the code of predicates and functions defined in other modules
> +because of separate compilation
> +(though intermodule optimization allows some exceptions to this), or
> + at item
> +the code or even the identities of the callees of higher-order calls,
> +including typeclass method calls,

s/typeclass/type class/

> +since the callee is selected at runtime, not compile time.
> + at end itemize
> +
> +Thus for the purposes of warning about non-tail recursion,

Add a comma after Thus.

> +the compiler considers
> +both intermodule calls and higher-order calls to be non-recursive.
> +
> +The simplest form of this pragma has a single argument
> +that specifies the name and arity
> +of the predicate or a function it is intended to apply to:
> +
> + at example
> +:- pragma require_tail_recursion(pred(@var{PredName}/@var{Arity})).
> +:- pragma require_tail_recursion(func(@var{FuncName}/@var{Arity})).
> + at end example
> +
> +These ask the compiler to generate a warning
> +if any recursive call in the body of the named predicate or function,
> +whether it be self-recursive or mutually recursive,
> +is not a @emph{tail} call.
> +It also asks for the warning to be generated

You swap from plural to singular here and then swap back and forth
again below.

> +only in grades that permit tail recursion at all.
> +(The implementation of some grades,
> +including grades that permit debugging or perform deep profiling,
> +need to get control for their own purposes at the end of every clause,
> +which means that @emph{no} call can be a tail call.)
> +
> +(The @samp{pred()} and @samp{func()} wrappers around the name/arity pair
> +are optional in the usual case where there is no risk of confusion,
> +but it is good practice to include them anyway.)
> +
> +By default, the pragma applies
> +to all the modes of the specified predicate or function.
> +If you want it to apply to only a specific subset of those modes,
> +you can use the first form for a predicate and the second form for a function:

Examples of the modes specific versions are missing (from above?)

> +These forms are almost never needed, because in practice,
> +the vast majority of predicates and functions have just one mode.
> +
> +The default is for a @samp{require_tail_recursion} pragma
> +to ask the compiler to generate a warning
> +if any recursive call in the body of the named predicate or function
> +(with the exception of non-last recursive calls in a conjunction)
> +whether it be self-recursive or mutually recursive,
> +is not a @emph{tail} call.
> +It also asks for the warning to be generated
> +only in grades that permit tail recursion at all.
> +However, programmers can specify options
> +that change one or more of these choices.
> +They can do so by adding to the pragma a second argument
> +that consists of a list of one or more of the options listed in this table.
> +
> + at table @code
> +
> + at item warn
> +Every recursive call (other than a non-last recursive call in a conjunction)
> +should generate a warning if it is not @emph{tail} recursive.
> +This option, which is the default, is incompatible with @samp{error}.
> +
> + at item error
> +Every recursive call (other than a non-last recursive call in a conjunction)
> +should generate an error if it is not @emph{tail} recursive.
> +This option is incompatible with @samp{warn}.
> +
> + at item self_or_mutual_recursion
> +Allow the compiler to generate a diagnostic (warning or error)
> +for both self-recursive and mutually recursive calls.
> +This option, which is the default,
> +is incompatible with @samp{self_recursion_only}.
> +
> + at item self_recursion_only
> +Allow the compiler to generate a diagnostic (warning or error)
> +only for self-recursive calls;
> +do not generate diagnostics
> +for mutually recursive calls that are not tail recursive.
> +This option is incompatible with @samp{self_or_mutual_recursion}.
> +
> + at item in_tailrec_grades_only
> +Tell the compiler to generate a diagnostic for non-tail recursion
> +only if the grade allows for the possibility of tail recursion.
> +This disables all such diagnostics
> +in grades in which @emph{no} call can be a tail call.
> +This option, which is the default,
> +is incompatible with @samp{self_or_mutual_recursion}.

s/self_or_mutual_recursion/in_all_grades/

> + at item in_all_grades
> +Tell the compiler to generate a diagnostic for non-tail recursion
> +even in grades that do not allow the possibility of tail recursion.
> +In such grades, which include debugging and deep profiling grades,

s/include/includes/

I suggest emphasising that as well.

> +this will generate a diagnostic for @emph{every} recursive call.
> +The resulting diagnostics can be a useful reminder
> +if you were intending to debug or to profile the program
> +with data sets that would exhaust the stack without tail recursion,
> +but they are likely to be nuisances otherwise.
> +This option is incompatible with @samp{in_tailrec_grades_only}.
> +
> + at end table
> +
> +As you can see, these options represent three possible binary choices.
> +
> +If you want to be told about
> + at emph{all} recursive calls in a module that not tail calls,

that *are* not tail calls

> +you @emph{could} add a @samp{require_tail_recursion} pragma
> +for every predicate and function in the module.
> +However, there is an easier way to achieve the same effect:
> +using the @samp{--warn-non-tail-recursion} option.
> +This option takes an argument which can be one of two words:
> +either @samp{self-and-mutual}, or just @samp{self}.
> +The first specifies the @samp{self_or_mutual_recursion}
> +for all the implicitly generated pragmas,
> +while the second likewise specifies @samp{self_recursion_only}.
> +In both cases, the other two choices
> +will be set to @samp{warn} and @samp{in_tailrec_grades_only}.
> +
> + at c @itemize
> + at c @item
> + at c Specifying @samp{--warn-non-tail-recursion self-and-mutual}
> + at c has the same effect as specifying
> + at c a @samp{require_tail_recursion} pragma
> + at c with the default values of all the options,
> + at c meaning @samp{[warn, self_or_mutual_recursion, in_tailrec_grades_only]}.
> + at c @item
> + at c Specifying @samp{--warn-non-tail-recursion self-mutual}
> + at c has the same effect as specifying
> + at c a @samp{require_tail_recursion} pragma
> + at c with the @samp{self_recursion_only} option,
> + at c and the default values of the other two options,
> + at c meaning @samp{[warn, self_recursion_only, in_tailrec_grades_only]}.
> + at c @end itemize.
> +
> +If you think that
> +the implicit pragmas specified by either form of this option
> +is right for @emph{almost, but not quite all}

s/is/are/

> +of the predicates and functions in a module,
> +you can still use the option, and override its effect where necessary.
> +You can do this either
> +
> + at itemize
> + at item by explicitly specifying
> +a @samp{require_tail_recursion} pragma for a predicate or function,
> +which will override the one that would be implicitly specified by the option,
> + at item or by specifying
> +a @samp{disable_non_tail_recursion_reports} pragma for a predicate or function,
> +which will turn off all non-tail recursion diagnostics
> +for that predicate or function.
> +These have the same forms as @samp{require_tail_recursion} pragmas:
> + at example
> +:- pragma disable_non_tail_recursion_reports(pred(@var{PredName}/@var{Arity})).
> +:- pragma disable_non_tail_recursion_reports(func(@var{FuncName}/@var{Arity})).
> +:- pragma disable_non_tail_recursion_reports(@var{Name}(@var{Modes})).
> +:- pragma disable_non_tail_recursion_reports(@var{Name}(@var{Modes}) = @var{ReturnMode}).
> + at end example
> +just with different pragma name, and with no second argument allowed.
> + at end itemize

Julien.