[m-dev.] For review: add '..'/2 and series/3 to list.m

[Fergus Henderson]

On 26-Sep-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> Added integer and generalised series functions.
> 
> library/list.m:
> 	Added '..'/2 - generates lists of ascending integers.
> 	Added list__series/3 - higher order function used to
> 		generate various kinds of series.

The new functions should be mentioned in the NEWS file.

> Index: list.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/library/list.m,v
> retrieving revision 1.93
> diff -u -r1.93 list.m
> --- list.m	2000/09/08 15:53:15	1.93
> +++ list.m	2000/09/26 15:06:52
> @@ -505,11 +505,26 @@
>  	in, in, out) is det.
>  
>  
> %---------------------------------------------------------------------------
> --%
> +
> +	% list__series(X, OK, Succ) = [X0, X1, ..., Xn]
> +	% 	where Xk = Succ^k(X) and OK(Xk) and not OK(Succ^(n+1)(X)).
> +	%
> +:- func list__series(T, pred(T), func(T) = T) = list(T).
> +:- mode list__series(in, pred(in) is semidet, func(in) = out is det) = out
> +		is det.

I think the documentation there is rather cryptic.
It uses a lot of semi-formal notation which is not defined anywhere.
It's not as understandable as an informal definition,
and not as well-defined or precise as a genuinely formal definition.

I think you should explain in informal english words what the function
does, and give an example.  For the formal definition, you should
explain the notation `Succ^k(X)'.  (It might be better to use parentheses
there, e.g. `(Succ^k)(X)' -- that way it is valid Mercury syntax.)
Also the line `where Xk = Succ^k(X) and OK(Xk) and not OK(Succ^(n+1)(X)).'
is confusing because the first part should really be quantified
by "forall k in 0, 1, ..., n", but the last term should not be
in the scope of that quantifier.

> ----------------------------------------------------------------------------
> %
> +
> +	% Lo `..` Hi = [Lo, Lo + 1, ..., Hi]
> +	%
> +:- func int `..` int = list(int).

Here you should document what happens when Hi < Lo.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------