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. --- library/summary.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'library/summary.ml') diff --git a/library/summary.ml b/library/summary.ml index 8e2abbf15b..6ef4e131c7 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -10,6 +10,8 @@ open Pp open Errors open Util +module Dyn = Dyn.Make(struct end) + type marshallable = [ `Yes | `No | `Shallow ] type 'a summary_declaration = { freeze_function : marshallable -> 'a; @@ -176,3 +178,5 @@ let ref ?(freeze=fun _ r -> r) ~name x = unfreeze_function = ((:=) r); init_function = (fun () -> r := x) }; r + +let dump = Dyn.dump -- 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. --- library/summary.ml | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) (limited to 'library/summary.ml') diff --git a/library/summary.ml b/library/summary.ml index 6ef4e131c7..a922e155dd 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 *) -- 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. --- library/summary.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/summary.ml') diff --git a/library/summary.ml b/library/summary.ml index 8e2abbf15b..46c52acc4c 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*