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. --- kernel/declareops.mli | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) (limited to 'kernel/declareops.mli') diff --git a/kernel/declareops.mli b/kernel/declareops.mli index ce65af975..1b8700958 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -9,6 +9,7 @@ open Declarations open Mod_subst open Univ +open Entries (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -49,17 +50,6 @@ val is_opaque : constant_body -> bool val string_of_side_effect : side_effect -> string -type side_effects -val no_seff : side_effects -val iter_side_effects : (side_effect -> unit) -> side_effects -> unit -val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a -val uniquize_side_effects : side_effects -> side_effects -val union_side_effects : side_effects -> side_effects -> side_effects -val flatten_side_effects : side_effects list -> side_effects -val side_effects_of_list : side_effect list -> side_effects -val cons_side_effects : side_effect -> side_effects -> side_effects -val side_effects_is_empty : side_effects -> bool - (** {6 Inductive types} *) val eq_recarg : recarg -> recarg -> bool -- cgit v1.2.3