rename Hashweak to Weakhtbl

Makefile.in

@@ -109,7 +109,7 @@ LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
 	       src/driver/driver_lexer.ml src/session/xml.ml
 
 LIB_UTIL = config opt lists strings stdlib exn_printer pp debug loc print_tree \
-	   cmdline hashweak hashcons util warning sysutil rc plugin
+	   cmdline weakhtbl hashcons util warning sysutil rc plugin
 
 LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
 

src/core/decl.ml

@@ -298,7 +298,7 @@ type decl = {
   d_node : decl_node;
   d_syms : Sid.t;         (* idents used in declaration *)
   d_news : Sid.t;         (* idents introduced in declaration *)
-  d_tag  : Hashweak.tag;  (* unique magical tag *)
+  d_tag  : Weakhtbl.tag;  (* unique magical tag *)
 }
 
 and decl_node =
@@ -362,7 +362,7 @@ module Hsdecl = Hashcons.Make (struct
     | Dind (_,l) -> Hashcons.combine_list hs_ind 7 l
     | Dprop (k,pr,f) -> Hashcons.combine (hs_kind k) (hs_prop (pr,f))
 
-  let tag n d = { d with d_tag = Hashweak.create_tag n }
+  let tag n d = { d with d_tag = Weakhtbl.create_tag n }
 
 end)
 
@@ -378,7 +378,7 @@ module Hdecl = Decl.H
 
 let d_equal : decl -> decl -> bool = (==)
 
-let d_hash d = Hashweak.tag_hash d.d_tag
+let d_hash d = Weakhtbl.tag_hash d.d_tag
 
 (** Declaration constructors *)
 
@@ -386,7 +386,7 @@ let mk_decl node syms news = Hsdecl.hashcons {
   d_node = node;
   d_syms = syms;
   d_news = news;
-  d_tag  = Hashweak.dummy_tag;
+  d_tag  = Weakhtbl.dummy_tag;
 }
 
 exception IllegalTypeAlias of tysymbol

src/core/decl.mli

@@ -62,7 +62,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 Wpr : Hashweak.S with type key = prsymbol
+module Wpr : Weakhtbl.S with type key = prsymbol
 
 val create_prsymbol : preid -> prsymbol
 
@@ -92,7 +92,7 @@ type decl = private {
   d_node : decl_node;
   d_syms : Sid.t;         (* idents used in declaration *)
   d_news : Sid.t;         (* idents introduced in declaration *)
-  d_tag  : Hashweak.tag;  (* unique magical tag *)
+  d_tag  : Weakhtbl.tag;  (* unique magical tag *)
 }
 
 and decl_node =
@@ -105,7 +105,7 @@ and decl_node =
 
 module Mdecl : Map.S with type key = decl
 module Sdecl : Mdecl.Set
-module Wdecl : Hashweak.S with type key = decl
+module Wdecl : Weakhtbl.S with type key = decl
 module Hdecl : Hashtbl.S  with type key = decl
 
 val d_equal : decl -> decl -> bool

src/core/env.ml

@@ -31,18 +31,18 @@ exception AmbiguousPath of filename * filename
 
 type env = {
   env_path : Sstr.t;
-  env_tag  : Hashweak.tag;
+  env_tag  : Weakhtbl.tag;
 }
 
 let env_tag env = env.env_tag
 
-module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end)
+module Wenv = Weakhtbl.Make(struct type t = env let tag = env_tag end)
 
 (** Environment construction and utilisation *)
 
 let create_env = let c = ref (-1) in fun lp -> {
   env_path = List.fold_right Sstr.add lp Sstr.empty;
-  env_tag  = (incr c; Hashweak.create_tag !c)
+  env_tag  = (incr c; Weakhtbl.create_tag !c)
 }
 
 let get_loadpath env = Sstr.elements env.env_path

src/core/env.mli

@@ -30,9 +30,9 @@ exception TheoryNotFound of pathname * string
 
 type env
 
-val env_tag : env -> Hashweak.tag
+val env_tag : env -> Weakhtbl.tag
 
-module Wenv : Hashweak.S with type key = env
+module Wenv : Weakhtbl.S with type key = env
 
 val create_env : filename list -> env
 (** creates an environment from a "loadpath", a list of directories

src/core/ident.ml

@@ -49,7 +49,7 @@ type ident = {
   id_string : string;               (* non-unique name *)
   id_label  : Slab.t;               (* identifier labels *)
   id_loc    : Loc.position option;  (* optional location *)
-  id_tag    : Hashweak.tag;         (* unique magical tag *)
+  id_tag    : Weakhtbl.tag;         (* unique magical tag *)
 }
 
 module Id = WeakStructMake (struct
@@ -66,18 +66,18 @@ type preid = ident
 
 let id_equal : ident -> ident -> bool = (==)
 
-let id_hash id = Hashweak.tag_hash id.id_tag
+let id_hash id = Weakhtbl.tag_hash id.id_tag
 
 (* constructors *)
 
 let id_register = let r = ref 0 in fun id ->
-  { id with id_tag = (incr r; Hashweak.create_tag !r) }
+  { id with id_tag = (incr r; Weakhtbl.create_tag !r) }
 
 let create_ident name labels loc = {
   id_string = name;
   id_label  = labels;
   id_loc    = loc;
-  id_tag    = Hashweak.dummy_tag;
+  id_tag    = Weakhtbl.dummy_tag;
 }
 
 let id_fresh ?(label = Slab.empty) ?loc nm =

src/core/ident.mli

@@ -34,13 +34,13 @@ type ident = private {
   id_string : string;               (* non-unique name *)
   id_label  : Slab.t;               (* identifier labels *)
   id_loc    : Loc.position option;  (* optional location *)
-  id_tag    : Hashweak.tag;         (* unique magical tag *)
+  id_tag    : Weakhtbl.tag;         (* unique magical tag *)
 }
 
 module Mid : Map.S with type key = ident
 module Sid : Mid.Set
 module Hid : Hashtbl.S with type key = ident
-module Wid : Hashweak.S with type key = ident
+module Wid : Weakhtbl.S with type key = ident
 
 val id_equal : ident -> ident -> bool
 

src/core/task.ml

@@ -20,7 +20,7 @@ open Theory
 
 type tdecl_set = {
   tds_set : Stdecl.t;
-  tds_tag : Hashweak.tag;
+  tds_tag : Weakhtbl.tag;
 }
 
 module Hstds = Hashcons.Make (struct
@@ -28,12 +28,12 @@ module Hstds = Hashcons.Make (struct
   let equal s1 s2 = Stdecl.equal s1.tds_set s2.tds_set
   let hs_td td acc = Hashcons.combine acc (td_hash td)
   let hash s = Stdecl.fold hs_td s.tds_set 0
-  let tag n s = { s with tds_tag = Hashweak.create_tag n }
+  let tag n s = { s with tds_tag = Weakhtbl.create_tag n }
 end)
 
 let mk_tds s = Hstds.hashcons {
   tds_set = s;
-  tds_tag = Hashweak.dummy_tag;
+  tds_tag = Weakhtbl.dummy_tag;
 }
 
 let tds_empty = mk_tds Stdecl.empty
@@ -41,9 +41,9 @@ let tds_add td s = mk_tds (Stdecl.add td s.tds_set)
 let tds_singleton td = mk_tds (Stdecl.singleton td)
 
 let tds_equal : tdecl_set -> tdecl_set -> bool = (==)
-let tds_hash tds = Hashweak.tag_hash tds.tds_tag
+let tds_hash tds = Weakhtbl.tag_hash tds.tds_tag
 let tds_compare tds1 tds2 = compare
-  (Hashweak.tag_hash tds1.tds_tag) (Hashweak.tag_hash tds2.tds_tag)
+  (Weakhtbl.tag_hash tds1.tds_tag) (Weakhtbl.tag_hash tds2.tds_tag)
 
 type clone_map = tdecl_set Mid.t
 type meta_map = tdecl_set Mmeta.t
@@ -73,12 +73,12 @@ and task_hd = {
   task_known : known_map;    (* known identifiers *)
   task_clone : clone_map;    (* cloning history *)
   task_meta  : meta_map;     (* meta properties *)
-  task_tag   : Hashweak.tag; (* unique magical tag *)
+  task_tag   : Weakhtbl.tag; (* unique magical tag *)
 }
 
 let task_hd_equal : task_hd -> task_hd -> bool = (==)
 
-let task_hd_hash t = Hashweak.tag_hash t.task_tag
+let task_hd_hash t = Weakhtbl.tag_hash t.task_tag
 
 let task_equal t1 t2 = match t1, t2 with
   | Some t1, Some t2 -> task_hd_equal t1 t2
@@ -95,7 +95,7 @@ module Hstask = Hashcons.Make (struct
 
   let hash t = Hashcons.combine (td_hash t.task_decl) (task_hash t.task_prev)
 
-  let tag i task = { task with task_tag = Hashweak.create_tag i }
+  let tag i task = { task with task_tag = Weakhtbl.create_tag i }
 end)
 
 let mk_task decl prev known clone meta = Some (Hstask.hashcons {
@@ -104,7 +104,7 @@ let mk_task decl prev known clone meta = Some (Hstask.hashcons {
   task_known = known;
   task_clone = clone;
   task_meta  = meta;
-  task_tag   = Hashweak.dummy_tag;
+  task_tag   = Weakhtbl.dummy_tag;
 })
 
 let task_known = Opt.fold (fun _ t -> t.task_known) Mid.empty

src/core/task.mli

@@ -20,7 +20,7 @@ open Theory
 
 type tdecl_set = private {
   tds_set : Stdecl.t;
-  tds_tag : Hashweak.tag;
+  tds_tag : Weakhtbl.tag;
 }
 
 val tds_equal : tdecl_set -> tdecl_set -> bool
@@ -43,7 +43,7 @@ and task_hd = private {
   task_known : known_map;    (* known identifiers *)
   task_clone : clone_map;    (* cloning history *)
   task_meta  : meta_map;     (* meta properties *)
-  task_tag   : Hashweak.tag; (* unique magical tag *)
+  task_tag   : Weakhtbl.tag; (* unique magical tag *)
 }
 
 val task_equal : task -> task -> bool

src/core/term.mli

@@ -25,7 +25,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 Wvs : Hashweak.S with type key = vsymbol
+module Wvs : Weakhtbl.S with type key = vsymbol
 
 val vs_equal : vsymbol -> vsymbol -> bool
 val vs_hash : vsymbol -> int
@@ -43,7 +43,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 Wls : Hashweak.S with type key = lsymbol
+module Wls : Weakhtbl.S with type key = lsymbol
 
 val ls_equal : lsymbol -> lsymbol -> bool
 val ls_hash : lsymbol -> int

src/core/trans.ml

@@ -44,7 +44,7 @@ let compose_l f g x = Lists.apply g (f x)
 let seq l x = List.fold_left (|>) x l
 let seq_l l x = List.fold_left (fun x f -> Lists.apply f x) [x] l
 
-module Wtask = Hashweak.Make (struct
+module Wtask = Weakhtbl.Make (struct
   type t = task_hd
   let tag t = t.task_tag
 end)
@@ -139,7 +139,7 @@ let add_tdecls = gen_add_decl add_tdecl
 
 (** dependent transformations *)
 
-module Wtds = Hashweak.Make (struct
+module Wtds = Weakhtbl.Make (struct
   type t = tdecl_set
   let tag s = s.tds_tag
 end)
@@ -235,7 +235,7 @@ let print_meta f m task =
 
 open Env
 
-module Wenv = Hashweak.Make (struct
+module Wenv = Weakhtbl.Make (struct
   type t = env
   let tag = env_tag
 end)

src/core/ty.ml

@@ -43,7 +43,7 @@ type tysymbol = {
 
 and ty = {
   ty_node : ty_node;
-  ty_tag  : Hashweak.tag;
+  ty_tag  : Weakhtbl.tag;
 }
 
 and ty_node =
@@ -64,7 +64,7 @@ let ts_equal : tysymbol -> tysymbol -> bool = (==)
 let ty_equal : ty       -> ty       -> bool = (==)
 
 let ts_hash ts = id_hash ts.ts_name
-let ty_hash ty = Hashweak.tag_hash ty.ty_tag
+let ty_hash ty = Weakhtbl.tag_hash ty.ty_tag
 
 let mk_ts name args def = {
   ts_name = id_register name;
@@ -85,7 +85,7 @@ module Hsty = Hashcons.Make (struct
     | Tyvar v -> tv_hash v
     | Tyapp (s,tl) -> Hashcons.combine_list ty_hash (ts_hash s) tl
 
-  let tag n ty = { ty with ty_tag = Hashweak.create_tag n }
+  let tag n ty = { ty with ty_tag = Weakhtbl.create_tag n }
 end)
 
 module Ty = WeakStructMake (struct
@@ -100,7 +100,7 @@ module Wty = Ty.W
 
 let mk_ty n = {
   ty_node = n;
-  ty_tag  = Hashweak.dummy_tag;
+  ty_tag  = Weakhtbl.dummy_tag;
 }
 
 let ty_var n = Hsty.hashcons (mk_ty (Tyvar n))

src/core/ty.mli

@@ -38,7 +38,7 @@ type tysymbol = private {
 
 and ty = private {
   ty_node : ty_node;
-  ty_tag  : Hashweak.tag;
+  ty_tag  : Weakhtbl.tag;
 }
 
 and ty_node = private
@@ -48,12 +48,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 Wts : Hashweak.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 Wty : Hashweak.S with type key = ty
+module Wty : Weakhtbl.S with type key = ty
 
 val ts_equal : tysymbol -> tysymbol -> bool
 val ty_equal : ty -> ty -> bool

src/util/util.ml

@@ -109,19 +109,19 @@ struct
   module H = Hashtbl.Make(T)
 end
 
-module MakeTagged (X : Hashweak.Weakey) =
+module MakeTagged (X : Weakhtbl.Weakey) =
 struct
   type t = X.t
-  let tag t = Hashweak.tag_hash (X.tag t)
+  let tag t = Weakhtbl.tag_hash (X.tag t)
 end
 
-module WeakStructMake (X : Hashweak.Weakey) =
+module WeakStructMake (X : Weakhtbl.Weakey) =
 struct
   module T = OrderedHash(MakeTagged(X))
   module M = Map.Make(T)
   module S = M.Set
   module H = Hashtbl.Make(T)
-  module W = Hashweak.Make(X)
+  module W = Weakhtbl.Make(X)
 end
 
 module type PrivateHashtbl = sig

src/util/util.mli

@@ -84,12 +84,12 @@ sig
   module H : Hashtbl.S with type key = X.t
 end
 
-module WeakStructMake (X : Hashweak.Weakey) :
+module WeakStructMake (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 W : Hashweak.S with type key = X.t
+  module W : Weakhtbl.S with type key = X.t
 end
 
 module type PrivateHashtbl = sig

src/whyml/mlw_expr.mli

@@ -102,7 +102,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 Wps : Hashweak.S with type key = psymbol
+module Wps : Weakhtbl.S with type key = psymbol
 
 val ps_equal : psymbol -> psymbol -> bool
 

src/whyml/mlw_ty.ml

@@ -39,7 +39,7 @@ module rec T : sig
   and ity = {
     ity_node : ity_node;
     ity_vars : varset;
-    ity_tag  : Hashweak.tag;
+    ity_tag  : Weakhtbl.tag;
   }
 
   and ity_node =
@@ -74,7 +74,7 @@ end = struct
   and ity = {
     ity_node : ity_node;
     ity_vars : varset;
-    ity_tag  : Hashweak.tag;
+    ity_tag  : Weakhtbl.tag;
   }
 
   and ity_node =
@@ -93,7 +93,7 @@ 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 W : Hashweak.S with type key = T.region
+  module W : Weakhtbl.S with type key = T.region
 end = WeakStructMake (struct
   type t = T.region
   let tag r = r.T.reg_name.id_tag
@@ -145,7 +145,7 @@ let its_equal : itysymbol -> itysymbol -> bool = (==)
 let ity_equal : ity       -> ity       -> bool = (==)
 
 let its_hash its = id_hash its.its_pure.ts_name
-let ity_hash ity = Hashweak.tag_hash ity.ity_tag
+let ity_hash ity = Weakhtbl.tag_hash ity.ity_tag
 
 module Hsity = Hashcons.Make (struct
   type t = ity
@@ -181,7 +181,7 @@ module Hsity = Hashcons.Make (struct
 
   let tag n ity = { ity with
     ity_vars = vars vars_empty ity;
-    ity_tag  = Hashweak.create_tag n }
+    ity_tag  = Weakhtbl.create_tag n }
 
 end)
 
@@ -198,7 +198,7 @@ module Wity = Ity.W
 let mk_ity n = {
   ity_node = n;
   ity_vars = vars_empty;
-  ity_tag  = Hashweak.dummy_tag;
+  ity_tag  = Weakhtbl.dummy_tag;
 }
 
 let ity_var n = Hsity.hashcons (mk_ity (Ityvar n))
@@ -536,7 +536,7 @@ let create_xsymbol id ity =
 
 module Exn = StructMake (struct
   type t = xsymbol
-  let tag xs = Hashweak.tag_hash xs.xs_name.id_tag
+  let tag xs = Weakhtbl.tag_hash xs.xs_name.id_tag
 end)
 
 module Sexn = Exn.S

src/whyml/mlw_ty.mli

@@ -38,7 +38,7 @@ module rec T : sig
   and ity = private {
     ity_node : ity_node;
     ity_vars : varset;
-    ity_tag  : Hashweak.tag;
+    ity_tag  : Weakhtbl.tag;
   }
 
   and ity_node = private
@@ -59,16 +59,16 @@ open T
 module Mits : Map.S with type key = itysymbol
 module Sits : Mits.Set
 module Hits : Hashtbl.S with type key = itysymbol
-module Wits : Hashweak.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 Wity : Hashweak.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 Wreg : Hashweak.S with type key = region
+module Wreg : Weakhtbl.S with type key = region
 
 val its_equal : itysymbol -> itysymbol -> bool
 val ity_equal : ity -> ity -> bool
@@ -270,7 +270,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 Wpv : Hashweak.S with type key = pvsymbol
+module Wpv : Weakhtbl.S with type key = pvsymbol
 
 val pv_equal : pvsymbol -> pvsymbol -> bool