Commit 068ddc7b authored by François Bobot's avatar François Bobot

stdlib: remove polymorphic hashtbl

   - add functions to Hashtbl.S
   - without ocaml 3.12 its not possible to do that for Hashtbl without
     copying the signature
   - "open Stdlib" hides the polymorphic hashtbl, perhaps a good idea
     since that avoid errors.
parent c30a45ad
......@@ -26,7 +26,7 @@ open Util
module BenchUtil = Bench.BenchUtil
let load_driver = Env.Wenv.memoize 2 (fun env ->
memo_string 10 (Driver.load_driver env))
Hstr.memo 10 (Driver.load_driver env))
let debug = Debug.register_info_flag "benchdb"
~desc:"About the communication from the database"
......
......@@ -384,6 +384,7 @@ end)
module Sdecl = Decl.S
module Mdecl = Decl.M
module Wdecl = Decl.W
module Hdecl = Decl.H
let d_equal : decl -> decl -> bool = (==)
......
......@@ -115,6 +115,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 Hdecl : Hashtbl.S with type key = decl
val d_equal : decl -> decl -> bool
val d_hash : decl -> int
......
......@@ -108,7 +108,7 @@ let preid_name id = id.id_string
(** Unique names for pretty printing *)
type ident_printer = {
indices : (string, int) Hashtbl.t;
indices : int Hstr.t;
values : string Hid.t;
sanitizer : string -> string;
blacklist : string list;
......@@ -116,7 +116,7 @@ type ident_printer = {
let find_unique indices name =
let specname ind = name ^ string_of_int ind in
let testname ind = Hashtbl.mem indices (specname ind) in
let testname ind = Hstr.mem indices (specname ind) in
let rec advance ind =
if testname ind then advance (succ ind) else ind in
let rec retreat ind =
......@@ -124,11 +124,11 @@ let find_unique indices name =
let fetch ind =
if testname ind then advance (succ ind) else retreat ind in
let name = try
let ind = fetch (succ (Hashtbl.find indices name)) in
Hashtbl.replace indices name ind;
let ind = fetch (succ (Hstr.find indices name)) in
Hstr.replace indices name ind;
specname ind
with Not_found -> name in
Hashtbl.replace indices name 0;
Hstr.replace indices name 0;
name
let reserve indices name = ignore (find_unique indices name)
......@@ -136,7 +136,7 @@ let reserve indices name = ignore (find_unique indices name)
let same x = x
let create_ident_printer ?(sanitizer = same) sl =
let indices = Hashtbl.create 1997 in
let indices = Hstr.create 1997 in
List.iter (reserve indices) sl;
{ indices = indices;
values = Hid.create 1997;
......@@ -157,13 +157,13 @@ let string_unique printer s = find_unique printer.indices s
let forget_id printer id =
try
let name = Hid.find printer.values id in
Hashtbl.remove printer.indices name;
Hstr.remove printer.indices name;
Hid.remove printer.values id
with Not_found -> ()
let forget_all printer =
Hid.clear printer.values;
Hashtbl.clear printer.indices;
Hstr.clear printer.indices;
List.iter (reserve printer.indices) printer.blacklist
(** Sanitizers *)
......
......@@ -21,6 +21,7 @@
open Util
open Ident
open Ty
open Stdlib
(** Variable symbols *)
......@@ -812,7 +813,7 @@ let t_bool_false = fs_app fs_bool_false [] ty_bool
let fs_tuple_ids = Hid.create 17
let fs_tuple = Util.memo_int 17 (fun n ->
let fs_tuple = Util.Hint.memo 17 (fun n ->
let ts = ts_tuple n in
let tl = List.map ty_var ts.ts_args in
let ty = ty_app ts tl in
......
......@@ -797,7 +797,7 @@ let highord_theory =
let uc = add_param_decl uc ps_pred_app in
close_theory uc
let tuple_theory = Util.memo_int 17 (fun n ->
let tuple_theory = Util.Hint.memo 17 (fun n ->
let ts = ts_tuple n and fs = fs_tuple n in
let pl = List.map (fun _ -> None) ts.ts_args in
let uc = empty_theory (id_fresh ("Tuple" ^ string_of_int n)) [] in
......
......@@ -299,43 +299,43 @@ let mk_reg_trans ?(desc_labels=[]) ?(desc_metas=[]) ~desc f =
reg_desc = desc}
let transforms : (string, task reg_trans) Hashtbl.t = Hashtbl.create 17
let transforms_l : (string, task list reg_trans) Hashtbl.t = Hashtbl.create 17
let transforms : (task reg_trans) Hstr.t = Hstr.create 17
let transforms_l : (task list reg_trans) Hstr.t = Hstr.create 17
let register_transform ?desc_labels ?desc_metas ~desc s p =
if Hashtbl.mem transforms s then raise (KnownTrans s);
Hashtbl.replace transforms s
if Hstr.mem transforms s then raise (KnownTrans s);
Hstr.replace transforms s
(mk_reg_trans ?desc_labels ?desc_metas ~desc (fun _ -> named s p))
let register_transform_l ?desc_labels ?desc_metas ~desc s p =
if Hashtbl.mem transforms_l s then raise (KnownTrans s);
Hashtbl.replace transforms_l s
if Hstr.mem transforms_l s then raise (KnownTrans s);
Hstr.replace transforms_l s
(mk_reg_trans ?desc_labels ?desc_metas ~desc (fun _ -> named s p))
let register_env_transform ?desc_labels ?desc_metas ~desc s p =
if Hashtbl.mem transforms s then raise (KnownTrans s);
Hashtbl.replace transforms s
if Hstr.mem transforms s then raise (KnownTrans s);
Hstr.replace transforms s
(mk_reg_trans ?desc_labels ?desc_metas ~desc
(Wenv.memoize 3 (fun e -> named s (p e))))
let register_env_transform_l ?desc_labels ?desc_metas ~desc s p =
if Hashtbl.mem transforms_l s then raise (KnownTrans s);
Hashtbl.replace transforms_l s
if Hstr.mem transforms_l s then raise (KnownTrans s);
Hstr.replace transforms_l s
(mk_reg_trans ?desc_labels ?desc_metas ~desc
(Wenv.memoize 3 (fun e -> named s (p e))))
let lookup_transform s =
try fst (Hashtbl.find transforms s)
try fst (Hstr.find transforms s)
with Not_found -> raise (UnknownTrans s)
let lookup_transform_l s =
try fst (Hashtbl.find transforms_l s)
try fst (Hstr.find transforms_l s)
with Not_found -> raise (UnknownTrans s)
let list_transforms () = Hashtbl.fold (fun k r acc ->
let list_transforms () = Hstr.fold (fun k r acc ->
(k,snd r)::acc) transforms []
let list_transforms_l () = Hashtbl.fold
let list_transforms_l () = Hstr.fold
(fun k r acc -> (k,snd r)::acc) transforms_l []
(** fast transform *)
......@@ -361,7 +361,7 @@ let apply_transform tr_name env task =
exception UnknownFlagTrans of meta * string * string list
exception IllegalFlagTrans of meta
type ('a,'b) flag_trans = (string, 'a -> 'b trans) Hashtbl.t
type ('a,'b) flag_trans = ('a -> 'b trans) Hstr.t
let on_flag m ft def arg =
on_meta_excl m (fun alo ->
......@@ -370,9 +370,9 @@ let on_flag m ft def arg =
| Some [MAstr s] -> s
| _ -> raise (IllegalFlagTrans m)
in
let t = try Hashtbl.find ft s with
let t = try Hstr.find ft s with
| Not_found ->
let l = Hashtbl.fold (fun s _ l -> s :: l) ft [] in
let l = Hstr.fold (fun s _ l -> s :: l) ft [] in
raise (UnknownFlagTrans (m,s,l))
in
let tr_name = Printf.sprintf "%s : %s" m.meta_name s in
......
......@@ -23,6 +23,7 @@ open Term
open Decl
open Theory
open Task
open Util
(** Task transformation *)
......@@ -90,7 +91,7 @@ val on_tagged_pr : meta -> (Spr.t -> 'a trans) -> 'a trans
exception UnknownFlagTrans of meta * string * string list
exception IllegalFlagTrans of meta
type ('a,'b) flag_trans = (string, 'a -> 'b trans) Hashtbl.t
type ('a,'b) flag_trans = ('a -> 'b trans) Hstr.t
val on_flag : meta -> ('a,'b) flag_trans -> string -> 'a -> 'b trans
(** [on_flag m ft def arg] takes an exclusive meta [m] of type [[MTstring]],
......
......@@ -240,7 +240,7 @@ let ty_pred ty_a = ty_app ts_pred [ty_a]
let ts_tuple_ids = Hid.create 17
let ts_tuple = Util.memo_int 17 (fun n ->
let ts_tuple = Util.Hint.memo 17 (fun n ->
let vl = ref [] in
for i = 1 to n do vl := create_tvsymbol (id_fresh "a") :: !vl done;
let ts = create_tysymbol (id_fresh ("tuple" ^ string_of_int n)) !vl None in
......
......@@ -226,13 +226,13 @@ let map env d = match d.d_node with
let ft_select_inst =
((Hashtbl.create 17) : (Env.env,Sty.t) Trans.flag_trans)
((Hstr.create 17) : (Env.env,Sty.t) Trans.flag_trans)
let ft_select_lskept =
((Hashtbl.create 17) : (Env.env,Sls.t) Trans.flag_trans)
((Hstr.create 17) : (Env.env,Sls.t) Trans.flag_trans)
let ft_select_lsinst =
((Hashtbl.create 17) : (Env.env,Lsmap.t) Trans.flag_trans)
((Hstr.create 17) : (Env.env,Lsmap.t) Trans.flag_trans)
let metas_from_env env =
let fold_inst tyl _ s = List.fold_left (fun s ty -> Sty.add ty s) s tyl in
let fold_ls _ insts s = Mtyl.fold fold_inst insts s in
......
......@@ -66,9 +66,9 @@ let def_enco_select_tptp = "none"
let def_enco_kept_tptp = "twin"
let def_enco_poly_tptp = "decorate"
let ft_select_kept = ((Hashtbl.create 17) : (Env.env,Sty.t) Trans.flag_trans)
let ft_enco_kept = ((Hashtbl.create 17) : (Env.env,task) Trans.flag_trans)
let ft_enco_poly = ((Hashtbl.create 17) : (Env.env,task) Trans.flag_trans)
let ft_select_kept = ((Hstr.create 17) : (Env.env,Sty.t) Trans.flag_trans)
let ft_enco_kept = ((Hstr.create 17) : (Env.env,task) Trans.flag_trans)
let ft_enco_poly = ((Hstr.create 17) : (Env.env,task) Trans.flag_trans)
let select_kept def env =
let select = Trans.on_flag meta_select_kept ft_select_kept def env in
......
......@@ -172,5 +172,5 @@ let mono kept =
let t = Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.compose (deco kept) (mono kept))
let () = Hashtbl.replace Encoding.ft_enco_poly "decoexp" (const t)
let () = Hstr.replace Encoding.ft_enco_poly "decoexp" (const t)
......@@ -119,5 +119,5 @@ let mono kept =
let t = Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.compose (deco kept) (mono kept))
let () = Hashtbl.replace Encoding.ft_enco_poly "decorate" (const t)
let () = Hstr.replace Encoding.ft_enco_poly "decorate" (const t)
......@@ -265,5 +265,5 @@ let monomorph = Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
let decl = d_monomorph kept (lsmap kept) in
Trans.decl decl (Task.add_decl None d_ts_base))
let () = Hashtbl.replace Encoding.ft_enco_poly "guard"
let () = Hstr.replace Encoding.ft_enco_poly "guard"
(fun _ -> Trans.compose guard monomorph)
......@@ -525,10 +525,10 @@ let encoding_instantiate complete =
(Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
create_trans_complete kept complete))
let () = Hashtbl.replace Encoding.ft_enco_kept "instantiate"
let () = Hstr.replace Encoding.ft_enco_kept "instantiate"
(const (encoding_instantiate Incomplete))
let () = Hashtbl.replace Encoding.ft_enco_kept "instantiate_complete"
let () = Hstr.replace Encoding.ft_enco_kept "instantiate_complete"
(const (encoding_instantiate Complete))
(*
......
......@@ -29,7 +29,7 @@ open Task
open Encoding
open Discriminate
let register pr l = List.iter (fun (n,f) -> Hashtbl.replace pr n (const f)) l
let register pr l = List.iter (fun (n,f) -> Hstr.replace pr n (const f)) l
let register pr none goal all =
register pr ["none",none; "goal",goal; "all",all]
......
......@@ -124,4 +124,4 @@ let decl tenv d =
let t = Trans.on_tagged_ty Libencoding.meta_kept (fun s ->
Trans.decl (decl (Mty.mapi make_pont s)) None)
let () = Hashtbl.replace Encoding.ft_enco_kept "twin" (const t)
let () = Hstr.replace Encoding.ft_enco_kept "twin" (const t)
......@@ -739,3 +739,39 @@ module Make(Ord: OrderedType) = struct
end
end
module Hashtbl = struct
let hash = Hashtbl.hash
module type S = sig
include Hashtbl.S
val is_empty : 'a t -> bool
val memo : int -> (key -> 'a) -> key -> 'a
exception Key_not_found of key
val find' : 'a t -> key -> 'a
val set : unit t -> key -> unit
end
module Make (X:Hashtbl.HashedType) = struct
module M = Hashtbl.Make(X)
include M
let is_empty h =
try
M.iter (fun _ _ -> raise Exit) h;
true
with Exit -> false
let memo size f =
let h = create size in
fun x -> try find h x
with Not_found -> let y = f x in add h x y; y
exception Key_not_found of key
let find' h k =
try find h k with Not_found -> raise (Key_not_found k)
let set h k = replace h k ()
end
end
......@@ -452,3 +452,28 @@ module Make (Ord : OrderedType) : S with type key = Ord.t
given a totally ordered type. *)
end
module Hashtbl : sig
val hash : 'a -> int
module type S = sig
include Hashtbl.S
val is_empty : 'a t -> bool
(** test if the hashtbl is empty *)
val memo : int -> (key -> 'a) -> key -> 'a
(** convenience function, memoize a function *)
exception Key_not_found of key
val find' : 'a t -> key -> 'a
(** return the first binding or raise Key_not_found with the given
key as argument *)
(** hashtbl used as hashset *)
val set : unit t -> key -> unit
(** Add a binding that can be tested by mem *)
end
module Make (X:Hashtbl.HashedType) : S with type key = X.t
end
......@@ -234,12 +234,23 @@ let is_uppercase c = 'A' <= c && c <= 'Z'
let concat_non_empty sep l =
String.concat sep (List.filter (fun s -> s <> "") l)
(** useful function on char *)
let count n =
let r = ref (n-1) in
fun _ -> incr r; !r
(* Set and Map on ints and strings *)
module Int = struct type t = int let compare = Pervasives.compare end
module Int = struct
type t = int
let compare = Pervasives.compare
let equal x y = x = y
let hash x = x
end
module Mint = Map.Make(Int)
module Sint = Mint.Set
module Hint = Hashtbl.Make(Int)
module Mstr = Map.Make(String)
module Sstr = Mstr.Set
......@@ -308,15 +319,6 @@ struct
module W = Hashweak.Make(X)
end
(* memoization *)
let memo_int size f =
let h = Hashtbl.create size in
fun x -> try Hashtbl.find h x
with Not_found -> let y = f x in Hashtbl.add h x y; y
let memo_string = memo_int
module type PrivateHashtbl = sig
(** Private Hashtbl *)
type 'a t
......
......@@ -160,18 +160,20 @@ val concat_non_empty : string -> string list -> string
(* useful function on char *)
val is_uppercase : char -> bool
(* useful function on int *)
val count : int -> ('a -> int)
(** return the consecutie number from the first given *)
(* Set and Map 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 Mstr : Map.S with type key = string
module Sstr : Mstr.Set
module Hstr : Hashtbl.S with type key = string
val memo_int : int -> (int -> 'a) -> int -> 'a
val memo_string : int -> (string -> 'a) -> string -> 'a
(* Set, Map, Hashtbl on structures with a unique tag *)
module type Tagged =
......@@ -212,14 +214,14 @@ module type PrivateHashtbl = sig
type key
val find : 'a t -> key -> 'a
(** Same as {Hashtbl.find} *)
(** Same as {!Hashtbl.find} *)
val iter : (key -> 'a -> unit) -> 'a t -> unit
(** Same as {Hashtbl.iter} *)
(** Same as {!Hashtbl.iter} *)
val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
(** Same as {Hashtbl.fold} *)
(** Same as {!Hashtbl.fold} *)
val mem : 'a t -> key -> bool
(** Same as {Hashtbl.mem} *)
(** Same as {!Hashtbl.mem} *)
val length : 'a t -> int
(** Same as {Hashtbl.length} *)
(** Same as {!Hashtbl.length} *)
end
......@@ -238,16 +238,16 @@ type pre_ppattern =
| PPas of pre_ppattern * preid
let make_ppattern pp vtv =
let hv = Hashtbl.create 3 in
let hv = Hstr.create 3 in
let find id vtv =
let nm = preid_name id in
try
let pv = Hashtbl.find hv nm in
let pv = Hstr.find hv nm in
ity_equal_check vtv.vtv_ity pv.pv_vtv.vtv_ity;
pv
with Not_found ->
let pv = create_pvsymbol id vtv in
Hashtbl.add hv nm pv; pv
Hstr.add hv nm pv; pv
in
let rec make vtv = function
| PPwild -> {
......@@ -311,7 +311,7 @@ let make_ppattern pp vtv =
ppat_effect = pp.ppat_effect; }
in
let pp = make (vtv_unmut vtv) pp in
Hashtbl.fold Mstr.add hv Mstr.empty, pp
Hstr.fold Mstr.add hv Mstr.empty, pp
(** program symbols *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment