Refactor of rollover laziness

2 files changed, 104 insertions, 134 deletions

diff --git a/src/kompsos.adb b/src/kompsos.adb
index b2ff1a2..99c8ad9 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -68,16 +68,16 @@ package body Kompsos is
         when No_Gen =>
             null;
         when Fresh_Gen =>
-            This.Engine.FrG_World := new Mu_World'Class'(This.Engine.FrG_World.all);
+            This.Engine.Frs_World := new Mu_World'Class'(This.Engine.Frs_World.all);
         when Unify_Gen =>
-            This.Engine.UniG_World := new Mu_World'Class'(This.Engine.UniG_World.all);
-        when Disjunct1_Gen =>
-            This.Engine.Dis1G_World := new Mu_World'Class'(This.Engine.Dis1G_World.all);
-        when Disjunct2_Gen =>
-            This.Engine.Dis2G_World1 := new Mu_World'Class'(This.Engine.Dis2G_World1.all);
-            This.Engine.Dis2G_World2 := new Mu_World'Class'(This.Engine.Dis2G_World2.all);
+            This.Engine.Uni_World := new Mu_World'Class'(This.Engine.Uni_World.all);
+        when Buffer_Gen =>
+            This.Engine.Buff_World := new Mu_World'Class'(This.Engine.Buff_World.all);
+        when Disjunct_Gen =>
+            This.Engine.Dis_World1 := new Mu_World'Class'(This.Engine.Dis_World1.all);
+            This.Engine.Dis_World2 := new Mu_World'Class'(This.Engine.Dis_World2.all);
         when Recurse_Gen =>
-            This.Engine.RecG_World := new Mu_World'Class'(This.Engine.RecG_World.all);
+            This.Engine.Rec_World := new Mu_World'Class'(This.Engine.Rec_World.all);
         end case;
     end Adjust;
 
@@ -89,16 +89,16 @@ package body Kompsos is
         when No_Gen =>
             null;
         when Fresh_Gen =>
-            Free (This.Engine.FrG_World);
+            Free (This.Engine.Frs_World);
         when Unify_Gen =>
-            Free (This.Engine.UniG_World);
-        when Disjunct1_Gen =>
-            Free (This.Engine.Dis1G_World);
-        when Disjunct2_Gen =>
-            Free (This.Engine.Dis2G_World1);
-            Free (This.Engine.Dis2G_World2);
+            Free (This.Engine.Uni_World);
+        when Buffer_Gen =>
+            Free (This.Engine.Buff_World);
+        when Disjunct_Gen =>
+            Free (This.Engine.Dis_World1);
+            Free (This.Engine.Dis_World2);
         when Recurse_Gen =>
-            Free (This.Engine.RecG_World);
+            Free (This.Engine.Rec_World);
         end case;
     end Finalize;
 
@@ -360,18 +360,16 @@ package body Kompsos is
     procedure Roll_Fresh_Gen
            (This : in out Mu_World) is
     begin
-        This.Engine.FrG_World.Rollover;
-        if This.Engine.FrG_World.Possibles.Last_Index < This.Engine.FrG_Index then
-            if This.Engine.FrG_World.Engine.Kind = No_Gen then
-                This.Engine := (Kind => No_Gen);
-            end if;
-            return;
+        This.Engine.Frs_World.Rollover;
+        for Potential of This.Engine.Frs_World.Possibles loop
+            Potential.LVars.Insert (This.Engine.Frs_World.Next_Ident, This.Engine.Frs_Name);
+            This.Possibles.Append (Potential);
+        end loop;
+        if This.Engine.Frs_World.Engine.Kind = No_Gen then
+            This.Engine := (Kind => No_Gen);
+        else
+            This.Engine.Frs_World.Possibles.Clear;
         end if;
-        This.Possibles.Append (This.Engine.FrG_World.Possibles.Element (This.Engine.FrG_Index));
-        This.Possibles.Reference (This.Possibles.Last_Index).LVars.Insert
-           (This.Engine.FrG_World.Next_Ident,
-            This.Engine.FrG_Name);
-        This.Engine.FrG_Index := This.Engine.FrG_Index + 1;
     end Roll_Fresh_Gen;
 
 
@@ -380,102 +378,84 @@ package body Kompsos is
     is
         Extended : State;
     begin
-        This.Engine.UniG_World.Rollover;
-        if This.Engine.UniG_World.Possibles.Last_Index < This.Engine.UniG_Index then
-            if This.Engine.UniG_World.Engine.Kind = No_Gen then
-                This.Engine := (Kind => No_Gen);
+        This.Engine.Uni_World.Rollover;
+        for Potential of This.Engine.Uni_World.Possibles loop
+            if Do_Unify (Potential, This.Engine.Uni_Term1, This.Engine.Uni_Term2, Extended) then
+                This.Possibles.Append (Extended);
             end if;
-            return;
-        end if;
-        if not Do_Unify
-               (This.Engine.UniG_World.Possibles (This.Engine.UniG_Index),
-                This.Engine.UniG_Term1,
-                This.Engine.UniG_Term2,
-                Extended)
-        then
-            This.Engine.UniG_Index := This.Engine.UniG_Index + 1;
-            return;
+        end loop;
+        if This.Engine.Uni_World.Engine.Kind = No_Gen then
+            This.Engine := (Kind => No_Gen);
+        else
+            This.Engine.Uni_World.Possibles.Clear;
         end if;
-        This.Possibles.Append (Extended);
-        This.Engine.UniG_Index := This.Engine.UniG_Index + 1;
     end Roll_Unify_Gen;
 
 
-    procedure Roll_Disjunct1_Gen
+    procedure Roll_Buffer_Gen
            (This : in out Mu_World) is
     begin
-        This.Engine.Dis1G_World.Rollover;
-        if This.Engine.Dis1G_World.Possibles.Last_Index < This.Engine.Dis1G_Index then
-            if This.Engine.Dis1G_World.Engine.Kind = No_Gen then
-                This.Engine := (Kind => No_Gen);
-            end if;
-            return;
+        This.Engine.Buff_World.Rollover;
+        This.Possibles.Append (This.Engine.Buff_World.Possibles);
+        if This.Engine.Buff_World.Engine.Kind = No_Gen then
+            This.Engine := (Kind => No_Gen);
+        else
+            This.Engine.Buff_World.Possibles.Clear;
         end if;
-        This.Possibles.Append (This.Engine.Dis1G_World.Possibles (This.Engine.Dis1G_Index));
-        This.Engine.Dis1G_Index := This.Engine.Dis1G_Index + 1;
-    end Roll_Disjunct1_Gen;
+    end Roll_Buffer_Gen;
 
 
-    procedure Roll_Disjunct2_Gen
+    procedure Roll_Disjunct_Gen
            (This : in out Mu_World)
     is
         Temp_World : World_Access;
-        Temp_Index : Positive;
-    begin
-        This.Engine.Dis2G_World1.Rollover;
-        if This.Engine.Dis2G_World1.Possibles.Last_Index < This.Engine.Dis2G_Index1 then
-            if This.Engine.Dis2G_World1.Engine.Kind = No_Gen then
-                This.Engine :=
-                   (Kind        => Disjunct1_Gen,
-                    Dis1G_World => This.Engine.Dis2G_World2,
-                    Dis1G_Index => This.Engine.Dis2G_Index2);
-                return;
-            end if;
+    begin
+        This.Engine.Dis_World1.Rollover;
+        This.Possibles.Append (This.Engine.Dis_World1.Possibles);
+        if This.Engine.Dis_World1.Engine.Kind = No_Gen then
+            This.Engine := (Kind => Buffer_Gen, Buff_World => This.Engine.Dis_World2);
         else
-            This.Possibles.Append (This.Engine.Dis2G_World1.Possibles (This.Engine.Dis2G_Index1));
-            This.Engine.Dis2G_Index1 := This.Engine.Dis2G_Index1 + 1;
+            This.Engine.Dis_World1.Possibles.Clear;
+            Temp_World := This.Engine.Dis_World1;
+            This.Engine.Dis_World1 := This.Engine.Dis_World2;
+            This.Engine.Dis_World2 := Temp_World;
         end if;
-        Temp_World := This.Engine.Dis2G_World1;
-        Temp_Index := This.Engine.Dis2G_Index1;
-        This.Engine.Dis2G_World1 := This.Engine.Dis2G_World2;
-        This.Engine.Dis2G_Index1 := This.Engine.Dis2G_Index2;
-        This.Engine.Dis2G_World2 := Temp_World;
-        This.Engine.Dis2G_Index2 := Temp_Index;
-    end Roll_Disjunct2_Gen;
+    end Roll_Disjunct_Gen;
 
 
     procedure Roll_Recurse_Gen
            (This : in out Mu_World) is
     begin
-        This.Engine.RecG_World.Rollover;
-        if This.Engine.RecG_World.Possibles.Last_Index < This.Engine.RecG_Index then
-            if This.Engine.RecG_World.Engine.Kind = No_Gen then
-                if This.Engine.RecG_Index = 1 then
+        This.Engine.Rec_World.Rollover;
+        if This.Engine.Rec_World.Possibles.Last_Index < This.Engine.Rec_Index then
+            if This.Engine.Rec_World.Engine.Kind = No_Gen then
+                if This.Engine.Rec_Index = 1 then
                     This.Engine := (Kind => No_Gen);
-                    return;
+                else
+                    This.Engine.Rec_Index := 1;
                 end if;
-                This.Engine.RecG_Index := 1;
             end if;
             return;
         end if;
-        This.Possibles.Append (This.Engine.RecG_World.Possibles (This.Engine.RecG_Index));
-        This.Engine.RecG_Index := This.Engine.RecG_Index + 1;
+        for Index in Integer range
+            This.Engine.Rec_Index .. This.Engine.Rec_World.Possibles.Last_Index
+        loop
+            This.Possibles.Append (This.Engine.Rec_World.Possibles (Index));
+        end loop;
+        This.Engine.Rec_Index := This.Engine.Rec_World.Possibles.Last_Index + 1;
     end Roll_Recurse_Gen;
 
 
-    --  Note that more than one call to Rollover may be needed to generate the next State.
-    --  This is intentional to get better behaviour with infinite Worlds.
-
     procedure Rollover
            (This : in out Mu_World) is
     begin
         case This.Engine.Kind is
-        when No_Gen        => null;
-        when Fresh_Gen     => This.Roll_Fresh_Gen;
-        when Unify_Gen     => This.Roll_Unify_Gen;
-        when Disjunct1_Gen => This.Roll_Disjunct1_Gen;
-        when Disjunct2_Gen => This.Roll_Disjunct2_Gen;
-        when Recurse_Gen   => This.Roll_Recurse_Gen;
+        when No_Gen       => null;
+        when Fresh_Gen    => This.Roll_Fresh_Gen;
+        when Unify_Gen    => This.Roll_Unify_Gen;
+        when Buffer_Gen   => This.Roll_Buffer_Gen;
+        when Disjunct_Gen => This.Roll_Disjunct_Gen;
+        when Recurse_Gen  => This.Roll_Recurse_Gen;
         end case;
     end Rollover;
 
@@ -523,9 +503,8 @@ package body Kompsos is
         return My_Term : constant Term := T (Variable'(Ident => This.Next_Ident, Name => Name)) do
             This.Engine :=
                (Kind      => Fresh_Gen,
-                FrG_World => new Mu_World'Class'(This),
-                FrG_Index => 1,
-                FrG_Name  => Name);
+                Frs_World => new Mu_World'Class'(This),
+                Frs_Name  => Name);
             This.Next_Ident := This.Next_Ident + 1;
             This.Possibles := State_Vectors.Empty_Vector;
         end return;
@@ -564,11 +543,10 @@ package body Kompsos is
             Possibles  => State_Vectors.Empty_Vector,
             Next_Ident => This.Next_Ident,
             Engine     =>
-               (Kind       => Unify_Gen,
-                UniG_World => new Mu_World'(This),
-                UniG_Index => 1,
-                UniG_Term1 => Term (Left),
-                UniG_Term2 => Term (Right)));
+               (Kind      => Unify_Gen,
+                Uni_World => new Mu_World'(This),
+                Uni_Term1 => Term (Left),
+                Uni_Term2 => Term (Right)));
     end Unify;
 
 
@@ -592,11 +570,9 @@ package body Kompsos is
             Possibles  => State_Vectors.Empty_Vector,
             Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident),
             Engine     =>
-               (Kind         => Disjunct2_Gen,
-                Dis2G_World1 => new Mu_World'(Left),
-                Dis2G_Index1 => 1,
-                Dis2G_World2 => new Mu_World'(Right),
-                Dis2G_Index2 => 1));
+               (Kind       => Disjunct_Gen,
+                Dis_World1 => new Mu_World'(Left),
+                Dis_World2 => new Mu_World'(Right)));
     end Disjunct;
 
 
@@ -624,16 +600,15 @@ package body Kompsos is
                 Possibles  => State_Vectors.Empty_Vector,
                 Next_Ident => 0,  --  dummy
                 Engine     =>
-                   (Kind         => Disjunct2_Gen,
-                    Dis2G_World1 => new Mu_World'(Inputs (Inputs'First)),
-                    Dis2G_Index1 => 1,
-                    Dis2G_World2 =>
-                        new Mu_World'(Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))),
-                    Dis2G_Index2 => 1))
+                   (Kind       => Disjunct_Gen,
+                    Dis_World1 =>
+                        new Mu_World'(Inputs (Inputs'First)),
+                    Dis_World2 =>
+                        new Mu_World'(Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last)))))
             do
                 Result.Next_Ident := ID_Number'Max
-                   (Result.Engine.Dis2G_World1.Next_Ident,
-                    Result.Engine.Dis2G_World2.Next_Ident);
+                   (Result.Engine.Dis_World1.Next_Ident,
+                    Result.Engine.Dis_World2.Next_Ident);
             end return;
         end if;
     end Disjunct;
@@ -659,9 +634,9 @@ package body Kompsos is
             Possibles  => State_Vectors.Empty_Vector,
             Next_Ident => This.Next_Ident,
             Engine     =>
-               (Kind       => Recurse_Gen,
-                RecG_World => new Mu_World'(This),
-                RecG_Index => 1));
+               (Kind      => Recurse_Gen,
+                Rec_World => new Mu_World'(This),
+                Rec_Index => 1));
     end Recurse;
 
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index a8b8851..d2b6fe5 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -237,8 +237,8 @@ private
        (No_Gen,
         Fresh_Gen,
         Unify_Gen,
-        Disjunct1_Gen,
-        Disjunct2_Gen,
+        Buffer_Gen,
+        Disjunct_Gen,
         Recurse_Gen);
 
     type Generator (Kind : Generator_Kind := No_Gen) is record
@@ -246,25 +246,20 @@ private
         when No_Gen =>
             null;
         when Fresh_Gen =>
-            FrG_World    : World_Access;
-            FrG_Index    : Positive;
-            FrG_Name     : SU.Unbounded_String;
+            Frs_World  : World_Access;
+            Frs_Name   : SU.Unbounded_String;
         when Unify_Gen =>
-            UniG_World   : World_Access;
-            UniG_Index   : Positive;
-            UniG_Term1   : Term;
-            UniG_Term2   : Term;
-        when Disjunct1_Gen =>
-            Dis1G_World  : World_Access;
-            Dis1G_Index  : Positive;
-        when Disjunct2_Gen =>
-            Dis2G_World1 : World_Access;
-            Dis2G_Index1 : Positive;
-            Dis2G_World2 : World_Access;
-            Dis2G_Index2 : Positive;
+            Uni_World  : World_Access;
+            Uni_Term1  : Term;
+            Uni_Term2  : Term;
+        when Buffer_Gen =>
+            Buff_World : World_Access;
+        when Disjunct_Gen =>
+            Dis_World1 : World_Access;
+            Dis_World2 : World_Access;
         when Recurse_Gen =>
-            RecG_World   : World_Access;
-            RecG_Index   : Positive;
+            Rec_World : World_Access;
+            Rec_Index : Positive;
         end case;
     end record;