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.

1 files changed, 26 insertions, 7 deletions

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 8d92bcc68..509160ccc 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,23 +12,42 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : env -> Id.t -> definition_entry ->
+val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
   constant_def * types * constant_universes
 
 val translate_local_assum : env -> types -> types
 
-val mk_pure_proof : constr -> proof_output
+val mk_pure_proof : constr -> side_effects proof_output
 
-val handle_side_effects : env -> constr -> Declareops.side_effects -> constr
+val handle_side_effects : env -> constr -> side_effects -> constr
 (** Returns the term where side effects have been turned into let-ins or beta
     redexes. *)
 
-val handle_entry_side_effects : env -> definition_entry -> definition_entry
+val handle_entry_side_effects : env -> side_effects definition_entry -> side_effects definition_entry
 (** Same as {!handle_side_effects} but applied to entries. Only modifies the
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
-val translate_constant : env -> constant -> constant_entry -> constant_body
+val uniq_seff : side_effects -> side_effects
+
+val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> constant_body
+
+(* Checks weather the side effects in constant_entry can be trusted.
+ * Returns the list of effects to be exported.
+ * Note: It forces the Future.computation.                           *)
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+type exported_side_effect = 
+  constant * constant_body * side_effects Entries.constant_entry * side_effect_role
+  
+val validate_side_effects_for_export :
+  structure_body -> env -> side_effects constant_entry ->
+    exported_side_effect list * side_effects constant_entry
+
+val constant_entry_of_side_effect :
+  constant_body -> seff_env -> side_effects constant_entry
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,8 +56,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : env -> constant option -> 
-  constant_entry -> Cooking.result
+val infer_declaration : trust:structure_body -> env -> constant option -> 
+  side_effects constant_entry -> Cooking.result
 
 val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body