ind_tables: properly handling side effects

If a constant is defined as transparent, not only its side effects
(opaque sub proofs as in abstract, and transparent ind schemes)
are declared globally, but the ones that are schemes are also declared
as such.

The only sub optimal thing is that the code handling in a special
way the side effects of transparent constants is in declare.ml that
does not see ind_tables.ml, hence a forward ref to a function is used.
IMO, ind_tables has no reason to stay in toplevel/.

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

2 files changed, 28 insertions, 9 deletions

diff --git a/library/declare.ml b/library/declare.ml
index c4651f0de4..96bbf07d5b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -181,22 +181,30 @@ 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 =
+let declare_scheme = ref (fun _ _ -> assert false)
+let set_declare_scheme f = declare_scheme := f
+let declare_sideff se =
+  let cbl, scheme = match se with
+    | SEsubproof (c, cb) -> [c, cb], None
+    | SEscheme (cbl, k) ->
+        List.map (fun (_,c,cb) -> c,cb) cbl, Some (List.map pi1 cbl,k) in
+  let id_of c = Names.Label.to_id (Names.Constant.label c) in
+  let pt_opaque_of cb =
     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 =
+  let ty_of cb =
     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);
+  let cst_of cb =
+    let pt, opaque = pt_opaque_of cb in
+    let ty = ty_of cb in
+    { cst_decl = ConstantEntry (DefinitionEntry {
+        const_entry_body = Future.from_here (pt, Declareops.no_seff);
         const_entry_secctx = Some cb.Declarations.const_hyps;
         const_entry_type = ty;
         const_entry_opaque = opaque;
@@ -206,7 +214,13 @@ let declare_sideff (NewConstant (c, cb)) =
     cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
     cst_locl = true;
   } in
-  ignore(declare_constant_common id cst)
+  let knl =
+    List.map (fun (c,cb) ->
+      declare_constant_common (id_of c) (cst_of cb)) cbl in
+  match scheme with
+  | None -> ()
+  | Some (inds,kind) ->
+      !declare_scheme kind (Array.of_list (List.combine inds knl))
 
 let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
   let cd = (* We deal with side effects of non-opaque constants *)
@@ -215,7 +229,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
       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
+        else begin 
           Declareops.iter_side_effects declare_sideff seff;
           Entries.DefinitionEntry { de with
             const_entry_body = Future.from_val (pt, Declareops.no_seff) }
diff --git a/library/declare.mli b/library/declare.mli
index ff4e20ad23..f33077ddb2 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -61,6 +61,11 @@ val declare_definition :
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> Id.t -> ?types:constr -> Entries.const_entry_body -> constant
 
+(** Since transparent constant's side effects are globally declared, we
+ *  need that *)
+val set_declare_scheme :
+  (string -> (inductive * constant) array -> unit) -> unit
+
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block (boolean must be true iff it is a record) *)