Evaluation algorithm changed to inverted interleaved depth first search

9 files changed, 450 insertions, 743 deletions

diff --git a/readme.md b/readme.md
index 28b1246..8b5fd08 100644
--- a/readme.md
+++ b/readme.md
@@ -78,12 +78,6 @@ placing them all in the main package would not have made sense due to the math
 operations needing to know what zero and one are. It would also have made the
 main package unreasonably large.
 
-Internally a Goal is structured as a directed acyclic graph. Evaluation of
-a Goal involves walking the graph while applying relevant operations to the
-base State and expanding any Conjuncts to more of the graph as they are
-encountered. The expanded portions, bookkeeping data, and memoised partial
-results are all discarded once evaluation is complete.
-
 The various cond operations are completely absent, as this implementation
 instead follows microKanren for its core workings. The cond variations do not
 really make sense in an object oriented context anyway. Use a Disjunct
@@ -95,13 +89,18 @@ implemented. The practical implication of this is there will be a lot of use
 of the `&` operator when using this library, as can be seen in the example
 programs.
 
-The State datatype makes use of custom unrolled linked lists, and the
-bookkeeping data in the Collector package uses a custom directed acyclic graph
-structure that reflects the main Goal graph. This is done instead of using
-Vectors or Maps from the standard library both to improve speed and reduce
-memory requirements. The improvement due to tail sharing is considerable,
-despite the theoretically expensive operations involved in walking the list to
-reify a variable.
+Internally a Goal is structured as a directed acyclic graph. Evaluation of a
+Goal involves inverting the arrows in the graph, interleaving those arrows
+according to Disjunct choices made from the top to get there, and then running
+a depth-first search from the bottom upwards using the inverted graph. When
+a Conjunct node is encountered it is expanded, inverted, and interleaved in a
+similar way before the search continues. The inversions and expanded portions
+are all discarded once evaluation is complete.
+
+The State datatype makes use of a Vector of Variable->Term bindings and a
+Hashed_Map to get from Variable to the index for the Vector. Both are needed so
+that lookups can be fast and truncations of the State to remove the newest
+bindings are easy to do when backtracking during the depth-first search.
 
 
 
diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb
index b8fc205..db499f2 100644
--- a/src/kompsos-collector.adb
+++ b/src/kompsos-collector.adb
@@ -5,10 +5,13 @@
 
 --  See license.txt for further details
 
+
 with
 
-    Ada.Assertions,
-    Ada.Unchecked_Deallocation;
+    Ada.Containers,
+    Ada.Unchecked_Deallocation,
+    System.Address_To_Access_Conversions,
+    System.Storage_Elements;
 
 
 package body Kompsos.Collector is
@@ -18,15 +21,22 @@ package body Kompsos.Collector is
     --  Progress State  --
     ----------------------
 
-    Book_Root   : Book_Node_Access := null;
-    Loose_Books : Loose_Book_Vectors.Vector;
+    Conjunct_Goals : Goal_Access_Vectors.Vector;
 
     Global_Var : Variable := Relation.Next_Var;
 
-    Next_Index  : Long_Positive := 1;
-    Next_State  : State;
-    State_Valid : Boolean       := False;
-    Exhausted   : Boolean       := False;
+    Up_Map    : Upwards_Maps.Map;
+    Up_Vector : Upwards_Vectors.Vector;
+
+    Do_Walk      : access procedure;
+    Walk_Trail   : Breadcrumb_Vectors.Vector;
+    Location     : Graph_Component_Access;
+    Local_Cursor : Upwards_Maps.Cursor;
+    Next_Pick    : Positive;
+
+    Result      : State   := Within;
+    State_Valid : Boolean := False;
+    Exhausted   : Boolean := False;
 
 
 
@@ -35,53 +45,84 @@ package body Kompsos.Collector is
     --  Memory Management  --
     -------------------------
 
-    procedure Free is new Ada.Unchecked_Deallocation (Book_Node, Book_Node_Access);
-    procedure Free is new Ada.Unchecked_Deallocation (Cache_Entry, Cache_Entry_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 Collector_Final_Controller) is
     begin
-        Reset (Relation.Graph.Actual, Book_Root);
+        for Ptr of Conjunct_Goals loop
+            Free (Ptr);
+        end loop;
     end Finalize;
 
 
 
 
-    ------------------------
-    --  Internal Helpers  --
-    ------------------------
+    -----------------
+    --  Datatypes  --
+    -----------------
 
-    --  Unification  --
+    function "<"
+           (Left, Right : in Disjuncts_Chosen)
+        return Boolean is
+    begin
+        if Left.Is_Empty then
+            return not Right.Is_Empty;
+        elsif Right.Is_Empty then
+            return False;
+        end if;
+        declare
+            Left_Spot  : Natural := Left.Last_Index;
+            Right_Spot : Natural := Right.Last_Index;
+        begin
+            loop
+                if Left (Left_Spot) < Right (Right_Spot) then
+                    return True;
+                elsif Left (Left_Spot) = Right (Right_Spot) then
+                    Left_Spot := Left_Spot - 1;
+                    Right_Spot := Right_Spot - 1;
+                    if Left_Spot = 0 then
+                        return Right_Spot /= 0;
+                    elsif Right_Spot = 0 then
+                        return False;
+                    end if;
+                else
+                    return False;
+                end if;
+            end loop;
+        end;
+    end "<";
 
-    Use_New_Node : Boolean := False;
 
-    function Append
-           (This  : in State;
-            Key   : in Variable;
-            Value : in Term)
-        return State is
+    function "<"
+           (Left, Right : in Parent_Arrow)
+        return Boolean is
     begin
-        if Use_New_Node or else This.Ctrl.Actual = null or else
-            (This.Ctrl.Actual /= null and then This.Ctrl.Actual.Valid = Valid_Count'Last)
-        then
-            Use_New_Node := False;
-            return (Ctrl => (Ada.Finalization.Controlled with
-                Actual => new State_Component'(
-                    Counter => 1,
-                    Valid   => Valid_Count'First,
-                    Data    => (1 => (Key, Value), others => <>),
-                    Next    => This)));
-        else
-            return Result : constant State := This do
-                Result.Ctrl.Actual.Valid := Result.Ctrl.Actual.Valid + 1;
-                Result.Ctrl.Actual.Data (Result.Ctrl.Actual.Valid) := (Key, Value);
-            end return;
-        end if;
-    end Append;
+        return Left.Order < Right.Order;
+    end "<";
+
+
+    package Graph_Comp_Conv is new System.Address_To_Access_Conversions (Graph_Component);
+
+    function Graph_Component_Access_Hash
+           (Key : in Graph_Component_Access)
+        return Ada.Containers.Hash_Type
+    is
+        use Ada.Containers, Graph_Comp_Conv, System.Storage_Elements;
+    begin
+        return Hash_Type (To_Integer (To_Address (Object_Pointer (Key))) mod Hash_Type'Modulus);
+    end Graph_Component_Access_Hash;
+
+
 
 
+    ------------------------
+    --  Internal Helpers  --
+    ------------------------
+
+    --  Unification  --
+
     procedure Walk
            (This : in     State;
             Item : in out Term)
@@ -95,17 +136,16 @@ package body Kompsos.Collector is
 
 
     function Do_Unify
-           (Potential   : in     State;
-            Left, Right : in     Term'Class;
-            Extended    :    out State)
+           (Subst       : in out State;
+            Left, Right : in     Term'Class)
         return Boolean
     is
         Real_Left  : Term := Term (Left);
         Real_Right : Term := Term (Right);
     begin
         --  Resolve Variable substitution
-        Walk (Potential, Real_Left);
-        Walk (Potential, Real_Right);
+        Walk (Subst, Real_Left);
+        Walk (Subst, Real_Right);
 
         --  Unify equal Variable/Atom/Null Terms
         if (Real_Left.Kind = Var_Term and then
@@ -116,24 +156,23 @@ package body Kompsos.Collector is
             Real_Left = Real_Right) or else
            (Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term)
         then
-            Extended := Potential;
             return True;
         end if;
 
         --  Unify Variable and other Terms by introducing a new substitution
         if Real_Left.Kind = Var_Term then
-            Extended := Append (Potential, Real_Left.Var, Real_Right);
+            Insert (Subst, Real_Left.Var, Real_Right);
             return True;
         end if;
         if Real_Right.Kind = Var_Term then
-            Extended := Append (Potential, Real_Right.Var, Real_Left);
+            Insert (Subst, Real_Right.Var, Real_Left);
             return True;
         end if;
 
         --  Unify Pair Terms by unifying each corresponding part
         if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then
-            return Do_Unify (Potential, Real_Left.Left, Real_Right.Left, Extended) and then
-                Do_Unify (Extended, Real_Left.Right, Real_Right.Right, Extended);
+            return Do_Unify (Subst, Real_Left.Left, Real_Right.Left) and then
+                Do_Unify (Subst, Real_Left.Right, Real_Right.Right);
         end if;
 
         --  Otherwise unification fails
@@ -142,402 +181,212 @@ package body Kompsos.Collector is
 
 
 
-    --  Result Collection --
+    --  Interleaved Graph Inversion  --
 
-    function Call_Lazy
-           (This : in Goal;
-            Data : in Lazy_Holders.Holder)
-        return Goal
+    function Null_Join
+           (Left, Right : in Graph_Component_Access)
+        return Graph_Component_Access is
+    begin
+        return (if Left = null then Right else Left);
+    end Null_Join;
+
+
+    procedure Sorted_Insert
+           (Quiver : in out Parent_Arrow_Vectors.Vector;
+            Arrow  : in     Parent_Arrow)
     is
-        Ref : constant Lazy_Holders.Constant_Reference_Type := Data.Constant_Reference;
+        Position : Parent_Arrow_Vectors.Extended_Index := Quiver.Last_Index + 1;
     begin
-        case Ref.Kind is
-        when Zero_Arg =>
-            return Ref.ZFunc (This);
-        when One_Arg  =>
-            return Ref.OFunc (This, Ref.OInput);
-        when Many_Arg =>
-            return Ref.MFunc (This, Term_Array_Holders.Constant_Reference (Ref.MInput));
-        end case;
-    end Call_Lazy;
+        while Position > 1 and then Arrow < Quiver (Position - 1) loop
+            Position := Position - 1;
+        end loop;
+        Quiver.Insert (Position, Arrow);
+    end Sorted_Insert;
 
 
-    procedure Do_Reset
-           (Ptr   : in     Graph_Component_Access;
-            Book  : in out Book_Node_Access;
-            Extra : in out Book_Node_Vectors.Vector) is
+    function Connect_Up_Map
+           (Parent, Child : in Graph_Component_Access;
+            Level         : in Disjuncts_Passed;
+            Choices       : in Disjuncts_Chosen)
+        return Boolean
+    is
+        use type Upwards_Maps.Cursor, Parent_Arrow_Vectors.Vector;
+        Index_Cursor : constant Upwards_Maps.Cursor := Up_Map.Find (Child);
     begin
-        if Ptr = null or Book = null then
-            return;
+        if Index_Cursor = Upwards_Maps.No_Element then
+            Up_Vector.Append ((Level, Parent_Arrow_Vectors.Empty_Vector & (Parent, Choices)));
+            Up_Map.Insert (Child, Up_Vector.Last_Index);
+            return True;
+        else
+            Sorted_Insert
+               (Up_Vector (Upwards_Maps.Element (Index_Cursor)).Parents,
+                (Parent, Choices));
+            return False;
         end if;
+    end Connect_Up_Map;
 
-        --  Delete cache
-        if Book.Cache /= null then
-            for Item of Book.Cache.Data loop
-                Free (Item.Data);
-            end loop;
-            Free (Book.Cache);
-        end if;
 
-        --  Delete all bookkeeping for lower nodes
-        case Book.Data.Kind is
+    procedure Build_Up_Map
+           (Top, Bottom : in     Graph_Component_Access;
+            Level       : in     Disjuncts_Passed;
+            Choices     : in out Disjuncts_Chosen) is
+    begin
+        if Top = null then
+            return;
+        end if;
+        case Top.Kind is
         when Unify_Node =>
-            Do_Reset (Ptr.Uni_Goal.Actual, Book.Next1, Extra);
+            if Connect_Up_Map (Top, Null_Join (Top.Uni_Goal.Actual, Bottom), Level, Choices) then
+                Build_Up_Map (Top.Uni_Goal.Actual, Bottom, Level, Choices);
+            end if;
         when Disjunct_Node =>
-            Do_Reset (Ptr.Dis_Goal1.Actual, Book.Next1, Extra);
-            Do_Reset (Ptr.Dis_Goal2.Actual, Book.Next2, Extra);
+            if Connect_Up_Map (Top, Null_Join (Top.Dis_Goal1.Actual, Bottom), Level + 1, Choices)
+            then
+                Build_Up_Map (Top.Dis_Goal1.Actual, Bottom, Level + 1, Choices);
+            end if;
+            Choices.Append (Level + 1);
+            if Connect_Up_Map (Top, Null_Join (Top.Dis_Goal2.Actual, Bottom), Level + 1, Choices)
+            then
+                Build_Up_Map (Top.Dis_Goal2.Actual, Bottom, Level + 1, Choices);
+            end if;
+            Choices.Delete_Last;
         when Conjunct_Node =>
-            Do_Reset (Ptr.Con_Goal.Actual, Book.Next1, Extra);
-            if Book.Data.Con_Part /= null then
-                Reset (Book.Data.Con_Part.Graph.Actual, Book.Next2);
-                Free (Book.Data.Con_Part);
+            if Connect_Up_Map (Top, Null_Join (Top.Con_Goal.Actual, Bottom), Level, Choices) then
+                Build_Up_Map (Top.Con_Goal.Actual, Bottom, Level, Choices);
             end if;
-            Free (Book.Data.Con_Base);
-        when Recurse_Node =>
-            Do_Reset (Ptr.Rec_Goal.Actual, Book.Next1, Extra);
         end case;
-
-        --  Set aside common nodes to be deleted later
-        if Ptr.Counter > 1 then
-            if not Extra.Contains (Book) then
-                Extra.Append (Book);
-            end if;
-        else
-            Free (Book);
-        end if;
-    end Do_Reset;
+    end Build_Up_Map;
 
 
-    procedure Reset
-           (Ptr  : in     Graph_Component_Access;
-            Book : in out Book_Node_Access)
-    is
-        Extra : Book_Node_Vectors.Vector;
-    begin
-        Do_Reset (Ptr, Book, Extra);
-
-        --  Handle common nodes
-        for Item of Extra loop
-            --  Ensure that Book doesn't end up dangling
-            if Item = Book then
-                Free (Book);
-            else
-                Free (Item);
-            end if;
-        end loop;
-    end Reset;
 
+    --  Conjunct Expansion  --
 
-    function New_Book_Factory
-           (Kind : in Node_Kind)
-        return Book_Node_Access is
+    function Call_Lazy
+           (This : in Goal;
+            Data : in Lazy_Data)
+        return Goal is
     begin
-        --  This is needed because Ada does not allow declaring an object using
-        --  a discriminant that is not statically known.
-        case Kind is
-        when Unify_Node =>
-            return new Book_Node'(Data => (Kind => Unify_Node,    others => <>), others => <>);
-        when Disjunct_Node =>
-            return new Book_Node'(Data => (Kind => Disjunct_Node, others => <>), others => <>);
-        when Conjunct_Node =>
-            return new Book_Node'(Data => (Kind => Conjunct_Node, others => <>), others => <>);
-        when Recurse_Node =>
-            return new Book_Node'(Data => (Kind => Recurse_Node,  others => <>), others => <>);
+        case Data.Kind is
+        when Zero_Arg =>
+            return Data.ZFunc (This);
+        when One_Arg  =>
+            return Data.OFunc (This, Data.OInput);
+        when Many_Arg =>
+            return Data.MFunc (This, Data.MInput.all);
         end case;
-    end New_Book_Factory;
+    end Call_Lazy;
 
 
-    function New_Book
-           (Ptr : in Graph_Component_Access)
-        return Book_Node_Access is
+    procedure Expand_Conjunct
+           (Node : in Graph_Component_Access)
+    is
+        Old_Choices : Disjuncts_Chosen :=
+            Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Order;
     begin
-        pragma Assert (Ptr.Counter /= 0);
-        if Ptr.Counter = 1 or Ptr = Relation.Graph.Actual then
-            return New_Book_Factory (Ptr.Kind);
-        else
-            return Acc : constant Book_Node_Access := New_Book_Factory (Ptr.Kind) do
-                Loose_Books.Append ((1, Ptr, Acc));
-            end return;
-        end if;
-    end New_Book;
-
-
-    function Connect_Loose
-           (Ptr : in Graph_Component_Access)
-        return Book_Node_Access is
+        Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Delete (Next_Pick);
+        Conjunct_Goals.Append (new Goal'(
+            Call_Lazy
+               ((Graph    => (Ada.Finalization.Controlled with Actual => null),
+                 Next_Var => Global_Var),
+                Node.Con_Data.all)));
+        Global_Var := Conjunct_Goals.Last_Element.Next_Var;
+        declare
+            Depth : constant Disjuncts_Passed :=
+                Up_Vector (Upwards_Maps.Element (Local_Cursor)).Depth;
+        begin
+            Build_Up_Map (Conjunct_Goals.Last_Element.Graph.Actual, Location, Depth, Old_Choices);
+        end;
+        Up_Map.Insert (Conjunct_Goals.Last_Element.Graph.Actual, Up_Map.Element (Node));
+    end Expand_Conjunct;
+
+
+
+    --  Upwards Depth First Search  --
+
+    function Choose_Another_Way
+        return Boolean
+    is
+        Marker : Natural := Walk_Trail.Last_Index;
+        Crumb : Breadcrumb;
     begin
-        for Index in Loose_Books.First_Index .. Loose_Books.Last_Index loop
-            if Loose_Books.Element (Index).Ptr = Ptr then
-                return Acc : constant Book_Node_Access := Loose_Books.Element (Index).Book do
-                    Loose_Books (Index).Used := Loose_Books (Index).Used + 1;
-                    if Loose_Books.Element (Index).Used >= Ptr.Counter then
-                        Loose_Books.Delete (Index);
-                    end if;
-                end return;
+        while Marker /= Breadcrumb_Vectors.No_Index loop
+            Crumb := Walk_Trail (Marker);
+            Location := Crumb.Choice_Node;
+            Local_Cursor := Up_Map.Find (Location);
+            if Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Last_Index >=
+                Crumb.Option + 1
+            then
+                Next_Pick := Crumb.Option + 1;
+                Truncate (Result, Crumb.State_Size);
+                Walk_Trail.Set_Length (Ada.Containers.Count_Type (Marker - 1));
+                return True;
+            else
+                Marker := Marker - 1;
             end if;
         end loop;
-        return null;
-    end Connect_Loose;
+        return False;
+    end Choose_Another_Way;
 
 
-    function Do_Get_Next
-           (Ptr    : in     Graph_Component_Access;
-            Book   : in out Book_Node_Access;
-            Base   : in     State;
-            Index  : in     Long_Positive;
-            Result :    out State)
-        return Boolean is
+    procedure Walk_Graph is
+        use type Upwards_Maps.Cursor;
+        Ptr : Graph_Component_Access;
     begin
-        case Ptr.Kind is
-        when Unify_Node =>
-            if Book = null then
-                Book := New_Book (Ptr);
-            end if;
-            while Get_Next
-               (Ptr.Uni_Goal'Unchecked_Access,
-                Book.Next1, Base,
-                Index + Book.Data.Uni_Offset,
-                Result)
-            loop
-                if Do_Unify (Result, Ptr.Uni_Term1, Ptr.Uni_Term2, Result) then
-                    return True;
-                else
-                    Book.Data.Uni_Offset := Book.Data.Uni_Offset + 1;
-                end if;
-            end loop;
-            return False;
-
-        when Disjunct_Node =>
-            if Book = null then
-                Book := New_Book (Ptr);
-            end if;
-            if Book.Data.Dis_Gone1 then
-                if Book.Data.Dis_Gone2 then
-                    return False;
-                elsif Get_Next
-                   (Ptr.Dis_Goal2'Unchecked_Access,
-                    Book.Next2, Base,
-                    Book.Data.Dis_Next2,
-                    Result)
-                then
-                    Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1;
-                    return True;
-                else
-                    Book.Data.Dis_Gone2 := True;
-                    return False;
+        loop
+            if Location = null or else Location.Kind /= Unify_Node or else
+                Do_Unify (Result, Location.Uni_Term1, Location.Uni_Term2)
+            then
+                if Local_Cursor = Upwards_Maps.No_Element then
+                    State_Valid := True;
+                    return;
                 end if;
-            elsif Book.Data.Dis_Gone2 then
-                if Get_Next
-                   (Ptr.Dis_Goal1'Unchecked_Access,
-                    Book.Next1, Base,
-                    Book.Data.Dis_Next1,
-                    Result)
-                then
-                    Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1;
-                    return True;
-                else
-                    Book.Data.Dis_Gone1 := True;
-                    return False;
+                Ptr := Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node;
+                if Ptr.Kind = Conjunct_Node then
+                    Expand_Conjunct (Ptr);
                 end if;
-            elsif Book.Data.Dis_Flag then
-                if Get_Next
-                   (Ptr.Dis_Goal1'Unchecked_Access,
-                    Book.Next1, Base,
-                    Book.Data.Dis_Next1,
-                    Result)
-                then
-                    Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1;
-                    Book.Data.Dis_Flag := not Book.Data.Dis_Flag;
-                    return True;
-                else
-                    Book.Data.Dis_Gone1 := True;
-                    if Get_Next
-                       (Ptr.Dis_Goal2'Unchecked_Access,
-                        Book.Next2, Base,
-                        Book.Data.Dis_Next2,
-                        Result)
-                    then
-                        Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1;
-                        return True;
-                    else
-                        Book.Data.Dis_Gone2 := True;
-                        return False;
-                    end if;
+                if Up_Vector (Upwards_Maps.Element (Local_Cursor)).Parents.Last_Index > 1 then
+                    Walk_Trail.Append ((Location, Next_Pick, Result.Binds.Last_Index));
                 end if;
+                Location := Up_Vector
+                    (Upwards_Maps.Element (Local_Cursor)).Parents (Next_Pick).Node;
+                Local_Cursor := Up_Map.Find (Location);
+                Next_Pick := 1;
             else
-                if Get_Next
-                   (Ptr.Dis_Goal2'Unchecked_Access,
-                    Book.Next2, Base,
-                    Book.Data.Dis_Next2,
-                    Result)
-                then
-                    Book.Data.Dis_Next2 := Book.Data.Dis_Next2 + 1;
-                    Book.Data.Dis_Flag := not Book.Data.Dis_Flag;
-                    return True;
-                else
-                    Book.Data.Dis_Gone2 := True;
-                    if Get_Next
-                       (Ptr.Dis_Goal1'Unchecked_Access,
-                        Book.Next1, Base,
-                        Book.Data.Dis_Next1,
-                        Result)
-                    then
-                        Book.Data.Dis_Next1 := Book.Data.Dis_Next1 + 1;
-                        return True;
-                    else
-                        Book.Data.Dis_Gone1 := True;
-                        return False;
-                    end if;
-                end if;
-            end if;
-
-        when Conjunct_Node =>
-            if Book = null then
-                Book := New_Book (Ptr);
-                if not Get_Next (Ptr.Con_Goal'Unchecked_Access, Book.Next1, Base, 1, Result) then
-                    Book.Data.Con_Gone := True;
-                else
-                    Book.Data.Con_Base := new State'(Result);
-                    Book.Data.Con_Part := new Goal'(
-                        Call_Lazy
-                           ((Graph    => (Ada.Finalization.Controlled with Actual => null),
-                             Next_Var => Global_Var),
-                            Ptr.Con_Data));
-                    Global_Var := Book.Data.Con_Part.Next_Var;
-                end if;
-            end if;
-            if Book.Data.Con_Gone then
-                return False;
-            end if;
-            while not Get_Next
-               (Constant_Graph_Access'(Book.Data.Con_Part.Graph'Access),
-                Book.Next2, Book.Data.Con_Base.all,
-                Book.Data.Con_Next,
-                Result)
-            loop
-                Reset (Book.Data.Con_Part.Graph.Actual, Book.Next2);
-                Book.Data.Con_From := Book.Data.Con_From + 1;
-                if Get_Next
-                   (Ptr.Con_Goal'Unchecked_Access,
-                    Book.Next1, Base,
-                    Book.Data.Con_From,
-                    Result)
-                then
-                    Book.Data.Con_Base.all := Result;
-                    Book.Data.Con_Next := 1;
-                else
-                    Book.Data.Con_Gone := True;
-                    Free (Book.Data.Con_Part);
-                    Free (Book.Data.Con_Base);
-                    return False;
+                if not Choose_Another_Way then
+                    State_Valid := False;
+                    Exhausted := True;
+                    return;
                 end if;
-            end loop;
-            Book.Data.Con_Next := Book.Data.Con_Next + 1;
-            return True;
-
-        when Recurse_Node =>
-            if Book = null then
-                Book := New_Book (Ptr);
             end if;
-            if Book.Next1 = null then
-                Book.Next1 := Connect_Loose (Ptr.Rec_Goal.Actual);
-            end if;
-            if Ptr.Rec_Goal.Actual /= null then
-                --  Reach forwards to ensure the next node has cached results
-                --  even if it normally wouldn't have and that those results
-                --  are not discarded, so we can loop through them as needed.
-                if Book.Next1 = null then
-                    Book.Next1 := New_Book (Ptr.Rec_Goal.Actual);
-                    Book.Next1.Cache := new Cache_Entry'(True, State_Vectors.Empty_Vector);
-                elsif Book.Next1.Cache = null then
-                    Book.Next1.Cache := new Cache_Entry'(True, State_Vectors.Empty_Vector);
-                else
-                    Book.Next1.Cache.Keep := True;
-                end if;
-            end if;
-            if Book.Data.Rec_Gone then
-                return False;
-            end if;
-            while not Get_Next
-               (Ptr.Rec_Goal'Unchecked_Access,
-                Book.Next1, Base,
-                Book.Data.Rec_Next,
-                Result)
-            loop
-                if Book.Data.Rec_Next = 1 then
-                    Book.Data.Rec_Gone := True;
-                    return False;
-                else
-                    Book.Data.Rec_Next := 1;
-                end if;
-            end loop;
-            Book.Data.Rec_Next := Book.Data.Rec_Next + 1;
-            return True;
-        end case;
-    end Do_Get_Next;
+        end loop;
+    end Walk_Graph;
 
 
-    function Get_Next
-           (Ptr    : in     Constant_Graph_Access;
-            Book   : in out Book_Node_Access;
-            Base   : in     State;
-            Index  : in     Long_Positive;
-            Result :    out State)
-        return Boolean is
+    procedure Continue_Walk is
     begin
-        if Ptr = null then
-            return False;
-        end if;
-
-        --  Lowest node in the graph always returns the Base State
-        if Ptr.Actual = null then
-            if Index = 1 then
-                Result := Base;
-                Use_New_Node := True;
-                return True;
-            else
-                return False;
-            end if;
+        if Choose_Another_Way then
+            Walk_Graph;
+        else
+            State_Valid := False;
+            Exhausted := True;
         end if;
+    end Continue_Walk;
 
-        --  Attempt to connect common bookkeeping branches
-        if Book = null then
-            Book := Connect_Loose (Ptr.Actual);
-        end if;
 
-        --  If cached results exist, use those
-        if Book /= null and then Book.Cache /= null and then
-            Index <= Book.Cache.Data.Last_Index
-        then
-            Result := Book.Cache.Data (Index).Data.all;
-            Book.Cache.Data (Index).Used := Book.Cache.Data (Index).Used + 1;
-            if not Book.Cache.Keep and then Book.Cache.Data (Index).Used >= Ptr.Actual.Counter then
-                Free (Book.Cache.Data (Index).Data);
-            end if;
-            Use_New_Node := True;
-            return True;
+    procedure Start_Walk is
+        use type Upwards_Maps.Cursor;
+    begin
+        Location := null;
+        Local_Cursor := Up_Map.Find (Location);
+        if Local_Cursor = Upwards_Maps.No_Element then
+            State_Valid := True;
+            Exhausted := True;
+        else
+            Do_Walk := Continue_Walk'Access;
+            Next_Pick := 1;
+            Walk_Graph;
         end if;
-
-        --  Otherwise, actual result calculation
-        return Found : constant Boolean :=
-            Do_Get_Next (Ptr.Actual, Book, Base, Index, Result)
-        do
-            if Found then
-                --  Cache results as needed
-                if Ptr.Actual.Counter > 1 and then
-                    Ptr.Actual /= Relation.Graph.Actual and then
-                    Book.Cache = null
-                then
-                    Book.Cache := new Cache_Entry'(False, State_Vectors.Empty_Vector);
-                end if;
-                if Book.Cache /= null then
-                    pragma Assert (Index = Book.Cache.Data.Last_Index + 1);
-                    Book.Cache.Data.Append ((1, new State'(Result)));
-                    Use_New_Node := True;
-                end if;
-            end if;
-        end return;
-    end Get_Next;
+    end Start_Walk;
 
 
 
@@ -547,21 +396,14 @@ package body Kompsos.Collector is
     -----------------------
 
     function Has_Next
-        return Boolean
-    is
-        Ptr : constant Constant_Graph_Access := Relation.Graph'Access;
+        return Boolean is
     begin
         if State_Valid then
             return True;
         elsif Exhausted then
             return False;
         else
-            State_Valid := Get_Next (Ptr, Book_Root, Within, Next_Index, Next_State);
-            if not State_Valid then
-                Exhausted := True;
-            else
-                Next_Index := Next_Index + 1;
-            end if;
+            Do_Walk.all;
             return State_Valid;
         end if;
     end Has_Next;
@@ -572,7 +414,7 @@ package body Kompsos.Collector is
     begin
         if Has_Next then
             State_Valid := False;
-            return Next_State;
+            return Result;
         else
             raise State_Not_Found_Error;
         end if;
@@ -585,22 +427,24 @@ package body Kompsos.Collector is
     begin
         if Has_Next then
             State_Valid := False;
-            return Next_State;
+            return Result;
         else
             return Default;
         end if;
     end Next;
 
 
-    procedure Reset is
-    begin
-        Reset (Relation.Graph.Actual, Book_Root);
-        Next_Index  := 1;
-        State_Valid := False;
-        Exhausted   := False;
-    end Reset;
 
 
+begin
+
+    declare
+        Temp : Positive_Vectors.Vector := Positive_Vectors.Empty_Vector;
+    begin
+        Build_Up_Map (Relation.Graph.Actual, null, 0, Temp);
+    end;
+    Do_Walk := Start_Walk'Access;
+
 end Kompsos.Collector;
 
 
diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads
index ac451c2..da3c592 100644
--- a/src/kompsos-collector.ads
+++ b/src/kompsos-collector.ads
@@ -8,6 +8,7 @@
 
 private with
 
+    Ada.Containers.Hashed_Maps,
     Ada.Containers.Vectors,
     Ada.Finalization;
 
@@ -31,108 +32,80 @@ package Kompsos.Collector is
            (Default : in State)
         return State;
 
-    procedure Reset;
-
 
 private
 
 
-    type Goal_Access is access all Goal;
-    type Constant_Goal_Access is access constant Goal;
-
-    type Graph_Access is access all Goal_Graph;
-    type Constant_Graph_Access is access constant Goal_Graph;
-
-
-
-    type Eval_Data (Kind : Node_Kind := Unify_Node) is record
-        case Kind is
-        when Unify_Node =>
-            Uni_Offset : Long_Natural  := 0;
-        when Disjunct_Node =>
-            Dis_Flag   : Boolean       := True;
-            Dis_Next1  : Long_Positive := 1;
-            Dis_Next2  : Long_Positive := 1;
-            Dis_Gone1  : Boolean       := False;
-            Dis_Gone2  : Boolean       := False;
-        when Conjunct_Node =>
-            Con_From   : Long_Positive := 1;
-            Con_Base   : State_Access  := null;
-            Con_Part   : Goal_Access   := null;
-            Con_Next   : Long_Positive := 1;
-            Con_Gone   : Boolean       := False;
-        when Recurse_Node =>
-            Rec_Next   : Long_Positive := 1;
-            Rec_Gone   : Boolean       := False;
-        end case;
-    end record;
+    --  Interleaved Graph Inversion  --
 
+    package Positive_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Positive);
 
+    subtype Disjuncts_Chosen is Positive_Vectors.Vector;
 
-    type Cached_State is record
-        Used : Positive     := 1;
-        Data : State_Access := null;
-    end record;
-
-    package State_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => Cached_State);
+    function "<"
+           (Left, Right : in Disjuncts_Chosen)
+        return Boolean;
 
-    type Cache_Entry is record
-        Keep : Boolean              := False;
-        Data : State_Vectors.Vector := State_Vectors.Empty_Vector;
+    type Parent_Arrow is record
+        Node  : Graph_Component_Access;
+        Order : Disjuncts_Chosen;
     end record;
 
-    type Cache_Entry_Access is access Cache_Entry;
-
-
+    function "<"
+           (Left, Right : in Parent_Arrow)
+        return Boolean;
 
-    type Book_Node;
+    package Parent_Arrow_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Parent_Arrow);
 
-    type Book_Node_Access is access Book_Node;
+    subtype Disjuncts_Passed is Natural;
 
-    type Book_Node is record
-        Data  : Eval_Data;
-        Cache : Cache_Entry_Access := null;
-        Next1 : Book_Node_Access   := null;
-        Next2 : Book_Node_Access   := null;
+    type Node_Upwards is record
+        Depth   : Disjuncts_Passed;
+        Parents : Parent_Arrow_Vectors.Vector;
     end record;
 
+    package Upwards_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Node_Upwards);
 
+    function Graph_Component_Access_Hash
+           (Key : in Graph_Component_Access)
+        return Ada.Containers.Hash_Type;
 
-    --  Used to keep track of and connect up bookkeeping nodes corresponding to
-    --  graph nodes with more than one parent, so as to avoid ending up with an
-    --  exponential tree instead of the desired directed acyclic graph.
+    package Upwards_Maps is new Ada.Containers.Hashed_Maps
+       (Key_Type        => Graph_Component_Access,
+        Element_Type    => Positive,
+        Hash            => Graph_Component_Access_Hash,
+        Equivalent_Keys => "=");
 
-    type Loose_Book is record
-        Used : Positive               := 1;
-        Ptr  : Graph_Component_Access := null;
-        Book : Book_Node_Access       := null;
-    end record;
 
-    package Loose_Book_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => Loose_Book);
+    --  Conjunct Expansion  --
 
-    package Book_Node_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Long_Positive,
-        Element_Type => Book_Node_Access);
+    type Goal_Access is access all Goal;
 
+    package Goal_Access_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Goal_Access);
 
 
-    procedure Reset
-           (Ptr  : in     Graph_Component_Access;
-            Book : in out Book_Node_Access);
+    --  Upwards Depth First Search  --
 
-    function Get_Next
-           (Ptr    : in     Constant_Graph_Access;
-            Book   : in out Book_Node_Access;
-            Base   : in     State;
-            Index  : in     Long_Positive;
-            Result :    out State)
-        return Boolean;
+    type Breadcrumb is record
+        Choice_Node : Graph_Component_Access;
+        Option      : Positive;
+        State_Size  : Long_Natural;
+    end record;
+
+    package Breadcrumb_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Positive,
+        Element_Type => Breadcrumb);
 
 
+    --  Cleanup  --
 
     type Collector_Final_Controller is new Ada.Finalization.Limited_Controlled with null record;
 
diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 2befe6d..328f467 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -112,21 +112,14 @@ package body Kompsos.Pretty_Print is
     is
         Result : SU.Unbounded_String;
     begin
-        if Item.Ctrl.Actual = null then
+        if Item.Binds.Is_Empty then
             SU.Append (Result, Latin.HT & "N/A" & Latin.LF);
         else
-            declare
-                Marker : State_Component_Access := Item.Ctrl.Actual;
-            begin
-                while Marker /= null loop
-                    for Index in Valid_Count range Valid_Count'First .. Marker.Valid loop
-                        SU.Append (Result, Latin.HT &
-                            Image (Marker.Data (Index).Key) & " => " &
-                            Image (Marker.Data (Index).Value) & Latin.LF);
-                    end loop;
-                    Marker := Marker.Next.Ctrl.Actual;
-                end loop;
-            end;
+            for Bind of Item.Binds loop
+                SU.Append (Result, Latin.HT &
+                    Image (Bind.Key) & " => " &
+                    Image (Bind.Value) & Latin.LF);
+            end loop;
         end if;
         return SU.To_String (Result);
     end Image;
@@ -224,15 +217,6 @@ package body Kompsos.Pretty_Print is
                     "n" & Image (Nodes.Element (This.Actual)) & " -> " &
                     "n" & Image (Nodes.Element (This.Actual.Con_Goal.Actual)) & ";" & Latin.LF);
             end if;
-        when Recurse_Node =>
-            SU.Append (Result, Latin.HT &
-                "n" & Image (Nodes.Element (This.Actual)) & " [label=""recurse""];" & Latin.LF);
-            Do_Structure_DOT (This.Actual.Rec_Goal, Nodes, Next, Result);
-            if Nodes.Contains (This.Actual.Rec_Goal.Actual) then
-                SU.Append (Result, Latin.HT &
-                    "n" & Image (Nodes.Element (This.Actual)) & " -> " &
-                    "n" & Image (Nodes.Element (This.Actual.Rec_Goal.Actual)) & ";" & Latin.LF);
-            end if;
         end case;
     end Do_Structure_DOT;
 
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;
 
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;
 
diff --git a/test/fivesix.adb b/test/fivesix.adb
index 9620c60..781b7c3 100644
--- a/test/fivesix.adb
+++ b/test/fivesix.adb
@@ -24,7 +24,6 @@ procedure FiveSix is
     use InPrin;
 
 
-    --  It is possible to create a recursion using functions like this...
     function Fives
            (This : in Goal)
         return Goal
@@ -36,9 +35,19 @@ procedure FiveSix is
         return Disjunct (One, Two);
     end Fives;
 
+    function Sixes
+           (This : in Goal)
+        return Goal
+    is
+        One, Two : Goal := This;
+    begin
+        One.Unify (One.Fresh, 6);
+        Two.Conjunct (Sixes'Access);
+        return Disjunct (One, Two);
+    end Sixes;
+
 
-    Sixes : Goal := Empty_Goal;
-    Result : Goal;
+    Relation : constant Goal := Disjunct (Fives (Empty_Goal), Sixes (Empty_Goal));
 
 begin
 
@@ -47,14 +56,11 @@ begin
 
     TIO.New_Line;
 
-    --  ...but it is a lot simpler and easier to create recursions this way instead.
-    Sixes.Unify (Sixes.Fresh, 6);
-    Sixes.Recurse;
-
-    Result := Disjunct (Fives (Empty_Goal), Sixes);
-
-    --  Note how the States from Fives keep creating new Variables instead of looping.
-    TIO.Put_Line (Image (Result.Run (5)));
+    --  Note how the States keep using new Variables instead of just reusing the same one.
+    --  This is an unavoidable side effect of setting up Variable Terms to be manually
+    --  created from a Goal by the programmer, instead of being supplied as needed in the
+    --  process of evaluation.
+    TIO.Put_Line (Image (Relation.Run (5)));
 
 end FiveSix;
 
diff --git a/test/repeat.adb b/test/repeat.adb
deleted file mode 100644
index 0eec066..0000000
--- a/test/repeat.adb
+++ /dev/null
@@ -1,46 +0,0 @@
-
-
---  Programmed by Jedidiah Barber
---  Licensed under the Sunset License v1.0
-
---  See license.txt for further details
-
-
-with
-
-    Ada.Text_IO,
-    Kompsos.Pretty_Print;
-
-
-procedure Repeat is
-
-    package TIO renames Ada.Text_IO;
-
-
-    package InKomp is new Kompsos (Integer);
-    use InKomp;
-
-    package Printer is new InKomp.Pretty_Print (Integer'Image);
-
-
-    Relation : Goal := Empty_Goal;
-
-    A : constant Term := Relation.Fresh;
-    B : constant Term := Relation.Fresh;
-
-begin
-
-    TIO.Put_Line ("Test program to check whether Recurse is working properly.");
-    TIO.Put_Line ("There should be 5 results, all identical.");
-
-    TIO.New_Line;
-
-    Relation := Disjunct (Relation.Unify (A, 1), Relation.Unify (B, 2));
-    Relation.Unify (A, 3);
-    Relation.Recurse;
-
-    TIO.Put_Line (Printer.Image (Relation.Run (5)));
-
-end Repeat;
-
-
diff --git a/tests.gpr b/tests.gpr
index 5f35146..8dc84f9 100644
--- a/tests.gpr
+++ b/tests.gpr
@@ -27,7 +27,6 @@ project Tests is
         "multo.adb",
         "pprint.adb",
         "rembero.adb",
-        "repeat.adb",
         "trees.adb");
 
     package Builder is
@@ -42,7 +41,6 @@ project Tests is
         for Executable ("multo.adb")   use "multo";
         for Executable ("pprint.adb")  use "pprint";
         for Executable ("rembero.adb") use "rembero";
-        for Executable ("repeat.adb")  use "repeat";
         for Executable ("trees.adb")   use "trees";
 
         for Default_Switches ("Ada") use