---------- Forwarded message ---------
From: John Cowan <xxxxxx@ccil.org>
Date: Tue, Jul 2, 2019 at 10:15 PM
Subject: Re: Problems in the specs for 'gdelete' and 'gindex'
To: Mark H Weaver <xxxxxx@netris.org>




On Tue, Jul 2, 2019 at 12:23 AM Mark H Weaver <xxxxxx@netris.org> wrote:
 
(1) The spec for 'gdelete' states:

      The = predicate is passed exactly two arguments, of which the
      first was generated by gen before the second.

Clearly that sentence was copied from gdelete-neighbor-dups.  But
in any case, the = argument should be an equivalence relation,
which means it is symmetrical.
 
(2) The spec for 'gindex' makes apparently conflicting assertions about
    what should happen if 'value-gen' is exhausted before 'index-gen' is
    exhausted.  First, it states:

      It is an error if the indices are not strictly increasing, or if
      any index exceeds the number of elements generated by value-gen.

    This seems to imply that it should be an error if 'value-gen' is
    exhausted first.

I don't think so, no.
 
    If 'index-gen' produces another index after
    'value-gen' is exhausted,

But that never actually happens.  If we run out of values while searching
for the next index, we simply stop: there is no attempt made to see if
the index generator is also exhausted.  Per contra, if the index generator
runs out, we simply stop calling the value generator.

So the general implementation is: get an index, read values until we
find the corresponding value, output it, and continue until either
is exhausted.

In other words, each index should be in the range 0..N-1, where N is the
number of elements generated by VALUE-GEN.  Is that right? 

Yes. 


John Cowan          http://vrici.lojban.org/~cowan        xxxxxx@ccil.org
De plichten van een docent zijn divers, die van het gehoor ook.
      --Edsger Dijkstra