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.

5 files changed, 21 insertions, 13 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index c232ae31a..d6c29283f 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-let map_const_entry_body (f:Term.constr->Term.constr) (x:Entries.const_entry_body)
-    : Entries.const_entry_body =
+let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
+    : Safe_typing.private_constants Entries.const_entry_body =
   Future.chain ~pure:true x begin fun ((b,ctx),fx) ->
     (f b , ctx) , fx
   end
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9e27ddf2e..c43932324 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -334,7 +334,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 	ignore(
 	  Declare.declare_constant
 	    name
-	    (Entries.DefinitionEntry ce,
+	    (DefinitionEntry ce,
 	     Decl_kinds.IsDefinition (Decl_kinds.Scheme))
 	);
 	Declare.definition_message name;
@@ -447,7 +447,7 @@ let get_funs_constant mp dp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list =
+let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list =
   let env = Global.env () in
   let funs = List.map fst fas in
   let first_fun = List.hd funs in
@@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
       let sorts = Array.of_list sorts in
       List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
-    let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
+    let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in
     let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in
     let other_result =
@@ -585,9 +585,9 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
 	     Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
 	   in
 	   {const with
-	      Entries.const_entry_body = 
-                (Future.from_val (Term_typing.mk_pure_proof princ_body));
-	      Entries.const_entry_type = Some scheme_type
+	      const_entry_body = 
+                (Future.from_val (Safe_typing.mk_pure_proof princ_body));
+	      const_entry_type = Some scheme_type
 	   }
       )
       other_fun_princ_types
@@ -620,7 +620,7 @@ let build_scheme fas =
        ignore
 	 (Declare.declare_constant
 	    princ_id
-	    (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+	    (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
        Declare.definition_message princ_id
     )
     fas
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index f6e5578d2..bc082f073 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 open Names
 open Term
 open Misctypes
@@ -29,7 +37,7 @@ val compute_new_princ_type_from_rel : constr array -> sorts array ->
 exception No_graph_found
 
 val make_scheme :   Evd.evar_map ref ->
- (pconstant*glob_sort) list -> Entries.definition_entry list
+ (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list
 
 val build_scheme : (Id.t*Libnames.reference*glob_sort) list ->  unit
 val build_case_scheme : (Id.t*Libnames.reference*glob_sort)  ->  unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 35bd1c36d..aa47e2619 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -149,7 +149,7 @@ let get_locality = function
 | Global -> false
 
 let save with_clean id const (locality,_,kind) hook =
-  let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
+  let fix_exn = Future.fix_exn_of const.const_entry_body in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
         let k = Kindops.logical_kind_of_goal_kind kind in
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 10daf6e84..23f1da1ba 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,7 +46,7 @@ val const_of_id: Id.t ->  Globnames.global_reference(* constantyes *)
 val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
-val save : bool -> Id.t -> Entries.definition_entry  -> Decl_kinds.goal_kind ->
+val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Lemmas.declaration_hook Ephemeron.key -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
@@ -54,7 +54,7 @@ val save : bool -> Id.t -> Entries.definition_entry  -> Decl_kinds.goal_kind ->
 *)
 val get_proof_clean : bool ->
   Names.Id.t *
-    (Entries.definition_entry * Decl_kinds.goal_kind)
+    (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind)