Removed Nametags and identifier aliasing for Variables

7 files changed, 56 insertions, 274 deletions

diff --git a/src/kompsos-advanced_reify.adb b/src/kompsos-advanced_reify.adb
index 42df1e7..c2d1670 100644
--- a/src/kompsos-advanced_reify.adb
+++ b/src/kompsos-advanced_reify.adb
@@ -96,49 +96,7 @@ package body Kompsos.Advanced_Reify is
            (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;
+        return To_Tree (Resolve_First (Subst));
     end Treeify_First;
 
 
diff --git a/src/kompsos-advanced_reify.ads b/src/kompsos-advanced_reify.ads
index ecda1c9..db51558 100644
--- a/src/kompsos-advanced_reify.ads
+++ b/src/kompsos-advanced_reify.ads
@@ -53,16 +53,6 @@ package Kompsos.Advanced_Reify is
            (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-collector.adb b/src/kompsos-collector.adb
index b076679..792c2b2 100644
--- a/src/kompsos-collector.adb
+++ b/src/kompsos-collector.adb
@@ -67,7 +67,7 @@ package body Kompsos.Collector is
         when Null_Term | Atom_Term =>
             return True;
         when Var_Term =>
-            return This.Ident.Contains (Item.Var.Ident);
+            return This.LVars.Contains (Item.Var);
         when Pair_Term =>
             return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right);
         end case;
@@ -79,10 +79,8 @@ package body Kompsos.Collector is
             Item : in Term'Class)
         return Term'Class is
     begin
-        if  Item.Kind = Var_Term and then
-            This.Subst.Contains (This.Ident.Element (Item.Var.Ident))
-        then
-            return Walk (This, This.Subst.Constant_Reference (This.Ident.Element (Item.Var.Ident)));
+        if Item.Kind = Var_Term and then This.Subst.Contains (Item.Var) then
+            return Walk (This, This.Subst.Element (Item.Var));
         else
             return Item;
         end if;
@@ -126,12 +124,12 @@ package body Kompsos.Collector is
         --  Unify Variable and other Terms by introducing a new substitution
         if Real_Left.Kind = Var_Term then
             Extended := Potential;
-            Extended.Subst.Insert (Extended.Ident.Element (Real_Left.Var.Ident), Term (Real_Right));
+            Extended.Subst.Insert (Real_Left.Var, Term (Real_Right));
             return True;
         end if;
         if Real_Right.Kind = Var_Term then
             Extended := Potential;
-            Extended.Subst.Insert (Extended.Ident.Element (Real_Right.Var.Ident), Term (Real_Left));
+            Extended.Subst.Insert (Real_Right.Var, Term (Real_Left));
             return True;
         end if;
 
@@ -233,8 +231,7 @@ package body Kompsos.Collector is
 
         when Fresh_Node =>
             if Get_Next (Ptr.Frs_Goal'Unchecked_Access, Base, Index, Result) then
-                Result.LVars.Append (Ptr.Frs_Var.Name);
-                Result.Ident.Insert (Ptr.Frs_Var.Ident, Result.LVars.Last_Index);
+                Result.LVars.Append (Ptr.Frs_Var);
                 return True;
             else
                 return False;
@@ -510,8 +507,7 @@ package body Kompsos.Collector is
     end Next;
 
 
-    procedure Reset
-    is
+    procedure Reset is
         Ptr : constant Constant_Goal_Access := Relation'Access;
     begin
         Reset (Ptr);
diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 250c6a6..c888e13 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -10,6 +10,7 @@ with
 
     Ada.Characters.Latin_1,
     Ada.Strings.Fixed,
+    Ada.Strings.Unbounded,
     Kompsos.Collector;
 
 
@@ -18,41 +19,41 @@ package body Kompsos.Pretty_Print is
 
     package Latin renames Ada.Characters.Latin_1;
     package Str   renames Ada.Strings;
+    package SU    renames Ada.Strings.Unbounded;
 
 
 
 
     function Image
-           (Item : in Integer)
+           (Item : in Long_Natural)
         return String is
     begin
-        return Str.Fixed.Trim (Integer'Image (Item), Str.Left);
+        return Str.Fixed.Trim (Long_Natural'Image (Item), Str.Left);
     end Image;
 
 
     function Image
-           (Item : in Long_Natural)
+           (Item : in Variable)
         return String is
     begin
-        return Str.Fixed.Trim (Long_Natural'Image (Item), Str.Left);
+        return "Var#" & Image (Long_Natural (Item));
     end Image;
 
 
 
 
+    -----------------------------------
+    --  Datatype->String Conversion  --
+    -----------------------------------
+
     function Image
-           (Item : in Variable)
+           (Item : in Integer)
         return String is
     begin
-        return "Vargen#" & Image (Long_Natural (Item.Ident)) &
-           (if SU.Length (Item.Name) /= 0
-            then "/" & SU.To_String (Item.Name)
-            else "");
+        return Str.Fixed.Trim (Integer'Image (Item), Str.Left);
     end Image;
 
 
-
-
     function Image
            (Item : in Term)
         return String
@@ -93,28 +94,13 @@ package body Kompsos.Pretty_Print is
     is
         Result : SU.Unbounded_String;
     begin
-        SU.Append (Result, Latin.HT & "Generation:");
-        if Item.Ident.Is_Empty then
-            SU.Append (Result, " N/A" & Latin.LF);
-        else
-            SU.Append (Result, Latin.LF);
-            for Iter in Item.Ident.Iterate loop
-                SU.Append (Result, Latin.HT & Latin.HT & "Vargen#" &
-                    Image (Long_Natural (ID_Number_Maps.Key (Iter))) & " => " &
-                    Image (Long_Natural (ID_Number_Maps.Element (Iter))) & Latin.LF);
-            end loop;
-        end if;
         SU.Append (Result, Latin.HT & "Variables:");
         if Item.LVars.Is_Empty then
             SU.Append (Result, " N/A" & Latin.LF);
         else
             SU.Append (Result, Latin.LF);
-            for Index in Item.LVars.First_Index .. Item.LVars.Last_Index loop
-                SU.Append (Result, Latin.HT & Latin.HT &
-                    "Var#" & Image (Long_Natural (Index)) &
-                   (if SU.Length (Item.LVars (Index)) /= 0
-                    then "/" & SU.To_String (Item.LVars (Index))
-                    else "") & Latin.LF);
+            for LVar of Item.LVars loop
+                SU.Append (Result, Latin.HT & Latin.HT & Image (LVar) & Latin.LF);
             end loop;
         end if;
         SU.Append (Result, Latin.HT & "Substitution:");
@@ -124,11 +110,11 @@ package body Kompsos.Pretty_Print is
             SU.Append (Result, Latin.LF);
             for Iter in Item.Subst.Iterate loop
                 SU.Append (Result, Latin.HT & Latin.HT &
-                    Image (Long_Natural (Binding_Maps.Key (Iter))) & " => " &
+                    Image (Binding_Maps.Key (Iter)) & " => " &
                     Image (Binding_Maps.Element (Iter)) & Latin.LF);
             end loop;
         end if;
-        return -Result;
+        return SU.To_String (Result);
     end Image;
 
 
@@ -173,6 +159,10 @@ package body Kompsos.Pretty_Print is
 
 
 
+    --------------------------------
+    --  Graphviz DAG Of Tomorrow  --
+    --------------------------------
+
     procedure Do_Structure_DOT
            (This   : in     Goal;
             Nodes  : in out DOT_Node_Maps.Map;
diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads
index 653858b..23c525e 100644
--- a/src/kompsos-pretty_print.ads
+++ b/src/kompsos-pretty_print.ads
@@ -18,6 +18,8 @@ generic
 package Kompsos.Pretty_Print is
 
 
+    --  Datatype->String Conversion  --
+
     function Image
            (Item : in Integer)
         return String;
@@ -39,7 +41,7 @@ package Kompsos.Pretty_Print is
         return String;
 
 
-
+    --  Graphviz DAG Of Tomorrow  --
 
     function Structure_DOT
            (This : in Goal;
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;
 
 
diff --git a/src/kompsos.ads b/src/kompsos.ads
index 862b345..19cfeb8 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -6,10 +6,6 @@
 --  See license.txt for further details
 
 
-with
-
-    Ada.Strings.Unbounded;
-
 private with
 
     Ada.Containers.Indefinite_Holders,
@@ -27,12 +23,6 @@ package Kompsos is
     --  Datatypes  --
     -----------------
 
-    --  Variable Names  --
-
-    subtype Nametag is Ada.Strings.Unbounded.Unbounded_String;
-    type Nametag_Array is array (Positive range <>) of Nametag;
-
-
     --  Terms  --
 
     type Term_Kind is (Null_Term, Atom_Term, Var_Term, Pair_Term);
@@ -67,11 +57,6 @@ package Kompsos is
         return Element_Type
     with Pre => This.Kind = Atom_Term;
 
-    function Name
-           (This : in Term)
-        return Nametag
-    with Pre => This.Kind = Var_Term;
-
     function Left
            (This : in Term)
         return Term
@@ -130,18 +115,6 @@ package Kompsos is
     with Post => Fresh'Result.Kind = Var_Term;
 
     function Fresh
-           (This : in out Goal'Class;
-            Name : in     String)
-        return Term
-    with Post => Fresh'Result.Kind = Var_Term;
-
-    function Fresh
-           (This : in out Goal'Class;
-            Name : in     Nametag)
-        return Term
-    with Post => Fresh'Result.Kind = Var_Term;
-
-    function Fresh
            (This  : in out Goal'Class;
             Count : in     Positive)
         return Term_Array
@@ -149,14 +122,6 @@ package Kompsos is
         Fresh'Result'Length = Count and
         (for all Item of Fresh'Result => Item.Kind = Var_Term);
 
-    function Fresh
-           (This  : in out Goal'Class;
-            Names : in     Nametag_Array)
-        return Term_Array
-    with Post =>
-        Fresh'Result'Length = Names'Length and
-        (for all Item of Fresh'Result => Item.Kind = Var_Term);
-
     generic
         Verse : in out Goal;
     function Make_Fresh
@@ -286,16 +251,6 @@ package Kompsos is
            (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;
-
 
 
 
@@ -452,33 +407,11 @@ package Kompsos is
 private
 
 
-    package SU renames Ada.Strings.Unbounded;
-
-
-    function "+"
-           (Item : in String)
-        return SU.Unbounded_String
-    renames SU.To_Unbounded_String;
-
-    function "-"
-           (Item : in SU.Unbounded_String)
-        return String
-    renames SU.To_String;
-
-
-
-
     --  around 2^31 possible Variables should be enough for anybody, right?
     subtype Long_Natural  is Long_Integer range 0 .. Long_Integer'Last;
     subtype Long_Positive is Long_Integer range 1 .. Long_Integer'Last;
 
-    type Generator_ID_Number is new Long_Natural;
-    type Variable_ID_Number  is new Long_Natural;
-
-    type Variable is record
-        Ident : Generator_ID_Number;
-        Name  : Nametag;
-    end record;
+    type Variable is new Long_Natural;
 
 
 
@@ -517,7 +450,8 @@ private
 
     function T
            (Item : in Variable)
-        return Term'Class;
+        return Term'Class
+    with Post => T'Result.Kind = Var_Term;
 
     function Var
            (This : in Term'Class)
@@ -531,22 +465,16 @@ private
 
 
 
-    package ID_Number_Maps is new Ada.Containers.Ordered_Maps
-       (Key_Type     => Generator_ID_Number,
-        Element_Type => Variable_ID_Number);
-
-    package Name_Vectors is new Ada.Containers.Vectors
-       (Index_Type   => Variable_ID_Number,
-        Element_Type => Nametag,
-        "="          => SU."=");
+    package Variable_Vectors is new Ada.Containers.Vectors
+       (Index_Type   => Long_Positive,
+        Element_Type => Variable);
 
     package Binding_Maps is new Ada.Containers.Ordered_Maps
-       (Key_Type     => Variable_ID_Number,
+       (Key_Type     => Variable,
         Element_Type => Term);
 
     type State is record
-        Ident : ID_Number_Maps.Map;
-        LVars : Name_Vectors.Vector;
+        LVars : Variable_Vectors.Vector;
         Subst : Binding_Maps.Map;
     end record;
 
@@ -555,8 +483,7 @@ private
         Element_Type => State);
 
     Empty_State : constant State :=
-       (Ident => ID_Number_Maps.Empty_Map,
-        LVars => Name_Vectors.Empty_Vector,
+       (LVars => Variable_Vectors.Empty_Vector,
         Subst => Binding_Maps.Empty_Map);