Worlds separated into Goals that run on a State, improvement to unification efficiencyHEADmaster

1 files changed, 55 insertions, 46 deletions

diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb
index d7c40eb..e2ee677 100644
--- a/src/kompsos-collector.adb
+++ b/src/kompsos-collector.adb
@@ -17,14 +17,15 @@ package body Kompsos.Collector is
     --  Memory Management  --
     -------------------------
 
-    procedure Free is new Ada.Unchecked_Deallocation (World, World_Access);
-
+    procedure Free is new Ada.Unchecked_Deallocation (Goal, Goal_Access);
+    procedure Free is new Ada.Unchecked_Deallocation (State, State_Access);
 
     procedure Finalize
            (This : in out Managed_Map) is
     begin
         for Datum of This.Actual loop
             if Datum.Kind = Conjunct_Data then
+                Free (Datum.Con_Base);
                 Free (Datum.Con_Part);
             end if;
         end loop;
@@ -138,12 +139,8 @@ package body Kompsos.Collector is
 
         --  Unify Pair Terms by unifying each corresponding part
         if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then
-            declare
-                Middle : State;
-            begin
-                return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Middle) and then
-                    Do_Unify (Middle, Real_Left.Right, Real_Right.Right, Extended);
-            end;
+            return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Extended) and then
+                Do_Unify (Extended, Real_Left.Right, Real_Right.Right, Extended);
         end if;
 
         --  Not sure how things get here, but if all else fails
@@ -155,9 +152,9 @@ package body Kompsos.Collector is
     --  Result Collection --
 
     function Call_Lazy
-           (This : in World;
+           (This : in Goal;
             Data : in Lazy_Holders.Holder)
-        return World
+        return Goal
     is
         Ref : constant Lazy_Holders.Constant_Reference_Type := Data.Constant_Reference;
     begin
@@ -173,7 +170,7 @@ package body Kompsos.Collector is
 
 
     procedure Reset
-           (Ptr : in Constant_World_Access) is
+           (Ptr : in Constant_Goal_Access) is
     begin
         if Ptr = null or else Ptr.Actual = null then
             return;
@@ -185,53 +182,55 @@ package body Kompsos.Collector is
         when Static_Node =>
             return;
         when Fresh_Node =>
-            Reset (Ptr.Actual.Frs_World'Unchecked_Access);
+            Reset (Ptr.Actual.Frs_Goal'Unchecked_Access);
         when Unify_Node =>
             Book.Exclude (Ptr.Actual);
-            Reset (Ptr.Actual.Uni_World'Unchecked_Access);
+            Reset (Ptr.Actual.Uni_Goal'Unchecked_Access);
         when Disjunct_Node =>
             Book.Exclude (Ptr.Actual);
-            Reset (Ptr.Actual.Dis_World1'Unchecked_Access);
-            Reset (Ptr.Actual.Dis_World2'Unchecked_Access);
+            Reset (Ptr.Actual.Dis_Goal1'Unchecked_Access);
+            Reset (Ptr.Actual.Dis_Goal2'Unchecked_Access);
         when Conjunct_Node =>
             if Book.Contains (Ptr.Actual) then
-                Reset (Constant_World_Access (Book.Element (Ptr.Actual).Con_Part));
+                Reset (Constant_Goal_Access (Book.Element (Ptr.Actual).Con_Part));
                 Free (Book (Ptr.Actual).Con_Part);
                 Free (Book (Ptr.Actual).Con_Base);
                 Book.Delete (Ptr.Actual);
             end if;
-            Reset (Ptr.Actual.Con_World'Unchecked_Access);
+            Reset (Ptr.Actual.Con_Goal'Unchecked_Access);
         when Recurse_Node =>
             Book.Exclude (Ptr.Actual);
-            Reset (Ptr.Actual.Rec_World'Unchecked_Access);
+            Reset (Ptr.Actual.Rec_Goal'Unchecked_Access);
         end case;
     end Reset;
 
 
     function Get_Next
-           (Ptr    : in     Constant_World_Access;
+           (Ptr    : in     Constant_Goal_Access;
+            Base   : in     State;
             Index  : in     Long_Positive;
             Result :    out State)
         return Boolean;
 
 
     function Do_Get_Next
-           (Ptr    : in     World_Component_Access;
+           (Ptr    : in     Goal_Component_Access;
+            Base   : in     State;
             Index  : in     Long_Positive;
             Result :    out State)
         return Boolean is
     begin
         case Ptr.Kind is
         when Static_Node =>
-            if Index <= Ptr.Stc_States.Last_Index then
-                Result := Ptr.Stc_States (Index);
+            if Index = 1 then
+                Result := Base;
                 return True;
             else
                 return False;
             end if;
 
         when Fresh_Node =>
-            if Get_Next (Ptr.Frs_World'Unchecked_Access, Index, Result) then
+            if Get_Next (Ptr.Frs_Goal'Unchecked_Access, Base, Index, Result) then
                 Result.LVars.Append (Ptr.Frs_Var.Name);
                 Result.Ident.Insert (Ptr.Frs_Var.Ident, Result.LVars.Last_Index);
                 return True;
@@ -244,7 +243,8 @@ package body Kompsos.Collector is
                 Book.Insert (Ptr, (Kind => Unify_Data, others => <>));
             end if;
             while Get_Next
-               (Ptr.Uni_World'Unchecked_Access,
+               (Ptr.Uni_Goal'Unchecked_Access,
+                Base,
                 Index + Book.Element (Ptr).Uni_Offset,
                 Result)
             loop
@@ -264,7 +264,8 @@ package body Kompsos.Collector is
                 if Book.Element (Ptr).Dis_Gone2 then
                     return False;
                 elsif Get_Next
-                   (Ptr.Dis_World2'Unchecked_Access,
+                   (Ptr.Dis_Goal2'Unchecked_Access,
+                    Base,
                     Book.Element (Ptr).Dis_Next2,
                     Result)
                 then
@@ -276,7 +277,8 @@ package body Kompsos.Collector is
                 end if;
             elsif Book.Element (Ptr).Dis_Gone2 then
                 if Get_Next
-                   (Ptr.Dis_World1'Unchecked_Access,
+                   (Ptr.Dis_Goal1'Unchecked_Access,
+                    Base,
                     Book.Element (Ptr).Dis_Next1,
                     Result)
                 then
@@ -288,7 +290,8 @@ package body Kompsos.Collector is
                 end if;
             elsif Book.Element (Ptr).Dis_Flag then
                 if Get_Next
-                   (Ptr.Dis_World1'Unchecked_Access,
+                   (Ptr.Dis_Goal1'Unchecked_Access,
+                    Base,
                     Book.Element (Ptr).Dis_Next1,
                     Result)
                 then
@@ -298,7 +301,8 @@ package body Kompsos.Collector is
                 else
                     Book (Ptr).Dis_Gone1 := True;
                     if Get_Next
-                       (Ptr.Dis_World2'Unchecked_Access,
+                       (Ptr.Dis_Goal2'Unchecked_Access,
+                        Base,
                         Book.Element (Ptr).Dis_Next2,
                         Result)
                     then
@@ -311,7 +315,8 @@ package body Kompsos.Collector is
                 end if;
             else
                 if Get_Next
-                   (Ptr.Dis_World2'Unchecked_Access,
+                   (Ptr.Dis_Goal2'Unchecked_Access,
+                    Base,
                     Book.Element (Ptr).Dis_Next2,
                     Result)
                 then
@@ -321,7 +326,8 @@ package body Kompsos.Collector is
                 else
                     Book (Ptr).Dis_Gone2 := True;
                     if Get_Next
-                       (Ptr.Dis_World1'Unchecked_Access,
+                       (Ptr.Dis_Goal1'Unchecked_Access,
+                        Base,
                         Book.Element (Ptr).Dis_Next1,
                         Result)
                     then
@@ -337,29 +343,30 @@ package body Kompsos.Collector is
         when Conjunct_Node =>
             if not Book.Contains (Ptr) then
                 Book.Insert (Ptr, (Kind => Conjunct_Data, others => <>));
-                if not Get_Next (Ptr.Con_World'Unchecked_Access, 1, Result) then
+                if not Get_Next (Ptr.Con_Goal'Unchecked_Access, Base, 1, Result) then
                     Book (Ptr).Con_Gone := True;
                 else
-                    Book (Ptr).Con_Base := new World'(World (Static (Result)));
-                    Book (Ptr).Con_Part := new World'(Call_Lazy
-                        (Book.Element (Ptr).Con_Base.all, Ptr.Con_Data));
+                    Book (Ptr).Con_Base := new State'(Result);
+                    Book (Ptr).Con_Part := new Goal'(Call_Lazy (Empty_Goal, Ptr.Con_Data));
                 end if;
             end if;
             if Book (Ptr).Con_Gone then
                 return False;
             end if;
             while not Get_Next
-               (Constant_World_Access (Book.Element (Ptr).Con_Part),
+               (Constant_Goal_Access (Book.Element (Ptr).Con_Part),
+                Book.Element (Ptr).Con_Base.all,
                 Book.Element (Ptr).Con_Next,
                 Result)
             loop
-                Reset (Constant_World_Access (Book.Element (Ptr).Con_Part));
+                Reset (Constant_Goal_Access (Book.Element (Ptr).Con_Part));
                 if Get_Next
-                   (Ptr.Con_World'Unchecked_Access,
+                   (Ptr.Con_Goal'Unchecked_Access,
+                    Base,
                     Book.Element (Ptr).Con_From,
                     Result)
                 then
-                    Book (Ptr).Con_Base.Actual.Stc_States (1) := Result;
+                    Book (Ptr).Con_Base.all := Result;
                     Book (Ptr).Con_Next := 1;
                     Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1;
                 else
@@ -380,7 +387,8 @@ package body Kompsos.Collector is
                 return False;
             end if;
             while not Get_Next
-               (Ptr.Rec_World'Unchecked_Access,
+               (Ptr.Rec_Goal'Unchecked_Access,
+                Base,
                 Book.Element (Ptr).Rec_Next,
                 Result)
             loop
@@ -398,7 +406,7 @@ package body Kompsos.Collector is
 
 
     function Cached
-           (Ptr    : in     World_Component_Access;
+           (Ptr    : in     Goal_Component_Access;
             Index  : in     Long_Positive;
             Result :    out State)
         return Boolean is
@@ -413,7 +421,7 @@ package body Kompsos.Collector is
 
 
     procedure Cache_This
-           (Ptr    : in World_Component_Access;
+           (Ptr    : in Goal_Component_Access;
             Index  : in Long_Positive;
             Result : in State) is
     begin
@@ -428,7 +436,8 @@ package body Kompsos.Collector is
 
 
     function Get_Next
-           (Ptr    : in     Constant_World_Access;
+           (Ptr    : in     Constant_Goal_Access;
+            Base   : in     State;
             Index  : in     Long_Positive;
             Result :    out State)
         return Boolean is
@@ -438,7 +447,7 @@ package body Kompsos.Collector is
         elsif Cached (Ptr.Actual, Index, Result) then
             return True;
         else
-            return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Index, Result) do
+            return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Base, Index, Result) do
                 if Found then
                     Cache_This (Ptr.Actual, Index, Result);
                 end if;
@@ -456,14 +465,14 @@ package body Kompsos.Collector is
     function Has_Next
         return Boolean
     is
-        Ptr : constant Constant_World_Access := Source'Access;
+        Ptr : constant Constant_Goal_Access := Relation'Access;
     begin
         if State_Valid then
             return True;
         elsif Exhausted then
             return False;
         else
-            State_Valid := Get_Next (Ptr, Next_Index, Next_State);
+            State_Valid := Get_Next (Ptr, Within, Next_Index, Next_State);
             if not State_Valid then
                 Exhausted := True;
             else
@@ -501,7 +510,7 @@ package body Kompsos.Collector is
 
     procedure Reset
     is
-        Ptr : constant Constant_World_Access := Source'Access;
+        Ptr : constant Constant_Goal_Access := Relation'Access;
     begin
         Reset (Ptr);
         Next_Index  := 1;