[m-rev.] Section for the Languge Reference Manual

[Peter Wang]

On Thu, 13 Oct 2022 14:13:18 +1100 Mark Brown <mark at mercurylang.org> wrote:

> diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> index 4934c6d88..8a26b50c6 100644
> --- a/doc/reference_manual.texi
> +++ b/doc/reference_manual.texi
> @@ -8488,6 +8492,64 @@ p_carefully(!IO) :-
>      ).
>  @end example
>  
> + at noindent
> +One common use for exceptions is to check the input
> +and throw an exception if it is invalid.
> +It might be tempting to implement this
> +with a predicate such as the following:
> +
> + at example
> +:- pred check_target(target::in) is det.
> +
> +check_target(Target) :-
> +    ( if ... then
> +        true
> +    else
> +        throw("invalid target")
> +    ).
> + at end example
> +
> + at noindent
> +This code warrants caution, however.
> +Consider the following usage:

Maybe just:

    However, consider the following usage:

> +
> + at example
> +shoot(Target, !IO) :-
> +    check_target(Target),
> +    unsafe_shoot(Target, !IO).
> + at end example
> +
> + at noindent
> +Mercury may reorder conjunctions,
> +which is (probably) not what the user intended in this case.
> +Furthermore,
> +Mercury may optimize away the call to @samp{check_target/1} entirely,

Unnecessary comma (?)

> +since the mode-determinism assertion for
> +a @samp{det} predicate with no outputs
> +essentially states that it is equivalent to @samp{true}.
> +

> +The strict sequential semantics can be used
> +to guarantee that these changes will not occur
> +(@pxref{Formal semantics}).
> +However,
> +we recommend implementing checks like these in the following way,

Unnecessary comma (?)

> +to avoid depending on the choice of operational semantics:
> +
> + at example
> +shoot(Target0, !IO) :-
> +    check_target(Target0, Target),
> +    unsafe_shoot(Target, !IO).
> +
> +:- pred check_target(target::in, target::out) is det.
> +
> +check_target(Target0, Target) :-
> +    ( if ... then
> +        Target = Target0
> +    else
> +        throw("invalid target")
> +    ).
> + at end example
> +
>  @node Formal semantics
>  @chapter Formal semantics
>  

> @@ -8519,12 +8581,16 @@ However, there are certain minimum requirements that they
>  must satisfy with respect to completeness.
>  
>  There is an operational semantics of Mercury programs called the
> - at dfn{strict sequential} operational semantics.  In this semantics,
> -the program is executed top-down, starting from @samp{main/2}
> + at dfn{strict sequential} semantics.
> +In this semantics,
> +the program is executed top-down using SLDNF resolution
> +(or something equivalent),
> +starting from @samp{main/2}

Comma.

>  preceded by any module initialisation goals
> -(as per @ref{Module initialisation}), followed by any module finalisation
> -goals (as per @ref{Module finalisation}),
> -and function calls within a goal, conjunctions and disjunctions are all
> +(as per @ref{Module initialisation}),
> +and followed by any module finalisation goals
> +(as per @ref{Module finalisation}).
> +Function calls, conjunctions and disjunctions are all
>  executed in depth-first left-to-right order.
>  Conjunctions and function calls are
>  ``minimally'' reordered as required by the modes:
> @@ -8532,57 +8598,60 @@ the order is determined by selecting the first mode-correct sub-goal
>  (conjunct or function call),
>  executing that, then selecting the first of the remaining sub-goals
>  which is now mode-correct, executing that, and so on.
> -(There is no interleaving of different individual conjuncts or function calls,
> -however; the sub-goals are reordered, not split and interleaved.)
> +There is no interleaving of different individual conjuncts or function calls:
> +the sub-goals are reordered, not split and interleaved.
>  Function application is strict, not lazy.
> +Predicate calls are strict in the sense that
> +goals will be executed irrespective of any mode-determinism asserions,
> +even if they loop,
> +are @samp{erroneous},
> +or are @samp{det} and contain no outputs.
>  @c XXX should document the operational semantics of switches and if-then-elses
>  
>  Mercury implementations are required to provide a method of processing
>  Mercury programs which is equivalent to the strict sequential
> -operational semantics.
> +semantics.
>  

>  There is another operational semantics of Mercury programs
> -called the @dfn{strict commutative} operational semantics.
> -This semantics is equivalent to the strict sequential operational semantics
> +called the @dfn{strict commutative} semantics.
> +This semantics is equivalent to the strict sequential semantics
>  except that there is no requirement that
>  function calls, conjunctions and disjunctions be executed left-to-right;
>  they may be executed in any order, and may even be interleaved.
> -Furthermore, the order may even be different
> +Furthermore, the order may be different
>  each time a particular goal is entered.

Or: may differ

Looks good to me.

Peter