Variable counting handled properly on a per-State basis

1 files changed, 36 insertions, 24 deletions

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;