diff options
-rw-r--r-- | lib/cSig.mli | 2 | ||||
-rw-r--r-- | lib/dyn.ml | 31 | ||||
-rw-r--r-- | lib/dyn.mli | 10 | ||||
-rw-r--r-- | lib/util.ml | 1 | ||||
-rw-r--r-- | lib/util.mli | 2 | ||||
-rw-r--r-- | library/declaremods.ml | 2 | ||||
-rw-r--r-- | library/libobject.ml | 17 | ||||
-rw-r--r-- | library/libobject.mli | 1 | ||||
-rw-r--r-- | library/summary.ml | 22 |
9 files changed, 57 insertions, 31 deletions
diff --git a/lib/cSig.mli b/lib/cSig.mli index 4463e8d9c..796e58cbf 100644 --- a/lib/cSig.mli +++ b/lib/cSig.mli @@ -14,6 +14,8 @@ type ('a, 'b) union = Inl of 'a | Inr of 'b type 'a until = Stop of 'a | Cont of 'a (** Used for browsable-until structures. *) +type (_, _) eq = Refl : ('a, 'a) eq + module type SetS = sig type elt diff --git a/lib/dyn.ml b/lib/dyn.ml index 60167ef1b..0571f3b5d 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -11,12 +11,12 @@ open Pp module type S = sig -type t +type 'a tag +type t = Dyn : 'a tag * 'a -> t -val create : string -> ('a -> t) * (t -> 'a) -val tag : t -> string -val has_tag : t -> string -> bool -val pointer_equal : t -> t -> bool +val create : string -> 'a tag +val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option +val repr : 'a tag -> string val dump : unit -> (int * string) list end @@ -24,7 +24,9 @@ module Make(M : CSig.EmptyS) = struct (* Dynamics, programmed with DANGER !!! *) -type t = int * Obj.t +type 'a tag = int + +type t = Dyn : 'a tag * 'a -> t let dyntab = ref (Int.Map.empty : string Int.Map.t) (** Instead of working with tags as strings, which are costly, we use their @@ -41,25 +43,16 @@ let create (s : string) = 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 - anomaly (str "dyn_out: expected " ++ str s) - in - (infun, outfun) + hash -let has_tag (s, _) tag = - let hash = Hashtbl.hash (tag : string) in - Int.equal s hash +let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option = + fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None -let tag (s,_) = +let repr s = try Int.Map.find s !dyntab with Not_found -> anomaly (str "Unknown dynamic tag " ++ int s) -let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2 - let dump () = Int.Map.bindings !dyntab end
\ No newline at end of file diff --git a/lib/dyn.mli b/lib/dyn.mli index 55c4f0ce8..28587859e 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -10,12 +10,12 @@ module type S = sig -type t +type 'a tag +type t = Dyn : 'a tag * 'a -> t -val create : string -> ('a -> t) * (t -> 'a) -val tag : t -> string -val has_tag : t -> string -> bool -val pointer_equal : t -> t -> bool +val create : string -> 'a tag +val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option +val repr : 'a tag -> string val dump : unit -> (int * string) list end diff --git a/lib/util.ml b/lib/util.ml index a20dba0fc..b67539918 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -124,6 +124,7 @@ let delayed_force f = f () type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a +type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq let map_union f g = function | Inl a -> Inl (f a) diff --git a/lib/util.mli b/lib/util.mli index 1dc405fcb..0ce6cc660 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -111,5 +111,7 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a (** Used for browsable-until structures. *) +type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq + val open_utf8_file_in : string -> in_channel (** Open an utf-8 encoded file and skip the byte-order mark if any. *) diff --git a/library/declaremods.ml b/library/declaremods.ml index 7f607a51c..d8c5ab5e7 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -371,7 +371,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 (object_has_tag obj "MODULE"); + assert (String.equal (object_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 c63875907..f0d281a2d 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -8,6 +8,7 @@ open Libnames open Pp +open Util module Dyn = Dyn.Make(struct end) @@ -72,15 +73,25 @@ type dynamic_object_declaration = { dyn_discharge_function : object_name * obj -> obj option; dyn_rebuild_function : obj -> obj } -let object_tag = Dyn.tag -let object_has_tag = Dyn.has_tag +let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) +let make_dyn (type a) (tag : a Dyn.tag) = + let infun x = Dyn.Dyn (tag, x) in + let outfun : (Dyn.t -> a) = fun dyn -> + let Dyn.Dyn (t, x) = dyn in + match Dyn.eq t tag with + | None -> assert false + | Some Refl -> x + in + (infun, outfun) + let declare_object_full odecl = let na = odecl.object_name in - let (infun,outfun) = Dyn.create na in + let tag = Dyn.create na in + let (infun, outfun) = make_dyn tag in 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) diff --git a/library/libobject.mli b/library/libobject.mli index e49f3fd5c..12b1a558f 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -99,7 +99,6 @@ 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/library/summary.ml b/library/summary.ml index 6ef4e131c..a922e155d 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -22,8 +22,19 @@ let summaries = ref Int.Map.empty let mangle id = id ^ "-SUMMARY" +let make_dyn (type a) (tag : a Dyn.tag) = + let infun x = Dyn.Dyn (tag, x) in + let outfun : (Dyn.t -> a) = fun dyn -> + let Dyn.Dyn (t, x) = dyn in + match Dyn.eq t tag with + | None -> assert false + | Some Refl -> x + in + (infun, outfun) + let internal_declare_summary hash sumname sdecl = - let (infun, outfun) = Dyn.create (mangle sumname) in + let tag = Dyn.create (mangle sumname) in + let (infun, outfun) = make_dyn tag in let dyn_freeze b = infun (sdecl.freeze_function b) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in @@ -166,8 +177,15 @@ let project_summary { summaries; ml_module } ?(complement=false) ids = List.filter (fun (id, _) -> List.mem id ids) summaries let pointer_equal l1 l2 = + let ptr_equal d1 d2 = + let Dyn.Dyn (t1, x1) = d1 in + let Dyn.Dyn (t2, x2) = d2 in + match Dyn.eq t1 t2 with + | None -> false + | Some Refl -> x1 == x2 + in CList.for_all2eq - (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2 + (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2 (** All-in-one reference declaration + registration *) |