From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- library/libobject.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'library/libobject.ml') diff --git a/library/libobject.ml b/library/libobject.ml index 2ee57baf9c..85c830ea2c 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -108,6 +108,9 @@ let declare_object_full odecl = let declare_object odecl = try fst (declare_object_full odecl) with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) +let declare_object_full odecl = + try declare_object_full odecl + with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) -- cgit v1.2.3 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/libobject.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'library/libobject.ml') diff --git a/library/libobject.ml b/library/libobject.ml index 85c830ea2c..c638759070 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -9,6 +9,8 @@ open Libnames open Pp +module Dyn = Dyn.Make(struct end) + (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one wants to work with restricted Coq programs that have only parts of @@ -158,3 +160,5 @@ let discharge_object ((_,lobj) as node) = let rebuild_object lobj = apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj + +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/libobject.ml | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) (limited to 'library/libobject.ml') diff --git a/library/libobject.ml b/library/libobject.ml index c638759070..f0d281a2dd 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) -- 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/libobject.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/libobject.ml') diff --git a/library/libobject.ml b/library/libobject.ml index 85c830ea2c..706e399159 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*