Evaluation algorithm changed to inverted interleaved depth first search

1 files changed, 67 insertions, 90 deletions

diff --git a/src/kompsos.adb b/src/kompsos.adb
index 4513706..b12e1fb 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -53,43 +53,11 @@ package body Kompsos is
 
 
 
-    --  States  --
-
-    procedure Free is new Ada.Unchecked_Deallocation (State_Component, State_Component_Access);
-
-
-    procedure Initialize
-           (This : in out State_Control) is
-    begin
-        This.Actual := null;
-    end Initialize;
-
-
-    procedure Adjust
-           (This : in out State_Control) is
-    begin
-        if This.Actual /= null then
-            This.Actual.Counter := This.Actual.Counter + 1;
-        end if;
-    end Adjust;
-
-
-    procedure Finalize
-           (This : in out State_Control) is
-    begin
-        if This.Actual /= null then
-            This.Actual.Counter := This.Actual.Counter - 1;
-            if This.Actual.Counter = 0 then
-                Free (This.Actual);
-            end if;
-        end if;
-    end Finalize;
-
-
-
     --  Goal Graphs  --
 
     procedure Free is new Ada.Unchecked_Deallocation (Graph_Component, Graph_Component_Access);
+    procedure Free is new Ada.Unchecked_Deallocation (Term_Array, Term_Array_Access);
+    procedure Free is new Ada.Unchecked_Deallocation (Lazy_Data, Lazy_Data_Access);
 
 
     procedure Initialize
@@ -114,6 +82,14 @@ package body Kompsos is
         if This.Actual /= null then
             This.Actual.Counter := This.Actual.Counter - 1;
             if This.Actual.Counter = 0 then
+                if This.Actual.Kind = Conjunct_Node then
+                    if This.Actual.Con_Data /= null and then
+                        This.Actual.Con_Data.Kind = Many_Arg
+                    then
+                        Free (This.Actual.Con_Data.MInput);
+                    end if;
+                    Free (This.Actual.Con_Data);
+                end if;
                 Free (This.Actual);
             end if;
         end if;
@@ -243,27 +219,54 @@ package body Kompsos is
 
     --  States  --
 
+    function Variable_Index_Hash
+           (Key : in Variable)
+        return Ada.Containers.Hash_Type is
+    begin
+        return Ada.Containers.Hash_Type (Key mod Ada.Containers.Hash_Type'Modulus);
+    end Variable_Index_Hash;
+
+
+    procedure Insert
+           (This  : in out State;
+            Key   : in     Variable;
+            Value : in     Term'Class) is
+    begin
+        This.Binds.Append ((Key, Term (Value)));
+        This.Refs.Insert (Key, This.Binds.Last_Index);
+    end Insert;
+
+
     function Lookup
            (This  : in     State;
             Key   : in     Variable;
             Value :    out Term'Class)
         return Boolean
     is
-        Ptr : State_Component_Access := This.Ctrl.Actual;
+        use type Variable_Index_Maps.Cursor;
+        Result : constant Variable_Index_Maps.Cursor := This.Refs.Find (Key);
     begin
-        while Ptr /= null loop
-            for Index in Valid_Count range Valid_Count'First .. Ptr.Valid loop
-                if Ptr.Data (Index).Key = Key then
-                    Value := Term'Class (Ptr.Data (Index).Value);
-                    return True;
-                end if;
-            end loop;
-            Ptr := Ptr.Next.Ctrl.Actual;
-        end loop;
+        if Result /= Variable_Index_Maps.No_Element then
+            Value := This.Binds (Variable_Index_Maps.Element (Result)).Value;
+            return True;
+        end if;
         return False;
     end Lookup;
 
 
+    procedure Truncate
+           (This   : in out State;
+            Length : in     Long_Natural) is
+    begin
+        if This.Binds.Last_Index > Length then
+            for Index in Long_Positive range Length + 1 .. This.Binds.Last_Index loop
+                This.Refs.Exclude (This.Binds (Index).Key);
+            end loop;
+            This.Binds.Set_Length (Ada.Containers.Count_Type (Length));
+        end if;
+    end Truncate;
+
+
 
 
     -------------------
@@ -413,7 +416,7 @@ package body Kompsos is
                    (Kind     => Conjunct_Node,
                     Counter  => 1,
                     Con_Goal => This.Graph,
-                    Con_Data => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func))))),
+                    Con_Data => new Lazy_Data'((Kind => Zero_Arg, ZFunc => Func))))),
             Next_Var => This.Next_Var);
     end Conjunct;
 
@@ -438,10 +441,10 @@ package body Kompsos is
                    (Kind     => Conjunct_Node,
                     Counter  => 1,
                     Con_Goal => This.Graph,
-                    Con_Data => Lazy_Holders.To_Holder
-                       ((Kind   => One_Arg,
-                         OFunc  => Func,
-                         OInput => Term (Input)))))),
+                    Con_Data => new Lazy_Data'(
+                       (Kind   => One_Arg,
+                        OFunc  => Func,
+                        OInput => Term (Input)))))),
             Next_Var => This.Next_Var);
     end Conjunct;
 
@@ -467,10 +470,10 @@ package body Kompsos is
                    (Kind     => Conjunct_Node,
                     Counter  => 1,
                     Con_Goal => This.Graph,
-                    Con_Data => Lazy_Holders.To_Holder
-                       ((Kind   => Many_Arg,
-                         MFunc  => Func,
-                         MInput => Term_Array_Holders.To_Holder (Inputs)))))),
+                    Con_Data => new Lazy_Data'(
+                       (Kind   => Many_Arg,
+                        MFunc  => Func,
+                        MInput => new Term_Array'(Inputs)))))),
             Next_Var => This.Next_Var);
     end Conjunct;
 
@@ -490,30 +493,6 @@ package body Kompsos is
     --  Auxiliary Helpers  --
     -------------------------
 
-    --  Infinite State Loops  --
-
-    function Recurse
-           (This : in Goal)
-        return Goal is
-    begin
-        return Result : constant Goal :=
-           (Graph    => (Ada.Finalization.Controlled with
-                Actual => new Graph_Component'(
-                   (Kind     => Recurse_Node,
-                    Counter  => 1,
-                    Rec_Goal => This.Graph))),
-            Next_Var => This.Next_Var);
-    end Recurse;
-
-
-    procedure Recurse
-           (This : in out Goal) is
-    begin
-        This := This.Recurse;
-    end Recurse;
-
-
-
     --  Evaluation  --
 
     function Run
@@ -599,24 +578,22 @@ package body Kompsos is
            (Subst : in State)
         return Term is
     begin
-        if Subst.Ctrl.Actual = null then
+        if Subst.Binds.Is_Empty then
             return Empty_Term;
         end if;
         declare
-            Min_Pos : State_Component_Access := Subst.Ctrl.Actual;
-            Min_Ind : Valid_Count            := Valid_Count'First;
-            Marker  : State_Component_Access := Min_Pos;
+            Min_Index : Long_Positive := 1;
+            Min_Var   : Variable      := Subst.Binds.First_Element.Key;
         begin
-            while Marker /= null loop
-                for Index in Valid_Count range Valid_Count'First .. Marker.Valid loop
-                    if Marker.Data (Index).Key < Min_Pos.Data (Min_Ind).Key then
-                        Min_Pos := Marker;
-                        Min_Ind := Index;
-                    end if;
-                end loop;
-                Marker := Marker.Next.Ctrl.Actual;
+            for Index in Long_Positive range
+                Subst.Binds.First_Index + 1 .. Subst.Binds.Last_Index
+            loop
+                if Subst.Binds (Index).Key < Min_Var then
+                    Min_Index := Index;
+                    Min_Var   := Subst.Binds (Index).Key;
+                end if;
             end loop;
-            return Min_Pos.Data (Min_Ind).Value.Resolve (Subst);
+            return Subst.Binds (Min_Index).Value.Resolve (Subst);
         end;
     end Resolve_First;