Prelude now derives its own World so dot notation works for those subprograms

6 files changed, 220 insertions, 253 deletions

diff --git a/src/kompsos-prelude.adb b/src/kompsos-prelude.adb
index 58b80f4..89cc100 100644
--- a/src/kompsos-prelude.adb
+++ b/src/kompsos-prelude.adb
@@ -15,7 +15,7 @@ package body Kompsos.Prelude is
         return World is
     begin
         return Result : World := This do
-            Result.Unify (T (Term (Head_Term), T (Result.Fresh)), Full_List);
+            Result.Unify (T (Head_Term, Result.Fresh), Full_List);
         end return;
     end Head;
 
@@ -24,7 +24,7 @@ package body Kompsos.Prelude is
            (This                 : in out World;
             Full_List, Head_Term : in     Term'Class) is
     begin
-        This := Head (This, Full_List, Head_Term);
+        This := This.Head (Full_List, Head_Term);
     end Head;
 
 
@@ -36,7 +36,7 @@ package body Kompsos.Prelude is
         return World is
     begin
         return Result : World := This do
-            Result.Unify (T (T (Result.Fresh), Term (Tail_Term)), Full_List);
+            Result.Unify (T (Result.Fresh, Tail_Term), Full_List);
         end return;
     end Tail;
 
@@ -45,7 +45,7 @@ package body Kompsos.Prelude is
            (This                 : in out World;
             Full_List, Tail_Term : in     Term'Class) is
     begin
-        This := Tail (This, Full_List, Tail_Term);
+        This := This.Tail (Full_List, Tail_Term);
     end Tail;
 
 
@@ -57,7 +57,7 @@ package body Kompsos.Prelude is
         return World is
     begin
         return Result : World := This do
-            Result.Unify (T (Term (Head_Term), Term (Tail_Term)), Full_List);
+            Result.Unify (T (Head_Term, Tail_Term), Full_List);
         end return;
     end Cons;
 
@@ -66,7 +66,7 @@ package body Kompsos.Prelude is
            (This                            : in out World;
             Head_Term, Tail_Term, Full_List : in     Term'Class) is
     begin
-        This := Cons (This, Head_Term, Tail_Term, Full_List);
+        This := This.Cons (Head_Term, Tail_Term, Full_List);
     end Cons;
 
 
@@ -87,7 +87,7 @@ package body Kompsos.Prelude is
            (This     : in out World;
             Nil_Term : in     Term'Class) is
     begin
-        This := Nil (This, Nil_Term);
+        This := This.Nil (Nil_Term);
     end Nil;
 
 
@@ -99,7 +99,7 @@ package body Kompsos.Prelude is
         return World is
     begin
         return Result : World := This do
-            Cons (Result, T (Result.Fresh), T (Result.Fresh), Pair_Term);
+            Result.Cons (Result.Fresh, Result.Fresh, Pair_Term);
         end return;
     end Pair;
 
@@ -108,7 +108,7 @@ package body Kompsos.Prelude is
            (This      : in out World;
             Pair_Term : in     Term'Class) is
     begin
-        This := Pair (This, Pair_Term);
+        This := This.Pair (Pair_Term);
     end Pair;
 
 
@@ -119,18 +119,18 @@ package body Kompsos.Prelude is
             List_Term : in Term'Class)
         return World
     is
-        Result_Nil, Result_Pair : World := This;
-        Ref_Term : constant Term := T (Result_Pair.Fresh);
+        One, Two : World := This;
+        Ref_Term : constant Term := Two.Fresh;
     begin
-        Nil (Result_Nil, List_Term);
+        One.Nil (List_Term);
 
-        Pair (Result_Pair, List_Term);
-        Tail (Result_Pair, List_Term, Ref_Term);
-        if not Result_Pair.Failed then
-            Linked_List (Result_Pair, Ref_Term);
+        Two.Pair (List_Term);
+        Two.Tail (List_Term, Ref_Term);
+        if not Two.Failed then
+            Two.Linked_List (Ref_Term);
         end if;
 
-        return Disjunct (Result_Nil, Result_Pair);
+        return Disjunct (One, Two);
     end Linked_List;
 
 
@@ -138,7 +138,7 @@ package body Kompsos.Prelude is
            (This      : in out World;
             List_Term : in     Term'Class) is
     begin
-        This := Linked_List (This, List_Term);
+        This := This.Linked_List (List_Term);
     end Linked_List;
 
 
@@ -149,17 +149,17 @@ package body Kompsos.Prelude is
             Item_Term, List_Term : in Term'Class)
         return World
     is
-        Result_Head, Result_Rest : World := This;
-        Ref_Term : constant Term := T (Result_Rest.Fresh);
+        One, Two : World := This;
+        Ref_Term : constant Term := Two.Fresh;
     begin
-        Head (Result_Head, List_Term, Item_Term);
+        One.Head (List_Term, Item_Term);
 
-        Tail (Result_Rest, List_Term, Ref_Term);
-        if not Result_Rest.Failed then
-            Member (Result_Rest, Item_Term, Ref_Term);
+        Two.Tail (List_Term, Ref_Term);
+        if not Two.Failed then
+            Two.Member (Item_Term, Ref_Term);
         end if;
 
-        return Disjunct (Result_Head, Result_Rest);
+        return Disjunct (One, Two);
     end Member;
 
 
@@ -167,7 +167,7 @@ package body Kompsos.Prelude is
            (This                 : in out World;
             Item_Term, List_Term : in     Term'Class) is
     begin
-        This := Member (This, Item_Term, List_Term);
+        This := This.Member (Item_Term, List_Term);
     end Member;
 
 
@@ -178,23 +178,23 @@ package body Kompsos.Prelude is
             Item_Term, List_Term, Out_Term : in Term'Class)
         return World
     is
-        Result_Head, Result_Rest : World := This;
-        Left  : constant Term := T (Result_Rest.Fresh);
-        Right : constant Term := T (Result_Rest.Fresh);
-        Rest  : constant Term := T (Result_Rest.Fresh);
+        One, Two : World := This;
+        Left  : constant Term := Two.Fresh;
+        Right : constant Term := Two.Fresh;
+        Rest  : constant Term := Two.Fresh;
     begin
-        Head (Result_Head, List_Term, Item_Term);
-        Tail (Result_Head, List_Term, Out_Term);
+        One.Head (List_Term, Item_Term);
+        One.Tail (List_Term, Out_Term);
 
         --  infinite loops if run in reverse with vars for item and list
         --  probably needs lazy conjunction to work properly
-        Cons (Result_Rest, Left, Right, List_Term);
-        if not Result_Rest.Failed then
-            Remove (Result_Rest, Item_Term, Right, Rest);
-            Cons (Result_Rest, Left, Rest, Out_Term);
+        Two.Cons (Left, Right, List_Term);
+        if not Two.Failed then
+            Two.Remove (Item_Term, Right, Rest);
+            Two.Cons (Left, Rest, Out_Term);
         end if;
 
-        return Disjunct (Result_Head, Result_Rest);
+        return Disjunct (One, Two);
     end Remove;
 
 
@@ -202,7 +202,7 @@ package body Kompsos.Prelude is
            (This                           : in out World;
             Item_Term, List_Term, Out_Term : in     Term'Class) is
     begin
-        This := Remove (This, Item_Term, List_Term, Out_Term);
+        This := This.Remove (Item_Term, List_Term, Out_Term);
     end Remove;
 
 
@@ -213,21 +213,21 @@ package body Kompsos.Prelude is
             List_Term, Item_Term, Out_Term : in Term'Class)
         return World
     is
-        Result_Nil, Result_Rest : World := This;
-        Left  : constant Term := T (Result_Rest.Fresh);
-        Right : constant Term := T (Result_Rest.Fresh);
-        Rest  : constant Term := T (Result_Rest.Fresh);
-    begin
-        Nil (Result_Nil, List_Term);
-        Unify (Result_Nil, Item_Term, Out_Term);
-
-        Cons (Result_Rest, Left, Right, List_Term);
-        Cons (Result_Rest, Left, Rest, Out_Term);
-        if not Result_Rest.Failed then
-            Append (Result_Rest, Right, Item_Term, Rest);
+        One, Two : World := This;
+        Left  : constant Term := Two.Fresh;
+        Right : constant Term := Two.Fresh;
+        Rest  : constant Term := Two.Fresh;
+    begin
+        One.Nil (List_Term);
+        One.Unify (Item_Term, Out_Term);
+
+        Two.Cons (Left, Right, List_Term);
+        Two.Cons (Left, Rest, Out_Term);
+        if not Two.Failed then
+            Two.Append (Right, Item_Term, Rest);
         end if;
 
-        return Disjunct (Result_Nil, Result_Rest);
+        return Disjunct (One, Two);
     end Append;
 
 
@@ -235,7 +235,7 @@ package body Kompsos.Prelude is
            (This                            : in out World;
             List_Term, Item_Term, Out_Term : in     Term'Class) is
     begin
-        This := Append (This, List_Term, Item_Term, Out_Term);
+        This := This.Append (List_Term, Item_Term, Out_Term);
     end Append;
 
 
diff --git a/src/kompsos-prelude.ads b/src/kompsos-prelude.ads
index 237edbf..2ad2309 100644
--- a/src/kompsos-prelude.ads
+++ b/src/kompsos-prelude.ads
@@ -10,6 +10,13 @@ generic
 package Kompsos.Prelude is
 
 
+    type World is new Mu_World with private;
+
+    Empty_World : constant World;
+
+
+
+
     --  caro  --
 
     function Head
@@ -138,6 +145,14 @@ package Kompsos.Prelude is
     --  Skipped due to Recurse doing the same thing
 
 
+private
+
+
+    type World is new Mu_World with null record;
+
+    Empty_World : constant World := (Empty_Mu_World with null record);
+
+
 end Kompsos.Prelude;
 
 
diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 87131e1..88c13c7 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -29,6 +29,8 @@ package body Kompsos.Pretty_Print is
     end Image;
 
 
+
+
     function Image
            (Item : in ID_Number)
         return String is
@@ -123,11 +125,11 @@ package body Kompsos.Pretty_Print is
 
 
     function Image
-           (Item : in World)
+           (Item : in Mu_World'Class)
         return String
     is
         Result  : SU.Unbounded_String;
-        Scratch : World := Item;
+        Scratch : Mu_World'Class := Item;
         Counter : Positive := 1;
     begin
         if not Scratch.Has_State (Counter) then
diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads
index 3ef7ac7..1359d1f 100644
--- a/src/kompsos-pretty_print.ads
+++ b/src/kompsos-pretty_print.ads
@@ -14,17 +14,35 @@ package Kompsos.Pretty_Print is
 
 
     function Image
-           (Item : in Variable)
+           (Item : in Term)
         return String;
 
 
     function Image
-           (Item : in Term)
+           (Item : in Mu_World'Class)
+        return String;
+
+
+private
+
+
+    function Image
+           (Item : in Integer)
+        return String;
+
+
+    function Image
+           (Item : in ID_Number)
+        return String;
+
+
+    function Image
+           (Item : in Variable)
         return String;
 
 
     function Image
-           (Item : in World)
+           (Item : in State)
         return String;
 
 
diff --git a/src/kompsos.adb b/src/kompsos.adb
index 3981005..b2ff1a2 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -56,34 +56,34 @@ package body Kompsos is
 
 
 
-    --  Worlds  --
+    --  Mu_Worlds  --
 
-    procedure Free is new Ada.Unchecked_Deallocation (World, World_Access);
+    procedure Free is new Ada.Unchecked_Deallocation (Mu_World'Class, World_Access);
 
 
     procedure Adjust
-           (This : in out World) is
+           (This : in out Mu_World) is
     begin
         case This.Engine.Kind is
         when No_Gen =>
             null;
         when Fresh_Gen =>
-            This.Engine.FrG_World := new World'(This.Engine.FrG_World.all);
+            This.Engine.FrG_World := new Mu_World'Class'(This.Engine.FrG_World.all);
         when Unify_Gen =>
-            This.Engine.UniG_World := new World'(This.Engine.UniG_World.all);
+            This.Engine.UniG_World := new Mu_World'Class'(This.Engine.UniG_World.all);
         when Disjunct1_Gen =>
-            This.Engine.Dis1G_World := new World'(This.Engine.Dis1G_World.all);
+            This.Engine.Dis1G_World := new Mu_World'Class'(This.Engine.Dis1G_World.all);
         when Disjunct2_Gen =>
-            This.Engine.Dis2G_World1 := new World'(This.Engine.Dis2G_World1.all);
-            This.Engine.Dis2G_World2 := new World'(This.Engine.Dis2G_World2.all);
+            This.Engine.Dis2G_World1 := new Mu_World'Class'(This.Engine.Dis2G_World1.all);
+            This.Engine.Dis2G_World2 := new Mu_World'Class'(This.Engine.Dis2G_World2.all);
         when Recurse_Gen =>
-            This.Engine.RecG_World := new World'(This.Engine.RecG_World.all);
+            This.Engine.RecG_World := new Mu_World'Class'(This.Engine.RecG_World.all);
         end case;
     end Adjust;
 
 
     procedure Finalize
-           (This : in out World) is
+           (This : in out Mu_World) is
     begin
         case This.Engine.Kind is
         when No_Gen =>
@@ -160,15 +160,15 @@ package body Kompsos is
 
 
     function T
-           (Item1, Item2 : in Term)
+           (Item1, Item2 : in Term'Class)
         return Term is
     begin
         return My_Term : Term do
             My_Term.Actual := new Term_Component'(
                 Kind  => Pair_Term,
                 Count => 1,
-                Left  => Item1,
-                Right => Item2);
+                Left  => Term (Item1),
+                Right => Term (Item2));
         end return;
     end T;
 
@@ -348,7 +348,7 @@ package body Kompsos is
     --  Lazy World Generation --
 
     function Has_State
-           (This  : in out World;
+           (This  : in out Mu_World;
             Index : in     Positive)
         return Boolean is
     begin
@@ -358,7 +358,7 @@ package body Kompsos is
 
 
     procedure Roll_Fresh_Gen
-           (This : in out World) is
+           (This : in out Mu_World) is
     begin
         This.Engine.FrG_World.Rollover;
         if This.Engine.FrG_World.Possibles.Last_Index < This.Engine.FrG_Index then
@@ -376,7 +376,7 @@ package body Kompsos is
 
 
     procedure Roll_Unify_Gen
-           (This : in out World)
+           (This : in out Mu_World)
     is
         Extended : State;
     begin
@@ -402,7 +402,7 @@ package body Kompsos is
 
 
     procedure Roll_Disjunct1_Gen
-           (This : in out World) is
+           (This : in out Mu_World) is
     begin
         This.Engine.Dis1G_World.Rollover;
         if This.Engine.Dis1G_World.Possibles.Last_Index < This.Engine.Dis1G_Index then
@@ -417,7 +417,7 @@ package body Kompsos is
 
 
     procedure Roll_Disjunct2_Gen
-           (This : in out World)
+           (This : in out Mu_World)
     is
         Temp_World : World_Access;
         Temp_Index : Positive;
@@ -445,7 +445,7 @@ package body Kompsos is
 
 
     procedure Roll_Recurse_Gen
-           (This : in out World) is
+           (This : in out Mu_World) is
     begin
         This.Engine.RecG_World.Rollover;
         if This.Engine.RecG_World.Possibles.Last_Index < This.Engine.RecG_Index then
@@ -467,7 +467,7 @@ package body Kompsos is
     --  This is intentional to get better behaviour with infinite Worlds.
 
     procedure Rollover
-           (This : in out World) is
+           (This : in out Mu_World) is
     begin
         case This.Engine.Kind is
         when No_Gen        => null;
@@ -481,7 +481,7 @@ package body Kompsos is
 
 
     procedure Roll_Until
-           (This  : in out World;
+           (This  : in out Mu_World;
             Index : in     Positive) is
     begin
         while This.Possibles.Last_Index < Index and This.Engine.Kind /= No_Gen loop
@@ -496,51 +496,38 @@ package body Kompsos is
     --  Public API Operations  --
     -----------------------------
 
-    --  Query  --
-
-    function Failed
-           (This : in out World)
-        return Boolean is
-    begin
-        return not This.Has_State (1);
-    end Failed;
-
-
-
-
     --  Fresh  --
 
     function Fresh
-           (This : in out World)
-        return Variable is
+           (This : in out Mu_World'Class)
+        return Term is
     begin
         return This.Fresh (+"");
     end Fresh;
 
 
     function Fresh
-           (This : in out World;
+           (This : in out Mu_World'Class;
             Name : in     String)
-        return Variable is
+        return Term is
     begin
         return This.Fresh (+Name);
     end Fresh;
 
 
     function Fresh
-           (This : in out World;
+           (This : in out Mu_World'Class;
             Name : in     Ada.Strings.Unbounded.Unbounded_String)
-        return Variable is
+        return Term is
     begin
-        return My_Var : constant Variable := (Ident => This.Next_Ident, Name => Name) do
-            This := (Ada.Finalization.Controlled with
-                Possibles  => State_Vectors.Empty_Vector,
-                Next_Ident => This.Next_Ident + 1,
-                Engine     =>
-                   (Kind      => Fresh_Gen,
-                    FrG_World => new World'(This),
-                    FrG_Index => 1,
-                    FrG_Name  => Name));
+        return My_Term : constant Term := T (Variable'(Ident => This.Next_Ident, Name => Name)) do
+            This.Engine :=
+               (Kind      => Fresh_Gen,
+                FrG_World => new Mu_World'Class'(This),
+                FrG_Index => 1,
+                FrG_Name  => Name);
+            This.Next_Ident := This.Next_Ident + 1;
+            This.Possibles := State_Vectors.Empty_Vector;
         end return;
     end Fresh;
 
@@ -550,71 +537,35 @@ package body Kompsos is
     --  Unify  --
 
     function Unify
-           (This  : in World;
-            Left  : in Variable;
+           (This  : in Mu_World;
+            Left  : in Term'Class;
             Right : in Element_Type)
-        return World is
+        return Mu_World is
     begin
-        return This.Unify (T (Left), T (Right));
+        return This.Unify (Left, T (Right));
     end Unify;
 
 
     procedure Unify
-           (This  : in out World;
-            Left  : in     Variable;
+           (This  : in out Mu_World;
+            Left  : in     Term'Class;
             Right : in     Element_Type) is
     begin
-        This := This.Unify (T (Left), T (Right));
-    end Unify;
-
-
-    function Unify
-           (This        : in World;
-            Left, Right : in Variable)
-        return World is
-    begin
-        return This.Unify (T (Left), T (Right));
-    end Unify;
-
-
-    procedure Unify
-           (This        : in out World;
-            Left, Right : in     Variable) is
-    begin
-        This := This.Unify (T (Left), T (Right));
+        This := This.Unify (Left, T (Right));
     end Unify;
 
 
     function Unify
-           (This  : in World;
-            Left  : in Variable;
-            Right : in Term'Class)
-        return World is
-    begin
-        return This.Unify (T (Left), Right);
-    end Unify;
-
-
-    procedure Unify
-           (This  : in out World;
-            Left  : in     Variable;
-            Right : in     Term'Class) is
-    begin
-        This := This.Unify (T (Left), Right);
-    end Unify;
-
-
-    function Unify
-           (This        : in World;
+           (This        : in Mu_World;
             Left, Right : in Term'Class)
-        return World is
+        return Mu_World is
     begin
-        return Result : constant World := (Ada.Finalization.Controlled with
+        return Result : constant Mu_World := (Ada.Finalization.Controlled with
             Possibles  => State_Vectors.Empty_Vector,
             Next_Ident => This.Next_Ident,
             Engine     =>
                (Kind       => Unify_Gen,
-                UniG_World => new World'(This),
+                UniG_World => new Mu_World'(This),
                 UniG_Index => 1,
                 UniG_Term1 => Term (Left),
                 UniG_Term2 => Term (Right)));
@@ -622,7 +573,7 @@ package body Kompsos is
 
 
     procedure Unify
-           (This        : in out World;
+           (This        : in out Mu_World;
             Left, Right : in     Term'Class) is
     begin
         This := This.Unify (Left, Right);
@@ -634,49 +585,50 @@ package body Kompsos is
     --  Disjunct  --
 
     function Disjunct
-           (Left, Right : in World)
-        return World is
+           (Left, Right : in Mu_World)
+        return Mu_World is
     begin
-        return Result : constant World := (Ada.Finalization.Controlled with
+        return Result : constant Mu_World := (Ada.Finalization.Controlled with
             Possibles  => State_Vectors.Empty_Vector,
             Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident),
             Engine     =>
                (Kind         => Disjunct2_Gen,
-                Dis2G_World1 => new World'(Left),
+                Dis2G_World1 => new Mu_World'(Left),
                 Dis2G_Index1 => 1,
-                Dis2G_World2 => new World'(Right),
+                Dis2G_World2 => new Mu_World'(Right),
                 Dis2G_Index2 => 1));
     end Disjunct;
 
 
     procedure Disjunct
-           (This  : in out World;
-            Right : in     World) is
+           (This  : in out Mu_World;
+            Right : in     Mu_World) is
     begin
         This := Disjunct (This, Right);
     end Disjunct;
 
 
     function Disjunct
-           (Inputs : in World_Array)
-        return World is
+           (Inputs : in Mu_World_Array)
+        return Mu_World is
     begin
         if Inputs'Length = 0 then
-            return Failed : constant World := (Ada.Finalization.Controlled with
+            return Failed : constant Mu_World := (Ada.Finalization.Controlled with
                 Possibles  => State_Vectors.Empty_Vector,
                 Next_Ident => 0,
                 Engine     => (Kind => No_Gen));
         elsif Inputs'Length = 1 then
             return Inputs (Inputs'First);
         else
-            return Result : World := (Ada.Finalization.Controlled with
+            return Result : Mu_World := (Ada.Finalization.Controlled with
                 Possibles  => State_Vectors.Empty_Vector,
                 Next_Ident => 0,  --  dummy
                 Engine     =>
                    (Kind         => Disjunct2_Gen,
-                    Dis2G_World1 => new World'(Inputs (Inputs'First)),
+                    Dis2G_World1 => new Mu_World'(Inputs (Inputs'First)),
                     Dis2G_Index1 => 1,
-                    Dis2G_World2 => new World'(Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))),
+                    Dis2G_World2 =>
+                        new Mu_World'(Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last))),
                     Dis2G_Index2 => 1))
             do
                 Result.Next_Ident := ID_Number'Max
@@ -688,8 +640,8 @@ package body Kompsos is
 
 
     procedure Disjunct
-           (This   : in out World;
-            Inputs : in     World_Array) is
+           (This   : in out Mu_World;
+            Inputs : in     Mu_World_Array) is
     begin
         This := Disjunct (This & Inputs);
     end Disjunct;
@@ -700,21 +652,21 @@ package body Kompsos is
     --  Recurse  --
 
     function Recurse
-           (This : in World)
-        return World is
+           (This : in Mu_World)
+        return Mu_World is
     begin
-        return Result : constant World := (Ada.Finalization.Controlled with
+        return Result : constant Mu_World := (Ada.Finalization.Controlled with
             Possibles  => State_Vectors.Empty_Vector,
             Next_Ident => This.Next_Ident,
             Engine     =>
                (Kind       => Recurse_Gen,
-                RecG_World => new World'(This),
+                RecG_World => new Mu_World'(This),
                 RecG_Index => 1));
     end Recurse;
 
 
     procedure Recurse
-           (This : in out World) is
+           (This : in out Mu_World) is
     begin
         This := This.Recurse;
     end Recurse;
@@ -725,9 +677,9 @@ package body Kompsos is
     --  Forced Evaluation  --
 
     function Take
-           (This  : in World;
+           (This  : in Mu_World;
             Count : in Natural)
-        return World is
+        return Mu_World is
     begin
         if Count = 0 then
             return (Ada.Finalization.Controlled with
@@ -735,7 +687,7 @@ package body Kompsos is
                 Next_Ident => ID_Number'First,
                 Engine     => (Kind => No_Gen));
         end if;
-        return Result : World := This do
+        return Result : Mu_World := This do
             Result.Roll_Until (Count);
             if Result.Possibles.Last_Index > Count then
                 Result.Possibles.Set_Length (Ada.Containers.Count_Type (Count));
@@ -746,7 +698,7 @@ package body Kompsos is
 
 
     procedure Take
-           (This  : in out World;
+           (This  : in out Mu_World;
             Count : in     Natural) is
     begin
         This := This.Take (Count);
@@ -754,7 +706,7 @@ package body Kompsos is
 
 
     procedure Force
-           (This  : in out World;
+           (This  : in out Mu_World;
             Count : in     Positive) is
     begin
         This.Roll_Until (Count);
@@ -762,7 +714,7 @@ package body Kompsos is
 
 
     procedure Force_All
-           (This : in out World) is
+           (This : in out Mu_World) is
     begin
         while This.Engine.Kind /= No_Gen loop
             This.Rollover;
@@ -770,6 +722,14 @@ package body Kompsos is
     end Force_All;
 
 
+    function Failed
+           (This : in out Mu_World)
+        return Boolean is
+    begin
+        return not This.Has_State (1);
+    end Failed;
+
+
 end Kompsos;
 
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index bed3d26..a8b8851 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -22,10 +22,6 @@ generic
 package Kompsos is
 
 
-    type Variable is private;
-    type Variable_Array is array (Positive range <>) of Variable;
-
-
     type Term is tagged private;
     type Term_Array is array (Positive range <>) of Term;
 
@@ -42,11 +38,7 @@ package Kompsos is
         return Term;
 
     function T
-           (Item : in Variable)
-        return Term;
-
-    function T
-           (Item1, Item2 : in Term)
+           (Item1, Item2 : in Term'Class)
         return Term;
 
     function T
@@ -56,122 +48,102 @@ package Kompsos is
     --  Might include subprograms to retrieve Term contents later?
 
 
-    type World is tagged private;
-    type World_Array is array (Positive range <>) of World;
+    type Mu_World is tagged private;
+    type Mu_World_Array is array (Positive range <>) of Mu_World;
 
-    Empty_World : constant World;
-
-    function Failed
-           (This : in out World)
-        return Boolean;
+    Empty_Mu_World : constant Mu_World;
 
 
 
 
     function Fresh
-           (This : in out World)
-        return Variable;
+           (This : in out Mu_World'Class)
+        return Term;
 
     function Fresh
-           (This : in out World;
+           (This : in out Mu_World'Class;
             Name : in     String)
-        return Variable;
+        return Term;
 
     function Fresh
-           (This : in out World;
+           (This : in out Mu_World'Class;
             Name : in     Ada.Strings.Unbounded.Unbounded_String)
-        return Variable;
+        return Term;
 
 
 
 
     function Unify
-           (This  : in World;
-            Left  : in Variable;
+           (This  : in Mu_World;
+            Left  : in Term'Class;
             Right : in Element_Type)
-        return World;
+        return Mu_World;
 
     procedure Unify
-           (This  : in out World;
-            Left  : in     Variable;
+           (This  : in out Mu_World;
+            Left  : in     Term'Class;
             Right : in     Element_Type);
 
     function Unify
-           (This        : in World;
-            Left, Right : in Variable)
-        return World;
-
-    procedure Unify
-           (This        : in out World;
-            Left, Right : in     Variable);
-
-    function Unify
-           (This  : in World;
-            Left  : in Variable;
-            Right : in Term'Class)
-        return World;
-
-    procedure Unify
-           (This  : in out World;
-            Left  : in     Variable;
-            Right : in     Term'Class);
-
-    function Unify
-           (This        : in World;
+           (This        : in Mu_World;
             Left, Right : in Term'Class)
-        return World;
+        return Mu_World;
 
     procedure Unify
-           (This        : in out World;
+           (This        : in out Mu_World;
             Left, Right : in     Term'Class);
 
 
 
 
     function Disjunct
-           (Left, Right : in World)
-        return World;
+           (Left, Right : in Mu_World)
+        return Mu_World;
 
     procedure Disjunct
-           (This  : in out World;
-            Right : in     World);
+           (This  : in out Mu_World;
+            Right : in     Mu_World);
 
     function Disjunct
-           (Inputs : in World_Array)
-        return World;
+           (Inputs : in Mu_World_Array)
+        return Mu_World;
 
     procedure Disjunct
-           (This   : in out World;
-            Inputs : in     World_Array);
+           (This   : in out Mu_World;
+            Inputs : in     Mu_World_Array);
 
 
 
 
     function Recurse
-           (This : in World)
-        return World;
+           (This : in Mu_World)
+        return Mu_World;
 
     procedure Recurse
-           (This : in out World);
+           (This : in out Mu_World);
 
 
 
 
     function Take
-           (This  : in World;
+           (This  : in Mu_World;
             Count : in Natural)
-        return World;
+        return Mu_World;
 
     procedure Take
-           (This  : in out World;
+           (This  : in out Mu_World;
             Count : in     Natural);
 
     procedure Force
-           (This  : in out World;
+           (This  : in out Mu_World;
             Count : in     Positive);
 
     procedure Force_All
-           (This : in out World);
+           (This : in out Mu_World);
+
+    function Failed
+           (This : in out Mu_World)
+        return Boolean;
 
 
 private
@@ -259,7 +231,7 @@ private
 
 
 
-    type World_Access is access World;
+    type World_Access is access Mu_World'Class;
 
     type Generator_Kind is
        (No_Gen,
@@ -300,33 +272,33 @@ private
        (Index_Type   => Positive,
         Element_Type => State);
 
-    type World is new Ada.Finalization.Controlled with record
+    type Mu_World is new Ada.Finalization.Controlled with record
         Possibles  : State_Vectors.Vector;
         Next_Ident : ID_Number;
         Engine     : Generator;
     end record;
 
     overriding procedure Adjust
-           (This : in out World);
+           (This : in out Mu_World);
 
     overriding procedure Finalize
-           (This : in out World);
+           (This : in out Mu_World);
 
     function Has_State
-           (This  : in out World;
+           (This  : in out Mu_World;
             Index : in     Positive)
         return Boolean;
 
     procedure Rollover
-           (This : in out World);
+           (This : in out Mu_World);
 
     procedure Roll_Until
-           (This  : in out World;
+           (This  : in out Mu_World;
             Index : in     Positive);
 
     use type State_Vectors.Vector;
 
-    Empty_World : constant World := (Ada.Finalization.Controlled with
+    Empty_Mu_World : constant Mu_World := (Ada.Finalization.Controlled with
         Possibles  => State_Vectors.Empty_Vector & Empty_State,
         Next_Ident => 0,
         Engine     => (Kind => No_Gen));