Infinite number of States in a World enabled with lazy evaluation

3 files changed, 353 insertions, 45 deletions

diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index d1d89b8..62f27fa 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -124,14 +124,18 @@ package body Kompsos.Pretty_Print is
            (Item : in World)
         return String
     is
-        Result : SU.Unbounded_String;
+        Result  : SU.Unbounded_String;
+        Scratch : World := Item;
+        Counter : Positive := 1;
     begin
-        if Item.Possibles.Is_Empty then
+        if not Scratch.Has_State (Counter) then
             return "States: N/A" & Latin.LF;
         end if;
-        for Index in Integer range Item.Possibles.First_Index .. Item.Possibles.Last_Index loop
-            SU.Append (Result, "State#" & Image (Index) & ":" & Latin.LF);
-            SU.Append (Result, Image (Item.Possibles.Constant_Reference (Index)));
+        loop
+            SU.Append (Result, "State#" & Image (Counter) & ":" & Latin.LF);
+            SU.Append (Result, Image (Scratch.Possibles.Constant_Reference (Counter)));
+            Counter := Counter + 1;
+            exit when not Scratch.Has_State (Counter);
         end loop;
         return SU.Slice (Result, 1, SU.Length (Result) - 1);
     end Image;
diff --git a/src/kompsos.adb b/src/kompsos.adb
index 5997ddf..a621b7f 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -14,9 +14,11 @@ with
 package body Kompsos is
 
 
-    ------------------------------
-    --  Controlled Subprograms  --
-    ------------------------------
+    -------------------------
+    --  Memory Management  --
+    -------------------------
+
+    --  Terms  --
 
     procedure Free is new Ada.Unchecked_Deallocation (Term_Component, Term_Component_Access);
 
@@ -54,6 +56,51 @@ package body Kompsos is
 
 
 
+    --  Worlds  --
+
+    procedure Free is new Ada.Unchecked_Deallocation (World, World_Access);
+
+
+    procedure Adjust
+           (This : in out World) is
+    begin
+        case This.Engine.Kind is
+        when No_Gen =>
+            null;
+        when Fresh_Gen =>
+            This.Engine.FrG_World := new World'(This.Engine.FrG_World.all);
+        when Unify_Gen =>
+            This.Engine.UniG_World := new World'(This.Engine.UniG_World.all);
+        when Disjunct_Gen =>
+            This.Engine.DisG_World1 := new World'(This.Engine.DisG_World1.all);
+            This.Engine.DisG_World2 := new World'(This.Engine.DisG_World2.all);
+        when Recurse_Gen =>
+            This.Engine.RecG_World := new World'(This.Engine.RecG_World.all);
+        end case;
+    end Adjust;
+
+
+    procedure Finalize
+           (This : in out World) is
+    begin
+        case This.Engine.Kind is
+        when No_Gen =>
+            null;
+        when Fresh_Gen =>
+            Free (This.Engine.FrG_World);
+        when Unify_Gen =>
+            Free (This.Engine.UniG_World);
+        when Disjunct_Gen =>
+            Free (This.Engine.DisG_World1);
+            Free (This.Engine.DisG_World2);
+        when Recurse_Gen =>
+            Free (This.Engine.RecG_World);
+        end case;
+    end Finalize;
+
+
+
+
     -------------
     --  Terms  --
     -------------
@@ -127,9 +174,11 @@ package body Kompsos is
 
 
 
-    ---------------------
-    --  Unify Helpers  --
-    ---------------------
+    ------------------------
+    --  Internal Helpers  --
+    ------------------------
+
+    --  Unification  --
 
     function Has_Var
            (This : in State;
@@ -273,9 +322,126 @@ package body Kompsos is
 
 
 
-    -------------
+    --  Lazy World Generation --
+
+    function Has_State
+           (This  : in out World;
+            Index : in     Positive)
+        return Boolean is
+    begin
+        This.Roll_Until (Index);
+        return This.Possibles.Last_Index >= Index;
+    end Has_State;
+
+
+    procedure Roll_Fresh_Gen
+           (This : in out World) is
+    begin
+        if not This.Engine.FrG_World.Has_State (This.Engine.FrG_Index) then
+            This.Engine := (Kind => No_Gen);
+            return;
+        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;
+
+
+    procedure Roll_Unify_Gen
+           (This : in out World)
+    is
+        Extended : State;
+    begin
+        loop
+            if not This.Engine.UniG_World.Has_State (This.Engine.UniG_Index) then
+                This.Engine := (Kind => No_Gen);
+                return;
+            end if;
+            exit when Do_Unify
+               (This.Engine.UniG_World.Possibles (This.Engine.UniG_Index),
+                This.Engine.UniG_Term1,
+                This.Engine.UniG_Term2,
+                Extended);
+            This.Engine.UniG_Index := This.Engine.UniG_Index + 1;
+        end loop;
+        This.Possibles.Append (Extended);
+        This.Engine.UniG_Index := This.Engine.UniG_Index + 1;
+    end Roll_Unify_Gen;
+
+
+    procedure Roll_Disjunct_Gen
+           (This : in out World)
+    is
+        Temp_World : World_Access;
+        Temp_Index : Positive;
+    begin
+        if not This.Engine.DisG_World1.Has_State (This.Engine.DisG_Index1) then
+            if not This.Engine.DisG_World2.Has_State (This.Engine.DisG_Index2) then
+                This.Engine := (Kind => No_Gen);
+                return;
+            end if;
+            This.Possibles.Append (This.Engine.DisG_World2.Possibles (This.Engine.DisG_Index2));
+            This.Engine.DisG_Index2 := This.Engine.DisG_Index2 + 1;
+        else
+            This.Possibles.Append (This.Engine.DisG_World1.Possibles (This.Engine.DisG_Index1));
+            This.Engine.DisG_Index1 := This.Engine.DisG_Index1 + 1;
+        end if;
+        Temp_World := This.Engine.DisG_World1;
+        Temp_Index := This.Engine.DisG_Index1;
+        This.Engine.DisG_World1 := This.Engine.DisG_World2;
+        This.Engine.DisG_Index1 := This.Engine.DisG_Index2;
+        This.Engine.DisG_World2 := Temp_World;
+        This.Engine.DisG_Index2 := Temp_Index;
+    end Roll_Disjunct_Gen;
+
+
+    procedure Roll_Recurse_Gen
+           (This : in out World) is
+    begin
+        if not This.Engine.RecG_World.Has_State (This.Engine.RecG_Index) then
+            if This.Engine.RecG_Index = 1 then
+                This.Engine := (Kind => No_Gen);
+                return;
+            end if;
+            This.Engine.RecG_Index := 1;
+        end if;
+        This.Possibles.Append (This.Engine.RecG_World.Possibles (This.Engine.RecG_Index));
+        This.Engine.RecG_Index := This.Engine.RecG_Index + 1;
+    end Roll_Recurse_Gen;
+
+
+    procedure Rollover
+           (This : in out 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 Disjunct_Gen => This.Roll_Disjunct_Gen;
+        when Recurse_Gen  => This.Roll_Recurse_Gen;
+        end case;
+    end Rollover;
+
+
+    procedure Roll_Until
+           (This  : in out World;
+            Index : in     Positive) is
+    begin
+        while This.Possibles.Last_Index < Index and This.Engine.Kind /= No_Gen loop
+            This.Rollover;
+        end loop;
+    end Roll_Until;
+
+
+
+
+    -----------------------------
+    --  Public API Operations  --
+    -----------------------------
+
     --  Fresh  --
-    -------------
 
     function Fresh
            (This : in out World)
@@ -300,19 +466,22 @@ package body Kompsos is
         return Variable is
     begin
         return My_Var : constant Variable := (Ident => This.Next_Ident, Name => Name) do
-            This.Next_Ident := This.Next_Ident + 1;
-            for Potential of This.Possibles loop
-                Potential.LVars.Insert (My_Var.Ident, My_Var.Name);
-            end loop;
+            This := (Ada.Finalization.Controlled with
+                Possibles  => State_Vectors.Empty_Vector,
+                Next_Ident => This.Next_Ident + 1,
+                Engine     =>
+                   (Kind      => Fresh_Gen,
+                    FrG_World => new World'(This),
+                    FrG_Index => 1,
+                    FrG_Name  => Name));
+            This.Rollover;
         end return;
     end Fresh;
 
 
 
 
-    -------------
     --  Unify  --
-    -------------
 
     function Unify
            (This  : in World;
@@ -372,18 +541,20 @@ package body Kompsos is
     function Unify
            (This        : in World;
             Left, Right : in Term'Class)
-        return World
-    is
-        Result : World;
-        Extended : State;
+        return World is
     begin
-        Result.Next_Ident := This.Next_Ident;
-        for Potential of This.Possibles loop
-            if Do_Unify (Potential, Left, Right, Extended) then
-                Result.Possibles.Append (Extended);
-            end if;
-        end loop;
-        return Result;
+        return Result : World := (Ada.Finalization.Controlled with
+            Possibles  => State_Vectors.Empty_Vector,
+            Next_Ident => This.Next_Ident,
+            Engine     =>
+               (Kind       => Unify_Gen,
+                UniG_World => new World'(This),
+                UniG_Index => 1,
+                UniG_Term1 => Term (Left),
+                UniG_Term2 => Term (Right)))
+        do
+            Result.Rollover;
+        end return;
     end Unify;
 
 
@@ -397,17 +568,24 @@ package body Kompsos is
 
 
 
-    ----------------
     --  Disjunct  --
-    ----------------
 
     function Disjunct
            (Left, Right : in World)
         return World is
     begin
-        return My_World : constant World :=
-           (Possibles  => Left.Possibles & Right.Possibles,
-            Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident));
+        return Result : World := (Ada.Finalization.Controlled with
+            Possibles  => State_Vectors.Empty_Vector,
+            Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident),
+            Engine     =>
+               (Kind        => Disjunct_Gen,
+                DisG_World1 => new World'(Left),
+                DisG_Index1 => 1,
+                DisG_World2 => new World'(Right),
+                DisG_Index2 => 1))
+        do
+            Result.Rollover;
+        end return;
     end Disjunct;
 
 
@@ -419,6 +597,67 @@ package body Kompsos is
     end Disjunct;
 
 
+
+
+    --  Recurse  --
+
+    function Recurse
+           (This : in World)
+        return World is
+    begin
+        return Result : World := (Ada.Finalization.Controlled with
+            Possibles  => State_Vectors.Empty_Vector,
+            Next_Ident => This.Next_Ident,
+            Engine     =>
+               (Kind       => Recurse_Gen,
+                RecG_World => new World'(This),
+                RecG_Index => 1))
+        do
+            Result.Rollover;
+        end return;
+    end Recurse;
+
+
+    procedure Recurse
+           (This : in out World) is
+    begin
+        This := This.Recurse;
+    end Recurse;
+
+
+
+
+    --  Take  --
+
+    function Take
+           (This  : in World;
+            Count : in Natural)
+        return World is
+    begin
+        if Count = 0 then
+            return (Ada.Finalization.Controlled with
+                Possibles  => State_Vectors.Empty_Vector,
+                Next_Ident => ID_Number'First,
+                Engine     => (Kind => No_Gen));
+        end if;
+        return Result : World := This do
+            Result.Roll_Until (Count);
+            if Result.Possibles.Last_Index > Count then
+                Result.Possibles.Set_Length (Ada.Containers.Count_Type (Count));
+            end if;
+            Result.Engine := (Kind => No_Gen);
+        end return;
+    end Take;
+
+
+    procedure Take
+           (This  : in out World;
+            Count : in     Natural) is
+    begin
+        This := This.Take (Count);
+    end Take;
+
+
 end Kompsos;
 
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index c25cf52..bca09b8 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -132,6 +132,28 @@ package Kompsos is
             Right : in     World);
 
 
+
+
+    function Recurse
+           (This : in World)
+        return World;
+
+    procedure Recurse
+           (This : in out World);
+
+
+
+
+    function Take
+           (This  : in World;
+            Count : in Natural)
+        return World;
+
+    procedure Take
+           (This  : in out World;
+            Count : in     Natural);
+
+
 private
 
 
@@ -151,7 +173,7 @@ private
 
 
 
-    --  2^32 possible variables per World is enough for anybody, right?
+    --  2^32 possible Variables per World is enough for anybody, right?
     type ID_Number is mod 2 ** 32;
 
     type Variable is record
@@ -217,25 +239,68 @@ private
 
 
 
-    --  obviously this World definition will need revision for delays and generators
+    type World_Access is access World;
 
-    --  going to have to turn worlds into a similar sort of reference counted recursive
-    --  controlled type along the lines of what terms are, in order to make them into generators
+    type Generator_Kind is (No_Gen, Fresh_Gen, Unify_Gen, Disjunct_Gen, Recurse_Gen);
+
+    type Generator (Kind : Generator_Kind := No_Gen) is record
+        case Kind is
+        when No_Gen =>
+            null;
+        when Fresh_Gen =>
+            FrG_World   : World_Access;
+            FrG_Index   : Positive;
+            FrG_Name    : SU.Unbounded_String;
+        when Unify_Gen =>
+            UniG_World  : World_Access;
+            UniG_Index  : Positive;
+            UniG_Term1  : Term;
+            UniG_Term2  : Term;
+        when Disjunct_Gen =>
+            DisG_World1 : World_Access;
+            DisG_Index1 : Positive;
+            DisG_World2 : World_Access;
+            DisG_Index2 : Positive;
+        when Recurse_Gen =>
+            RecG_World  : World_Access;
+            RecG_Index  : Positive;
+        end case;
+    end record;
 
     package State_Vectors is new Ada.Containers.Vectors
        (Index_Type   => Positive,
         Element_Type => State);
 
-    use type State_Vectors.Vector;
-
-    type World is tagged record
+    type World is new Ada.Finalization.Controlled with record
         Possibles  : State_Vectors.Vector;
         Next_Ident : ID_Number;
+        Engine     : Generator;
     end record;
 
-    Empty_World : constant World :=
-       (Possibles  => State_Vectors.Empty_Vector & Empty_State,
-        Next_Ident => 0);
+    overriding procedure Adjust
+           (This : in out World);
+
+    overriding procedure Finalize
+           (This : in out World);
+
+    function Has_State
+           (This  : in out World;
+            Index : in     Positive)
+        return Boolean;
+
+    procedure Rollover
+           (This : in out World);
+
+    procedure Roll_Until
+           (This  : in out World;
+            Index : in     Positive);
+
+    use type State_Vectors.Vector;
+
+    Empty_World : constant World := (Ada.Finalization.Controlled with
+        Possibles  => State_Vectors.Empty_Vector & Empty_State,
+        Next_Ident => 0,
+        Engine     => (Kind => No_Gen));
 
 
 end Kompsos;