ind_tables: always declare side effects (Closes: HOTT#110)

declare takes care of ignoring side effects that are available in the
global environment.  This is yet another instance of what the "abominion"
(aka abstract) can do: the code was checking for the existence in the
environment of the elimination principle, and not regenerating it (nor
declaring the corresponding side effect) if the elimination principle
is used twice.
Of course to functionalize the imperative actions on the environment
when two proofs generated by abstract use the same elim principle,
such elim principle has to be inlined twice, once in each abstracted
proof.  In other words, a side effect generated by a tactic inside
an abstract is *global* but will be made local, si it must always
be declared, no matter what.

Now the system works like this:
- side effects are always declared, even if a caching mechanism thinks
  the constant is already there (it can be there, no need to regenerate it
  but the intent to generate it *must* be declared anyhow)
- at Qed time, we filter the list of side effects and decide which ones are
  really needed to be inlined.

bottom line: STOP using abstract.

5 files changed, 28 insertions, 14 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index dd906bab24..149eeba287 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -284,7 +284,7 @@ type side_effects = side_effect list
 let no_seff = ([] : side_effects)
 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 = l (** FIXME: there is something dubious here *)
+let uniquize_side_effects l = CList.uniquize l
 let union_side_effects l1 l2 = l1 @ l2
 let flatten_side_effects l = List.flatten l
 let side_effects_of_list l = l
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8c4ec8cbfc..770c720d89 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -64,6 +64,10 @@ let handle_side_effects env body side_eff =
     let cbl = match se with
       | SEsubproof (c,cb) -> [c,cb]
       | SEscheme (cl,_) -> List.map (fun (_,c,cb) -> c,cb) cl in
+    let not_exists (c,_) =
+      try ignore(Environ.lookup_constant c env); false
+      with Not_found -> true in 
+    let cbl = List.filter not_exists cbl in
     let cname c = 
       let name = string_of_con c in
       for i = 0 to String.length name - 1 do
diff --git a/library/declare.ml b/library/declare.ml
index 4364461ef5..dce346782c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -208,11 +208,11 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
 
 let declare_scheme = ref (fun _ _ -> assert false)
 let set_declare_scheme f = declare_scheme := f
-let declare_sideff fix_exn se =
+let declare_sideff env fix_exn 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
+        List.map (fun (_,c,cb) -> c,cb) cbl, Some (cbl,k) in
   let id_of c = Names.Label.to_id (Names.Constant.label c) in
   let pt_opaque_of cb =
     match cb with
@@ -243,13 +243,21 @@ let declare_sideff fix_exn se =
     cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
     cst_locl = true;
   } in
+  let exists c =
+    try ignore(Environ.lookup_constant c env); true
+    with Not_found -> false in 
   let knl =
-    List.map (fun (c,cb) ->
-      declare_constant_common (id_of c) (cst_of cb)) cbl in
+    CList.map_filter (fun (c,cb) ->
+      if exists c then None
+      else Some (c,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))
+  | Some (inds_consts,kind) ->
+      !declare_scheme kind (Array.of_list
+         (List.map (fun (c,kn) ->
+             CList.find_map (fun (x,c',_) ->
+               if Constant.equal c c' then Some (x,kn) else None) inds_consts)
+           knl))
 
 let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
   let cd = (* We deal with side effects of non-opaque constants *)
@@ -264,7 +272,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
         else begin
           let seff = Declareops.uniquize_side_effects seff in
           Declareops.iter_side_effects
-            (declare_sideff (Future.fix_exn_of bo)) seff;
+            (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
           Entries.DefinitionEntry { de with
             const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
               pt, Declareops.no_seff) }
diff --git a/test-suite/bugs/opened/HoTT_coq_110.v b/test-suite/bugs/closed/HoTT_coq_110.v
index c9874f898c..5ec40dbcb9 100644
--- a/test-suite/bugs/opened/HoTT_coq_110.v
+++ b/test-suite/bugs/closed/HoTT_coq_110.v
@@ -19,5 +19,5 @@ Module Y.
   Definition foo : (A = B) * (A = B).
     split; abstract (rewrite <- P; reflexivity).
   (* Error: internal_paths_rew already exists. *)
-  Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
-Fail End Y.
+  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+End Y.
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 1ee2adcd8c..1f09d76205 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -181,12 +181,14 @@ let define_mutual_scheme kind internal names mind =
       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 s = String.Map.find kind (Indmap.find ind !scheme_map) in
+  s, Declareops.cons_side_effects
+      (Safe_typing.sideff_of_scheme
+            kind (Global.safe_env()) [ind, s])
+      Declareops.no_seff 
 
 let find_scheme kind (mind,i as ind) =
-  try 
-    let s = find_scheme_on_env_too kind ind in
-    s, Declareops.no_seff
+  try find_scheme_on_env_too kind ind
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
   | s,IndividualSchemeFunction f ->