diff options
-rw-r--r-- | interp/notation.ml | 15 | ||||
-rw-r--r-- | kernel/cooking.ml | 27 | ||||
-rw-r--r-- | kernel/names.mli | 2 | ||||
-rw-r--r-- | kernel/nativecode.ml | 63 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 17 | ||||
-rw-r--r-- | kernel/nativevalues.ml | 2 | ||||
-rw-r--r-- | kernel/vm.ml | 19 | ||||
-rw-r--r-- | lib/option.ml | 4 | ||||
-rw-r--r-- | lib/option.mli | 3 |
9 files changed, 118 insertions, 34 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 262cbab2f..6e5ac5f33 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -254,7 +254,8 @@ let keymap_find key map = (* Scopes table : interpretation -> scope_name *) let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) -let prim_token_key_table = Hashtbl.create 7 + +let prim_token_key_table = ref KeyMap.empty let glob_prim_constr_key = function | GApp (_,GRef (_,ref),_) | GRef (_,ref) -> RefKey (canonical_gr ref) @@ -309,8 +310,8 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) = declare_scope sc; add_prim_token_interpreter sc interp; List.iter (fun pat -> - Hashtbl.add prim_token_key_table - (glob_prim_constr_key pat) (sc,uninterp,b)) + prim_token_key_table := KeyMap.add + (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) patl let mkNumeral n = Numeral n @@ -487,7 +488,7 @@ let availability_of_notation (ntn_scope,ntn) scopes = let uninterp_prim_token c = try let (sc,numpr,_) = - Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in + KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in match numpr c with | None -> raise Notation_ops.No_match | Some n -> (sc,n) @@ -496,8 +497,8 @@ let uninterp_prim_token c = let uninterp_prim_token_ind_pattern ind args = let ref = IndRef ind in try - let (sc,numpr,b) = Hashtbl.find prim_token_key_table - (RefKey (canonical_gr ref)) in + let k = RefKey (canonical_gr ref) in + let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in if not b then raise Notation_ops.No_match; let args' = List.map (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in @@ -510,7 +511,7 @@ let uninterp_prim_token_ind_pattern ind args = let uninterp_prim_token_cases_pattern c = try let k = cases_pattern_key c in - let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in + let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in if not b then raise Notation_ops.No_match; let na,c = glob_constr_of_closed_cases_pattern c in match numpr c with diff --git a/kernel/cooking.ml b/kernel/cooking.ml index f81bcceb3..f8724180e 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -40,8 +40,25 @@ type my_global_reference = | IndRef of inductive | ConstructRef of constructor +module RefHash = +struct + type t = my_global_reference + let equal gr1 gr2 = match gr1, gr2 with + | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2 + | IndRef i1, IndRef i2 -> eq_ind i1 i2 + | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2 + | _ -> false + open Hashset.Combine + let hash = function + | ConstRef c -> combinesmall 1 (Constant.hash c) + | IndRef i -> combinesmall 2 (ind_hash i) + | ConstructRef c -> combinesmall 3 (constructor_hash c) +end + +module RefTable = Hashtbl.Make(RefHash) + let share cache r (cstl,knl) = - try Hashtbl.find cache r + try RefTable.find cache r with Not_found -> let f,l = match r with @@ -52,7 +69,7 @@ let share cache r (cstl,knl) = | ConstRef cst -> mkConst (pop_con cst), Cmap.find cst cstl in let c = mkApp (f, Array.map mkVar l) in - Hashtbl.add cache r c; + RefTable.add cache r c; c let update_case_info cache ci modlist = @@ -129,12 +146,12 @@ let constr_of_def = function | OpaqueDef lc -> Opaqueproof.force_proof lc let cook_constr { Opaqueproof.modlist ; abstract } c = - let cache = Hashtbl.create 13 in + let cache = RefTable.create 13 in let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in abstract_constant_body (expmod_constr cache modlist c) hyps let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = - let cache = Hashtbl.create 13 in + let cache = RefTable.create 13 in let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in let body = on_body modlist hyps (fun c -> abstract_constant_body (expmod_constr cache modlist c) hyps) @@ -158,4 +175,4 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = in (body, typ, cb.const_constraints, cb.const_inline_code, Some const_hyps) -let expmod_constr modlist c = expmod_constr (Hashtbl.create 13) modlist c +let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c diff --git a/kernel/names.mli b/kernel/names.mli index 816467721..56b812fd0 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -371,6 +371,8 @@ sig val equal : t -> t -> bool (** Default comparison, alias for [CanOrd.equal] *) + val hash : t -> int + (** Displaying *) val to_string : t -> string diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 3be56b189..5fa0d41e0 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -80,6 +80,21 @@ let eq_gname gn1 gn2 = | Gnamed id1, Gnamed id2 -> Id.equal id1 id2 | _ -> false +open Hashset.Combine + +let gname_hash gn = match gn with +| Gind (s, i) -> combinesmall 1 (combine (String.hash s) (ind_hash i)) +| Gconstruct (s, c) -> combinesmall 2 (combine (String.hash s) (constructor_hash c)) +| Gconstant (s, c) -> combinesmall 3 (combine (String.hash s) (Constant.hash c)) +| Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i)) +| Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i)) +| Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i)) +| Gnorm (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i)) +| Gnormtbl (l, i) -> combinesmall 8 (combine (Option.hash Label.hash l) (Int.hash i)) +| Ginternal s -> combinesmall 9 (String.hash s) +| Grel i -> combinesmall 10 (Int.hash i) +| Gnamed id -> combinesmall 11 (Id.hash id) + let case_ctr = ref (-1) let reset_gcase () = case_ctr := -1 @@ -148,11 +163,9 @@ let eq_symbol sy1 sy2 = Evar.equal evk1 evk2 && Array.for_all2 eq_constr args1 args2 | _, _ -> false -open Hashset.Combine - let hash_symbol symb = match symb with - | SymbValue v -> combinesmall 1 (Hashtbl.hash v) + | SymbValue v -> combinesmall 1 (Hashtbl.hash v) (** FIXME *) | SymbSort s -> combinesmall 2 (Sorts.hash s) | SymbName name -> combinesmall 3 (Name.hash name) | SymbConst c -> combinesmall 4 (Constant.hash c) @@ -266,6 +279,28 @@ let eq_primitive p1 p2 = | Mk_evar, Mk_evar -> true | _ -> false +let primitive_hash = function +| Mk_prod -> 1 +| Mk_sort -> 2 +| Mk_ind -> 3 +| Mk_const -> 4 +| Mk_sw -> 5 +| Mk_fix (r, i) -> + let h = Array.fold_left (fun h i -> combine h (Int.hash i)) 0 r in + combinesmall 6 (combine h (Int.hash i)) +| Mk_cofix i -> + combinesmall 7 (Int.hash i) +| Mk_rel i -> + combinesmall 8 (Int.hash i) +| Mk_var id -> + combinesmall 9 (Id.hash id) +| Is_accu -> 10 +| Cast_accu -> 11 +| Upd_cofix -> 12 +| Force_cofix -> 13 +| Mk_meta -> 14 +| Mk_evar -> 15 + type mllambda = | MLlocal of lname | MLglobal of gname @@ -373,8 +408,8 @@ and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 = let rec hash_mllambda gn n env t = match t with | MLlocal ln -> combinesmall 1 (LNmap.find ln env) - | MLglobal gn' -> combinesmall 2 (if eq_gname gn gn' then 0 else Hashtbl.hash gn') - | MLprimitive prim -> combinesmall 3 (Hashtbl.hash prim) + | MLglobal gn' -> combinesmall 2 (if eq_gname gn gn' then 0 else gname_hash gn') + | MLprimitive prim -> combinesmall 3 (primitive_hash prim) | MLlam (lns, ml) -> let env = push_lnames n env lns in combinesmall 4 (combine (Array.length lns) (hash_mllambda gn (n+1) env ml)) @@ -397,18 +432,18 @@ let rec hash_mllambda gn n env t = let hbr' = hash_mllambda gn n env br' in combinesmall 8 (combine3 hcond hbr hbr') | MLmatch (annot, c, accu, br) -> - let hannot = Hashtbl.hash annot in + let hannot = hash_annot_sw annot in let hc = hash_mllambda gn n env c in let haccu = hash_mllambda gn n env accu in combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br) | MLconstruct (pf, cs, args) -> - let hpf = Hashtbl.hash pf in - let hcs = Hashtbl.hash cs in + let hpf = String.hash pf in + let hcs = constructor_hash cs in combinesmall 10 (hash_mllambda_array gn n env (combine hpf hcs) args) | MLint (ty,v) -> - combinesmall 11 (combine (Hashtbl.hash ty) v) + combinesmall 11 (combine (if ty then 0 else 1) v) | MLsetref (id, ml) -> - let hid = Hashtbl.hash id in + let hid = String.hash id in let hml = hash_mllambda gn n env ml in combinesmall 12 (combine hid hml) | MLsequence (ml, ml') -> @@ -430,7 +465,7 @@ and hash_mllambda_array gn n env init arr = and hash_mllam_branches gn n env init br = let hash_cargs (cs, args) body = let nargs = Array.length args in - let hcs = Hashtbl.hash cs in + let hcs = constructor_hash cs in let env = opush_lnames n env args in let hbody = hash_mllambda gn (n + nargs) env body in combine3 nargs hcs hbody @@ -564,10 +599,10 @@ let hash_global g = let env = push_lnames 0 LNmap.empty lns in let t = MLmatch (annot,c,accu,br) in combinesmall 4 (combine nlns (hash_mllambda gn nlns env t)) - | Gopen s -> combinesmall 5 (Hashtbl.hash s) + | Gopen s -> combinesmall 5 (String.hash s) | Gtype (ind, arr) -> - combinesmall 6 (combine (Hashtbl.hash ind) (Hashtbl.hash arr)) - | Gcomment s -> combinesmall 7 (Hashtbl.hash s) + combinesmall 6 (combine (ind_hash ind) (Array.fold_left combine 0 arr)) + | Gcomment s -> combinesmall 7 (String.hash s) let global_stack = ref ([] : global list) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index e6a579c5b..a757f013a 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -473,18 +473,27 @@ let empty_args = [||] module Renv = struct + module ConstrHash = + struct + type t = constructor + let equal = eq_constructor + let hash = constructor_hash + end + + module ConstrTable = Hashtbl.Make(ConstrHash) + type constructor_info = tag * int * int (* nparam nrealargs *) type t = { name_rel : name Vect.t; - construct_tbl : (constructor, constructor_info) Hashtbl.t; + construct_tbl : constructor_info ConstrTable.t; } let make () = { name_rel = Vect.make 16 Anonymous; - construct_tbl = Hashtbl.create 111 + construct_tbl = ConstrTable.create 111 } let push_rel env id = Vect.push env.name_rel id @@ -501,7 +510,7 @@ module Renv = Lrel (Vect.get_last env.name_rel (n-1), n) let get_construct_info env c = - try Hashtbl.find env.construct_tbl c + try ConstrTable.find env.construct_tbl c with Not_found -> let ((mind,j), i) = c in let oib = lookup_mind mind !global_env in @@ -509,7 +518,7 @@ module Renv = let tag,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in let r = (tag, nparams, arity) in - Hashtbl.add env.construct_tbl c r; + ConstrTable.add env.construct_tbl c r; r end diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index c3e2b3ab7..98094f795 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -39,7 +39,7 @@ let eq_annot_sw asw1 asw2 = open Hashset.Combine let hash_annot_sw asw = - combine (Hashtbl.hash asw.asw_ind) (Hashtbl.hash asw.asw_prefix) + combine (ind_hash asw.asw_ind) (String.hash asw.asw_prefix) type sort_annot = string * int diff --git a/kernel/vm.ml b/kernel/vm.ml index bc7116a35..30add56f9 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -304,13 +304,26 @@ let val_of_str_const str = val_of_obj (obj_of_str_const str) let val_of_atom a = val_of_obj (obj_of_atom a) -let idkey_tbl = Hashtbl.create 31 +module IdKeyHash = +struct + type t = id_key + let equal = Names.eq_id_key + open Hashset.Combine + let hash = function + | ConstKey c -> combinesmall 1 (Constant.hash c) + | VarKey id -> combinesmall 2 (Id.hash id) + | RelKey i -> combinesmall 3 (Int.hash i) +end + +module KeyTable = Hashtbl.Make(IdKeyHash) + +let idkey_tbl = KeyTable.create 31 let val_of_idkey key = - try Hashtbl.find idkey_tbl key + try KeyTable.find idkey_tbl key with Not_found -> let v = val_of_atom (Aid key) in - Hashtbl.add idkey_tbl key v; + KeyTable.add idkey_tbl key v; v let val_of_rel k = val_of_idkey (RelKey k) diff --git a/lib/option.ml b/lib/option.ml index 1ef45d232..abdae892f 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -35,6 +35,10 @@ let compare f x y = match x, y with | None, Some _ -> -1 | Some _, None -> 1 +let hash f = function +| None -> 0 +| Some x -> f x + exception IsNone (** [get x] returns [y] where [x] is [Some y]. It raises IsNone diff --git a/lib/option.mli b/lib/option.mli index d390edb63..af8696a5e 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -31,6 +31,9 @@ val equal : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool (** Same as [equal], but with comparison. *) val compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int +(** Lift a hash to option types. *) +val hash : ('a -> int) -> 'a option -> int + (** [get x] returns [y] where [x] is [Some y]. It raises IsNone if [x] equals [None]. *) val get : 'a option -> 'a |