Prelude combined into base, lazy Conjunct kinda working but still loops in some circumstances

10 files changed, 755 insertions, 529 deletions

diff --git a/src/kompsos-prelude.adb b/src/kompsos-prelude.adb
deleted file mode 100644
index 896e918..0000000
--- a/src/kompsos-prelude.adb
+++ /dev/null
@@ -1,244 +0,0 @@
-
-
---  Programmed by Jedidiah Barber
---  Licensed under the Sunset License v1.0
-
---  See license.txt for further details
-
-
-package body Kompsos.Prelude is
-
-
-    function Head
-           (This                 : in World;
-            Full_List, Head_Term : in Term'Class)
-        return World is
-    begin
-        return Result : World := This do
-            Result.Unify (T (Head_Term, Result.Fresh), Full_List);
-        end return;
-    end Head;
-
-
-    procedure Head
-           (This                 : in out World;
-            Full_List, Head_Term : in     Term'Class) is
-    begin
-        This := This.Head (Full_List, Head_Term);
-    end Head;
-
-
-
-
-    function Tail
-           (This                 : in World;
-            Full_List, Tail_Term : in Term'Class)
-        return World is
-    begin
-        return Result : World := This do
-            Result.Unify (T (Result.Fresh, Tail_Term), Full_List);
-        end return;
-    end Tail;
-
-
-    procedure Tail
-           (This                 : in out World;
-            Full_List, Tail_Term : in     Term'Class) is
-    begin
-        This := This.Tail (Full_List, Tail_Term);
-    end Tail;
-
-
-
-
-    function Cons
-           (This                            : in World;
-            Head_Term, Tail_Term, Full_List : in Term'Class)
-        return World is
-    begin
-        return Result : World := This do
-            Result.Unify (T (Head_Term, Tail_Term), Full_List);
-        end return;
-    end Cons;
-
-
-    procedure Cons
-           (This                            : in out World;
-            Head_Term, Tail_Term, Full_List : in     Term'Class) is
-    begin
-        This := This.Cons (Head_Term, Tail_Term, Full_List);
-    end Cons;
-
-
-
-
-    function Nil
-           (This     : in World;
-            Nil_Term : in Term'Class)
-        return World is
-    begin
-        return Result : World := This do
-            Result.Unify (Null_Term, Nil_Term);
-        end return;
-    end Nil;
-
-
-    procedure Nil
-           (This     : in out World;
-            Nil_Term : in     Term'Class) is
-    begin
-        This := This.Nil (Nil_Term);
-    end Nil;
-
-
-
-
-    function Pair
-           (This      : in World;
-            Pair_Term : in Term'Class)
-        return World is
-    begin
-        return Result : World := This do
-            Result.Cons (Result.Fresh, Result.Fresh, Pair_Term);
-        end return;
-    end Pair;
-
-
-    procedure Pair
-           (This      : in out World;
-            Pair_Term : in     Term'Class) is
-    begin
-        This := This.Pair (Pair_Term);
-    end Pair;
-
-
-
-
-    function Linked_List
-           (This      : in World;
-            List_Term : in Term'Class)
-        return World
-    is
-        One, Two : World := This;
-        Ref_Term : constant Term := Two.Fresh;
-    begin
-        One.Nil (List_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 (One, Two);
-    end Linked_List;
-
-
-    procedure Linked_List
-           (This      : in out World;
-            List_Term : in     Term'Class) is
-    begin
-        This := This.Linked_List (List_Term);
-    end Linked_List;
-
-
-
-
-    function Member
-           (This                 : in World;
-            Item_Term, List_Term : in Term'Class)
-        return World
-    is
-        One, Two : World := This;
-        Ref_Term : constant Term := Two.Fresh;
-    begin
-        One.Head (List_Term, Item_Term);
-
-        Two.Tail (List_Term, Ref_Term);
-        if not Two.Failed then
-            Two.Member (Item_Term, Ref_Term);
-        end if;
-
-        return Disjunct (One, Two);
-    end Member;
-
-
-    procedure Member
-           (This                 : in out World;
-            Item_Term, List_Term : in     Term'Class) is
-    begin
-        This := This.Member (Item_Term, List_Term);
-    end Member;
-
-
-
-
-    function Remove
-           (This                           : in World;
-            Item_Term, List_Term, Out_Term : in Term'Class)
-        return World
-    is
-        One, Two : World := This;
-        Left  : constant Term := Two.Fresh;
-        Right : constant Term := Two.Fresh;
-        Rest  : constant Term := Two.Fresh;
-    begin
-        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
-        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 (One, Two);
-    end Remove;
-
-
-    procedure Remove
-           (This                           : in out World;
-            Item_Term, List_Term, Out_Term : in     Term'Class) is
-    begin
-        This := This.Remove (Item_Term, List_Term, Out_Term);
-    end Remove;
-
-
-
-
-    function Append
-           (This                           : in World;
-            List_Term, Item_Term, Out_Term : in Term'Class)
-        return World
-    is
-        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 (One, Two);
-    end Append;
-
-
-    procedure Append
-           (This                           : in out World;
-            List_Term, Item_Term, Out_Term : in     Term'Class) is
-    begin
-        This := This.Append (List_Term, Item_Term, Out_Term);
-    end Append;
-
-
-end Kompsos.Prelude;
-
-
diff --git a/src/kompsos-prelude.ads b/src/kompsos-prelude.ads
deleted file mode 100644
index 2ad2309..0000000
--- a/src/kompsos-prelude.ads
+++ /dev/null
@@ -1,158 +0,0 @@
-
-
---  Programmed by Jedidiah Barber
---  Licensed under the Sunset License v1.0
-
---  See license.txt for further details
-
-
-generic
-package Kompsos.Prelude is
-
-
-    type World is new Mu_World with private;
-
-    Empty_World : constant World;
-
-
-
-
-    --  caro  --
-
-    function Head
-           (This                 : in World;
-            Full_List, Head_Term : in Term'Class)
-        return World;
-
-    procedure Head
-           (This                 : in out World;
-            Full_List, Head_Term : in     Term'Class);
-
-
-    --  cdro  --
-
-    function Tail
-           (This                 : in World;
-            Full_List, Tail_Term : in Term'Class)
-        return World;
-
-    procedure Tail
-           (This                 : in out World;
-            Full_List, Tail_Term : in     Term'Class);
-
-
-    --  conso  --
-
-    function Cons
-           (This                            : in World;
-            Head_Term, Tail_Term, Full_List : in Term'Class)
-        return World;
-
-    procedure Cons
-           (This                            : in out World;
-            Head_Term, Tail_Term, Full_List : in     Term'Class);
-
-
-    --  nullo  --
-
-    function Nil
-           (This     : in World;
-            Nil_Term : in Term'Class)
-        return World;
-
-    procedure Nil
-           (This     : in out World;
-            Nil_Term : in     Term'Class);
-
-
-    --  eqo  --
-    --  Skipped due to being a synonym for Unify
-
-
-    --  eq-caro  --
-    --  Skipped due to being a synonym for Head
-
-
-    --  pairo  --
-
-    function Pair
-           (This      : in World;
-            Pair_Term : in Term'Class)
-        return World;
-
-    procedure Pair
-           (This      : in out World;
-            Pair_Term : in     Term'Class);
-
-
-    --  listo  --
-
-    function Linked_List
-           (This      : in World;
-            List_Term : in Term'Class)
-        return World;
-
-    procedure Linked_List
-           (This      : in out World;
-            List_Term : in     Term'Class);
-
-
-    --  membero  --
-
-    function Member
-           (This                 : in World;
-            Item_Term, List_Term : in Term'Class)
-        return World;
-
-    procedure Member
-           (This                 : in out World;
-            Item_Term, List_Term : in     Term'Class);
-
-
-    --  rembero  --
-
-    function Remove
-           (This                           : in World;
-            Item_Term, List_Term, Out_Term : in Term'Class)
-        return World;
-
-    procedure Remove
-           (This                           : in out World;
-            Item_Term, List_Term, Out_Term : in     Term'Class);
-
-
-    --  appendo  --
-
-    function Append
-           (This                           : in World;
-            List_Term, Item_Term, Out_Term : in Term'Class)
-        return World;
-
-    procedure Append
-           (This                            : in out World;
-            List_Term, Item_Term, Out_Term : in     Term'Class);
-
-
-    --  anyo  --
-    --  Skipped due to Recurse doing the same thing
-
-
-    --  nevero  --
-    --  Skipped since it just creates a failed World
-
-
-    --  alwayso  --
-    --  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 88c13c7..7ecbb75 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -125,11 +125,11 @@ package body Kompsos.Pretty_Print is
 
 
     function Image
-           (Item : in Mu_World'Class)
+           (Item : in World)
         return String
     is
         Result  : SU.Unbounded_String;
-        Scratch : Mu_World'Class := Item;
+        Scratch : World := 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 1359d1f..ed9509a 100644
--- a/src/kompsos-pretty_print.ads
+++ b/src/kompsos-pretty_print.ads
@@ -19,7 +19,7 @@ package Kompsos.Pretty_Print is
 
 
     function Image
-           (Item : in Mu_World'Class)
+           (Item : in World)
         return String;
 
 
diff --git a/src/kompsos.adb b/src/kompsos.adb
index cb2f775..c1d63da 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -55,10 +55,9 @@ package body Kompsos is
 
 
 
-
     --  World_Holders  --
 
-    procedure Free is new Ada.Unchecked_Deallocation (Mu_World'Class, World_Access);
+    procedure Free is new Ada.Unchecked_Deallocation (World'Class, World_Access);
 
 
     procedure Initialize
@@ -71,7 +70,7 @@ package body Kompsos is
     procedure Adjust
            (This : in out World_Holder) is
     begin
-        This.Ptr := new Mu_World'Class'(This.Ptr.all);
+        This.Ptr := new World'Class'(This.Ptr.all);
     end Adjust;
 
 
@@ -83,10 +82,10 @@ package body Kompsos is
 
 
     function Hold
-           (This : in Mu_World'Class)
+           (This : in World'Class)
         return World_Holder is
     begin
-        return (Ada.Finalization.Controlled with Ptr => new Mu_World'Class'(This));
+        return (Ada.Finalization.Controlled with Ptr => new World'Class'(This));
     end Hold;
 
 
@@ -102,9 +101,11 @@ package body Kompsos is
 
 
 
-    -------------
+    -----------------
+    --  Datatypes  --
+    -----------------
+
     --  Terms  --
-    -------------
 
     function "="
            (Left, Right : in Term)
@@ -341,11 +342,10 @@ package body Kompsos is
 
 
 
-
     --  Lazy World Generation --
 
     function Has_State
-           (This  : in out Mu_World;
+           (This  : in out World;
             Index : in     Positive)
         return Boolean is
     begin
@@ -355,7 +355,7 @@ package body Kompsos is
 
 
     procedure Roll_Fresh_Gen
-           (This : in out Mu_World) is
+           (This : in out World) is
     begin
         This.Engine.Frs_World.Ptr.Rollover;
         for Potential of This.Engine.Frs_World.Ptr.Possibles loop
@@ -371,7 +371,7 @@ package body Kompsos is
 
 
     procedure Roll_Unify_Gen
-           (This : in out Mu_World)
+           (This : in out World)
     is
         Extended : State;
     begin
@@ -390,7 +390,7 @@ package body Kompsos is
 
 
     procedure Roll_Buffer_Gen
-           (This : in out Mu_World) is
+           (This : in out World) is
     begin
         This.Engine.Buff_World.Ptr.Rollover;
         This.Possibles.Append (This.Engine.Buff_World.Ptr.Possibles);
@@ -403,7 +403,7 @@ package body Kompsos is
 
 
     procedure Roll_Disjunct_Gen
-           (This : in out Mu_World) is
+           (This : in out World) is
     begin
         This.Engine.Dis_World1.Ptr.Rollover;
         This.Possibles.Append (This.Engine.Dis_World1.Ptr.Possibles);
@@ -416,8 +416,67 @@ package body Kompsos is
     end Roll_Disjunct_Gen;
 
 
+    procedure Roll_Conjunct_Zero_Gen
+           (This : in out World)
+    is
+        use type Ada.Containers.Count_Type;
+    begin
+        This.Engine.ConZ_World.Ptr.Rollover;
+        if This.Engine.ConZ_World.Ptr.Possibles.Length > 0 then
+            declare
+                Next : constant World := This.Engine.ConZ_Func
+                   (World (This.Engine.ConZ_World.Ptr.all));
+            begin
+                This := Next;
+            end;
+        elsif This.Engine.ConZ_World.Ptr.Engine.Kind = No_Gen then
+            This.Engine := (Kind => No_Gen);
+        end if;
+    end Roll_Conjunct_Zero_Gen;
+
+
+    procedure Roll_Conjunct_One_Gen
+           (This : in out World)
+    is
+        use type Ada.Containers.Count_Type;
+    begin
+        This.Engine.ConO_World.Ptr.Rollover;
+        if This.Engine.ConO_World.Ptr.Possibles.Length > 0 then
+            declare
+                Next : constant World := This.Engine.ConO_Func
+                   (World (This.Engine.ConO_World.Ptr.all),
+                    This.Engine.ConO_Input);
+            begin
+                This := Next;
+            end;
+        elsif This.Engine.ConO_World.Ptr.Engine.Kind = No_Gen then
+            This.Engine := (Kind => No_Gen);
+        end if;
+    end Roll_Conjunct_One_Gen;
+
+
+    procedure Roll_Conjunct_Many_Gen
+           (This : in out World)
+    is
+        use type Ada.Containers.Count_Type;
+    begin
+        This.Engine.ConM_World.Ptr.Rollover;
+        if This.Engine.ConM_World.Ptr.Possibles.Length > 0 then
+            declare
+                Next : constant World := This.Engine.ConM_Func
+                   (World (This.Engine.ConM_World.Ptr.all),
+                    This.Engine.ConM_Inputs.Constant_Reference);
+            begin
+                This := Next;
+            end;
+        elsif This.Engine.ConM_World.Ptr.Engine.Kind = No_Gen then
+            This.Engine := (Kind => No_Gen);
+        end if;
+    end Roll_Conjunct_Many_Gen;
+
+
     procedure Roll_Recurse_Gen
-           (This : in out Mu_World) is
+           (This : in out World) is
     begin
         This.Engine.Rec_World.Ptr.Rollover;
         if This.Engine.Rec_World.Ptr.Possibles.Last_Index < This.Engine.Rec_Index then
@@ -440,21 +499,24 @@ package body Kompsos is
 
 
     procedure Rollover
-           (This : in out Mu_World) is
+           (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 Buffer_Gen   => This.Roll_Buffer_Gen;
-        when Disjunct_Gen => This.Roll_Disjunct_Gen;
-        when Recurse_Gen  => This.Roll_Recurse_Gen;
+        when No_Gen            => null;
+        when Fresh_Gen         => This.Roll_Fresh_Gen;
+        when Unify_Gen         => This.Roll_Unify_Gen;
+        when Buffer_Gen        => This.Roll_Buffer_Gen;
+        when Disjunct_Gen      => This.Roll_Disjunct_Gen;
+        when Conjunct_Zero_Gen => This.Roll_Conjunct_Zero_Gen;
+        when Conjunct_One_Gen  => This.Roll_Conjunct_One_Gen;
+        when Conjunct_Many_Gen => This.Roll_Conjunct_Many_Gen;
+        when Recurse_Gen       => This.Roll_Recurse_Gen;
         end case;
     end Rollover;
 
 
     procedure Roll_Until
-           (This  : in out Mu_World;
+           (This  : in out World;
             Index : in     Positive) is
     begin
         while This.Possibles.Last_Index < Index and This.Engine.Kind /= No_Gen loop
@@ -465,14 +527,14 @@ package body Kompsos is
 
 
 
-    -----------------------------
-    --  Public API Operations  --
-    -----------------------------
+    -------------------
+    --  microKanren  --
+    -------------------
 
-    --  Fresh  --
+    --  Variable Introduction  --
 
     function Fresh
-           (This : in out Mu_World'Class)
+           (This : in out World'Class)
         return Term is
     begin
         return This.Fresh (+"");
@@ -480,7 +542,7 @@ package body Kompsos is
 
 
     function Fresh
-           (This : in out Mu_World'Class;
+           (This : in out World'Class;
             Name : in     String)
         return Term is
     begin
@@ -489,7 +551,7 @@ package body Kompsos is
 
 
     function Fresh
-           (This : in out Mu_World'Class;
+           (This : in out World'Class;
             Name : in     Ada.Strings.Unbounded.Unbounded_String)
         return Term is
     begin
@@ -505,21 +567,20 @@ package body Kompsos is
 
 
 
-
-    --  Unify  --
+    --  Unification  --
 
     function Unify
-           (This  : in Mu_World;
+           (This  : in World;
             Left  : in Term'Class;
             Right : in Element_Type)
-        return Mu_World is
+        return World is
     begin
         return This.Unify (Left, T (Right));
     end Unify;
 
 
     procedure Unify
-           (This  : in out Mu_World;
+           (This  : in out World;
             Left  : in     Term'Class;
             Right : in     Element_Type) is
     begin
@@ -528,11 +589,11 @@ package body Kompsos is
 
 
     function Unify
-           (This        : in Mu_World;
+           (This        : in World;
             Left, Right : in Term'Class)
-        return Mu_World is
+        return World is
     begin
-        return Result : constant Mu_World :=
+        return Result : constant World :=
            (Possibles  => State_Vectors.Empty_Vector,
             Next_Ident => This.Next_Ident,
             Engine     =>
@@ -544,7 +605,7 @@ package body Kompsos is
 
 
     procedure Unify
-           (This        : in out Mu_World;
+           (This        : in out World;
             Left, Right : in     Term'Class) is
     begin
         This := This.Unify (Left, Right);
@@ -552,14 +613,13 @@ package body Kompsos is
 
 
 
-
-    --  Disjunct  --
+    --  Combining / Disjunction  --
 
     function Disjunct
-           (Left, Right : in Mu_World)
-        return Mu_World is
+           (Left, Right : in World)
+        return World is
     begin
-        return Result : constant Mu_World :=
+        return Result : constant World :=
            (Possibles  => State_Vectors.Empty_Vector,
             Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident),
             Engine     =>
@@ -570,26 +630,26 @@ package body Kompsos is
 
 
     procedure Disjunct
-           (This  : in out Mu_World;
-            Right : in     Mu_World) is
+           (This  : in out World;
+            Right : in     World) is
     begin
         This := Disjunct (This, Right);
     end Disjunct;
 
 
     function Disjunct
-           (Inputs : in Mu_World_Array)
-        return Mu_World is
+           (Inputs : in World_Array)
+        return World is
     begin
         if Inputs'Length = 0 then
-            return Failed : constant Mu_World :=
+            return Failed : constant World :=
                (Possibles  => State_Vectors.Empty_Vector,
                 Next_Ident => 0,
                 Engine     => (Kind => No_Gen));
         elsif Inputs'Length = 1 then
             return Inputs (Inputs'First);
         else
-            return Result : Mu_World :=
+            return Result : World :=
                (Possibles  => State_Vectors.Empty_Vector,
                 Next_Ident => 0,  --  dummy
                 Engine     =>
@@ -606,22 +666,104 @@ package body Kompsos is
 
 
     procedure Disjunct
-           (This   : in out Mu_World;
-            Inputs : in     Mu_World_Array) is
+           (This   : in out World;
+            Inputs : in     World_Array) is
     begin
         This := Disjunct (This & Inputs);
     end Disjunct;
 
 
 
+    --  Lazy Sequencing / Conjunction  --
+
+    function Conjunct
+           (This : in World;
+            Func : in Conjunct_Zero_Func)
+        return World is
+    begin
+        return Result : constant World :=
+           (Possibles  => State_Vectors.Empty_Vector,
+            Next_Ident => 0,  --  dummy
+            Engine     =>
+               (Kind       => Conjunct_Zero_Gen,
+                ConZ_World => Hold (This),
+                ConZ_Func  => Func));
+    end Conjunct;
+
+
+    procedure Conjunct
+           (This : in out World;
+            Func : in     Conjunct_Zero_Func) is
+    begin
+        This := This.Conjunct (Func);
+    end Conjunct;
 
-    --  Recurse  --
+
+    function Conjunct
+           (This  : in World;
+            Func  : in Conjunct_One_Func;
+            Input : in Term'Class)
+        return World is
+    begin
+        return Result : constant World :=
+           (Possibles  => State_Vectors.Empty_Vector,
+            Next_Ident => 0,  --  dummy
+            Engine     =>
+               (Kind       => Conjunct_One_Gen,
+                ConO_World => Hold (This),
+                ConO_Func  => Func,
+                ConO_Input => Term (Input)));
+    end Conjunct;
+
+
+    procedure Conjunct
+           (This  : in out World;
+            Func  : in     Conjunct_One_Func;
+            Input : in     Term'Class) is
+    begin
+        This := This.Conjunct (Func, Input);
+    end Conjunct;
+
+
+    function Conjunct
+           (This   : in World;
+            Func   : in Conjunct_Many_Func;
+            Inputs : in Term_Array)
+        return World is
+    begin
+        return Result : constant World :=
+           (Possibles  => State_Vectors.Empty_Vector,
+            Next_Ident => 0,  --  dummy
+            Engine     =>
+               (Kind        => Conjunct_Many_Gen,
+                ConM_World  => Hold (This),
+                ConM_Func   => Func,
+                ConM_Inputs => Term_Array_Holders.To_Holder (Inputs)));
+    end Conjunct;
+
+
+    procedure Conjunct
+           (This   : in out World;
+            Func   : in     Conjunct_Many_Func;
+            Inputs : in     Term_Array) is
+    begin
+        This := This.Conjunct (Func, Inputs);
+    end Conjunct;
+
+
+
+
+    -------------------------
+    --  Auxiliary Helpers  --
+    -------------------------
+
+    --  Infinite State Loops  --
 
     function Recurse
-           (This : in Mu_World)
-        return Mu_World is
+           (This : in World)
+        return World is
     begin
-        return Result : constant Mu_World :=
+        return Result : constant World :=
            (Possibles  => State_Vectors.Empty_Vector,
             Next_Ident => This.Next_Ident,
             Engine     =>
@@ -632,20 +774,19 @@ package body Kompsos is
 
 
     procedure Recurse
-           (This : in out Mu_World) is
+           (This : in out World) is
     begin
         This := This.Recurse;
     end Recurse;
 
 
 
-
     --  Forced Evaluation  --
 
     function Take
-           (This  : in Mu_World;
+           (This  : in World;
             Count : in Natural)
-        return Mu_World is
+        return World is
     begin
         if Count = 0 then
             return
@@ -653,7 +794,7 @@ package body Kompsos is
                 Next_Ident => ID_Number'First,
                 Engine     => (Kind => No_Gen));
         end if;
-        return Result : Mu_World := This do
+        return Result : World := This do
             Result.Roll_Until (Count);
             if Result.Possibles.Last_Index > Count then
                 Result.Possibles.Set_Length (Ada.Containers.Count_Type (Count));
@@ -664,7 +805,7 @@ package body Kompsos is
 
 
     procedure Take
-           (This  : in out Mu_World;
+           (This  : in out World;
             Count : in     Natural) is
     begin
         This := This.Take (Count);
@@ -672,7 +813,7 @@ package body Kompsos is
 
 
     procedure Force
-           (This  : in out Mu_World;
+           (This  : in out World;
             Count : in     Positive) is
     begin
         This.Roll_Until (Count);
@@ -680,7 +821,7 @@ package body Kompsos is
 
 
     procedure Force_All
-           (This : in out Mu_World) is
+           (This : in out World) is
     begin
         while This.Engine.Kind /= No_Gen loop
             This.Rollover;
@@ -689,13 +830,270 @@ package body Kompsos is
 
 
     function Failed
-           (This : in out Mu_World)
+           (This : in out World)
         return Boolean is
     begin
         return not This.Has_State (1);
     end Failed;
 
 
+
+
+    --------------------------
+    --  miniKanren Prelude  --
+    --------------------------
+
+    --  caro  --
+
+    function Head
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    is
+        List_Term : Term renames Inputs (1);
+        Head_Term : Term renames Inputs (2);
+    begin
+        return Result : World := This do
+            Result.Unify (T (Head_Term, Result.Fresh), List_Term);
+        end return;
+    end Head;
+
+
+    procedure Head
+           (This   : in out World;
+            Inputs : in     Term_Array) is
+    begin
+        This := This.Head (Inputs);
+    end Head;
+
+
+
+    --  cdro  --
+
+    function Tail
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    is
+        List_Term : Term renames Inputs (1);
+        Tail_Term : Term renames Inputs (2);
+    begin
+        return Result : World := This do
+            Result.Unify (T (Result.Fresh, Tail_Term), List_Term);
+        end return;
+    end Tail;
+
+
+    procedure Tail
+           (This   : in out World;
+            Inputs : in     Term_Array) is
+    begin
+        This := This.Tail (Inputs);
+    end Tail;
+
+
+
+    --  conso  --
+
+    function Cons
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    is
+        Head_Term : Term renames Inputs (1);
+        Tail_Term : Term renames Inputs (2);
+        List_Term : Term renames Inputs (3);
+    begin
+        return Result : World := This do
+            Result.Unify (T (Head_Term, Tail_Term), List_Term);
+        end return;
+    end Cons;
+
+
+    procedure Cons
+           (This   : in out World;
+            Inputs : in     Term_Array) is
+    begin
+        This := This.Cons (Inputs);
+    end Cons;
+
+
+
+    --  nullo  --
+
+    function Nil
+           (This     : in World;
+            Nil_Term : in Term'Class)
+        return World is
+    begin
+        return Result : World := This do
+            Result.Unify (Null_Term, Nil_Term);
+        end return;
+    end Nil;
+
+
+    procedure Nil
+           (This     : in out World;
+            Nil_Term : in     Term'Class) is
+    begin
+        This := This.Nil (Nil_Term);
+    end Nil;
+
+
+
+    --  pairo  --
+
+    function Pair
+           (This      : in World;
+            Pair_Term : in Term'Class)
+        return World is
+    begin
+        return Result : World := This do
+            Result.Cons (Result.Fresh & Result.Fresh & Term (Pair_Term));
+        end return;
+    end Pair;
+
+
+    procedure Pair
+           (This      : in out World;
+            Pair_Term : in     Term'Class) is
+    begin
+        This := This.Pair (Pair_Term);
+    end Pair;
+
+
+
+    --  listo  --
+
+    function Linked_List
+           (This      : in World;
+            List_Term : in Term'Class)
+        return World
+    is
+        One, Two : World := This;
+        Ref_Term : constant Term := Two.Fresh;
+    begin
+        One.Nil (List_Term);
+
+        Two.Pair (List_Term);
+        Two.Tail (Term (List_Term) & Ref_Term);
+        Two.Conjunct (Linked_List'Access, Ref_Term);
+
+        return Disjunct (One, Two);
+    end Linked_List;
+
+
+    procedure Linked_List
+           (This      : in out World;
+            List_Term : in     Term'Class) is
+    begin
+        This := This.Linked_List (List_Term);
+    end Linked_List;
+
+
+
+    --  membero  --
+
+    function Member
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    is
+        Item_Term : Term renames Inputs (1);
+        List_Term : Term renames Inputs (2);
+
+        One, Two : World := This;
+        Ref_Term : constant Term := Two.Fresh;
+    begin
+        One.Head (List_Term & Item_Term);
+
+        Two.Tail (List_Term & Ref_Term);
+        Two.Conjunct (Member'Access, Item_Term & Ref_Term);
+
+        return Disjunct (One, Two);
+    end Member;
+
+
+    procedure Member
+           (This   : in out World;
+            Inputs : in     Term_Array) is
+    begin
+        This := This.Member (Inputs);
+    end Member;
+
+
+
+    --  rembero  --
+
+    function Remove
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    is
+        Item_Term : Term renames Inputs (1);
+        List_Term : Term renames Inputs (2);
+        Out_Term  : Term renames Inputs (3);
+
+        One, Two : World := This;
+        Left  : constant Term := Two.Fresh;
+        Right : constant Term := Two.Fresh;
+        Rest  : constant Term := Two.Fresh;
+    begin
+        One.Head (List_Term & Item_Term);
+        One.Tail (List_Term & Out_Term);
+
+        Two.Cons (Left & Right & List_Term);
+        Two.Conjunct (Remove'Access, Item_Term & Right & Rest);
+        Two.Cons (Left & Rest & Out_Term);
+
+        return Disjunct (One, Two);
+    end Remove;
+
+
+    procedure Remove
+           (This   : in out World;
+            Inputs : in     Term_Array) is
+    begin
+        This := This.Remove (Inputs);
+    end Remove;
+
+
+
+    --  appendo  --
+
+    function Append
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    is
+        List_Term : Term renames Inputs (1);
+        Item_Term : Term renames Inputs (2);
+        Out_Term  : Term renames Inputs (3);
+
+        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);
+        Two.Conjunct (Append'Access, Right & Item_Term & Rest);
+
+        return Disjunct (One, Two);
+    end Append;
+
+
+    procedure Append
+           (This   : in out World;
+            Inputs : in     Term_Array) is
+    begin
+        This := This.Append (Inputs);
+    end Append;
+
+
 end Kompsos;
 
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index f3f8470..0463f6f 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -12,6 +12,7 @@ with
 
 private with
 
+    Ada.Containers.Indefinite_Holders,
     Ada.Containers.Ordered_Maps,
     Ada.Containers.Vectors,
     Ada.Finalization;
@@ -22,11 +23,13 @@ generic
 package Kompsos is
 
 
+    -----------------
+    --  Datatypes  --
+    -----------------
+
     type Term is tagged private;
     type Term_Array is array (Positive range <>) of Term;
 
-    --  Can also be constructed by supplying an empty array to T
-    --  or just declaring a Term without initial value.
     Null_Term : constant Term;
 
     function "="
@@ -48,104 +51,317 @@ package Kompsos is
     --  Might include subprograms to retrieve Term contents later?
 
 
-    type Mu_World is tagged private;
-    type Mu_World_Array is array (Positive range <>) of Mu_World;
+    type World is tagged private;
+    type World_Array is array (Positive range <>) of World;
+
+    Empty_World : constant World;
+
+
+    type Conjunct_Zero_Func is access function
+           (This : in World)
+        return World;
 
-    Empty_Mu_World : constant Mu_World;
+    type Conjunct_One_Func is access function
+           (This  : in World;
+            Input : in Term'Class)
+        return World;
 
+    type Conjunct_Many_Func is access function
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World;
 
 
 
+
+    -------------------
+    --  microKanren  --
+    -------------------
+
+    --  Variable Introduction  --
+
     function Fresh
-           (This : in out Mu_World'Class)
+           (This : in out World'Class)
         return Term;
 
     function Fresh
-           (This : in out Mu_World'Class;
+           (This : in out World'Class;
             Name : in     String)
         return Term;
 
     function Fresh
-           (This : in out Mu_World'Class;
+           (This : in out World'Class;
             Name : in     Ada.Strings.Unbounded.Unbounded_String)
         return Term;
 
 
-
+    --  Unification  --
 
     function Unify
-           (This  : in Mu_World;
+           (This  : in World;
             Left  : in Term'Class;
             Right : in Element_Type)
-        return Mu_World;
+        return World;
 
     procedure Unify
-           (This  : in out Mu_World;
+           (This  : in out World;
             Left  : in     Term'Class;
             Right : in     Element_Type);
 
     function Unify
-           (This        : in Mu_World;
+           (This        : in World;
             Left, Right : in Term'Class)
-        return Mu_World;
+        return World;
 
     procedure Unify
-           (This        : in out Mu_World;
+           (This        : in out World;
             Left, Right : in     Term'Class);
 
 
-
+    --  Combining / Disjunction  --
 
     function Disjunct
-           (Left, Right : in Mu_World)
-        return Mu_World;
+           (Left, Right : in World)
+        return World;
 
     procedure Disjunct
-           (This  : in out Mu_World;
-            Right : in     Mu_World);
+           (This  : in out World;
+            Right : in     World);
 
     function Disjunct
-           (Inputs : in Mu_World_Array)
-        return Mu_World;
+           (Inputs : in World_Array)
+        return World;
 
     procedure Disjunct
-           (This   : in out Mu_World;
-            Inputs : in     Mu_World_Array);
+           (This   : in out World;
+            Inputs : in     World_Array);
+
+
+    --  Lazy Sequencing / Conjunction  --
+
+    function Conjunct
+           (This : in World;
+            Func : in Conjunct_Zero_Func)
+        return World;
+
+    procedure Conjunct
+           (This : in out World;
+            Func : in     Conjunct_Zero_Func);
+
+    function Conjunct
+           (This  : in World;
+            Func  : in Conjunct_One_Func;
+            Input : in Term'Class)
+        return World;
+
+    procedure Conjunct
+           (This  : in out World;
+            Func  : in     Conjunct_One_Func;
+            Input : in     Term'Class);
+
+    function Conjunct
+           (This   : in World;
+            Func   : in Conjunct_Many_Func;
+            Inputs : in Term_Array)
+        return World;
 
+    procedure Conjunct
+           (This   : in out World;
+            Func   : in     Conjunct_Many_Func;
+            Inputs : in     Term_Array);
 
 
 
+
+    -------------------------
+    --  Auxiliary Helpers  --
+    -------------------------
+
+    --  Infinite State Loops  --
+
     function Recurse
-           (This : in Mu_World)
-        return Mu_World;
+           (This : in World)
+        return World;
 
     procedure Recurse
-           (This : in out Mu_World);
-
+           (This : in out World);
 
 
+    --  Forced Evaluation  --
 
     function Take
-           (This  : in Mu_World;
+           (This  : in World;
             Count : in Natural)
-        return Mu_World;
+        return World;
 
     procedure Take
-           (This  : in out Mu_World;
+           (This  : in out World;
             Count : in     Natural);
 
     procedure Force
-           (This  : in out Mu_World;
+           (This  : in out World;
             Count : in     Positive);
 
     procedure Force_All
-           (This : in out Mu_World);
+           (This : in out World);
 
     function Failed
-           (This : in out Mu_World)
+           (This : in out World)
         return Boolean;
 
 
+
+
+    --------------------------
+    --  miniKanren Prelude  --
+    --------------------------
+
+    --  caro  --
+    --  Inputs = List_Term & Head_Term
+    function Head
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    with Pre => Inputs'Length = 2;
+
+    --  Inputs = List_Term & Head_Term
+    procedure Head
+           (This   : in out World;
+            Inputs : in     Term_Array)
+    with Pre => Inputs'Length = 2;
+
+
+    --  cdro  --
+    --  Inputs = List_Term & Tail_Term
+    function Tail
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    with Pre => Inputs'Length = 2;
+
+    --  Inputs = List_Term & Tail_Term
+    procedure Tail
+           (This   : in out World;
+            Inputs : in     Term_Array)
+    with Pre => Inputs'Length = 2;
+
+
+    --  conso  --
+    --  Inputs = Head_Term & Tail_Term & List_Term
+    function Cons
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    with Pre => Inputs'Length = 3;
+
+    --  Inputs = Head_Term & Tail_Term & List_Term
+    procedure Cons
+           (This   : in out World;
+            Inputs : in     Term_Array)
+    with Pre => Inputs'Length = 3;
+
+
+    --  nullo  --
+
+    function Nil
+           (This     : in World;
+            Nil_Term : in Term'Class)
+        return World;
+
+    procedure Nil
+           (This     : in out World;
+            Nil_Term : in     Term'Class);
+
+
+    --  eqo  --
+    --  Skipped due to being a synonym for Unify
+
+
+    --  eq-caro  --
+    --  Skipped due to being a synonym for Head
+
+
+    --  pairo  --
+
+    function Pair
+           (This      : in World;
+            Pair_Term : in Term'Class)
+        return World;
+
+    procedure Pair
+           (This      : in out World;
+            Pair_Term : in     Term'Class);
+
+
+    --  listo  --
+
+    function Linked_List
+           (This      : in World;
+            List_Term : in Term'Class)
+        return World;
+
+    procedure Linked_List
+           (This      : in out World;
+            List_Term : in     Term'Class);
+
+
+    --  membero  --
+    --  Inputs = Item_Term & List_Term
+    function Member
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    with Pre => Inputs'Length = 2;
+
+    --  Inputs = Item_Term & List_Term
+    procedure Member
+           (This   : in out World;
+            Inputs : in     Term_Array)
+    with Pre => Inputs'Length = 2;
+
+
+    --  rembero  --
+    --  Inputs = Item_Term & List_Term & Out_Term
+    function Remove
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    with Pre => Inputs'Length = 3;
+
+    --  Inputs = Item_Term & List_Term & Out_Term
+    procedure Remove
+           (This   : in out World;
+            Inputs : in     Term_Array)
+    with Pre => Inputs'Length = 3;
+
+
+    --  appendo  --
+    --  Inputs = List_Term & Item_Term & Out_Term
+    function Append
+           (This   : in World;
+            Inputs : in Term_Array)
+        return World
+    with Pre => Inputs'Length = 3;
+
+    --  Inputs = List_Term & Item_Term & Out_Term
+    procedure Append
+           (This   : in out World;
+            Inputs : in     Term_Array)
+    with Pre => Inputs'Length = 3;
+
+
+    --  anyo  --
+    --  Skipped due to Recurse doing the same thing
+
+
+    --  nevero  --
+    --  Skipped since it just creates a failed World
+
+
+    --  alwayso  --
+    --  Skipped due to Recurse doing the same thing
+
+
 private
 
 
@@ -207,6 +423,8 @@ private
 
     Null_Term : constant Term := (Ada.Finalization.Controlled with Actual => null);
 
+    package Term_Array_Holders is new Ada.Containers.Indefinite_Holders (Term_Array);
+
 
 
 
@@ -231,7 +449,7 @@ private
 
 
 
-    type World_Access is access Mu_World'Class;
+    type World_Access is access World'Class;
 
     type World_Holder is new Ada.Finalization.Controlled with record
         Ptr : World_Access;
@@ -247,7 +465,7 @@ private
            (This : in out World_Holder);
 
     function Hold
-           (This : in Mu_World'Class)
+           (This : in World'Class)
         return World_Holder;
 
     procedure Swap
@@ -259,6 +477,9 @@ private
         Unify_Gen,
         Buffer_Gen,
         Disjunct_Gen,
+        Conjunct_Zero_Gen,
+        Conjunct_One_Gen,
+        Conjunct_Many_Gen,
         Recurse_Gen);
 
     type Generator (Kind : Generator_Kind := No_Gen) is record
@@ -266,20 +487,31 @@ private
         when No_Gen =>
             null;
         when Fresh_Gen =>
-            Frs_World  : World_Holder;
-            Frs_Name   : SU.Unbounded_String;
+            Frs_World   : World_Holder;
+            Frs_Name    : SU.Unbounded_String;
         when Unify_Gen =>
-            Uni_World  : World_Holder;
-            Uni_Term1  : Term;
-            Uni_Term2  : Term;
+            Uni_World   : World_Holder;
+            Uni_Term1   : Term;
+            Uni_Term2   : Term;
         when Buffer_Gen =>
-            Buff_World : World_Holder;
+            Buff_World  : World_Holder;
         when Disjunct_Gen =>
-            Dis_World1 : World_Holder;
-            Dis_World2 : World_Holder;
+            Dis_World1  : World_Holder;
+            Dis_World2  : World_Holder;
+        when Conjunct_Zero_Gen =>
+            ConZ_World  : World_Holder;
+            ConZ_Func   : Conjunct_Zero_Func;
+        when Conjunct_One_Gen =>
+            ConO_World  : World_Holder;
+            ConO_Func   : Conjunct_One_Func;
+            ConO_Input  : Term;
+        when Conjunct_Many_Gen =>
+            ConM_World  : World_Holder;
+            ConM_Func   : Conjunct_Many_Func;
+            ConM_Inputs : Term_Array_Holders.Holder;
         when Recurse_Gen =>
-            Rec_World  : World_Holder;
-            Rec_Index  : Positive;
+            Rec_World   : World_Holder;
+            Rec_Index   : Positive;
         end case;
     end record;
 
@@ -287,27 +519,27 @@ private
        (Index_Type   => Positive,
         Element_Type => State);
 
-    type Mu_World is tagged record
+    type World is tagged record
         Possibles  : State_Vectors.Vector;
         Next_Ident : ID_Number;
         Engine     : Generator;
     end record;
 
     function Has_State
-           (This  : in out Mu_World;
+           (This  : in out World;
             Index : in     Positive)
         return Boolean;
 
     procedure Rollover
-           (This : in out Mu_World);
+           (This : in out World);
 
     procedure Roll_Until
-           (This  : in out Mu_World;
+           (This  : in out World;
             Index : in     Positive);
 
     use type State_Vectors.Vector;
 
-    Empty_Mu_World : constant Mu_World :=
+    Empty_World : constant World :=
        (Possibles  => State_Vectors.Empty_Vector & Empty_State,
         Next_Ident => 0,
         Engine     => (Kind => No_Gen));
diff --git a/test/ab.adb b/test/ab.adb
index 5df34e2..3ca2fee 100644
--- a/test/ab.adb
+++ b/test/ab.adb
@@ -23,7 +23,7 @@ procedure AB is
     package InPrin is new InKomp.Pretty_Print (Integer'Image);
     use InPrin;
 
-    Verse : Mu_World := Empty_Mu_World;
+    Verse : World := Empty_World;
     Ref : Term;
 
 begin
diff --git a/test/fivesix.adb b/test/fivesix.adb
index b8046af..3eabf6a 100644
--- a/test/fivesix.adb
+++ b/test/fivesix.adb
@@ -23,8 +23,8 @@ procedure FiveSix is
     package InPrin is new InKomp.Pretty_Print (Integer'Image);
     use InPrin;
 
-    Fives, Sixes : Mu_World := Empty_Mu_World;
-    Result : Mu_World;
+    Fives, Sixes : World := Empty_World;
+    Result : World;
 
 begin
 
diff --git a/test/membero.adb b/test/membero.adb
index 1143df2..46127d7 100644
--- a/test/membero.adb
+++ b/test/membero.adb
@@ -10,7 +10,6 @@ with
 
     Ada.Strings.Unbounded,
     Ada.Text_IO,
-    Kompsos.Prelude,
     Kompsos.Pretty_Print;
 
 
@@ -28,10 +27,9 @@ procedure Membero is
     package InKomp is new Kompsos (SU.Unbounded_String);
     use InKomp;
 
-    package Prelude is new InKomp.Prelude;
     package Printer is new InKomp.Pretty_Print (SU.To_String);
 
-    Verse : Prelude.World := Prelude.Empty_World;
+    Verse : World := Empty_World;
 
     Test_Item : constant Term := T (T (+"one") & T (+"two") & T (+"three") & T (+"four"));
 
@@ -44,9 +42,9 @@ begin
 
     TIO.New_Line;
 
-    Verse.Member (Verse.Fresh ("result"), Test_Item);
+    Verse.Member (Verse.Fresh ("result") & Test_Item);
 
-    TIO.Put_Line (Printer.Image (Verse));
+    TIO.Put_Line (Printer.Image (Verse.Take (5)));
 
 end Membero;
 
diff --git a/test/pprint.adb b/test/pprint.adb
index 8bce15e..b34f255 100644
--- a/test/pprint.adb
+++ b/test/pprint.adb
@@ -50,7 +50,7 @@ begin
 
     TIO.New_Line;
 
-    TIO.Put_Line (Image (Empty_Mu_World));
+    TIO.Put_Line (Image (Empty_World));
 
 end PPrint;