From 153d77d00ccbacf22aa5d70ca2c1cacab2749339 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Dec 2015 21:46:12 +0100 Subject: Specializing the Dyn module to each usecase. Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point. --- lib/dyn.ml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'lib/dyn.ml') diff --git a/lib/dyn.ml b/lib/dyn.ml index 056b687313..60167ef1ba 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -9,6 +9,19 @@ open Errors open Pp +module type S = +sig +type 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 dump : unit -> (int * string) list +end + +module Make(M : CSig.EmptyS) = +struct (* Dynamics, programmed with DANGER !!! *) type t = int * Obj.t @@ -48,3 +61,5 @@ let tag (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 -- cgit v1.2.3 From 895d34a264d9d90adfe4f0618c3bb0663dc01615 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Dec 2015 12:53:20 +0100 Subject: Leveraging GADTs to provide a better Dyn API. --- lib/dyn.ml | 31 ++++++++++++------------------- 1 file changed, 12 insertions(+), 19 deletions(-) (limited to 'lib/dyn.ml') diff --git a/lib/dyn.ml b/lib/dyn.ml index 60167ef1ba..0571f3b5d6 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 -- cgit v1.2.3 From 126a3c998c62bfd9f9b570f12b2e29576dd94cdd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Dec 2015 13:43:07 +0100 Subject: Factorizing unsafe code by relying on the new Dyn module. --- lib/dyn.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'lib/dyn.ml') diff --git a/lib/dyn.ml b/lib/dyn.ml index 0571f3b5d6..826cfaf8db 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -6,9 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Pp - module type S = sig type 'a tag @@ -39,8 +36,8 @@ let create (s : string) = let () = if Int.Map.mem hash !dyntab then let old = Int.Map.find hash !dyntab in - let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in - anomaly ~label:"Dyn.create" msg + let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in + assert false in let () = dyntab := Int.Map.add hash s !dyntab in hash @@ -51,7 +48,8 @@ let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option = let repr s = try Int.Map.find s !dyntab with Not_found -> - anomaly (str "Unknown dynamic tag " ++ int s) + let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in + assert false let dump () = Int.Map.bindings !dyntab -- cgit v1.2.3 From 32a18b19f99c82dea5358bdebeb19862d30c4973 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Jan 2016 22:39:23 +0100 Subject: Adding a structure indexed by tags. --- lib/dyn.ml | 56 +++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 55 insertions(+), 1 deletion(-) (limited to 'lib/dyn.ml') diff --git a/lib/dyn.ml b/lib/dyn.ml index 826cfaf8db..660ffc44ec 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -6,6 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +module type TParam = +sig + type 'a t +end + module type S = sig type 'a tag @@ -14,6 +19,30 @@ type t = Dyn : 'a tag * 'a -> t val create : string -> 'a tag val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option val repr : 'a tag -> string + +type any = Any : 'a tag -> any + +val name : string -> any option + +module Map(M : TParam) : +sig + type t + val empty : t + val add : 'a tag -> 'a M.t -> t -> t + val remove : 'a tag -> t -> t + val find : 'a tag -> t -> 'a M.t + val mem : 'a tag -> t -> bool + + type any = Any : 'a tag * 'a M.t -> any + + type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } + val map : map -> t -> t + + val iter : (any -> unit) -> t -> unit + val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r + +end + val dump : unit -> (int * string) list end @@ -25,6 +54,8 @@ type 'a tag = int type t = Dyn : 'a tag * 'a -> t +type any = Any : 'a tag -> any + 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 @@ -51,6 +82,29 @@ let repr s = let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in assert false +let name s = + let hash = Hashtbl.hash s in + if Int.Map.mem hash !dyntab then Some (Any hash) else None + let dump () = Int.Map.bindings !dyntab -end \ No newline at end of file +module Map(M : TParam) = +struct +type t = Obj.t M.t Int.Map.t +let cast : 'a M.t -> 'b M.t = Obj.magic +let empty = Int.Map.empty +let add tag v m = Int.Map.add tag (cast v) m +let remove tag m = Int.Map.remove tag m +let find tag m = cast (Int.Map.find tag m) +let mem = Int.Map.mem + +type any = Any : 'a tag * 'a M.t -> any + +type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } +let map f m = Int.Map.mapi f.map m + +let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m +let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu +end + +end -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- lib/dyn.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/dyn.ml') diff --git a/lib/dyn.ml b/lib/dyn.ml index 056b687313..04b32870ac 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*