Reification, including Term flattening and Treeification

9 files changed, 454 insertions, 14 deletions

diff --git a/src/kompsos-advanced_reify.adb b/src/kompsos-advanced_reify.adb
new file mode 100644
index 0000000..42df1e7
--- /dev/null
+++ b/src/kompsos-advanced_reify.adb
@@ -0,0 +1,147 @@
+
+
+--  Programmed by Jedidiah Barber
+--  Licensed under the Sunset License v1.0
+
+--  See license.txt for further details
+
+
+package body Kompsos.Advanced_Reify is
+
+
+    --  Term->Array Conversion  --
+
+    function Flatten
+           (Item : in Term)
+        return Element_Array is
+    begin
+        case Item.Kind is
+        when Null_Term =>
+            return (1 => Null_Element);
+        when Atom_Term =>
+            return (1 => Item.Atom);
+        when Var_Term =>
+            return (1 => Variable_Convert (Item));
+        when Pair_Term =>
+            if Item.Right = Empty_Term then
+                return Flatten (Item.Left);
+            else
+                return Flatten (Item.Left) & Flatten (Item.Right);
+            end if;
+        end case;
+    end Flatten;
+
+
+
+    --  Term->Tree Conversion  --
+
+    function To_Tree
+           (Item : in Term)
+        return Element_Trees.Tree is
+    begin
+        return Result : Element_Trees.Tree := Element_Trees.Empty_Tree do
+            case Item.Kind is
+            when Null_Term =>
+                Result.Append_Child (Result.Root, Null_Element);
+            when Atom_Term =>
+                Result.Append_Child (Result.Root, Item.Atom);
+            when Var_Term =>
+                Result.Append_Child (Result.Root, Variable_Convert (Item));
+            when Pair_Term =>
+                declare
+                    The_Subtree : Element_Trees.Tree := To_Tree (Item.Left);
+                    The_Place   : Element_Trees.Cursor;
+                begin
+                    if Item.Left.Kind = Pair_Term then
+                        Result.Insert_Child
+                           (Result.Root,
+                            Element_Trees.No_Element,
+                            Null_Element,
+                            The_Place);
+                    else
+                        The_Place := Result.Root;
+                    end if;
+                    Result.Splice_Children
+                       (The_Place,
+                        Element_Trees.No_Element,
+                        The_Subtree,
+                        The_Subtree.Root);
+                    if Item.Right /= Empty_Term then
+                        The_Subtree := To_Tree (Item.Right);
+                        Result.Splice_Children
+                           (Result.Root,
+                            Element_Trees.No_Element,
+                            The_Subtree,
+                            The_Subtree.Root);
+                    end if;
+                end;
+            end case;
+        end return;
+    end To_Tree;
+
+
+
+    --  Tree Reification  --
+
+    function Treeify
+           (Item  : in Term;
+            Subst : in State)
+        return Element_Trees.Tree is
+    begin
+        return To_Tree (Item.Resolve (Subst));
+    end Treeify;
+
+
+    function Treeify_First
+           (Subst : in State)
+        return Element_Trees.Tree is
+    begin
+        if Subst.LVars.Is_Empty then
+            return Element_Trees.Empty_Tree;
+        end if;
+        for Iter in Subst.Ident.Iterate loop
+            if ID_Number_Maps.Element (Iter) = Subst.LVars.First_Index then
+                return Treeify (Term (T (Variable'(
+                    Ident => ID_Number_Maps.Key (Iter),
+                    Name  => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))),
+                    Subst);
+            end if;
+        end loop;
+        return Element_Trees.Empty_Tree;
+    end Treeify_First;
+
+
+    function Treeify_First
+           (Subst : in State;
+            Name  : in String)
+        return Element_Trees.Tree is
+    begin
+        return Treeify_First (Subst, +Name);
+    end Treeify_First;
+
+
+    function Treeify_First
+           (Subst : in State;
+            Name  : in Nametag)
+        return Element_Trees.Tree
+    is
+        Name_Index : constant Name_Vectors.Extended_Index := Subst.LVars.Find_Index (Name);
+    begin
+        if Name_Index = Name_Vectors.No_Index then
+            return Element_Trees.Empty_Tree;
+        end if;
+        for Iter in Subst.Ident.Iterate loop
+            if ID_Number_Maps.Element (Iter) = Name_Index then
+                return Treeify (Term (T (Variable'(
+                    Ident => ID_Number_Maps.Key (Iter),
+                    Name  => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))),
+                    Subst);
+            end if;
+        end loop;
+        return Element_Trees.Empty_Tree;
+    end Treeify_First;
+
+
+end Kompsos.Advanced_Reify;
+
+
diff --git a/src/kompsos-advanced_reify.ads b/src/kompsos-advanced_reify.ads
new file mode 100644
index 0000000..ecda1c9
--- /dev/null
+++ b/src/kompsos-advanced_reify.ads
@@ -0,0 +1,69 @@
+
+
+--  Programmed by Jedidiah Barber
+--  Licensed under the Sunset License v1.0
+
+--  See license.txt for further details
+
+
+with
+
+    Ada.Containers.Multiway_Trees;
+
+
+generic
+    type Element_Array is array (Positive range <>) of Element_Type;
+
+    Null_Element : Element_Type;
+
+    with function Variable_Convert
+           (Item : in Term)
+        return Element_Type is <>;
+
+    --  Element_Trees must be passed in rather than instantiated inside the generic
+    --  due to an issue with implementation-defined Disable_Controlled aspect in GNAT.
+    with package Element_Trees is new Ada.Containers.Multiway_Trees
+       (Element_Type => Element_Type,
+        "="          => "=");
+package Kompsos.Advanced_Reify is
+
+
+    --  Term->Array Conversion  --
+
+    function Flatten
+           (Item : in Term)
+        return Element_Array;
+
+
+    --  Term->Tree Conversion  --
+
+    function To_Tree
+          (Item : in Term)
+        return Element_Trees.Tree;
+
+
+    --  Tree Reification  --
+
+    function Treeify
+           (Item  : in Term;
+            Subst : in State)
+        return Element_Trees.Tree;
+
+    function Treeify_First
+           (Subst : in State)
+        return Element_Trees.Tree;
+
+    function Treeify_First
+           (Subst : in State;
+            Name  : in String)
+        return Element_Trees.Tree;
+
+    function Treeify_First
+           (Subst : in State;
+            Name  : in Nametag)
+        return Element_Trees.Tree;
+
+
+end Kompsos.Advanced_Reify;
+
+
diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads
index 3d5963e..73e50db 100644
--- a/src/kompsos-pretty_print.ads
+++ b/src/kompsos-pretty_print.ads
@@ -14,12 +14,12 @@ package Kompsos.Pretty_Print is
 
 
     function Image
-           (Item : in Term)
+           (Item : in Integer)
         return String;
 
 
     function Image
-           (Item : in out World)
+           (Item : in Term)
         return String;
 
 
@@ -33,6 +33,11 @@ package Kompsos.Pretty_Print is
         return String;
 
 
+    function Image
+           (Item : in out World)
+        return String;
+
+
     function Image_Constant
            (Item : in World)
         return String;
@@ -42,11 +47,6 @@ private
 
 
     function Image
-           (Item : in Integer)
-        return String;
-
-
-    function Image
            (Item : in ID_Number)
         return String;
 
diff --git a/src/kompsos.adb b/src/kompsos.adb
index 1370f37..d973452 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -35,9 +35,9 @@ package body Kompsos is
 
     function T
            (Item : in Variable)
-        return Term is
+        return Term'Class is
     begin
-        return (Actual => Term_Holders.To_Holder (Term_Component'(
+        return Term'(Actual => Term_Holders.To_Holder (Term_Component'(
             Kind  => Var_Term,
             Refer => Item)));
     end T;
@@ -436,7 +436,7 @@ package body Kompsos is
     is
         My_ID : constant Generator_ID_Number := Next_Gen;
     begin
-        return My_Term : constant Term := T (Variable'(Ident => My_ID, Name => Name)) do
+        return My_Term : constant Term := Term (T (Variable'(Ident => My_ID, Name => Name))) do
             This.Engine :=
                (Kind      => Fresh_Gen,
                 Frs_Ident => My_ID,
@@ -706,6 +706,19 @@ package body Kompsos is
     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
@@ -732,6 +745,86 @@ package body Kompsos is
 
 
 
+    --  Reification  --
+
+    function Resolve
+           (This  : in Term;
+            Subst : in State)
+        return Term
+    is
+        use type SU.Unbounded_String;
+    begin
+        case This.Kind is
+        when Null_Term | Atom_Term =>
+            return This;
+        when Var_Term =>
+            if  Subst.Ident.Contains (This.Var.Ident) and then
+                Subst.Ident.Element (This.Var.Ident) in
+                    Subst.LVars.First_Index .. Subst.LVars.Last_Index and then
+                Subst.LVars.Element (Subst.Ident.Element (This.Var.Ident)) = This.Name and then
+                Subst.Subst.Contains (Subst.Ident.Element (This.Var.Ident))
+            then
+                return Subst.Subst.Element (Subst.Ident.Element (This.Var.Ident)).Resolve (Subst);
+            else
+                return This;
+            end if;
+        when Pair_Term =>
+            return T (This.Left.Resolve (Subst), This.Right.Resolve (Subst));
+        end case;
+    end Resolve;
+
+
+    function Resolve_First
+           (Subst : in State)
+        return Term is
+    begin
+        if Subst.LVars.Is_Empty then
+            return Empty_Term;
+        end if;
+        for Iter in Subst.Ident.Iterate loop
+            if ID_Number_Maps.Element (Iter) = Subst.LVars.First_Index then
+                return Resolve (Term (T (Variable'(
+                    Ident => ID_Number_Maps.Key (Iter),
+                    Name  => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))),
+                    Subst);
+            end if;
+        end loop;
+        return Empty_Term;
+    end Resolve_First;
+
+
+    function Resolve_First
+           (Subst : in State;
+            Name  : in String)
+        return Term is
+    begin
+        return Resolve_First (Subst, +Name);
+    end Resolve_First;
+
+
+    function Resolve_First
+           (Subst : in State;
+            Name  : in Nametag)
+        return Term
+    is
+        Name_Index : constant Name_Vectors.Extended_Index := Subst.LVars.Find_Index (Name);
+    begin
+        if Name_Index = Name_Vectors.No_Index then
+            return Empty_Term;
+        end if;
+        for Iter in Subst.Ident.Iterate loop
+            if ID_Number_Maps.Element (Iter) = Name_Index then
+                return Resolve (Term (T (Variable'(
+                    Ident => ID_Number_Maps.Key (Iter),
+                    Name  => Subst.LVars.Element (ID_Number_Maps.Element (Iter))))),
+                    Subst);
+            end if;
+        end loop;
+        return Empty_Term;
+    end Resolve_First;
+
+
+
 
     --------------------------
     --  miniKanren Prelude  --
diff --git a/src/kompsos.ads b/src/kompsos.ads
index 89ea88b..3164996 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -256,6 +256,10 @@ package Kompsos is
            (This : in out World)
         return State;
 
+    function Take_All
+           (This : in out World)
+        return State_Array;
+
     procedure Force
            (This  : in out World;
             Count : in     Positive);
@@ -268,6 +272,28 @@ package Kompsos is
         return Boolean;
 
 
+    --  Reification  --
+
+    function Resolve
+           (This  : in Term;
+            Subst : in State)
+        return Term;
+
+    function Resolve_First
+           (Subst : in State)
+        return Term;
+
+    function Resolve_First
+           (Subst : in State;
+            Name  : in String)
+        return Term;
+
+    function Resolve_First
+           (Subst : in State;
+            Name  : in Nametag)
+        return Term;
+
+
 
 
     --------------------------
@@ -474,6 +500,10 @@ private
         Actual : Term_Holders.Holder;
     end record;
 
+    function T
+           (Item : in Variable)
+        return Term'Class;
+
     function Var
            (This : in Term'Class)
         return Variable
diff --git a/test/membero.adb b/test/membero.adb
index 89e7f2e..827e6ab 100644
--- a/test/membero.adb
+++ b/test/membero.adb
@@ -44,8 +44,16 @@ begin
 
     Verse.Member (Verse.Fresh ("result") & Test_Item);
 
+    TIO.Put_Line ("Raw results:");
     TIO.Put_Line (Printer.Image (Verse));
 
+    TIO.New_Line;
+
+    TIO.Put_Line ("Reified results:");
+    for Subst of Verse.Take_All loop
+        TIO.Put_Line (Printer.Image (Resolve_First (Subst, "result")));
+    end loop;
+
 end Membero;
 
 
diff --git a/test/rembero.adb b/test/rembero.adb
index e2f9a87..669d42a 100644
--- a/test/rembero.adb
+++ b/test/rembero.adb
@@ -8,13 +8,15 @@
 
 with
 
+    Ada.Characters.Latin_1,
     Ada.Text_IO,
     Kompsos.Pretty_Print;
 
 
 procedure Rembero is
 
-    package TIO renames Ada.Text_IO;
+    package Latin renames Ada.Characters.Latin_1;
+    package TIO   renames Ada.Text_IO;
 
 
     package InKomp is new Kompsos (Integer);
@@ -29,13 +31,31 @@ begin
     TIO.Put_Line ("Test program to check if calculating an infinite number of results works.");
     TIO.New_Line;
     TIO.Put_Line ("It will call rembero with variables as all arguments.");
-    TIO.Put_Line ("The first 10 results will be displayed.");
+    TIO.Put_Line ("The first 5 results will be displayed.");
 
     TIO.New_Line;
 
     Verse.Remove (Verse.Fresh ("item") & Verse.Fresh ("list") & Verse.Fresh ("out"));
 
-    TIO.Put_Line (Printer.Image (Verse.Take (10)));
+    declare
+        First_Five : constant State_Array := Verse.Take (5);
+    begin
+        TIO.Put_Line ("Raw results:");
+        TIO.Put_Line (Printer.Image (First_Five));
+
+        TIO.New_Line;
+
+        TIO.Put_Line ("Reified results:");
+        for Index in First_Five'Range loop
+            TIO.Put_Line ("#" & Printer.Image (Index) & ":");
+            TIO.Put_Line (Latin.HT & "item: " &
+                Printer.Image (Resolve_First (First_Five (Index), "item")));
+            TIO.Put_Line (Latin.HT & "list: " &
+                Printer.Image (Resolve_First (First_Five (Index), "list")));
+            TIO.Put_Line (Latin.HT & "out: " &
+                Printer.Image (Resolve_First (First_Five (Index), "out")));
+        end loop;
+    end;
 
 end Rembero;
 
diff --git a/test/trees.adb b/test/trees.adb
new file mode 100644
index 0000000..7f199ad
--- /dev/null
+++ b/test/trees.adb
@@ -0,0 +1,71 @@
+
+
+--  Programmed by Jedidiah Barber
+--  Licensed under the Sunset License v1.0
+
+--  See license.txt for further details
+
+
+with
+
+    Ada.Containers.Multiway_Trees,
+    Ada.Text_IO,
+    Kompsos.Advanced_Reify,
+    Kompsos.Pretty_Print;
+
+
+procedure Trees is
+
+    package TIO renames Ada.Text_IO;
+
+
+    package InKomp is new Kompsos (Integer);
+    use InKomp;
+
+
+    type Integer_Array is array (Positive range <>) of Integer;
+
+    function Var_Minus_One
+           (Item : in Term)
+        return Integer is
+    begin
+        return -1;
+    end Var_Minus_One;
+
+    package Int_Trees is new Ada.Containers.Multiway_Trees (Integer);
+
+    package Reify is new InKomp.Advanced_Reify
+       (Element_Array    => Integer_Array,
+        Null_Element     => 0,
+        Variable_Convert => Var_Minus_One,
+        Element_Trees    => Int_Trees);
+
+
+    package Printer is new InKomp.Pretty_Print (Integer'Image);
+
+
+    Test_Item : constant Term := T (T (T (1) & T (2) & T (3)) & T (T (10) & T (20)));
+
+    Result : constant Int_Trees.Tree := Reify.To_Tree (Test_Item);
+
+begin
+
+    TIO.Put_Line ("Test term is " & Printer.Image (Test_Item));
+
+    TIO.New_Line;
+
+    TIO.Put_Line ("Root has " &
+        Printer.Image (Integer (Int_Trees.Child_Count (Result.Root))) & " children.");
+
+    for Child in Result.Iterate_Children (Result.Root) loop
+        TIO.Put ("Child has " &
+            Printer.Image (Integer (Int_Trees.Child_Count (Child))) & " children:");
+        for Child_Child in Result.Iterate_Children (Child) loop
+            TIO.Put (" " & Printer.Image (Int_Trees.Element (Child_Child)));
+        end loop;
+        TIO.New_Line;
+    end loop;
+
+end Trees;
+
+
diff --git a/tests.gpr b/tests.gpr
index a8007d8..b330b78 100644
--- a/tests.gpr
+++ b/tests.gpr
@@ -20,7 +20,8 @@ project Tests is
         "fivesix.adb",
         "membero.adb",
         "pprint.adb",
-        "rembero.adb");
+        "rembero.adb",
+        "trees.adb");
 
     package Builder is
         for Executable ("ab.adb")      use "ab";
@@ -28,6 +29,7 @@ project Tests is
         for Executable ("membero.adb") use "membero";
         for Executable ("pprint.adb")  use "pprint";
         for Executable ("rembero.adb") use "rembero";
+        for Executable ("trees.adb")   use "trees";
 
         for Default_Switches ("Ada") use
             Common.Builder'Default_Switches ("Ada");