Evaluation algorithm changed to inverted interleaved depth first search

1 files changed, 34 insertions, 62 deletions

diff --git a/src/kompsos.ads b/src/kompsos.ads
index dc9341f..ab50a08 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -8,7 +8,8 @@
 
 private with
 
-    Ada.Containers.Indefinite_Holders,
+    Ada.Containers.Hashed_Maps,
+    Ada.Containers.Vectors,
     Ada.Finalization;
 
 
@@ -212,16 +213,6 @@ package Kompsos is
     --  Auxiliary Helpers  --
     -------------------------
 
-    --  Infinite State Loops  --
-
-    function Recurse
-           (This : in Goal)
-        return Goal;
-
-    procedure Recurse
-           (This : in out Goal);
-
-
     --  Evaluation  --
 
     function Run
@@ -393,16 +384,8 @@ package Kompsos is
     with Pre => Inputs'Length = 3;
 
 
-    --  anyo  --
-    --  Skipped due to Recurse doing the same thing
-
-
-    --  nevero  --
-    --  Skipped since it just creates a failed Goal
-
-
-    --  alwayso  --
-    --  Skipped due to Recurse doing the same thing
+    --  anyo, nevero, alwayso  --
+    --  Skipped since these seem to be artifacts of conde, which isn't used here
 
 
 private
@@ -411,7 +394,7 @@ private
     --  Variables  --
     --  Around 2^31 possible Variables per Goal should be enough for anybody, right?
     subtype Long_Natural  is Long_Integer range 0 .. Long_Integer'Last;
-    subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last;
+    subtype Long_Positive is Long_Integer range 1 .. Long_Natural'Last;
 
     type Variable is new Long_Natural;
 
@@ -460,7 +443,7 @@ private
 
     Empty_Term : constant Term := (Ada.Finalization.Controlled with Actual => null);
 
-    package Term_Array_Holders is new Ada.Containers.Indefinite_Holders (Term_Array);
+    type Term_Array_Access is access Term_Array;
 
 
     --  States  --
@@ -470,40 +453,29 @@ private
         Value : Term;
     end record;
 
-    type Binding_Array is array (Positive range <>) of Binding;
-
-    --  Values of 2, 3, 4 here are honestly fairly similar, but of those, 4 seems to work best
-    Unroll_Max : constant Integer := 4;
-
-    subtype Valid_Count is Integer range 1 .. Unroll_Max;
-
-    type State_Component is limited record
-        Counter : Natural;
-        Valid   : Valid_Count;
-        Data    : Binding_Array (Valid_Count'Range);
-        Next    : State;
-    end record;
-
-    type State_Component_Access is access State_Component;
-
-    type State_Control is new Ada.Finalization.Controlled with record
-        Actual : State_Component_Access := null;
-    end record;
-
-    overriding procedure Initialize
-           (This : in out State_Control);
+    package Binding_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Long_Positive,
+        Element_Type => Binding);
 
-    overriding procedure Adjust
-           (This : in out State_Control);
+    function Variable_Index_Hash
+           (Key : in Variable)
+        return Ada.Containers.Hash_Type;
 
-    overriding procedure Finalize
-           (This : in out State_Control);
+    package Variable_Index_Maps is new Ada.Containers.Hashed_Maps
+       (Key_Type        => Variable,
+        Element_Type    => Long_Positive,
+        Hash            => Variable_Index_Hash,
+        Equivalent_Keys => "=");
 
     type State is record
-        Ctrl : State_Control := (Ada.Finalization.Controlled with Actual => null);
+        Binds : Binding_Vectors.Vector;
+        Refs  : Variable_Index_Maps.Map;
     end record;
 
-    type State_Access is access State;
+    procedure Insert
+           (This  : in out State;
+            Key   : in     Variable;
+            Value : in     Term'Class);
 
     function Lookup
            (This  : in     State;
@@ -511,7 +483,13 @@ private
             Value :    out Term'Class)
         return Boolean;
 
-    Empty_State : constant State := (Ctrl => (Ada.Finalization.Controlled with Actual => null));
+    procedure Truncate
+           (This   : in out State;
+            Length : in     Long_Natural);
+
+    Empty_State : constant State :=
+       (Binds => Binding_Vectors.Empty_Vector,
+        Refs  => Variable_Index_Maps.Empty_Map);
 
 
     --  Goals  --
@@ -544,17 +522,13 @@ private
             OInput : Term;
         when Many_Arg =>
             MFunc  : Junction_Many_Func;
-            MInput : Term_Array_Holders.Holder;
+            MInput : Term_Array_Access;
         end case;
     end record;
 
-    package Lazy_Holders is new Ada.Containers.Indefinite_Holders (Lazy_Data);
+    type Lazy_Data_Access is access Lazy_Data;
 
-    type Node_Kind is
-       (Unify_Node,
-        Disjunct_Node,
-        Conjunct_Node,
-        Recurse_Node);
+    type Node_Kind is (Unify_Node, Disjunct_Node, Conjunct_Node);
 
     type Graph_Component (Kind : Node_Kind) is limited record
         Counter : Natural;
@@ -568,9 +542,7 @@ private
             Dis_Goal2 : aliased Goal_Graph;
         when Conjunct_Node =>
             Con_Goal  : aliased Goal_Graph;
-            Con_Data  : Lazy_Holders.Holder;
-        when Recurse_Node =>
-            Rec_Goal  : aliased Goal_Graph;
+            Con_Data  : Lazy_Data_Access;
         end case;
     end record;