Reification, including Term flattening and Treeification

5 files changed, 349 insertions, 10 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