do not hide OCaml's Hashtbl

export Why3's extended hash tables as Stdlib.XHashtbl
in order to keep OCaml's Hashtbl accessible. Unlike Stdlib.Map
which fully covers the OCaml's interface, Stdlib.XHashtbl does
not provide polymorphic hash tables.

src/core/decl.mli

@@ -61,7 +61,7 @@ type prsymbol = private {
 
 module Mpr : Map.S with type key = prsymbol
 module Spr : Mpr.Set
-module Hpr : Hashtbl.S with type key = prsymbol
+module Hpr : XHashtbl.S with type key = prsymbol
 module Wpr : Weakhtbl.S with type key = prsymbol
 
 val create_prsymbol : preid -> prsymbol
@@ -106,7 +106,7 @@ and decl_node =
 module Mdecl : Map.S with type key = decl
 module Sdecl : Mdecl.Set
 module Wdecl : Weakhtbl.S with type key = decl
-module Hdecl : Hashtbl.S  with type key = decl
+module Hdecl : XHashtbl.S with type key = decl
 
 val d_equal : decl -> decl -> bool
 val d_hash : decl -> int

src/core/ident.mli

@@ -39,7 +39,7 @@ type ident = private {
 
 module Mid : Map.S with type key = ident
 module Sid : Mid.Set
-module Hid : Hashtbl.S with type key = ident
+module Hid : XHashtbl.S with type key = ident
 module Wid : Weakhtbl.S with type key = ident
 
 val id_equal : ident -> ident -> bool

src/core/term.ml

@@ -1297,7 +1297,7 @@ let rec t_hash_alpha c m t =
 
 let t_hash_alpha = t_hash_alpha (ref (-1)) Mvs.empty
 
-module Hterm_alpha = Hashtbl.Make (struct
+module Hterm_alpha = XHashtbl.Make (struct
   type t = term
   let equal = t_equal_alpha
   let hash = t_hash_alpha

src/core/term.mli

@@ -24,7 +24,7 @@ type vsymbol = private {
 
 module Mvs : Map.S with type key = vsymbol
 module Svs : Mvs.Set
-module Hvs : Hashtbl.S with type key = vsymbol
+module Hvs : XHashtbl.S with type key = vsymbol
 module Wvs : Weakhtbl.S with type key = vsymbol
 
 val vs_equal : vsymbol -> vsymbol -> bool
@@ -42,7 +42,7 @@ type lsymbol = private {
 
 module Mls : Map.S with type key = lsymbol
 module Sls : Mls.Set
-module Hls : Hashtbl.S with type key = lsymbol
+module Hls : XHashtbl.S with type key = lsymbol
 module Wls : Weakhtbl.S with type key = lsymbol
 
 val ls_equal : lsymbol -> lsymbol -> bool
@@ -154,7 +154,7 @@ and trigger = term list list
 
 module Mterm : Map.S with type key = term
 module Sterm : Mterm.Set
-module Hterm : Hashtbl.S with type key = term
+module Hterm : XHashtbl.S with type key = term
 
 val t_equal : term -> term -> bool
 val t_hash : term -> int
@@ -421,7 +421,7 @@ val t_app_fold :
 
 val t_equal_alpha : term -> term -> bool
 
-module Hterm_alpha : Hashtbl.S with type key = term
+module Hterm_alpha : XHashtbl.S with type key = term
 
 (** Subterm occurrence check and replacement *)
 

src/core/theory.mli

@@ -60,7 +60,7 @@ val print_meta_desc : Pp.formatter -> meta -> unit
 
 module Mmeta : Map.S with type key = meta
 module Smeta : Mmeta.Set
-module Hmeta : Hashtbl.S with type key = meta
+module Hmeta : XHashtbl.S with type key = meta
 
 val meta_equal : meta -> meta -> bool
 val meta_hash : meta -> int
@@ -107,7 +107,7 @@ and symbol_map = private {
 
 module Mtdecl : Map.S with type key = tdecl
 module Stdecl : Mtdecl.Set
-module Htdecl : Hashtbl.S with type key = tdecl
+module Htdecl : XHashtbl.S with type key = tdecl
 
 val td_equal : tdecl -> tdecl -> bool
 val td_hash : tdecl -> int

src/core/ty.mli

@@ -20,7 +20,7 @@ type tvsymbol = private {
 
 module Mtv : Map.S with type key = tvsymbol
 module Stv : Mtv.Set
-module Htv : Hashtbl.S with type key = tvsymbol
+module Htv : XHashtbl.S with type key = tvsymbol
 
 val tv_equal : tvsymbol -> tvsymbol -> bool
 
@@ -47,12 +47,12 @@ and ty_node = private
 
 module Mts : Map.S with type key = tysymbol
 module Sts : Mts.Set
-module Hts : Hashtbl.S with type key = tysymbol
+module Hts : XHashtbl.S with type key = tysymbol
 module Wts : Weakhtbl.S with type key = tysymbol
 
 module Mty : Map.S with type key = ty
 module Sty : Mty.Set
-module Hty : Hashtbl.S with type key = ty
+module Hty : XHashtbl.S with type key = ty
 module Wty : Weakhtbl.S with type key = ty
 
 val ts_equal : tysymbol -> tysymbol -> bool

src/driver/whyconf.ml

@@ -91,7 +91,7 @@ end
 
 module Mprover = Map.Make(Prover)
 module Sprover = Mprover.Set
-module Hprover = Hashtbl.Make(Prover)
+module Hprover = XHashtbl.Make(Prover)
 
 module Editor = struct
   type t = string

src/driver/whyconf.mli

@@ -101,7 +101,7 @@ val print_prover_parsable_format : Format.formatter -> prover -> unit
 module Prover   : OrderedHashedType with type t = prover
 module Mprover  : Map.S with type key = prover
 module Sprover  : Mprover.Set
-module Hprover  : Hashtbl.S with type key = prover
+module Hprover  : XHashtbl.S with type key = prover
 
 (** {3 Prover configuration} *)
 

src/session/session.ml

@@ -72,7 +72,7 @@ end
 
 module Mpos = Map.Make(Pos)
 module Spos = Mpos.Set
-module Hpos = Hashtbl.Make(Pos)
+module Hpos = XHashtbl.Make(Pos)
 
 type meta_args = meta_arg list
 
@@ -102,7 +102,8 @@ module Mmeta_args = Map.Make(struct
 end)
 module Smeta_args = Mmeta_args.Set
 
-type metas_args =  Smeta_args.t Mstr.t
+type metas_args = Smeta_args.t Mstr.t
+
 module Mmetas_args = Map.Make(struct
   type t = metas_args
   let compare = Mstr.compare Smeta_args.compare

src/session/session.mli

@@ -21,8 +21,8 @@ open Stdlib
 val debug : Debug.flag
 (** The debug flag "session" *)
 
-module PHstr : Hashtbl.Private with type key = string
-module PHprover : Hashtbl.Private with type key = Whyconf.prover
+module PHstr : XHashtbl.Private with type key = string
+module PHprover : XHashtbl.Private with type key = Whyconf.prover
 
 (** {2 Proof attempts} *)
 

src/transform/induction.ml

@@ -71,25 +71,10 @@ type vlex =
 
   This definitions and methods using them are without use if some induction tags
   are provided in the goal by user.*)
-module VsList =
-struct
-  type t = vsymbol list
-  let hash = Hashcons.combine_list vs_hash 3
-  let equal = Lists.equal vs_equal
-  let cmp_vs vs1 vs2 = Pervasives.compare (vs_hash vs2) (vs_hash vs1)
-  let compare t1 t2 =
-    let rec aux t1 t2 = match t1,t2 with
-      | [],[] -> 0
-      | v1 :: q1, v2 :: q2 ->
-	if vs_equal v1 v2
-	then aux q1 q2
-	else cmp_vs v1 v2
-      | _ -> assert false;
-    in
-    if List.length t1 < List.length t2 then -1
-    else if List.length t1 > List.length t2 then 1
-    else aux t1 t2
-end
+module VsList = Stdlib.OrderedHashedList(struct
+  type t = vsymbol
+  let tag = vs_hash
+end)
 module Mvsl = Stdlib.Map.Make(VsList)
 module Svsl = Mvsl.Set
 

src/util/stdlib.ml

@@ -10,7 +10,7 @@
 (********************************************************************)
 
 module Map = Extmap.Map
-module Hashtbl = Exthtbl.Hashtbl
+module XHashtbl = Exthtbl.Hashtbl
 
 (* Set, Map, Hashtbl on ints and strings *)
 
@@ -23,11 +23,11 @@ module Int = struct
 
 module Mint = Map.Make(Int)
 module Sint = Mint.Set
-module Hint = Hashtbl.Make(Int)
+module Hint = XHashtbl.Make(Int)
 
 module Mstr = Map.Make(String)
 module Sstr = Mstr.Set
-module Hstr = Hashtbl.Make
+module Hstr = XHashtbl.Make
   (struct
     type t = String.t
     let hash    = (Hashtbl.hash : string -> int)
@@ -73,7 +73,7 @@ struct
   module T = OrderedHashed(X)
   module M = Map.Make(T)
   module S = M.Set
-  module H = Hashtbl.Make(T)
+  module H = XHashtbl.Make(T)
 end
 
 module MakeTagged (X : Weakhtbl.Weakey) =
@@ -87,6 +87,6 @@ struct
   module T = OrderedHashed(MakeTagged(X))
   module M = Map.Make(T)
   module S = M.Set
-  module H = Hashtbl.Make(T)
+  module H = XHashtbl.Make(T)
   module W = Weakhtbl.Make(X)
 end

src/util/stdlib.mli

@@ -10,17 +10,17 @@
 (********************************************************************)
 
 module Map : Extmap.Map
-module Hashtbl : Exthtbl.Hashtbl
+module XHashtbl : Exthtbl.Hashtbl
 
 (* Set, Map, Hashtbl on ints and strings *)
 
 module Mint : Map.S with type key = int
 module Sint : Mint.Set
-module Hint : Hashtbl.S with type key = int
+module Hint : XHashtbl.S with type key = int
 
 module Mstr : Map.S with type key = string
 module Sstr : Mstr.Set
-module Hstr : Hashtbl.S with type key = string
+module Hstr : XHashtbl.S with type key = string
 
 (* Set, Map, Hashtbl on structures with a unique tag *)
 
@@ -48,13 +48,13 @@ module MakeMSH (X : TaggedType) :
 sig
   module M : Map.S with type key = X.t
   module S : M.Set
-  module H : Hashtbl.S with type key = X.t
+  module H : XHashtbl.S with type key = X.t
 end
 
 module MakeMSHW (X : Weakhtbl.Weakey) :
 sig
   module M : Map.S with type key = X.t
   module S : M.Set
-  module H : Hashtbl.S with type key = X.t
+  module H : XHashtbl.S with type key = X.t
   module W : Weakhtbl.S with type key = X.t
 end

src/whyml/mlw_expr.mli

@@ -100,7 +100,7 @@ type psymbol = private {
 
 module Mps : Map.S with type key = psymbol
 module Sps : Mps.Set
-module Hps : Hashtbl.S with type key = psymbol
+module Hps : XHashtbl.S with type key = psymbol
 module Wps : Weakhtbl.S with type key = psymbol
 
 val ps_equal : psymbol -> psymbol -> bool

src/whyml/mlw_ty.ml

@@ -91,7 +91,7 @@ end
 and Reg : sig
   module M : Map.S with type key = T.region
   module S : M.Set
-  module H : Hashtbl.S with type key = T.region
+  module H : XHashtbl.S with type key = T.region
   module W : Weakhtbl.S with type key = T.region
 end = MakeMSHW (struct
   type t = T.region

src/whyml/mlw_ty.mli

@@ -58,16 +58,16 @@ open T
 
 module Mits : Map.S with type key = itysymbol
 module Sits : Mits.Set
-module Hits : Hashtbl.S with type key = itysymbol
+module Hits : XHashtbl.S with type key = itysymbol
 module Wits : Weakhtbl.S with type key = itysymbol
 
 module Mity : Map.S with type key = ity
 module Sity : Mity.Set
-module Hity : Hashtbl.S with type key = ity
+module Hity : XHashtbl.S with type key = ity
 module Wity : Weakhtbl.S with type key = ity
 
 module Sreg : Mreg.Set
-module Hreg : Hashtbl.S with type key = region
+module Hreg : XHashtbl.S with type key = region
 module Wreg : Weakhtbl.S with type key = region
 
 val its_equal : itysymbol -> itysymbol -> bool
@@ -269,7 +269,7 @@ type pvsymbol = private {
 
 module Mpv : Map.S with type key = pvsymbol
 module Spv : Mpv.Set
-module Hpv : Hashtbl.S with type key = pvsymbol
+module Hpv : XHashtbl.S with type key = pvsymbol
 module Wpv : Weakhtbl.S with type key = pvsymbol
 
 val pv_equal : pvsymbol -> pvsymbol -> bool