Commit b2f5865e authored by Andrei Paskevich's avatar Andrei Paskevich

move extended hash tables to Exthtbl

parent 68cfe57e
......@@ -108,7 +108,8 @@ LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_lexer.ml src/session/xml.ml
LIB_UTIL = config opt lists strings stdlib exn_printer pp debug loc print_tree \
LIB_UTIL = config opt lists strings exthtbl stdlib exn_printer pp debug \
loc print_tree \
cmdline weakhtbl hashcons util warning sysutil rc plugin
LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
......
......@@ -134,7 +134,11 @@ let load_prover_shortcut acc (_, section) =
(fp,shortcut)::acc
) acc shortcuts
module Hstr2 = Hashtbl.Make_Poly(struct type t = string * string end)
module Hstr2 = Hashtbl.Make(struct
type t = string * string
let hash = Hashtbl.hash
let equal = (=)
end)
type env =
{
......@@ -296,7 +300,7 @@ let add_prover_shortcuts env prover =
env.possible_prover_shortcuts <- aux env.possible_prover_shortcuts
let add_id_prover_shortcut env id prover priority =
match Hstr.find_option env.prover_shortcuts id with
match Hstr.find_opt env.prover_shortcuts id with
| Some (p,_) when p >= priority -> ()
| _ -> Hstr.replace env.prover_shortcuts id (priority,prover)
......
......@@ -101,7 +101,7 @@ val print_prover_parsable_format : Format.formatter -> prover -> unit
module Prover : Util.OrderedHash with type t = prover
module Mprover : Stdlib.Map.S with type key = prover
module Sprover : Mprover.Set
module Hprover : Hashtbl.S with type key = prover
module Hprover : Stdlib.Hashtbl.S with type key = prover
(** {3 Prover configuration} *)
......
......@@ -1871,6 +1871,10 @@ let merge_proof ~keygen obsolete to_goal _ from_proof =
exception MalformedMetas of ident_path
*)
exception Ts_not_found of tysymbol
exception Ls_not_found of lsymbol
exception Pr_not_found of prsymbol
(** ~theories is the current theory library path empty : [] *)
let rec merge_any_goal ~keygen ~theories env obsolete from_goal to_goal =
set_goal_expanded to_goal from_goal.goal_expanded;
......@@ -1993,11 +1997,14 @@ and merge_metas_aux ~keygen ~theories env to_goal _ from_metas =
(** Now convert the metas to the new symbol *)
let add_meta ((metas,task) as acc) meta_name meta_args =
let conv_ts ts = Hts.find_exn hts (Ts_not_found ts) ts in
let conv_ls ls = Hls.find_exn hls (Ls_not_found ls) ls in
let conv_pr pr = Hpr.find_exn hpr (Pr_not_found pr) pr in
let map = function
| MAty ty -> MAty (Ty.ty_s_map (Hts.find' hts) ty)
| MAts ts -> MAts (Hts.find' hts ts)
| MAls ls -> MAls (Hls.find' hls ls)
| MApr pr -> MApr (Hpr.find' hpr pr)
| MAty ty -> MAty (Ty.ty_s_map conv_ts ty)
| MAts ts -> MAts (conv_ts ts)
| MAls ls -> MAls (conv_ls ls)
| MApr pr -> MApr (conv_pr pr)
| (MAstr _ | MAint _) as m -> m
in
try
......@@ -2009,7 +2016,7 @@ and merge_metas_aux ~keygen ~theories env to_goal _ from_metas =
Smeta_args.add meta_args smeta_args,
Task.add_meta task meta meta_args
with
| Hts.Key_not_found ts ->
| Ts_not_found ts ->
obsolete := true;
let pos = Mts.find ts from_metas.metas_idpos.idpos_ts in
dprintf debug
......@@ -2018,7 +2025,7 @@ and merge_metas_aux ~keygen ~theories env to_goal _ from_metas =
print_meta (meta_name,meta_args)
print_ident_path pos;
acc
| Hls.Key_not_found ls ->
| Ls_not_found ls ->
obsolete := true;
let pos = Mls.find ls from_metas.metas_idpos.idpos_ls in
dprintf debug
......@@ -2027,7 +2034,7 @@ and merge_metas_aux ~keygen ~theories env to_goal _ from_metas =
print_meta (meta_name,meta_args)
print_ident_path pos;
acc
| Hpr.Key_not_found pr ->
| Pr_not_found pr ->
obsolete := true;
let pos = Mpr.find pr from_metas.metas_idpos.idpos_pr in
dprintf debug
......
......@@ -21,8 +21,8 @@ open Stdlib
val debug : Debug.flag
(** The debug flag "session" *)
module PHstr : Util.PrivateHashtbl with type key = string
module PHprover : Util.PrivateHashtbl with type key = Whyconf.prover
module PHstr : Hashtbl.Private with type key = string
module PHprover : Hashtbl.Private with type key = Whyconf.prover
(** {2 Proof attempts} *)
......
......@@ -69,7 +69,7 @@ let compute_diff t1 t2 =
Mid.fold_left (fun acc _ decl ->
if Hdecl.mem hdone decl then acc
else begin
Hdecl.set hdone decl;
Hdecl.replace hdone decl ();
match decl.d_node with
| Dtype ts -> remove_ts acc ts
| Ddata l -> List.fold_left (fun acc (ts,_) -> remove_ts acc ts) acc l
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2012 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
module type S =
sig
include Hashtbl.S
val find_def : 'a t -> 'a -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_exn : 'a t -> exn -> key -> 'a
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
val memo : int -> (key -> 'a) -> key -> 'a
val is_empty : 'a t -> bool
end
module type Private =
sig
type 'a t
type key
val find : 'a t -> key -> 'a
val find_def : 'a t -> 'a -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_exn : 'a t -> exn -> key -> 'a
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
val mem : 'a t -> key -> bool
val length : 'a t -> int
val is_empty : 'a t -> bool
end
module type Hashtbl =
sig
val hash : 'a -> int
module type S = S
module type Private = Private
module Make (X:Hashtbl.HashedType) : S with type key = X.t
end
module Hashtbl =
struct
let hash = Hashtbl.hash
module type S = S
module type Private = Private
module Make (X:Hashtbl.HashedType) : S with type key = X.t =
struct
module M = Hashtbl.Make(X)
include M
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
let find_def h d k =
try find h k with Not_found -> d
let find_exn h e k =
try find h k with Not_found -> raise e
let find_opt h k =
try Some (find h k) with Not_found -> None
let map f h =
let h' = create (length h) in
iter (fun k x -> add h' k (f k x)) h;
h'
let is_empty h = length h = 0
end
end
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2012 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
module type Hashtbl =
sig
val hash : 'a -> int
module type S =
sig
include Hashtbl.S
val find_def : 'a t -> 'a -> key -> 'a
(** return the first binding or the given value if none found *)
val find_opt : 'a t -> key -> 'a option
(** return the first binding or None if none found *)
val find_exn : 'a t -> exn -> key -> 'a
(** return the first binding or raise the given exception if none found *)
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
(** a shortcut less efficient than possible *)
val memo : int -> (key -> 'a) -> key -> 'a
(** convenience function, memoize a function *)
val is_empty : 'a t -> bool
(** test if the hashtbl is empty *)
end
module type Private =
sig
(** Private Hashtbl *)
type 'a t
type key
val find : 'a t -> key -> 'a
(** Same as {!Hashtbl.find} *)
val find_def : 'a t -> 'a -> key -> 'a
(** return the first binding or the given value if none found *)
val find_opt : 'a t -> key -> 'a option
(** return the first binding or None if none found *)
val find_exn : 'a t -> exn -> key -> 'a
(** return the first binding or raise the given exception if none found *)
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
(** a shortcut less efficient than possible *)
val iter : (key -> 'a -> unit) -> 'a t -> unit
(** Same as {!Hashtbl.iter} *)
val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
(** Same as {!Hashtbl.fold} *)
val mem : 'a t -> key -> bool
(** Same as {!Hashtbl.mem} *)
val length : 'a t -> int
(** Same as {!Hashtbl.length} *)
val is_empty : 'a t -> bool
(** test if the hashtbl is empty *)
end
module Make (X:Hashtbl.HashedType) : S with type key = X.t
end
module Hashtbl : Hashtbl
......@@ -762,55 +762,4 @@ 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
val map : ('a -> 'b) -> 'a t -> 'b t
val find_option : 'a t -> key -> 'a option
end
module Make (X:Hashtbl.HashedType) : S with type key = X.t = 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 ()
let map f h =
let h' = create (length h) in
iter (fun k x -> add h' k (f x)) h;
h'
let find_option h k =
try Some (find h k) with Not_found -> None
end
module Make_Poly (X : sig type t end) =
Make(struct type t = X.t
let hash = Hashtbl.hash
let equal = (=)
end)
end
module Hashtbl = Exthtbl.Hashtbl
......@@ -468,35 +468,4 @@ module Make (Ord : OrderedType) : S with type key = Ord.t
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 *)
val map : ('a -> 'b) -> 'a t -> 'b t
(** just a shortcut not as efficient as doable *)
val find_option : 'a t -> key -> 'a option
(** version of find without exception *)
end
module Make (X:Hashtbl.HashedType) : S with type key = X.t
module Make_Poly (X:sig type t end) : S with type key = X.t
end
module Hashtbl : Exthtbl.Hashtbl
......@@ -123,33 +123,3 @@ struct
module H = Hashtbl.Make(T)
module W = Weakhtbl.Make(X)
end
module type PrivateHashtbl = sig
(** Private Hashtbl *)
type 'a t
type key
val find : 'a t -> key -> 'a
(** Same as {Hashtbl.find} *)
val iter : (key -> 'a -> unit) -> 'a t -> unit
(** Same as {Hashtbl.iter} *)
val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
(** Same as {Hashtbl.fold} *)
val mem : 'a t -> key -> bool
(** Same as {Hashtbl.mem} *)
val length : 'a t -> int
(** Same as {Hashtbl.length} *)
end
module type PrivateArray = sig
(** Private Array *)
type 'a t
val get : 'a t -> int -> 'a
val iter : ('a -> unit) -> 'a t -> unit
(** Same as {!Array.iter} *)
val fold_left : ('acc -> 'a -> 'acc) -> 'acc -> 'a t -> 'acc
(** Same as {!Array.fold} *)
end
......@@ -91,33 +91,3 @@ sig
module H : Hashtbl.S with type key = X.t
module W : Weakhtbl.S with type key = X.t
end
module type PrivateHashtbl = sig
(** Private Hashtbl *)
type 'a t
type key
val find : 'a t -> key -> 'a
(** Same as {!Hashtbl.find} *)
val iter : (key -> 'a -> unit) -> 'a t -> unit
(** Same as {!Hashtbl.iter} *)
val fold : (key -> 'a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
(** Same as {!Hashtbl.fold} *)
val mem : 'a t -> key -> bool
(** Same as {!Hashtbl.mem} *)
val length : 'a t -> int
(** Same as {!Hashtbl.length} *)
end
module type PrivateArray = sig
(** Private Array *)
type 'a t
val get : 'a t -> int -> 'a
val iter : ('a -> unit) -> 'a t -> unit
(** Same as {!Array.iter} *)
val fold_left : ('acc -> 'a -> 'acc) -> 'acc -> 'a t -> 'acc
(** Same as {!Array.fold} *)
end
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