The rfind challenge

[Timon Gehr]

On 01/15/2013 12:53 PM, FG wrote:
> On 2013-01-15 06:51, Andrei Alexandrescu wrote:
>> If r is a forward range but not better, this is rather simple:
>>
>> R rfind(R, E)(R range, E element)
>> {
>>      for (;;)
>>      {
>>          auto ahead = range.save.find(element);
>>          if (ahead.empty) return range;
>>          range = ahead;
>>      }
>> }
>
> That example creates an infinite loop. Needs a popFront:
>
>      R rfind(R, E)(R range, E element)
>      {
>          if (range.empty) return range;
>          for (;;)
>          {
>              auto ahead = range.save;
>              ahead.popFront();
>              ahead = ahead.find(element);
>              if (ahead.empty) return range;
>              range = ahead;
>          }
>      }
>

That is buggy too.

> Another thing: if the element is not found, I think an empty range
> should be returned and not the whole range.

Yup.

R rfind(R, E)(R range,E element){
     auto r=range.find(element);
     if(r.empty) return r;
     for(;;){
         auto ahead=r.save;
         ahead.popFront();
         ahead=ahead.find(element);
         if(ahead.empty) return r;
         r=ahead;
     }
}


Full proof (assuming purity of the range primitives):

/+pure+/ R tail(R)(R r)out(result){
     assert(result=={
         auto a=r;
         a.popFront();
         return a;
     }());
}body{
     auto a=r;
     a.popFront();
     return a;
}

/+pure+/ R rfind(R, E)(R range,E element)out(result){
	assert(range.find(element).empty&&result.empty||!range.find(element).empty&&!result.empty&&result.front==element&&result.tail.find(element).empty);
}body{
     auto r=range.find(element);
     assert(r==range.find(element)&&(r.empty||r.front==element));
     if(r.empty){
         assert(r==range.find(element)&&r.empty);
         return r;
         /+assert(result==range.find(element)&&result.empty);
         assert(range.find(element).empty&&result.empty);+/
     }
     assert(r==range.find(element)&&!r.empty&&r.front==element);
     assert(!range.find(element).empty&&!r.empty&&r.front==element);
     for(;;){
 
assert(true&&!range.find(element).empty&&!r.empty&&r.front==element);
 
assert(!range.find(element).empty&&!r.empty&&r.front==element&&!r.empty);
         auto ahead=r.save;
 
assert(!range.find(element).empty&&!r.empty&&r.front==element&&!ahead.empty&&ahead==r.save);
         ahead.popFront();
 
assert(!range.find(element).empty&&!r.empty&&r.front==element&&ahead=={
             auto ahead=r.save;
             ahead.popFront();
             return ahead;
         }());
 
assert(!range.find(element).empty&&!r.empty&&r.front==element&&ahead==r.tail);
         ahead=ahead.find(element);
 
assert(!range.find(element).empty&&!r.empty&&r.front==element&&(ahead.empty||ahead.front==element)&&ahead==r.tail.find(element));
         if(ahead.empty){
 
assert(!range.find(element).empty&&ahead.empty&&!r.empty&&r.front==element&&ahead==r.tail.find(element));
             return r;
 
/+assert(!range.find(element).empty&&ahead.empty&&!result.empty&&result.front==element&&ahead==result.tail.find(element));
 
assert(!range.find(element).empty&&!result.empty&&result.front==element&&result.tail.find(element).empty);+/
         }
 
assert(!range.find(element).empty&&!ahead.empty&&ahead.front==element);
         r=ahead;
         assert(!range.find(element).empty&&!r.empty&&r.front==element);
     }
     assert(false);
}