Variable counting handled properly on a per-State basis

6 files changed, 151 insertions, 137 deletions

diff --git a/src/kompsos-pretty_print.adb b/src/kompsos-pretty_print.adb
index 8739af8..772c0cd 100644
--- a/src/kompsos-pretty_print.adb
+++ b/src/kompsos-pretty_print.adb
@@ -45,7 +45,7 @@ package body Kompsos.Pretty_Print is
            (Item : in Variable)
         return String is
     begin
-        return "Var#" & Image (Item.Ident) &
+        return "Vargen#" & Image (ID_Number (Item.Ident)) &
            (if SU.Length (Item.Name) /= 0
             then "/" & SU.To_String (Item.Name)
             else "");
@@ -95,16 +95,29 @@ package body Kompsos.Pretty_Print is
         return String
     is
         Result : SU.Unbounded_String;
-        My_Var : Variable;
     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 (ID_Number (ID_Number_Maps.Key (Iter))) & " => " &
+                    Image (ID_Number (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 Iter in Item.LVars.Iterate loop
-                My_Var := (Ident => Name_Maps.Key (Iter), Name => Name_Maps.Element (Iter));
-                SU.Append (Result, Latin.HT & Latin.HT & Image (My_Var) & Latin.LF);
+            for Index in Item.LVars.First_Index .. Item.LVars.Last_Index loop
+                SU.Append (Result, Latin.HT & Latin.HT &
+                    "Var#" & Image (ID_Number (Index)) &
+                   (if SU.Length (Item.LVars (Index)) /= 0
+                    then "/" & SU.To_String (Item.LVars (Index))
+                    else "") & Latin.LF);
             end loop;
         end if;
         SU.Append (Result, Latin.HT & "Substitution:");
@@ -114,7 +127,7 @@ 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 (Binding_Maps.Key (Iter)) & " => " &
+                    Image (ID_Number (Binding_Maps.Key (Iter))) & " => " &
                     Image (Binding_Maps.Element (Iter)) & Latin.LF);
             end loop;
         end if;
@@ -125,26 +138,35 @@ package body Kompsos.Pretty_Print is
 
 
     function Image
-           (Item : in World)
+           (Item : in out World)
         return String
     is
         Result  : SU.Unbounded_String;
-        Scratch : World := Item;
         Counter : Positive := 1;
     begin
-        if not Scratch.Has_State (Counter) then
+        if not Item.Has_State (Counter) then
             return "States: N/A" & Latin.LF;
         end if;
         loop
             SU.Append (Result, "State#" & Image (Counter) & ":" & Latin.LF);
-            SU.Append (Result, Image (Scratch.Possibles.Constant_Reference (Counter)));
+            SU.Append (Result, Image (Item.Possibles.Constant_Reference (Counter)));
             Counter := Counter + 1;
-            exit when not Scratch.Has_State (Counter);
+            exit when not Item.Has_State (Counter);
         end loop;
         return SU.Slice (Result, 1, SU.Length (Result) - 1);
     end Image;
 
 
+    function Image_Constant
+           (Item : in World)
+        return String
+    is
+        Scratch : World := Item;
+    begin
+        return Image (Scratch);
+    end Image_Constant;
+
+
 end Kompsos.Pretty_Print;
 
 
diff --git a/src/kompsos-pretty_print.ads b/src/kompsos-pretty_print.ads
index bf0b9d7..bcaf86e 100644
--- a/src/kompsos-pretty_print.ads
+++ b/src/kompsos-pretty_print.ads
@@ -14,16 +14,16 @@ package Kompsos.Pretty_Print is
 
 
     function Image
-           (Item : in Variable)
+           (Item : in Term)
         return String;
 
 
     function Image
-           (Item : in Term)
+           (Item : in out World)
         return String;
 
 
-    function Image
+    function Image_Constant
            (Item : in World)
         return String;
 
@@ -42,6 +42,11 @@ private
 
 
     function Image
+           (Item : in Variable)
+        return String;
+
+
+    function Image
            (Item : in State)
         return String;
 
diff --git a/src/kompsos.adb b/src/kompsos.adb
index 9d45f66..b3816fa 100644
--- a/src/kompsos.adb
+++ b/src/kompsos.adb
@@ -75,13 +75,21 @@ package body Kompsos is
 
 
     function Var
-           (This : in Term)
+           (This : in Term'Class)
         return Variable is
     begin
         return Term_Component (This.Actual.Constant_Reference.Element.all).Refer;
     end Var;
 
 
+    function Name
+           (This : in Term)
+        return SU.Unbounded_String is
+    begin
+        return This.Var.Name;
+    end Name;
+
+
     function Left
            (This : in Term)
         return Term is
@@ -134,20 +142,22 @@ package body Kompsos is
     --  Internal Helpers  --
     ------------------------
 
-    --  Unification  --
+    --  Variable IDs  --
 
-    function Has_Var
-           (This : in State;
-            Var  : in Variable)
-        return Boolean
-    is
-        use type SU.Unbounded_String;
+    Next_Generator_ID : Generator_ID_Number := Generator_ID_Number'First;
+
+    function Next_Gen
+        return Generator_ID_Number is
     begin
-        return This.LVars.Contains (Var.Ident) and then
-            This.LVars.Constant_Reference (Var.Ident) = Var.Name;
-    end Has_Var;
+        return Result : constant Generator_ID_Number := Next_Generator_ID do
+            Next_Generator_ID := Next_Generator_ID + 1;
+        end return;
+    end Next_Gen;
+
 
 
+    --  Unification  --
+
     function Fully_Contains
            (This : in State;
             Item : in Term'Class)
@@ -157,7 +167,7 @@ package body Kompsos is
         when Null_Term | Atom_Term =>
             return True;
         when Var_Term =>
-            return Has_Var (This, Item.Var);
+            return This.Ident.Contains (Item.Var.Ident);
         when Pair_Term =>
             return Fully_Contains (This, Item.Left) and then Fully_Contains (This, Item.Right);
         end case;
@@ -169,8 +179,10 @@ package body Kompsos is
             Item : in Term'Class)
         return Term'Class is
     begin
-        if Item.Kind = Var_Term and then This.Subst.Contains (Item.Var.Ident) then
-            return Walk (This, This.Subst.Constant_Reference (Item.Var.Ident));
+        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)));
         else
             return Item;
         end if;
@@ -186,32 +198,29 @@ package body Kompsos is
         Real_Left  : Term'Class := Left;
         Real_Right : Term'Class := Right;
     begin
+        --  Check for Variable validity with respect to State
+        if  not Fully_Contains (Potential, Real_Left) or
+            not Fully_Contains (Potential, Real_Right)
+        then
+            return False;
+        end if;
+
         --  Resolve Variable substitution
         if Left.Kind = Var_Term then
-            if Has_Var (Potential, Left.Var) then
-                Real_Left := Walk (Potential, Left);
-            else
-                return False;
-            end if;
+            Real_Left := Walk (Potential, Real_Left);
         end if;
         if Right.Kind = Var_Term then
-            if Has_Var (Potential, Right.Var) then
-                Real_Right := Walk (Potential, Right);
-            else
-                return False;
-            end if;
+            Real_Right := Walk (Potential, Real_Right);
         end if;
 
-        --  Check for equal Null Terms
-        if Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term then
-            Extended := Potential;
-            return True;
-        end if;
-
-        --  Unify equal Variable Terms
-        if  Real_Left.Kind = Var_Term and then
+        --  Unify equal Variable/Atom/Null Terms
+        if (Real_Left.Kind = Var_Term and then
             Real_Right.Kind = Var_Term and then
-            Real_Left = Real_Right
+            Real_Left = Real_Right) or else
+           (Real_Left.Kind = Atom_Term and then
+            Real_Right.Kind = Atom_Term and then
+            Real_Left = Real_Right) or else
+           (Real_Left.Kind = Null_Term and Real_Right.Kind = Null_Term)
         then
             Extended := Potential;
             return True;
@@ -219,41 +228,18 @@ package body Kompsos is
 
         --  Unify Variable and other Terms by introducing a new substitution
         if Real_Left.Kind = Var_Term then
-            if  Real_Right.Kind = Pair_Term and then
-                not Fully_Contains (Potential, Real_Right)
-            then
-                return False;
-            end if;
             Extended := Potential;
-            Extended.Subst.Insert (Real_Left.Var.Ident, Term (Real_Right));
+            Extended.Subst.Insert (Extended.Ident.Element (Real_Left.Var.Ident), Term (Real_Right));
             return True;
         end if;
         if Real_Right.Kind = Var_Term then
-            if  Real_Left.Kind = Pair_Term and then
-                not Fully_Contains (Potential, Real_Left)
-            then
-                return False;
-            end if;
-            Extended := Potential;
-            Extended.Subst.Insert (Real_Right.Var.Ident, Term (Real_Left));
-            return True;
-        end if;
-
-        --  Unify equal Atom Terms
-        if  Real_Left.Kind = Atom_Term and then
-            Real_Right.Kind = Atom_Term and then
-            Real_Left = Real_Right
-        then
             Extended := Potential;
+            Extended.Subst.Insert (Extended.Ident.Element (Real_Right.Var.Ident), Term (Real_Left));
             return True;
         end if;
 
         --  Unify Pair Terms by unifying each corresponding part
-        if  Real_Left.Kind = Pair_Term and then
-            Real_Right.Kind = Pair_Term and then
-            Fully_Contains (Potential, Real_Left) and then
-            Fully_Contains (Potential, Real_Right)
-        then
+        if Real_Left.Kind = Pair_Term and then Real_Right.Kind = Pair_Term then
             declare
                 Middle : State;
             begin
@@ -285,7 +271,8 @@ package body Kompsos is
     begin
         Ptr (This.Engine.Frs_World).Rollover;
         for Potential of Ptr (This.Engine.Frs_World).Possibles loop
-            Potential.LVars.Insert (Ptr (This.Engine.Frs_World).Next_Ident, This.Engine.Frs_Name);
+            Potential.LVars.Append (This.Engine.Frs_Name);
+            Potential.Ident.Insert (This.Engine.Frs_Ident, Potential.LVars.Last_Index);
             This.Possibles.Append (Potential);
         end loop;
         if Ptr (This.Engine.Frs_World).Engine.Kind = No_Gen then
@@ -478,14 +465,16 @@ package body Kompsos is
     function Fresh
            (This : in out World'Class;
             Name : in     Ada.Strings.Unbounded.Unbounded_String)
-        return Term is
+        return Term
+    is
+        My_ID : constant Generator_ID_Number := Next_Gen;
     begin
-        return My_Term : constant Term := T (Variable'(Ident => This.Next_Ident, Name => Name)) do
+        return My_Term : constant Term := T (Variable'(Ident => My_ID, Name => Name)) do
             This.Engine :=
                (Kind      => Fresh_Gen,
+                Frs_Ident => My_ID,
                 Frs_World => Hold (This),
                 Frs_Name  => Name);
-            This.Next_Ident := This.Next_Ident + 1;
             This.Possibles := State_Vectors.Empty_Vector;
         end return;
     end Fresh;
@@ -519,9 +508,8 @@ package body Kompsos is
         return World is
     begin
         return Result : constant World :=
-           (Possibles  => State_Vectors.Empty_Vector,
-            Next_Ident => This.Next_Ident,
-            Engine     =>
+           (Possibles => State_Vectors.Empty_Vector,
+            Engine    =>
                (Kind      => Unify_Gen,
                 Uni_World => Hold (This),
                 Uni_Term1 => Term (Left),
@@ -545,9 +533,8 @@ package body Kompsos is
         return World is
     begin
         return Result : constant World :=
-           (Possibles  => State_Vectors.Empty_Vector,
-            Next_Ident => ID_Number'Max (Left.Next_Ident, Right.Next_Ident),
-            Engine     =>
+           (Possibles => State_Vectors.Empty_Vector,
+            Engine    =>
                (Kind       => Disjunct_Gen,
                 Dis_World1 => Hold (Left),
                 Dis_World2 => Hold (Right)));
@@ -568,24 +555,17 @@ package body Kompsos is
     begin
         if Inputs'Length = 0 then
             return Failed : constant World :=
-               (Possibles  => State_Vectors.Empty_Vector,
-                Next_Ident => 0,
-                Engine     => (Kind => No_Gen));
+               (Possibles => State_Vectors.Empty_Vector,
+                Engine    => (Kind => No_Gen));
         elsif Inputs'Length = 1 then
             return Inputs (Inputs'First);
         else
-            return Result : World :=
-               (Possibles  => State_Vectors.Empty_Vector,
-                Next_Ident => 0,  --  dummy
-                Engine     =>
+            return Result : constant World :=
+               (Possibles => State_Vectors.Empty_Vector,
+                Engine    =>
                    (Kind       => Disjunct_Gen,
                     Dis_World1 => Hold (Inputs (Inputs'First)),
-                    Dis_World2 => Hold (Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last)))))
-            do
-                Result.Next_Ident := ID_Number'Max
-                   (Ptr (Result.Engine.Dis_World1).Next_Ident,
-                    Ptr (Result.Engine.Dis_World2).Next_Ident);
-            end return;
+                    Dis_World2 => Hold (Disjunct (Inputs (Inputs'First + 1 .. Inputs'Last)))));
         end if;
     end Disjunct;
 
@@ -607,9 +587,8 @@ package body Kompsos is
         return World is
     begin
         return Result : constant World :=
-           (Possibles  => State_Vectors.Empty_Vector,
-            Next_Ident => 0,  --  dummy
-            Engine     =>
+           (Possibles => State_Vectors.Empty_Vector,
+            Engine    =>
                (Kind       => Conjunct_Zero_Gen,
                 ConZ_World => Hold (This),
                 ConZ_Func  => Func));
@@ -631,9 +610,8 @@ package body Kompsos is
         return World is
     begin
         return Result : constant World :=
-           (Possibles  => State_Vectors.Empty_Vector,
-            Next_Ident => 0,  --  dummy
-            Engine     =>
+           (Possibles => State_Vectors.Empty_Vector,
+            Engine    =>
                (Kind       => Conjunct_One_Gen,
                 ConO_World => Hold (This),
                 ConO_Func  => Func,
@@ -657,9 +635,8 @@ package body Kompsos is
         return World is
     begin
         return Result : constant World :=
-           (Possibles  => State_Vectors.Empty_Vector,
-            Next_Ident => 0,  --  dummy
-            Engine     =>
+           (Possibles => State_Vectors.Empty_Vector,
+            Engine    =>
                (Kind        => Conjunct_Many_Gen,
                 ConM_World  => Hold (This),
                 ConM_Func   => Func,
@@ -689,9 +666,8 @@ package body Kompsos is
         return World is
     begin
         return Result : constant World :=
-           (Possibles  => State_Vectors.Empty_Vector,
-            Next_Ident => This.Next_Ident,
-            Engine     =>
+           (Possibles => State_Vectors.Empty_Vector,
+            Engine    =>
                (Kind      => Recurse_Gen,
                 Rec_World => Hold (This),
                 Rec_Index => 1));
@@ -715,9 +691,8 @@ package body Kompsos is
     begin
         if Count = 0 then
             return
-               (Possibles  => State_Vectors.Empty_Vector,
-                Next_Ident => ID_Number'First,
-                Engine     => (Kind => No_Gen));
+               (Possibles => State_Vectors.Empty_Vector,
+                Engine    => (Kind => No_Gen));
         end if;
         return Result : World := This do
             Result.Roll_Until (Count);
diff --git a/src/kompsos.ads b/src/kompsos.ads
index cf4ba31..c336a41 100644
--- a/src/kompsos.ads
+++ b/src/kompsos.ads
@@ -14,8 +14,7 @@ private with
 
     Ada.Containers.Indefinite_Holders,
     Ada.Containers.Ordered_Maps,
-    Ada.Containers.Vectors,
-    Ada.Finalization;
+    Ada.Containers.Vectors;
 
 
 generic
@@ -27,9 +26,6 @@ package Kompsos is
     --  Datatypes  --
     -----------------
 
-    type Variable is private;
-
-
     type Term_Kind is (Null_Term, Atom_Term, Var_Term, Pair_Term);
 
     type Term is tagged private;
@@ -58,9 +54,9 @@ package Kompsos is
         return Element_Type
     with Pre => This.Kind = Atom_Term;
 
-    function Var
+    function Name
            (This : in Term)
-        return Variable
+        return Ada.Strings.Unbounded.Unbounded_String
     with Pre => This.Kind = Var_Term;
 
     function Left
@@ -105,17 +101,20 @@ package Kompsos is
 
     function Fresh
            (This : in out World'Class)
-        return Term;
+        return Term
+    with Post => Fresh'Result.Kind = Var_Term;
 
     function Fresh
            (This : in out World'Class;
             Name : in     String)
-        return Term;
+        return Term
+    with Post => Fresh'Result.Kind = Var_Term;
 
     function Fresh
            (This : in out World'Class;
             Name : in     Ada.Strings.Unbounded.Unbounded_String)
-        return Term;
+        return Term
+    with Post => Fresh'Result.Kind = Var_Term;
 
 
     --  Unification  --
@@ -404,11 +403,14 @@ private
 
 
 
-    --  2^32 possible Variables per World is enough for anybody, right?
-    type ID_Number is mod 2 ** 32;
+    --  around 2^31 possible Variables should be enough for anybody, right?
+    type ID_Number is new Long_Integer range 0 .. Long_Integer'Last;
+
+    type Generator_ID_Number is new ID_Number;
+    type Variable_ID_Number  is new ID_Number;
 
     type Variable is record
-        Ident : ID_Number;
+        Ident : Generator_ID_Number;
         Name  : SU.Unbounded_String;
     end record;
 
@@ -436,6 +438,11 @@ private
         Actual : Term_Holders.Holder;
     end record;
 
+    function Var
+           (This : in Term'Class)
+        return Variable
+    with Pre => This.Kind = Var_Term;
+
     Empty_Term : constant Term :=
         (Actual => Term_Holders.To_Holder (Term_Component'(Kind => Null_Term)));
 
@@ -444,22 +451,28 @@ private
 
 
 
-    package Name_Maps is new Ada.Containers.Ordered_Maps
-       (Key_Type     => ID_Number,
+    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 => SU.Unbounded_String,
         "="          => SU."=");
 
     package Binding_Maps is new Ada.Containers.Ordered_Maps
-       (Key_Type     => ID_Number,
+       (Key_Type     => Variable_ID_Number,
         Element_Type => Term);
 
     type State is record
-        LVars : Name_Maps.Map;
+        Ident : ID_Number_Maps.Map;
+        LVars : Name_Vectors.Vector;
         Subst : Binding_Maps.Map;
     end record;
 
     Empty_State : constant State :=
-       (LVars => Name_Maps.Empty_Map,
+       (Ident => ID_Number_Maps.Empty_Map,
+        LVars => Name_Vectors.Empty_Vector,
         Subst => Binding_Maps.Empty_Map);
 
 
@@ -501,6 +514,7 @@ private
         when No_Gen =>
             null;
         when Fresh_Gen =>
+            Frs_Ident   : Generator_ID_Number;
             Frs_World   : World_Holders.Holder;
             Frs_Name    : SU.Unbounded_String;
         when Unify_Gen =>
@@ -534,9 +548,8 @@ private
         Element_Type => State);
 
     type World is new World_Root with record
-        Possibles  : State_Vectors.Vector;
-        Next_Ident : ID_Number;
-        Engine     : Generator;
+        Possibles : State_Vectors.Vector;
+        Engine    : Generator;
     end record;
 
     function Has_State
@@ -554,9 +567,8 @@ private
     use type State_Vectors.Vector;
 
     Empty_World : constant World :=
-       (Possibles  => State_Vectors.Empty_Vector & Empty_State,
-        Next_Ident => 0,
-        Engine     => (Kind => No_Gen));
+       (Possibles => State_Vectors.Empty_Vector & Empty_State,
+        Engine    => (Kind => No_Gen));
 
 
 end Kompsos;
diff --git a/test/membero.adb b/test/membero.adb
index 46127d7..bc51c33 100644
--- a/test/membero.adb
+++ b/test/membero.adb
@@ -44,7 +44,7 @@ begin
 
     Verse.Member (Verse.Fresh ("result") & Test_Item);
 
-    TIO.Put_Line (Printer.Image (Verse.Take (5)));
+    TIO.Put_Line (Printer.Image (Verse));
 
 end Membero;
 
diff --git a/test/pprint.adb b/test/pprint.adb
index c42b2c8..2003238 100644
--- a/test/pprint.adb
+++ b/test/pprint.adb
@@ -50,7 +50,7 @@ begin
 
     TIO.New_Line;
 
-    TIO.Put_Line (Image (Empty_World));
+    TIO.Put_Line (Image_Constant (Empty_World));
 
 end PPrint;