Support generalized loop iteration

[senier]

Cf. http://docs.adacore.com/live/wave/spark2014/html/spark2014_rm/statements.html#user-defined-iterator-types

[senier]

Example implementation for a simple linked list:

package Iterate with SPARK_Mode
is
   type Byte is mod 2**8;
   type Byte_Array is array (Byte range <>) of Byte;

   type Cursor is private;
   type Container (<>) is private with
      Iterable => (First       => First,
                   Next        => Next,
                   Has_Element => Has_Element,
                   Element     => Element);

   function First       (Cont : Container) return Cursor;
   function Has_Element (Cont : Container; C : Cursor) return Boolean;
   function Next        (Cont : Container; C : Cursor) return Cursor;
   function Element     (Cont : Container; C : Cursor) return Byte;

   function Init (A : Byte_Array) return Container with
      Pre => A'Length > 0 and A'Length <= 100;

   function To_Byte (C : Cursor) return Byte;

private
   type Container is array (Byte range 1 .. 100) of Byte;
   type Cursor is new Byte;

   function First (Cont : Container) return Cursor is (Cursor (Cont'First));

   function Has_Element (Cont : Container; C : Cursor) return Boolean is
     (Byte (C) in Cont'Range and then Cont (Byte (C)) /= 0);

   function Next (Cont : Container; C : Cursor) return Cursor is
     (if Byte (C) in Cont'Range
      then Cursor (Cont (Byte (C)))
      else Cursor (Cont'Last + 1));

   function Element (Cont : Container; C : Cursor) return Byte is
      (if Byte (C) in Cont'Range
       then Byte (Cont (Byte (C)))
       else 0);

   function To_Byte (C : Cursor) return Byte is (Byte (C));

end Iterate;

with Ada.Text_IO; use Ada.Text_IO;

package body Iterate with SPARK_Mode
is
   function Init (A : Byte_Array) return Container
   is
      Result : Container := (others => 0);
   begin
      for I in A'Range loop
         Result (Cursor'Pos (Cursor'Val (Result'First) + Byte'Pos (I))) := A (I);
      end loop;
      return Result;
   end Init;
end Iterate;

with Ada.Text_IO; use Ada.Text_IO;
with Iterate; use Iterate;

procedure Main with SPARK_Mode
is
   C : Container := Init ((2, 5, 6, 0, 3, 4));
begin
   for E of C loop
      Put_Line ("Element: " & To_Byte (E)'Img);
   end loop;
end Main;

$ ./obj/main 
Element:  2
Element:  5
Element:  3
Element:  6
Element:  4

[senier]

Due to our separation of State_Type and Document, it does not seem like we can implement that easily (without using pointers).