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

5 files changed, 34 insertions, 20 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 6a5b0dbb2..d74c9a0d5 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -59,7 +59,9 @@ type constant_body = {
     const_native_name : native_name ref;
     const_inline_code : bool }
 
-type side_effect = NewConstant of constant * constant_body
+type side_effect =
+  | SEsubproof of constant * constant_body
+  | SEscheme of (inductive * constant * constant_body) list * string
     
 (** {6 Representation of mutual inductive types in the kernel } *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 518a40a6e..9f981f482 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -254,7 +254,9 @@ let prune_constant_body cb =
   else {cb with const_constraints = cst'; const_body = cbo'}
 
 let string_of_side_effect = function
-  | NewConstant (c,_) -> Names.string_of_con c
+  | SEsubproof (c,_) -> Names.string_of_con c
+  | SEscheme (cl,_) ->
+      String.concat ", " (List.map (fun (_,c,_) -> Names.string_of_con c) cl)
 type side_effects = side_effect list
 let no_seff = ([] : side_effects)
 let iter_side_effects f l = List.iter f (List.rev l)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7a25cc5f8..3cde1538d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -169,8 +169,10 @@ let check_engagement env c =
 
 (** {6 Stm machinery } *)
 
-type side_effect = Declarations.side_effect
-let sideff_of_con env c = NewConstant (c, Environ.lookup_constant c env.env)
+let sideff_of_con env c = SEsubproof (c, Environ.lookup_constant c env.env)
+let sideff_of_scheme kind env cl =
+  SEscheme(
+    List.map (fun (i,c) -> i, c, Environ.lookup_constant c env.env) cl,kind)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5d1c98de5..a56bb8578 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -34,6 +34,9 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 (** {6 Stm machinery } *)
 
 val sideff_of_con : safe_environment -> constant -> Declarations.side_effect
+val sideff_of_scheme :
+  string -> safe_environment -> (inductive * constant) list ->
+    Declarations.side_effect
 
 val is_curmod_library : safe_environment -> bool
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c65ca8fc0..ef0270e9d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -47,27 +47,32 @@ let translate_local_assum env t =
 (* Insertion of constants and parameters in environment. *)
 
 let handle_side_effects env body side_eff =
-  let handle_sideff t (NewConstant (c,cb)) =
-    let cname = 
+  let handle_sideff t se =
+    let cbl = match se with
+      | SEsubproof (c,cb) -> [c,cb]
+      | SEscheme (cl,_) -> List.map (fun (_,c,cb) -> c,cb) cl in
+    let cname c = 
       let name = string_of_con c in
       for i = 0 to String.length name - 1 do
         if name.[i] = '.' || name.[i] = '#' then name.[i] <- '_' done;
       Name (id_of_string name) in
-    let rec sub i x = match kind_of_term x with
+    let rec sub c i x = match kind_of_term x with
       | Const c' when eq_constant c c' -> mkRel i
-      | _ -> map_constr_with_binders ((+) 1) sub i x in
-    match cb.const_body with
-    | Undef _ -> assert false
-    | Def b ->
-        let b = Lazyconstr.force b in
-        let b_ty = Typeops.type_of_constant_type env cb.const_type in
-        let t = sub 1 (Vars.lift 1 t) in
-        mkLetIn (cname, b, b_ty, t)
-    | OpaqueDef b -> 
-        let b = Lazyconstr.force_opaque (Future.force b) in
-        let b_ty = Typeops.type_of_constant_type env cb.const_type in
-        let t = sub 1 (Vars.lift 1 t) in
-        mkApp (mkLambda (cname, b_ty, t), [|b|])
+      | _ -> map_constr_with_binders ((+) 1) (sub c) i x in
+    let fix_body (c,cb) t =
+      match cb.const_body with
+      | Undef _ -> assert false
+      | Def b ->
+          let b = Lazyconstr.force b in
+          let b_ty = Typeops.type_of_constant_type env cb.const_type in
+          let t = sub c 1 (Vars.lift 1 t) in
+          mkLetIn (cname c, b, b_ty, t)
+      | OpaqueDef b -> 
+          let b = Lazyconstr.force_opaque (Future.force b) in
+          let b_ty = Typeops.type_of_constant_type env cb.const_type in
+          let t = sub c 1 (Vars.lift 1 t) in
+          mkApp (mkLambda (cname c, b_ty, t), [|b|]) in
+    List.fold_right fix_body cbl t
   in
   (* CAVEAT: we assure a proper order *)
   Declareops.fold_side_effects handle_sideff body