Make fresh variables really fresh

Add a global variable table, so when we call "Var.mk id" twice, the
same variable is returned and when we call "Var.fresh v" we always
return a truly globally fresh variable.

types/types.ml

@@ -689,7 +689,8 @@ module Witness = struct
       ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
       ~atom:f
 
-  let rec node_has n = function
+  let rec node_has n = 
+    function
     | WXml (_,_,s) | WPair (_,_,s) | WFun (_,s) | WRecord (_,_,s) as w ->
 	if NodeSet.mem n s.wnodes_in then true
 	else if NodeSet.mem n s.wnodes_out then false
@@ -701,7 +702,8 @@ module Witness = struct
 
   (* type_has checks if a witness is contained in the union of
    * the leafs of a bdd, ignoring all variables. *)
-  and type_has t = function
+  and type_has t = 
+    function
     | WInt i -> Intervals.contains i (BoolIntervals.leafconj t.ints)
     | WChar c -> Chars.contains c (BoolChars.leafconj t.chars)
     | WAtom a -> Atoms.contains_sample a (BoolAtoms.leafconj t.atoms)
@@ -805,8 +807,7 @@ let rec slot d =
   then slot_nempty (Witness.WChar (Chars.sample (BoolChars.leafconj d.chars)))
   else if not (Abstracts.is_empty (BoolAbstracts.leafconj d.abstract))
   then slot_nempty (Witness.WAbstract (Abstracts.sample (BoolAbstracts.leafconj d.abstract)))
-  else try
-         DescrHash.find memo d
+  else try DescrHash.find memo d
   with Not_found ->
     let s = { status = Maybe; active = false; notify = Nothing } in
     DescrHash.add memo d s;
@@ -3114,15 +3115,6 @@ module Tallying = struct
     type m = M.t
     type es = ES.t
     type sigma = Descr.s E.t
-    module SUB = SortedList.FiniteCofinite(struct
-      type t = Descr.s E.t
-      let compare = E.compare compare
-      let equal = E.equal equal
-      let hash = Hashtbl.hash
-      let dump = E.pp
-      let check _ = ()
-    end)
-
     type sl = sigma list
 
     let singleton c =
@@ -3225,7 +3217,7 @@ module Tallying = struct
 
   let rec norm (t,delta,mem) =
     (* if we already evaluated it, it is sat *)
-      let res =
+    let res =
       if DescrSet.mem t mem || is_empty t then CS.sat
       else if is_var t then begin
       (* if there is only one variable then is it A <= 0 or 1 <= A *)
@@ -3259,7 +3251,7 @@ module Tallying = struct
           in
           res
         end
-      in
+    in
       (* Format.printf "Normalizing %a yields %a\n%!" Print.pp_type t CS.pp_s res; *) res
 
   (* (t1,t2) = intersection of all (fst pos,snd pos) \in P

types/var.ml

@@ -7,13 +7,29 @@ module V = struct
   let hash x = Hashtbl.hash (x.id,x.fr)
   let check _ = ()
 
+  let id x = Ident.U.get_str x.id
+  let cache = Hashtbl.create 17
+
   let is_fresh x = x.fr > 0
-  let fresh v = { v with fr = v.fr + 1 }
+  let fresh v =
+    try
+      let w = Hashtbl.find cache (id v) in
+      let w = { w with fr = w.fr + 1 } in
+      Hashtbl.replace cache (id w) w;
+      w
+    with Not_found ->
+      assert false
 
-  let mk id = { id = Ident.U.mk id; fr = 0 }
-  let id x = Ident.U.get_str x.id
+  let mk id = 
+    try Hashtbl.find cache id
+    with Not_found -> begin
+      let v = { id = Ident.U.mk id; fr = 0 } in
+      Hashtbl.add cache id v;
+      v
+    end
 
   let pp ppf x = Format.fprintf ppf "'%a" Ident.U.print x.id
+  let pp ppf x = dump ppf x
 end
 
 include V

typing/typer.ml

@@ -395,8 +395,8 @@ module IType = struct
              let l = ref [] in
              for i=0 to (Array.length pargs) - 1 do
                try
-                 let err s = Error s in
-                 l := (pargs.(i), typ ~err (derecurs env a.(i)))::!l
+                 let tt = typ ~err:(fun s -> Error s) (derecurs env a.(i)) in
+                 l := (pargs.(i), tt)::!l
                with 
                |Error s -> raise_loc_generic loc s
                |_ -> assert false
@@ -458,13 +458,19 @@ module IType = struct
     in
     let b =
       List.map2 (fun ((loc,v),pl,p) (v',_,d) ->
-        let t = aux loc d in
+        let t = Types.Positive.substitutefree Var.Set.empty (aux loc d) in
+        let vars = Var.Set.fold (fun acc v -> (Var.id v,v)::acc) [] (Types.all_vars t) in
         if (loc <> noloc) && (Types.is_empty t) then
          warning loc
            ("This definition yields an empty type for " ^ (U.to_string v));
+        if (List.length vars) <> (List.length pl) then
+          warning loc
+            ("Definition of type" ^ (U.to_string v) ^ 
+            " contains unused/undeclared type variables");
         let al =
           let a = Array.make (List.length pl) (Var.mk "dummy")in
-          List.iteri (fun i v -> a.(i) <- Var.mk (Ident.U.to_string v)) pl;
+          (* XXX here I use pervasive.compare instead of string compare *)
+          List.iteri (fun i v -> a.(i) <- (List.assoc (U.to_string v) vars)) pl;
           a
         in 
         (v',t,al)