Reification, including Term flattening and Treeification

1 files changed, 96 insertions, 3 deletions

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  --