diff options
| -rw-r--r-- | lib/dyn.ml | 42 | ||||
| -rw-r--r-- | lib/dyn.mli | 1 | ||||
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/libobject.ml | 43 | ||||
| -rw-r--r-- | library/libobject.mli | 1 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 11 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 2 |
7 files changed, 55 insertions, 47 deletions
diff --git a/lib/dyn.ml b/lib/dyn.ml index 93f19fce9..abb2fbcee 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -10,16 +10,38 @@ open Errors (* Dynamics, programmed with DANGER !!! *) -type t = string * Obj.t +type t = int * Obj.t -let dyntab = ref ([] : string list) +let dyntab = ref (Int.Map.empty : string Int.Map.t) +(** Instead of working with tags as strings, which are costly, we use their + hash. We ensure unicity of the hash in the [create] function. If ever a + collision occurs, which is unlikely, it is sufficient to tweak the offending + dynamic tag. *) -let create s = - if List.exists (fun s' -> CString.equal s s') !dyntab then - anomaly ~label:"Dyn.create" (Pp.str ("already declared dynamic " ^ s)); - dyntab := s :: !dyntab; - ((fun v -> (s,Obj.repr v)), - (fun (s',rv) -> - if s = s' then Obj.magic rv else failwith "dyn_out")) +let create (s : string) = + let hash = Hashtbl.hash s in + let () = + if Int.Map.mem hash !dyntab then + let old = Int.Map.find hash !dyntab in + let msg = Pp.str ("Dynamic tag collision: " ^ s ^ " vs. " ^ old) in + anomaly ~label:"Dyn.create" msg + in + let () = dyntab := Int.Map.add hash s !dyntab in + let infun v = (hash, Obj.repr v) in + let outfun (nh, rv) = + if Int.equal hash nh then Obj.magic rv + else + let msg = (Pp.str ("dyn_out: expected " ^ s)) in + anomaly msg + in + (infun, outfun) -let tag (s,_) = s +let has_tag (s, _) tag = + let hash = Hashtbl.hash (tag : string) in + Int.equal s hash + +let tag (s,_) = + try Int.Map.find s !dyntab + with Not_found -> + let msg = Pp.str ("Unknown dynamic tag " ^ (string_of_int s)) in + anomaly msg diff --git a/lib/dyn.mli b/lib/dyn.mli index 9173e8101..00c030177 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -12,3 +12,4 @@ type t val create : string -> ('a -> t) * (t -> 'a) val tag : t -> string +val has_tag : t -> string -> bool diff --git a/library/declaremods.ml b/library/declaremods.ml index dae585d5a..c60e008d1 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -369,7 +369,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 = match idl, objs0 with | _,[] -> [] | id::idl,(id',obj)::tail when Id.equal id id' -> - assert (String.equal (object_tag obj) "MODULE"); + assert (object_has_tag obj "MODULE"); let mp_id = MPdot(mp0, Label.of_id id) in let objs = match idl with | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1 diff --git a/library/libobject.ml b/library/libobject.ml index 7cf286321..3bbb1e90e 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -74,7 +74,8 @@ type dynamic_object_declaration = { dyn_discharge_function : object_name * obj -> obj option; dyn_rebuild_function : obj -> obj } -let object_tag lobj = Dyn.tag lobj +let object_tag = Dyn.tag +let object_has_tag = Dyn.has_tag let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) @@ -82,36 +83,18 @@ let cache_tab = let declare_object_full odecl = let na = odecl.object_name in let (infun,outfun) = Dyn.create na in - let cacher (oname,lobj) = - if String.equal (Dyn.tag lobj) na then odecl.cache_function (oname,outfun lobj) - else anomaly (Pp.str "somehow we got the wrong dynamic object in the cachefun") - and loader i (oname,lobj) = - if String.equal (Dyn.tag lobj) na then odecl.load_function i (oname,outfun lobj) - else anomaly (Pp.str "somehow we got the wrong dynamic object in the loadfun") - and opener i (oname,lobj) = - if String.equal (Dyn.tag lobj) na then odecl.open_function i (oname,outfun lobj) - else anomaly (Pp.str "somehow we got the wrong dynamic object in the openfun") - and substituter (sub,lobj) = - if String.equal (Dyn.tag lobj) na then - infun (odecl.subst_function (sub,outfun lobj)) - else anomaly (Pp.str "somehow we got the wrong dynamic object in the substfun") - and classifier lobj = - if String.equal (Dyn.tag lobj) na then - match odecl.classify_function (outfun lobj) with - | Dispose -> Dispose - | Substitute obj -> Substitute (infun obj) - | Keep obj -> Keep (infun obj) - | Anticipate (obj) -> Anticipate (infun obj) - else - anomaly (Pp.str "somehow we got the wrong dynamic object in the classifyfun") + let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj) + and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj) + and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj) + and substituter (sub,lobj) = infun (odecl.subst_function (sub,outfun lobj)) + and classifier lobj = match odecl.classify_function (outfun lobj) with + | Dispose -> Dispose + | Substitute obj -> Substitute (infun obj) + | Keep obj -> Keep (infun obj) + | Anticipate (obj) -> Anticipate (infun obj) and discharge (oname,lobj) = - if String.equal (Dyn.tag lobj) na then - Option.map infun (odecl.discharge_function (oname,outfun lobj)) - else - anomaly (Pp.str "somehow we got the wrong dynamic object in the dischargefun") - and rebuild lobj = - if String.equal (Dyn.tag lobj) na then infun (odecl.rebuild_function (outfun lobj)) - else anomaly (Pp.str "somehow we got the wrong dynamic object in the rebuildfun") + Option.map infun (odecl.discharge_function (oname,outfun lobj)) + and rebuild lobj = infun (odecl.rebuild_function (outfun lobj)) in Hashtbl.add cache_tab na { dyn_cache_function = cacher; dyn_load_function = loader; diff --git a/library/libobject.mli b/library/libobject.mli index e886c4db0..3986b3d3f 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -100,6 +100,7 @@ val declare_object : 'a object_declaration -> ('a -> obj) val object_tag : obj -> string +val object_has_tag : obj -> string -> bool val cache_object : object_name * obj -> unit val load_object : int -> object_name * obj -> unit diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 1bba78334..261e8583e 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -689,11 +689,12 @@ and intern_tacarg strict onlytac ist = function let (_, arg) = Genintern.generic_intern ist arg in TacGeneric arg | TacDynamic(loc,t) as x -> - (match Dyn.tag t with - | "tactic" | "value" -> x - | "constr" -> if onlytac then error_tactic_expected loc else x - | s -> anomaly ~loc - (str "Unknown dynamic: <" ++ str s ++ str ">")) + if Dyn.has_tag t "tactic" || Dyn.has_tag t "value" then x + else if Dyn.has_tag t "constr" then + if onlytac then error_tactic_expected loc else x + else + let tag = Dyn.tag t in + anomaly ~loc (str "Unknown dynamic: <" ++ str tag ++ str ">") (* Reads the rules of a Match Context or a Match *) and intern_match_rule onlytac ist = function diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 3eb61ccdf..4f2dd2f33 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -251,7 +251,7 @@ let eterm_obligations env name evm fs ?status t ty = in let tac = match Store.get ev.evar_extra evar_tactic with | Some t -> - if String.equal (Dyn.tag t) "tactic" then + if Dyn.has_tag t "tactic" then Some (Tacinterp.interp (Tacinterp.globTacticIn (Tacinterp.tactic_out t))) else None |