Removed Nametags and identifier aliasing for Variables

1 files changed, 16 insertions, 97 deletions

diff --git a/src/kompsos.adb b/src/kompsos.adb
index 56c22cd..7054714 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -112,6 +112,8 @@ package body Kompsos is
                 return Left.Actual.Left = Right.Actual.Left and
                     Left.Actual.Right = Right.Actual.Right;
             when Null_Term =>
+                --  Should never actually get here because Null_Terms
+                --  are covered by checking Left.Actual = Right.Actual
                 return True;
             end case;
         else
@@ -190,14 +192,6 @@ package body Kompsos is
     end Var;
 
 
-    function Name
-           (This : in Term)
-        return Nametag is
-    begin
-        return This.Var.Name;
-    end Name;
-
-
     function Left
            (This : in Term)
         return Term is
@@ -237,15 +231,15 @@ package body Kompsos is
     --  Internal Helpers  --
     ------------------------
 
-    --  Variable IDs  --
+    --  Variables  --
 
-    Next_Generator_ID : Generator_ID_Number := Generator_ID_Number'First;
+    Next_Variable : Variable := Variable'First;
 
     function Next_Gen
-        return Generator_ID_Number is
+        return Variable is
     begin
-        return Result : constant Generator_ID_Number := Next_Generator_ID do
-            Next_Generator_ID := Next_Generator_ID + 1;
+        return Result : constant Variable := Next_Variable do
+            Next_Variable := Next_Variable + 1;
         end return;
     end Next_Gen;
 
@@ -260,28 +254,9 @@ package body Kompsos is
 
     function Fresh
            (This : in out Goal'Class)
-        return Term is
-    begin
-        return This.Fresh (+"");
-    end Fresh;
-
-
-    function Fresh
-           (This : in out Goal'Class;
-            Name : in     String)
-        return Term is
-    begin
-        return This.Fresh (+Name);
-    end Fresh;
-
-
-    function Fresh
-           (This : in out Goal'Class;
-            Name : in     Nametag)
         return Term
     is
-        My_ID  : constant Generator_ID_Number := Next_Gen;
-        My_Var : constant Variable := (Ident => My_ID, Name => Name);
+        My_Var : constant Variable := Next_Gen;
     begin
         return My_Term : constant Term := Term (T (My_Var)) do
             This.Actual := new Goal_Component'(
@@ -296,22 +271,11 @@ package body Kompsos is
     function Fresh
            (This  : in out Goal'Class;
             Count : in     Positive)
-        return Term_Array
-    is
-        Names : constant Nametag_Array (1 .. Count) := (others => +"");
-    begin
-        return This.Fresh (Names);
-    end Fresh;
-
-
-    function Fresh
-           (This  : in out Goal'Class;
-            Names : in     Nametag_Array)
         return Term_Array is
     begin
-        return Terms : Term_Array (1 .. Names'Length) do
-            for Index in Terms'Range loop
-                Terms (Index) := This.Fresh (Names (Names'First + Index - 1));
+        return My_Terms : Term_Array (1 .. Count) do
+            for Item of My_Terms loop
+                Item := This.Fresh;
             end loop;
         end return;
     end Fresh;
@@ -587,21 +551,14 @@ package body Kompsos is
     function Resolve
            (This  : in Term;
             Subst : in State)
-        return Term
-    is
-        use type SU.Unbounded_String;
+        return Term is
     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);
+            if Subst.LVars.Contains (This.Var) and then Subst.Subst.Contains (This.Var) then
+                return Subst.Subst.Element (This.Var).Resolve (Subst);
             else
                 return This;
             end if;
@@ -617,47 +574,9 @@ package body Kompsos is
     begin
         if Subst.LVars.Is_Empty then
             return Empty_Term;
+        else
+            return Resolve (Term (T (Subst.LVars.First_Element)), Subst);
         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;