Core rewritten with memoisation, but somehow Zebra example is buggedHEADmaster

8 files changed, 835 insertions, 493 deletions

diff --git a/example/zebra.adb b/example/zebra.adb
index 7917421..b5449f5 100644
--- a/example/zebra.adb
+++ b/example/zebra.adb
@@ -52,11 +52,6 @@ procedure Zebra is
     function On_Right
            (This   : in World;
             Inputs : in Term_Array)
-        return World;
-
-    function On_Right
-           (This   : in World;
-            Inputs : in Term_Array)
         return World
     is
         Left_Term  : Term renames Inputs (1);
@@ -130,8 +125,6 @@ begin
         T (N & N & N & T (+"fox") & N) &
         T (N & T (+"chesterfields") & N & N & N) & Houses_Term);
 
-    Verse.Force (1);
-
     Verse.Member (T (N & N & T (+"water") & N & N) & Houses_Term);
     Verse.Member (T (N & N & N & T (+"zebra") & N) & Houses_Term);
 
diff --git a/src/kompsos-collector.adb b/src/kompsos-collector.adb
new file mode 100644
index 0000000..16e2b1f
--- /dev/null
+++ b/src/kompsos-collector.adb
@@ -0,0 +1,526 @@
+
+
+--  Programmed by Jedidiah Barber
+--  Licensed under the Sunset license v1.0
+
+--  See license.txt for further details
+
+with
+
+    Ada.Unchecked_Deallocation,
+    System.Address_To_Access_Conversions,
+    System.Storage_Elements;
+
+
+package body Kompsos.Collector is
+
+
+    -------------------------
+    --  Memory Management  --
+    -------------------------
+
+    procedure Free is new Ada.Unchecked_Deallocation (World, World_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_Part);
+            end if;
+        end loop;
+    end Finalize;
+
+
+
+
+    ----------------------
+    --  Progress State  --
+    ----------------------
+
+    Cache_Memo : Cache_Maps.Map := Cache_Maps.Empty_Map;
+    Bookkeep   : Managed_Map    := (Ada.Finalization.Controlled with Actual => Eval_Maps.Empty_Map);
+
+    Book : Eval_Maps.Map renames Bookkeep.Actual;
+
+    Next_Index  : Long_Positive := 1;
+    Next_State  : State;
+    State_Valid : Boolean       := False;
+    Exhausted   : Boolean       := False;
+
+
+
+
+    ------------------------
+    --  Internal Helpers  --
+    ------------------------
+
+    --  Map Keys  --
+
+    package World_Convert is new System.Address_To_Access_Conversions (World_Component);
+
+    function "<"
+           (Left, Right : in World_Component_Access)
+        return Boolean
+    is
+        use System.Storage_Elements;
+    begin
+        return
+            To_Integer (World_Convert.To_Address (World_Convert.Object_Pointer (Left))) <
+            To_Integer (World_Convert.To_Address (World_Convert.Object_Pointer (Right)));
+    end "<";
+
+
+
+    --  Unification  --
+
+    function Fully_Contains
+           (This : in State;
+            Item : in Term'Class)
+        return Boolean is
+    begin
+        case Item.Kind is
+        when Null_Term | Atom_Term =>
+            return True;
+        when Var_Term =>
+            return This.Ident.Contains (Item.Var.Ident);
+        when Pair_Term =>
+            return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right);
+        end case;
+    end Fully_Contains;
+
+
+    function Walk
+           (This : in State;
+            Item : in Term'Class)
+        return Term'Class is
+    begin
+        if  Item.Kind = Var_Term and then
+            This.Subst.Contains (This.Ident.Element (Item.Var.Ident))
+        then
+            return Walk (This, This.Subst.Constant_Reference (This.Ident.Element (Item.Var.Ident)));
+        else
+            return Item;
+        end if;
+    end Walk;
+
+
+    function Do_Unify
+           (Potential   : in     State;
+            Left, Right : in     Term'Class;
+            Extended    :    out State)
+        return Boolean
+    is
+        Real_Left  : Term'Class := Left;
+        Real_Right : Term'Class := Right;
+    begin
+        --  Check for Variable validity with respect to State
+        if  not Fully_Contains (Potential, Real_Left) or
+            not Fully_Contains (Potential, Real_Right)
+        then
+            return False;
+        end if;
+
+        --  Resolve Variable substitution
+        if Left.Kind = Var_Term then
+            Real_Left := Walk (Potential, Real_Left);
+        end if;
+        if Right.Kind = Var_Term then
+            Real_Right := Walk (Potential, Real_Right);
+        end if;
+
+        --  Unify equal Variable/Atom/Null Terms
+        if (Real_Left.Kind = Var_Term and then
+            Real_Right.Kind = Var_Term and then
+            Real_Left = Real_Right) or else
+           (Real_Left.Kind = Atom_Term and then
+            Real_Right.Kind = Atom_Term and then
+            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 := Potential;
+            Extended.Subst.Insert (Extended.Ident.Element (Real_Left.Var.Ident), Term (Real_Right));
+            return True;
+        end if;
+        if Real_Right.Kind = Var_Term then
+            Extended := Potential;
+            Extended.Subst.Insert (Extended.Ident.Element (Real_Right.Var.Ident), Term (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
+            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;
+        end if;
+
+        --  Not sure how things get here, but if all else fails
+        return False;
+    end Do_Unify;
+
+
+
+    --  Result Collection --
+
+    function Call_Lazy
+           (This : in World;
+            Data : in Lazy_Holders.Holder)
+        return World
+    is
+        Ref : constant Lazy_Holders.Constant_Reference_Type := Data.Constant_Reference;
+    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;
+
+
+    procedure Reset
+           (Ptr : in Constant_World_Access) is
+    begin
+        if Ptr = null or else Ptr.Actual = null then
+            return;
+        end if;
+
+        Cache_Memo.Exclude (Ptr.Actual);
+
+        case Ptr.Actual.Kind is
+        when Static_Node =>
+            return;
+        when Fresh_Node =>
+            Reset (Ptr.Actual.Frs_World'Unchecked_Access);
+        when Unify_Node =>
+            Book.Exclude (Ptr.Actual);
+            Reset (Ptr.Actual.Uni_World'Unchecked_Access);
+        when Disjunct_Node =>
+            Book.Exclude (Ptr.Actual);
+            Reset (Ptr.Actual.Dis_World1'Unchecked_Access);
+            Reset (Ptr.Actual.Dis_World2'Unchecked_Access);
+        when Conjunct_Node =>
+            if Book.Contains (Ptr.Actual) then
+                Reset (Constant_World_Access (Book.Element (Ptr.Actual).Con_Part));
+                Free (Book (Ptr.Actual).Con_Part);
+                Book.Delete (Ptr.Actual);
+            end if;
+            Reset (Ptr.Actual.Con_World'Unchecked_Access);
+        when Recurse_Node =>
+            Book.Exclude (Ptr.Actual);
+            Reset (Ptr.Actual.Rec_World'Unchecked_Access);
+        end case;
+    end Reset;
+
+
+    function Get_Next
+           (Ptr    : in     Constant_World_Access;
+            Index  : in     Long_Positive;
+            Result :    out State)
+        return Boolean;
+
+
+    function Do_Get_Next
+           (Ptr    : in     World_Component_Access;
+            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);
+                return True;
+            else
+                return False;
+            end if;
+
+        when Fresh_Node =>
+            if Get_Next (Ptr.Frs_World'Unchecked_Access, Index, Result) then
+                Result.LVars.Append (Ptr.Frs_Var.Name);
+                Result.Ident.Insert (Ptr.Frs_Var.Ident, Result.LVars.Last_Index);
+                return True;
+            else
+                return False;
+            end if;
+
+        when Unify_Node =>
+            if not Book.Contains (Ptr) then
+                Book.Insert (Ptr, (Kind => Unify_Data, others => <>));
+            end if;
+            while Get_Next
+               (Ptr.Uni_World'Unchecked_Access,
+                Index + Book.Element (Ptr).Uni_Offset,
+                Result)
+            loop
+                if Do_Unify (Result, Ptr.Uni_Term1, Ptr.Uni_Term2, Result) then
+                    return True;
+                else
+                    Book (Ptr).Uni_Offset := Book.Element (Ptr).Uni_Offset + 1;
+                end if;
+            end loop;
+            return False;
+
+        when Disjunct_Node =>
+            if not Book.Contains (Ptr) then
+                Book.Insert (Ptr, (Kind => Disjunct_Data, others => <>));
+            end if;
+            if Book.Element (Ptr).Dis_Gone1 then
+                if Book.Element (Ptr).Dis_Gone2 then
+                    return False;
+                elsif Get_Next
+                   (Ptr.Dis_World2'Unchecked_Access,
+                    Book.Element (Ptr).Dis_Next2,
+                    Result)
+                then
+                    Book (Ptr).Dis_Next2 := Book.Element (Ptr).Dis_Next2 + 1;
+                    return True;
+                else
+                    Book (Ptr).Dis_Gone2 := True;
+                    return False;
+                end if;
+            elsif Book.Element (Ptr).Dis_Gone2 then
+                if Get_Next
+                   (Ptr.Dis_World1'Unchecked_Access,
+                    Book.Element (Ptr).Dis_Next1,
+                    Result)
+                then
+                    Book (Ptr).Dis_Next1 := Book.Element (Ptr).Dis_Next1 + 1;
+                    return True;
+                else
+                    Book (Ptr).Dis_Gone1 := True;
+                    return False;
+                end if;
+            elsif Book.Element (Ptr).Dis_Flag then
+                if Get_Next
+                   (Ptr.Dis_World1'Unchecked_Access,
+                    Book.Element (Ptr).Dis_Next1,
+                    Result)
+                then
+                    Book (Ptr).Dis_Next1 := Book.Element (Ptr).Dis_Next1 + 1;
+                    Book (Ptr).Dis_Flag := not Book.Element (Ptr).Dis_Flag;
+                    return True;
+                else
+                    Book (Ptr).Dis_Gone1 := True;
+                    if Get_Next
+                       (Ptr.Dis_World2'Unchecked_Access,
+                        Book.Element (Ptr).Dis_Next2,
+                        Result)
+                    then
+                        Book (Ptr).Dis_Next2 := Book.Element (Ptr).Dis_Next2 + 1;
+                        return True;
+                    else
+                        Book (Ptr).Dis_Gone2 := True;
+                        return False;
+                    end if;
+                end if;
+            else
+                if Get_Next
+                   (Ptr.Dis_World2'Unchecked_Access,
+                    Book.Element (Ptr).Dis_Next2,
+                    Result)
+                then
+                    Book (Ptr).Dis_Next2 := Book.Element (Ptr).Dis_Next2 + 1;
+                    Book (Ptr).Dis_Flag := not Book.Element (Ptr).Dis_Flag;
+                    return True;
+                else
+                    Book (Ptr).Dis_Gone2 := True;
+                    if Get_Next
+                       (Ptr.Dis_World1'Unchecked_Access,
+                        Book.Element (Ptr).Dis_Next1,
+                        Result)
+                    then
+                        Book (Ptr).Dis_Next1 := Book.Element (Ptr).Dis_Next1 + 1;
+                        return True;
+                    else
+                        Book (Ptr).Dis_Gone1 := True;
+                        return False;
+                    end if;
+                end if;
+            end if;
+
+        when Conjunct_Node =>
+            if not Book.Contains (Ptr) then
+                Book.Insert (Ptr, (Kind => Conjunct_Data, others => <>));
+            end if;
+            if Book (Ptr).Con_Gone then
+                return False;
+            end if;
+            while not Get_Next
+               (Constant_World_Access (Book.Element (Ptr).Con_Part),
+                Book.Element (Ptr).Con_Next,
+                Result)
+            loop
+                Reset (Constant_World_Access (Book.Element (Ptr).Con_Part));
+                Free (Book (Ptr).Con_Part);
+                if Get_Next
+                   (Ptr.Con_World'Unchecked_Access,
+                    Book.Element (Ptr).Con_From,
+                    Result)
+                then
+                    Book (Ptr).Con_Part :=
+                        new World'(Call_Lazy (World (Static (Result)), Ptr.Con_Data));
+                    Book (Ptr).Con_Next := 1;
+                    Book (Ptr).Con_From := Book.Element (Ptr).Con_From + 1;
+                else
+                    Book (Ptr).Con_Gone := True;
+                    return False;
+                end if;
+            end loop;
+            Book (Ptr).Con_Next := Book.Element (Ptr).Con_Next + 1;
+            return True;
+
+        when Recurse_Node =>
+            if not Book.Contains (Ptr) then
+                Book.Insert (Ptr, (Kind => Recurse_Data, others => <>));
+            end if;
+            if Book (Ptr).Rec_Gone then
+                return False;
+            end if;
+            while not Get_Next
+               (Ptr.Rec_World'Unchecked_Access,
+                Book.Element (Ptr).Rec_Next,
+                Result)
+            loop
+                if Book.Element (Ptr).Rec_Next = 1 then
+                    Book (Ptr).Rec_Gone := True;
+                    return False;
+                else
+                    Book (Ptr).Rec_Next := 1;
+                end if;
+            end loop;
+            Book (Ptr).Rec_Next := Book.Element (Ptr).Rec_Next + 1;
+            return True;
+        end case;
+    end Do_Get_Next;
+
+
+    function Cached
+           (Ptr    : in     World_Component_Access;
+            Index  : in     Long_Positive;
+            Result :    out State)
+        return Boolean is
+    begin
+        if Cache_Memo.Contains (Ptr) and then Index <= Cache_Memo (Ptr).Last_Index then
+            Result := Cache_Memo (Ptr) (Index);
+            return True;
+        else
+            return False;
+        end if;
+    end Cached;
+
+
+    procedure Cache_This
+           (Ptr    : in World_Component_Access;
+            Index  : in Long_Positive;
+            Result : in State) is
+    begin
+        if Ptr.Counter > 1 and Ptr.Kind /= Static_Node then
+            if not Cache_Memo.Contains (Ptr) then
+                Cache_Memo.Insert (Ptr, State_Vectors.Empty_Vector);
+            end if;
+            pragma Assert (Index = Cache_Memo (Ptr).Last_Index + 1);
+            Cache_Memo (Ptr).Append (Result);
+        end if;
+    end Cache_This;
+
+
+    function Get_Next
+           (Ptr    : in     Constant_World_Access;
+            Index  : in     Long_Positive;
+            Result :    out State)
+        return Boolean is
+    begin
+        if Ptr = null or else Ptr.Actual = null then
+            return False;
+        elsif Cached (Ptr.Actual, Index, Result) then
+            return True;
+        else
+            return Found : constant Boolean := Do_Get_Next (Ptr.Actual, Index, Result) do
+                if Found then
+                    Cache_This (Ptr.Actual, Index, Result);
+                end if;
+            end return;
+        end if;
+    end Get_Next;
+
+
+
+
+    -----------------------
+    --  API Subprograms  --
+    -----------------------
+
+    function Has_Next
+        return Boolean
+    is
+        Ptr : constant Constant_World_Access := Source'Access;
+    begin
+        if State_Valid then
+            return True;
+        elsif Exhausted then
+            return False;
+        else
+            State_Valid := Get_Next (Ptr, Next_Index, Next_State);
+            if not State_Valid then
+                Exhausted := True;
+            else
+                Next_Index := Next_Index + 1;
+            end if;
+            return State_Valid;
+        end if;
+    end Has_Next;
+
+
+    function Next
+        return State is
+    begin
+        if Has_Next then
+            State_Valid := False;
+            return Next_State;
+        else
+            raise State_Not_Found_Error;
+        end if;
+    end Next;
+
+
+    function Next
+           (Default : in State)
+        return State is
+    begin
+        if Has_Next then
+            State_Valid := False;
+            return Next_State;
+        else
+            return Default;
+        end if;
+    end Next;
+
+
+    procedure Reset
+    is
+        Ptr : constant Constant_World_Access := Source'Access;
+    begin
+        Reset (Ptr);
+        Next_Index  := 1;
+        State_Valid := False;
+        Exhausted   := False;
+    end Reset;
+
+
+end Kompsos.Collector;
+
+
diff --git a/src/kompsos-collector.ads b/src/kompsos-collector.ads
new file mode 100644
index 0000000..4bca3b4
--- /dev/null
+++ b/src/kompsos-collector.ads
@@ -0,0 +1,94 @@
+
+
+--  Programmed by Jedidiah Barber
+--  Licensed under the Sunset License v1.0
+
+--  See license.txt for further details
+
+
+private with
+
+    Ada.Containers.Ordered_Maps,
+    Ada.Containers.Vectors,
+    Ada.Finalization;
+
+
+generic
+    Source : in World;
+package Kompsos.Collector is
+
+
+    State_Not_Found_Error : exception;
+
+
+    function Has_Next
+        return Boolean;
+
+    function Next
+        return State;
+
+    function Next
+           (Default : in State)
+        return State;
+
+    procedure Reset;
+
+
+private
+
+
+    type World_Access is access all World;
+
+    type Constant_World_Access is access constant World;
+
+    function "<"
+           (Left, Right : in World_Component_Access)
+        return Boolean;
+
+    type Eval_Kind is
+       (Unify_Data,
+        Disjunct_Data,
+        Conjunct_Data,
+        Recurse_Data);
+
+    type Eval_Data (Kind : Eval_Kind := Unify_Data) is record
+        case Kind is
+        when Unify_Data =>
+            Uni_Offset : Long_Natural  := 0;
+        when Disjunct_Data =>
+            Dis_Flag   : Boolean       := True;
+            Dis_Next1  : Long_Positive := 1;
+            Dis_Next2  : Long_Positive := 1;
+            Dis_Gone1  : Boolean       := False;
+            Dis_Gone2  : Boolean       := False;
+        when Conjunct_Data =>
+            Con_Part   : World_Access  := null;
+            Con_From   : Long_Positive := 1;
+            Con_Next   : Long_Positive := 1;
+            Con_Gone   : Boolean       := False;
+        when Recurse_Data =>
+            Rec_Next   : Long_Positive := 1;
+            Rec_Gone   : Boolean       := False;
+        end case;
+    end record;
+
+    package Eval_Maps is new Ada.Containers.Ordered_Maps
+       (Key_Type     => World_Component_Access,
+        Element_Type => Eval_Data);
+
+    type Managed_Map is new Ada.Finalization.Controlled with record
+        Actual : Eval_Maps.Map;
+    end record;
+
+    overriding procedure Finalize
+           (This : in out Managed_Map);
+
+    package Cache_Maps is new Ada.Containers.Ordered_Maps
+       (Key_Type     => World_Component_Access,
+        Element_Type => State_Vectors.Vector,
+        "="          => State_Vectors."=");
+
+
+end Kompsos.Collector;
+
+
diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 73cee40..834c0ca 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -9,7 +9,8 @@
 with
 
     Ada.Characters.Latin_1,
-    Ada.Strings.Fixed;
+    Ada.Strings.Fixed,
+    Kompsos.Collector;
 
 
 package body Kompsos.Pretty_Print is
@@ -30,10 +31,10 @@ package body Kompsos.Pretty_Print is
 
 
     function Image
-           (Item : in ID_Number)
+           (Item : in Long_Natural)
         return String is
     begin
-        return Str.Fixed.Trim (ID_Number'Image (Item), Str.Left);
+        return Str.Fixed.Trim (Long_Natural'Image (Item), Str.Left);
     end Image;
 
 
@@ -43,7 +44,7 @@ package body Kompsos.Pretty_Print is
            (Item : in Variable)
         return String is
     begin
-        return "Vargen#" & Image (ID_Number (Item.Ident)) &
+        return "Vargen#" & Image (Long_Natural (Item.Ident)) &
            (if SU.Length (Item.Name) /= 0
             then "/" & SU.To_String (Item.Name)
             else "");
@@ -101,8 +102,8 @@ package body Kompsos.Pretty_Print is
             SU.Append (Result, Latin.LF);
             for Iter in Item.Ident.Iterate loop
                 SU.Append (Result, Latin.HT & Latin.HT & "Vargen#" &
-                    Image (ID_Number (ID_Number_Maps.Key (Iter))) & " => " &
-                    Image (ID_Number (ID_Number_Maps.Element (Iter))) & Latin.LF);
+                    Image (Long_Natural (ID_Number_Maps.Key (Iter))) & " => " &
+                    Image (Long_Natural (ID_Number_Maps.Element (Iter))) & Latin.LF);
             end loop;
         end if;
         SU.Append (Result, Latin.HT & "Variables:");
@@ -112,7 +113,7 @@ package body Kompsos.Pretty_Print is
             SU.Append (Result, Latin.LF);
             for Index in Item.LVars.First_Index .. Item.LVars.Last_Index loop
                 SU.Append (Result, Latin.HT & Latin.HT &
-                    "Var#" & Image (ID_Number (Index)) &
+                    "Var#" & Image (Long_Natural (Index)) &
                    (if SU.Length (Item.LVars (Index)) /= 0
                     then "/" & SU.To_String (Item.LVars (Index))
                     else "") & Latin.LF);
@@ -125,7 +126,7 @@ package body Kompsos.Pretty_Print is
             SU.Append (Result, Latin.LF);
             for Iter in Item.Subst.Iterate loop
                 SU.Append (Result, Latin.HT & Latin.HT &
-                    Image (ID_Number (Binding_Maps.Key (Iter))) & " => " &
+                    Image (Long_Natural (Binding_Maps.Key (Iter))) & " => " &
                     Image (Binding_Maps.Element (Iter)) & Latin.LF);
             end loop;
         end if;
@@ -134,17 +135,17 @@ package body Kompsos.Pretty_Print is
 
 
     function Image
-           (Items : in State_Array)
+           (Item : in State_Array)
         return String
     is
         Result : SU.Unbounded_String;
     begin
-        if Items'Length = 0 then
+        if Item'Length = 0 then
             return "States: N/A" & Latin.LF;
         end if;
-        for Index in Items'Range loop
+        for Index in Item'Range loop
             SU.Append (Result, "State#" & Image (Index) & ":" & Latin.LF);
-            SU.Append (Result, Image (Items (Index)));
+            SU.Append (Result, Image (Item (Index)));
         end loop;
         return SU.Slice (Result, 1, SU.Length (Result) - 1);
     end Image;
@@ -153,35 +154,27 @@ package body Kompsos.Pretty_Print is
 
 
     function Image
-           (Item : in out World)
+           (Item : in World)
         return String
     is
         Result  : SU.Unbounded_String;
         Counter : Positive := 1;
+
+        package Collect is new Collector (Item);
     begin
-        if not Item.Has_State (Counter) then
+        if not Collect.Has_Next then
             return "States: N/A" & Latin.LF;
         end if;
         loop
             SU.Append (Result, "State#" & Image (Counter) & ":" & Latin.LF);
-            SU.Append (Result, Image (Item.Possibles.Constant_Reference (Counter)));
+            SU.Append (Result, Image (Collect.Next));
+            exit when not Collect.Has_Next;
             Counter := Counter + 1;
-            exit when not Item.Has_State (Counter);
         end loop;
         return SU.Slice (Result, 1, SU.Length (Result) - 1);
     end Image;
 
 
-    function Image_Constant
-           (Item : in World)
-        return String
-    is
-        Scratch : World := Item;
-    begin
-        return Image (Scratch);
-    end Image_Constant;
-
-
 end Kompsos.Pretty_Print;
 
 
diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads
index 73e50db..1316d5a 100644
--- a/src/kompsos-pretty_print.ads
+++ b/src/kompsos-pretty_print.ads
@@ -29,16 +29,11 @@ package Kompsos.Pretty_Print is
 
 
     function Image
-           (Items : in State_Array)
+           (Item : in State_Array)
         return String;
 
 
     function Image
-           (Item : in out World)
-        return String;
-
-
-    function Image_Constant
            (Item : in World)
         return String;
 
@@ -47,7 +42,7 @@ private
 
 
     function Image
-           (Item : in ID_Number)
+           (Item : in Long_Natural)
         return String;
 
 
diff --git a/src/kompsos.adb b/src/kompsos.adb
index d531f25..e525f23 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -8,7 +8,8 @@
 
 with
 
-    Ada.Unchecked_Deallocation;
+    Ada.Unchecked_Deallocation,
+    Kompsos.Collector;
 
 
 package body Kompsos is
@@ -52,6 +53,40 @@ package body Kompsos is
 
 
 
+    --  Worlds  --
+
+    procedure Free is new Ada.Unchecked_Deallocation (World_Component, World_Component_Access);
+
+
+    procedure Initialize
+           (This : in out World) is
+    begin
+        This.Actual := null;
+    end Initialize;
+
+
+    procedure Adjust
+           (This : in out World) is
+    begin
+        if This.Actual /= null then
+            This.Actual.Counter := This.Actual.Counter + 1;
+        end if;
+    end Adjust;
+
+
+    procedure Finalize
+           (This : in out World) 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;
+
+
+
 
     -----------------
     --  Datatypes  --
@@ -156,31 +191,18 @@ package body Kompsos is
 
     --  Worlds  --
 
-    function Hold
-           (This : in World)
-        return World_Holders.Holder is
-    begin
-        return World_Holders.To_Holder (World_Root'Class (This));
-    end Hold;
-
-
-    function Ptr
-           (This : in out World_Holders.Holder)
-        return World_Access is
-    begin
-        return World (This.Reference.Element.all)'Unchecked_Access;
-    end Ptr;
-
-
-    procedure Swap
-           (Left, Right : in out World_Holders.Holder)
+    function Static
+           (Item : in State)
+        return World'Class
     is
-        Temp : World_Holders.Holder;
+        use type State_Vectors.Vector;
     begin
-        Temp.Move (Left);
-        Left.Move (Right);
-        Right.Move (Temp);
-    end Swap;
+        return Result : constant World := (Ada.Finalization.Controlled with
+            Actual => new World_Component'(
+               (Kind       => Static_Node,
+                Counter    => 1,
+                Stc_States => State_Vectors.Empty_Vector & Item)));
+    end Static;
 
 
 
@@ -203,255 +225,6 @@ package body Kompsos is
 
 
 
-    --  Unification  --
-
-    function Fully_Contains
-           (This : in State;
-            Item : in Term'Class)
-        return Boolean is
-    begin
-        case Item.Kind is
-        when Null_Term | Atom_Term =>
-            return True;
-        when Var_Term =>
-            return This.Ident.Contains (Item.Var.Ident);
-        when Pair_Term =>
-            return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right);
-        end case;
-    end Fully_Contains;
-
-
-    function Walk
-           (This : in State;
-            Item : in Term'Class)
-        return Term'Class is
-    begin
-        if  Item.Kind = Var_Term and then
-            This.Subst.Contains (This.Ident.Element (Item.Var.Ident))
-        then
-            return Walk (This, This.Subst.Constant_Reference (This.Ident.Element (Item.Var.Ident)));
-        else
-            return Item;
-        end if;
-    end Walk;
-
-
-    function Do_Unify
-           (Potential   : in     State;
-            Left, Right : in     Term'Class;
-            Extended    :    out State)
-        return Boolean
-    is
-        Real_Left  : Term'Class := Left;
-        Real_Right : Term'Class := Right;
-    begin
-        --  Check for Variable validity with respect to State
-        if  not Fully_Contains (Potential, Real_Left) or
-            not Fully_Contains (Potential, Real_Right)
-        then
-            return False;
-        end if;
-
-        --  Resolve Variable substitution
-        if Left.Kind = Var_Term then
-            Real_Left := Walk (Potential, Real_Left);
-        end if;
-        if Right.Kind = Var_Term then
-            Real_Right := Walk (Potential, Real_Right);
-        end if;
-
-        --  Unify equal Variable/Atom/Null Terms
-        if (Real_Left.Kind = Var_Term and then
-            Real_Right.Kind = Var_Term and then
-            Real_Left = Real_Right) or else
-           (Real_Left.Kind = Atom_Term and then
-            Real_Right.Kind = Atom_Term and then
-            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 := Potential;
-            Extended.Subst.Insert (Extended.Ident.Element (Real_Left.Var.Ident), Term (Real_Right));
-            return True;
-        end if;
-        if Real_Right.Kind = Var_Term then
-            Extended := Potential;
-            Extended.Subst.Insert (Extended.Ident.Element (Real_Right.Var.Ident), Term (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
-            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;
-        end if;
-
-        --  Not sure how things get here, but if all else fails
-        return False;
-    end Do_Unify;
-
-
-
-    --  Lazy World Generation --
-
-    function Call_Lazy
-           (This : in World;
-            Data : in Lazy_Holders.Holder)
-        return World
-    is
-        Ref : constant Lazy_Holders.Constant_Reference_Type := Data.Constant_Reference;
-    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;
-
-
-    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
-        Ptr (This.Engine.Frs_World).Rollover;
-        for Potential of Ptr (This.Engine.Frs_World).Possibles loop
-            Potential.LVars.Append (This.Engine.Frs_Name);
-            Potential.Ident.Insert (This.Engine.Frs_Ident, Potential.LVars.Last_Index);
-            This.Possibles.Append (Potential);
-        end loop;
-        if Ptr (This.Engine.Frs_World).Engine.Kind = No_Gen then
-            This.Engine := (Kind => No_Gen);
-        else
-            Ptr (This.Engine.Frs_World).Possibles.Clear;
-        end if;
-    end Roll_Fresh_Gen;
-
-
-    procedure Roll_Unify_Gen
-           (This : in out World)
-    is
-        Extended : State;
-    begin
-        Ptr (This.Engine.Uni_World).Rollover;
-        for Potential of Ptr (This.Engine.Uni_World).Possibles loop
-            if Do_Unify (Potential, This.Engine.Uni_Term1, This.Engine.Uni_Term2, Extended) then
-                This.Possibles.Append (Extended);
-            end if;
-        end loop;
-        if Ptr (This.Engine.Uni_World).Engine.Kind = No_Gen then
-            This.Engine := (Kind => No_Gen);
-        else
-            Ptr (This.Engine.Uni_World).Possibles.Clear;
-        end if;
-    end Roll_Unify_Gen;
-
-
-    procedure Roll_Disjunct_Gen
-           (This : in out World) is
-    begin
-        Ptr (This.Engine.Dis_World1).Rollover;
-        This.Possibles.Append (Ptr (This.Engine.Dis_World1).Possibles);
-        if Ptr (This.Engine.Dis_World1).Engine.Kind = No_Gen then
-            Ptr (This.Engine.Dis_World2).Rollover;  --  why is this line needed?
-            This.Possibles.Append (Ptr (This.Engine.Dis_World2).Possibles);
-            This.Engine := World (This.Engine.Dis_World2.Element).Engine;
-        else
-            Ptr (This.Engine.Dis_World1).Possibles.Clear;
-            Swap (This.Engine.Dis_World1, This.Engine.Dis_World2);
-        end if;
-    end Roll_Disjunct_Gen;
-
-
-    procedure Roll_Conjunct_Gen
-           (This : in out World)
-    is
-        use type Ada.Containers.Count_Type;
-    begin
-        Ptr (This.Engine.Con_World).Rollover;
-        if Ptr (This.Engine.Con_World).Possibles.Length > 0 then
-            declare
-                So_Far : constant World :=
-                   ((Possibles => Ptr (This.Engine.Con_World).Possibles,
-                     Engine    => (Kind => No_Gen)));
-            begin
-                Ptr (This.Engine.Con_World).Possibles.Clear;
-                This := Disjunct (Call_Lazy (So_Far, This.Engine.Con_Data), This);
-            end;
-        elsif Ptr (This.Engine.Con_World).Engine.Kind = No_Gen then
-            This.Engine := (Kind => No_Gen);
-        end if;
-    end Roll_Conjunct_Gen;
-
-
-    procedure Roll_Recurse_Gen
-           (This : in out World) is
-    begin
-        Ptr (This.Engine.Rec_World).Rollover;
-        if Ptr (This.Engine.Rec_World).Possibles.Last_Index < This.Engine.Rec_Index then
-            if Ptr (This.Engine.Rec_World).Engine.Kind = No_Gen then
-                if This.Engine.Rec_Index = 1 then
-                    This.Engine := (Kind => No_Gen);
-                else
-                    This.Engine.Rec_Index := 1;
-                end if;
-            end if;
-            return;
-        end if;
-        for Index in Integer range
-            This.Engine.Rec_Index .. Ptr (This.Engine.Rec_World).Possibles.Last_Index
-        loop
-            This.Possibles.Append (Ptr (This.Engine.Rec_World).Possibles (Index));
-        end loop;
-        This.Engine.Rec_Index := Ptr (This.Engine.Rec_World).Possibles.Last_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 Conjunct_Gen => This.Roll_Conjunct_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;
-
-
-
 
     -------------------
     --  microKanren  --
@@ -481,15 +254,15 @@ package body Kompsos is
             Name : in     Nametag)
         return Term
     is
-        My_ID : constant Generator_ID_Number := Next_Gen;
-    begin
-        return My_Term : constant Term := Term (T (Variable'(Ident => My_ID, Name => Name))) do
-            This.Engine :=
-               (Kind      => Fresh_Gen,
-                Frs_Ident => My_ID,
-                Frs_World => Hold (This),
-                Frs_Name  => Name);
-            This.Possibles := State_Vectors.Empty_Vector;
+        My_ID  : constant Generator_ID_Number := Next_Gen;
+        My_Var : constant Variable := (Ident => My_ID, Name => Name);
+    begin
+        return My_Term : constant Term := Term (T (My_Var)) do
+            This.Actual := new World_Component'(
+               (Kind      => Fresh_Node,
+                Counter   => 1,
+                Frs_World => World (This),
+                Frs_Var   => My_Var));
         end return;
     end Fresh;
 
@@ -552,13 +325,13 @@ package body Kompsos is
             Left, Right : in Term'Class)
         return World is
     begin
-        return Result : constant World :=
-           (Possibles => State_Vectors.Empty_Vector,
-            Engine    =>
-               (Kind      => Unify_Gen,
-                Uni_World => Hold (This),
+        return Result : constant World := (Ada.Finalization.Controlled with
+            Actual => new World_Component'(
+               (Kind      => Unify_Node,
+                Counter   => 1,
+                Uni_World => This,
                 Uni_Term1 => Term (Left),
-                Uni_Term2 => Term (Right)));
+                Uni_Term2 => Term (Right))));
     end Unify;
 
 
@@ -577,12 +350,12 @@ package body Kompsos is
            (Left, Right : in World)
         return World is
     begin
-        return Result : constant World :=
-           (Possibles => State_Vectors.Empty_Vector,
-            Engine    =>
-               (Kind       => Disjunct_Gen,
-                Dis_World1 => Hold (Left),
-                Dis_World2 => Hold (Right)));
+        return Result : constant World := (Ada.Finalization.Controlled with
+            Actual => new World_Component'(
+               (Kind       => Disjunct_Node,
+                Counter    => 1,
+                Dis_World1 => Left,
+                Dis_World2 => Right)));
     end Disjunct;
 
 
@@ -599,18 +372,20 @@ package body Kompsos is
         return World is
     begin
         if Inputs'Length = 0 then
-            return Failed : constant World :=
-               (Possibles => State_Vectors.Empty_Vector,
-                Engine    => (Kind => No_Gen));
+            return Result : constant World := (Ada.Finalization.Controlled with
+                Actual => new World_Component'(
+                   (Kind       => Static_Node,
+                    Counter    => 1,
+                    Stc_States => State_Vectors.Empty_Vector)));
         elsif Inputs'Length = 1 then
             return Inputs (Inputs'First);
         else
-            return Result : constant World :=
-               (Possibles => State_Vectors.Empty_Vector,
-                Engine    =>
-                   (Kind       => Disjunct_Gen,
-                    Dis_World1 => Hold (Inputs (Inputs'First)),
-                    Dis_World2 => Hold (Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last)))));
+            return Result : constant World := (Ada.Finalization.Controlled with
+                Actual => new World_Component'(
+                   (Kind       => Disjunct_Node,
+                    Counter    => 1,
+                    Dis_World1 => Inputs (Inputs'First),
+                    Dis_World2 => Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last)))));
         end if;
     end Disjunct;
 
@@ -631,12 +406,12 @@ package body Kompsos is
             Func : in Junction_Zero_Func)
         return World is
     begin
-        return Result : constant World :=
-           (Possibles => State_Vectors.Empty_Vector,
-            Engine    =>
-               (Kind      => Conjunct_Gen,
-                Con_World => Hold (This),
-                Con_Data  => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func))));
+        return Result : constant World := (Ada.Finalization.Controlled with
+            Actual => new World_Component'(
+               (Kind      => Conjunct_Node,
+                Counter   => 1,
+                Con_World => This,
+                Con_Data  => Lazy_Holders.To_Holder ((Kind => Zero_Arg, ZFunc => Func)))));
     end Conjunct;
 
 
@@ -654,15 +429,15 @@ package body Kompsos is
             Input : in Term'Class)
         return World is
     begin
-        return Result : constant World :=
-           (Possibles => State_Vectors.Empty_Vector,
-            Engine    =>
-               (Kind      => Conjunct_Gen,
-                Con_World => Hold (This),
+        return Result : constant World := (Ada.Finalization.Controlled with
+            Actual => new World_Component'(
+               (Kind      => Conjunct_Node,
+                Counter   => 1,
+                Con_World => This,
                 Con_Data  => Lazy_Holders.To_Holder
                    ((Kind   => One_Arg,
                      OFunc  => Func,
-                     OInput => Term (Input)))));
+                     OInput => Term (Input))))));
     end Conjunct;
 
 
@@ -681,15 +456,15 @@ package body Kompsos is
             Inputs : in Term_Array)
         return World is
     begin
-        return Result : constant World :=
-           (Possibles => State_Vectors.Empty_Vector,
-            Engine    =>
-               (Kind      => Conjunct_Gen,
-                Con_World => Hold (This),
+        return Result : constant World := (Ada.Finalization.Controlled with
+            Actual => new World_Component'(
+               (Kind      => Conjunct_Node,
+                Counter   => 1,
+                Con_World => This,
                 Con_Data  => Lazy_Holders.To_Holder
                    ((Kind   => Many_Arg,
                      MFunc  => Func,
-                     MInput => Term_Array_Holders.To_Holder (Inputs)))));
+                     MInput => Term_Array_Holders.To_Holder (Inputs))))));
     end Conjunct;
 
 
@@ -714,12 +489,11 @@ package body Kompsos is
            (This : in World)
         return World is
     begin
-        return Result : constant World :=
-           (Possibles => State_Vectors.Empty_Vector,
-            Engine    =>
-               (Kind      => Recurse_Gen,
-                Rec_World => Hold (This),
-                Rec_Index => 1));
+        return Result : constant World := (Ada.Finalization.Controlled with
+            Actual => new World_Component'(
+               (Kind      => Recurse_Node,
+                Counter   => 1,
+                Rec_World => This)));
     end Recurse;
 
 
@@ -731,71 +505,55 @@ package body Kompsos is
 
 
 
-    --  Forced Evaluation  --
+    --  Evaluation  --
 
     function Take
-           (This  : in out World;
-            Count : in     Positive)
-        return State_Array is
+           (This  : in World;
+            Count : in Positive)
+        return State_Array
+    is
+        Result : State_Array (1 .. Count);
+        Valid  : Natural := 0;
+
+        package Collect is new Collector (This);
     begin
-        This.Force (Count);
-        return Result : State_Array (1 .. Integer'Min (Count, This.Possibles.Last_Index)) do
-            for Index in Result'Range loop
-                Result (Index) := This.Possibles.Element (Index);
-            end loop;
-        end return;
+        for Item of Result loop
+            exit when not Collect.Has_Next;
+            Item := Collect.Next;
+            Valid := Valid + 1;
+        end loop;
+        return Result (1 .. Valid);
     end Take;
 
 
     function Take_First
-           (This : in out World)
-        return State is
+           (This : in World)
+        return State
+    is
+        package Collect is new Collector (This);
     begin
-        This.Force (1);
-        if This.Possibles.Is_Empty then
-            return Empty_State;
-        else
-            return This.Possibles.First_Element;
-        end if;
+        return Collect.Next (Empty_State);
     end Take_First;
 
 
     function Take_All
-           (This : in out World)
-        return State_Array is
-    begin
-        This.Force_All;
-        return Result : State_Array (1 .. Natural (This.Possibles.Length)) do
-            for Index in Result'Range loop
-                Result (Index) := This.Possibles.Element (Index);
-            end loop;
-        end return;
-    end Take_All;
-
-
-    procedure Force
-           (This  : in out World;
-            Count : in     Positive) is
-    begin
-        This.Roll_Until (Count);
-    end Force;
-
-
-    procedure Force_All
-           (This : in out World) is
-    begin
-        while This.Engine.Kind /= No_Gen loop
-            This.Rollover;
-        end loop;
-    end Force_All;
-
+           (This : in World)
+        return State_Array
+    is
+        package Collect is new Collector (This);
 
-    function Failed
-           (This : in out World)
-        return Boolean is
+        function Do_Take
+            return State_Array is
+        begin
+            if Collect.Has_Next then
+                return Collect.Next & Do_Take;
+            else
+                return Result : State_Array (1 .. 0);
+            end if;
+        end Do_Take;
     begin
-        return not This.Has_State (1);
-    end Failed;
+        return Do_Take;
+    end Take_All;
 
 
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index 0483fa1..e9bbefd 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -252,32 +252,21 @@ package Kompsos is
            (This : in out World);
 
 
-    --  Forced Evaluation  --
+    --  Evaluation  --
 
     function Take
-           (This  : in out World;
-            Count : in     Positive)
+           (This  : in World;
+            Count : in Positive)
         return State_Array;
 
     function Take_First
-           (This : in out World)
+           (This : in World)
         return State;
 
     function Take_All
-           (This : in out World)
+           (This : in World)
         return State_Array;
 
-    procedure Force
-           (This  : in out World;
-            Count : in     Positive);
-
-    procedure Force_All
-           (This : in out World);
-
-    function Failed
-           (This : in out World)
-        return Boolean;
-
 
     --  Reification  --
 
@@ -473,10 +462,11 @@ private
 
 
     --  around 2^31 possible Variables should be enough for anybody, right?
-    type ID_Number is new Long_Integer range 0 .. Long_Integer'Last;
+    subtype Long_Natural  is Long_Integer range 0 .. Long_Integer'Last;
+    subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last;
 
-    type Generator_ID_Number is new ID_Number;
-    type Variable_ID_Number  is new ID_Number;
+    type Generator_ID_Number is new Long_Natural;
+    type Variable_ID_Number  is new Long_Natural;
 
     type Variable is record
         Ident : Generator_ID_Number;
@@ -490,9 +480,9 @@ private
 
     type Term_Component_Access is access Term_Component;
 
-    subtype Non_Null_Term_Kind is Term_Kind range Atom_Term .. Pair_Term;
+    subtype Not_Null_Term_Kind is Term_Kind range Atom_Term .. Pair_Term;
 
-    type Term_Component (Kind : Non_Null_Term_Kind) is limited record
+    type Term_Component (Kind : Not_Null_Term_Kind) is limited record
         Counter : Natural;
         case Kind is
         when Atom_Term =>
@@ -500,7 +490,8 @@ private
         when Var_Term =>
             Refer : Variable;
         when Pair_Term =>
-            Left, Right : Term;
+            Left  : Term;
+            Right : Term;
         end case;
     end record;
 
@@ -552,6 +543,10 @@ private
         Subst : Binding_Maps.Map;
     end record;
 
+    package State_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Long_Positive,
+        Element_Type => State);
+
     Empty_State : constant State :=
        (Ident => ID_Number_Maps.Empty_Map,
         LVars => Name_Vectors.Empty_Vector,
@@ -560,16 +555,9 @@ private
 
 
 
-    type World_Root is abstract tagged null record;
-
-    package World_Holders is new Ada.Containers.Indefinite_Holders (World_Root'Class);
+    type World_Component;
 
-    type World_Access is access all World;
-
-    function Hold
-           (This : in World)
-        return World_Holders.Holder
-    with Inline;
+    type World_Component_Access is access World_Component;
 
     type Lazy_Kind is (Zero_Arg, One_Arg, Many_Arg);
 
@@ -588,64 +576,59 @@ private
 
     package Lazy_Holders is new Ada.Containers.Indefinite_Holders (Lazy_Data);
 
-    type Generator_Kind is
-       (No_Gen,
-        Fresh_Gen,
-        Unify_Gen,
-        Disjunct_Gen,
-        Conjunct_Gen,
-        Recurse_Gen);
+    type Node_Kind is
+       (Static_Node,
+        Fresh_Node,
+        Unify_Node,
+        Disjunct_Node,
+        Conjunct_Node,
+        Recurse_Node);
 
-    type Generator (Kind : Generator_Kind := No_Gen) is record
+    type World_Component (Kind : Node_Kind) is limited record
+        Counter : Natural;
         case Kind is
-        when No_Gen =>
-            null;
-        when Fresh_Gen =>
-            Frs_Ident  : Generator_ID_Number;
-            Frs_World  : World_Holders.Holder;
-            Frs_Name   : Nametag;
-        when Unify_Gen =>
-            Uni_World  : World_Holders.Holder;
+        when Static_Node =>
+            Stc_States : State_Vectors.Vector;
+        when Fresh_Node =>
+            Frs_World  : aliased World;
+            Frs_Var    : Variable;
+        when Unify_Node =>
+            Uni_World  : aliased World;
             Uni_Term1  : Term;
             Uni_Term2  : Term;
-        when Disjunct_Gen =>
-            Dis_World1 : World_Holders.Holder;
-            Dis_World2 : World_Holders.Holder;
-        when Conjunct_Gen =>
-            Con_World  : World_Holders.Holder;
+        when Disjunct_Node =>
+            Dis_World1 : aliased World;
+            Dis_World2 : aliased World;
+        when Conjunct_Node =>
+            Con_World  : aliased World;
             Con_Data   : Lazy_Holders.Holder;
-        when Recurse_Gen =>
-            Rec_World  : World_Holders.Holder;
-            Rec_Index  : Positive;
+        when Recurse_Node =>
+            Rec_World  : aliased World;
         end case;
     end record;
 
-    package State_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Positive,
-        Element_Type => State);
-
-    type World is new World_Root with record
-        Possibles : State_Vectors.Vector;
-        Engine    : Generator;
+    type World is new Ada.Finalization.Controlled with record
+        Actual : World_Component_Access := null;
     end record;
 
-    function Has_State
-           (This  : in out World;
-            Index : in     Positive)
-        return Boolean;
+    overriding procedure Initialize
+           (This : in out World);
 
-    procedure Rollover
+    overriding procedure Adjust
            (This : in out World);
 
-    procedure Roll_Until
-           (This  : in out World;
-            Index : in     Positive);
+    overriding procedure Finalize
+           (This : in out World);
 
-    use type State_Vectors.Vector;
+    function Static
+           (Item : in State)
+        return World'Class;
 
-    Empty_World : constant World :=
-       (Possibles => State_Vectors.Empty_Vector & Empty_State,
-        Engine    => (Kind => No_Gen));
+    Empty_World : constant World := (Ada.Finalization.Controlled with
+        Actual => new World_Component'(
+           (Kind       => Static_Node,
+            Counter    => 1,
+            Stc_States => State_Vectors."&" (State_Vectors.Empty_Vector, Empty_State))));
 
 
 end Kompsos;
diff --git a/test/pprint.adb b/test/pprint.adb
index 2003238..c42b2c8 100644
--- a/test/pprint.adb
+++ b/test/pprint.adb
@@ -50,7 +50,7 @@ begin
 
     TIO.New_Line;
 
-    TIO.Put_Line (Image_Constant (Empty_World));
+    TIO.Put_Line (Image (Empty_World));
 
 end PPrint;