abstract+Defined: create opaque sub proofs (as pre-ParalITP)

Non-opaque-constant's side effects are processed before
the constant enters the kernel and global constants are
generated for them (as before, but not by side effect in
the middle of the proof construction).
This makes sense because proofs ending with Defined have
to be run immediately, so the list of side effects is
immediately available.

These side effects are type checked again.
To fix that the idea of kernel signatures could be employed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16702 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 41 insertions, 1 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index b0f320942..ac3aad15e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -226,7 +226,7 @@ let string_of_side_effect = function
   | NewConstant (c,_) -> Names.string_of_con c
 type side_effects = side_effect list
 let no_seff = ([] : side_effects)
-let iter_side_effects f l = List.iter f l
+let iter_side_effects f l = List.iter f (List.rev l)
 let fold_side_effects f a l = List.fold_left f a l
 let uniquize_side_effects l = List.uniquize l
 let union_side_effects l1 l2 = l1 @ l2
diff --git a/library/declare.ml b/library/declare.ml
index e2831b862..c4651f0de 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -181,7 +181,47 @@ let declare_constant_common id cst =
   Notation.declare_ref_arguments_scope (ConstRef c);
   c
 
+let declare_sideff (NewConstant (c, cb)) =
+  let id = Names.Label.to_id (Names.Constant.label c) in
+  let pt, opaque =
+    match cb with
+    | { const_body = Def sc } -> Lazyconstr.force sc, false
+    | { const_body = OpaqueDef fc } ->
+          Lazyconstr.force_opaque (Future.force fc), true
+    | { const_body = Undef _ } -> anomaly(str"Undefined side effect")
+  in
+  let ty =
+    match cb.Declarations.const_type with
+    | Declarations.NonPolymorphicType t -> Some t
+    | _ -> None in
+  let cst = {
+    cst_decl = ConstantEntry (DefinitionEntry {
+        const_entry_body = Future.from_val (pt,Declareops.no_seff);
+        const_entry_secctx = Some cb.Declarations.const_hyps;
+        const_entry_type = ty;
+        const_entry_opaque = opaque;
+        const_entry_inline_code = false;
+    });
+    cst_hyps = [] ;
+    cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
+    cst_locl = true;
+  } in
+  ignore(declare_constant_common id cst)
+
 let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
+  let cd = (* We deal with side effects of non-opaque constants *)
+    match cd with
+    | Entries.DefinitionEntry ({
+      const_entry_opaque = false; const_entry_body = bo } as de) ->
+        let pt, seff = Future.force bo in
+        if seff = Declareops.no_seff then cd
+        else begin
+          Declareops.iter_side_effects declare_sideff seff;
+          Entries.DefinitionEntry { de with
+            const_entry_body = Future.from_val (pt, Declareops.no_seff) }
+        end
+    | _ -> cd
+  in
   let cst = {
     cst_decl = ConstantEntry cd;
     cst_hyps = [] ;