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

8 files changed, 77 insertions, 38 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
diff --git a/library/declare.ml b/library/declare.ml
index c4651f0de..96bbf07d5 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 ff4e20ad2..f33077ddb 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) *)
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 0a5f7d25f..45621ced8 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -99,6 +99,8 @@ let declare_individual_scheme_object s ?(aux="") f =
 let declare_scheme kind indcl =
   Lib.add_anonymous_leaf (inScheme (kind,indcl))
 
+let () = Declare.set_declare_scheme declare_scheme
+
 let is_visible_name id =
   try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true
   with Not_found -> false
@@ -134,7 +136,8 @@ let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
   let const = define internal id c in
   declare_scheme kind [|ind,const|];
-  const, Declareops.cons_side_effects (Safe_typing.sideff_of_con (Global.safe_env()) const) eff
+  const, Declareops.cons_side_effects
+     (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff
 
 let define_individual_scheme kind internal names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
@@ -149,13 +152,13 @@ let define_mutual_scheme_base kind suff f internal names mind =
       try List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
   let consts = Array.map2 (define internal) ids cl in
-  declare_scheme kind (Array.mapi (fun i cst -> ((mind,i),cst)) consts);
+  let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
+  declare_scheme kind schemes;
   consts,
-  Declareops.union_side_effects eff 
-    (Declareops.side_effects_of_list
-      (List.map 
-        (fun x -> Safe_typing.sideff_of_con (Global.safe_env()) x)
-        (Array.to_list consts)))
+  Declareops.cons_side_effects 
+    (Safe_typing.sideff_of_scheme
+      kind (Global.safe_env()) (Array.to_list schemes))
+    eff 
 
 let define_mutual_scheme kind internal names mind =
   match Hashtbl.find scheme_object_table kind with
@@ -163,9 +166,12 @@ let define_mutual_scheme kind internal names mind =
   | s,MutualSchemeFunction f ->
       define_mutual_scheme_base kind s f internal names mind
 
+let find_scheme_on_env_too kind ind =
+  String.Map.find kind (Indmap.find ind !scheme_map)
+
 let find_scheme kind (mind,i as ind) =
   try 
-    let s = String.Map.find kind (Indmap.find ind !scheme_map) in
+    let s = find_scheme_on_env_too kind ind in
     s, Declareops.no_seff
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
@@ -176,6 +182,6 @@ let find_scheme kind (mind,i as ind) =
       ca.(i), eff
 
 let check_scheme kind ind =
-  try let _ = String.Map.find kind (Indmap.find ind !scheme_map) in true
+  try let _ = find_scheme_on_env_too kind ind in true
   with Not_found -> false