Stop relying on side-effects for recursive scheme declaration.

Instead, we register functions dynamically declaring the dependencies of the
scheme to be generated.

We had to fix the test-suite because an internal scheme name changed.
We could also tweak the internal flag of scheme dependencies, but in this
particular case it looks more like a bug from the previous implementation.

5 files changed, 91 insertions, 52 deletions

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 910e042e7a..b08f4c8be7 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -62,7 +62,7 @@ let build_induction_scheme_in_type dep sort ind =
 
 let declare_individual_scheme_object name ?aux f =
   let f : individual_scheme_object_function =
-    fun _ ind -> f ind, Evd.empty_side_effects
+    fun _ ind -> f ind
   in
   declare_individual_scheme_object name ?aux f
 
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 98da61781e..000896bfea 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -229,7 +229,7 @@ let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
   (fun _ ind ->
     let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
-      (c, ctx), Evd.empty_side_effects)
+      (c, ctx))
 
 (**********************************************************************)
 (* Build the involutivity of symmetry for an inductive type           *)
@@ -248,17 +248,18 @@ let sym_scheme_kind =
 (**********************************************************************)
 
 let const_of_scheme kind env ind ctx =
-  let sym_scheme, eff = (find_scheme kind ind) in
+  let () = assert (check_scheme kind ind) in
+  let sym_scheme = lookup_scheme kind ind in
   let sym, ctx = with_context_set ctx
     (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in
-    mkConstU sym, ctx, eff
+    mkConstU sym, ctx
 
 let build_sym_involutive_scheme env ind =
   let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let eq,eqrefl,ctx = get_coq_eq ctx in
-  let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
+  let sym, ctx = const_of_scheme sym_scheme_kind env ind ctx in
   let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect mkRel n paramsctxt) in
   let inds = snd (mind_arity mip) in
   let indr = Sorts.relevance_of_sort_family inds in
@@ -297,10 +298,11 @@ let build_sym_involutive_scheme env ind =
                mkRel 1|])),
                mkRel 1 (* varH *),
                [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
-  in (c, UState.of_context_set ctx), eff
+  in (c, UState.of_context_set ctx)
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "_sym_involutive"
+  ~deps:(fun ind -> [SchemeIndividualDep (ind, sym_scheme_kind)])
   (fun _ ind ->
     build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
 
@@ -368,8 +370,8 @@ let build_l2r_rew_scheme dep env ind kind =
   let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
-  let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
-  let sym_involutive, ctx, eff' = const_of_scheme sym_involutive_scheme_kind env ind ctx in
+  let sym, ctx = const_of_scheme sym_scheme_kind env ind ctx in
+  let sym_involutive, ctx = const_of_scheme sym_involutive_scheme_kind env ind ctx in
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
@@ -454,8 +456,7 @@ let build_l2r_rew_scheme dep env ind kind =
        [|main_body|])
    else
      main_body))))))
-  in (c, UState.of_context_set ctx),
-      Evd.concat_side_effects eff' eff
+  in (c, UState.of_context_set ctx)
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -698,6 +699,10 @@ let build_r2l_rew_scheme dep env ind k =
 (**********************************************************************)
 let rew_l2r_dep_scheme_kind =
   declare_individual_scheme_object "_rew_r_dep"
+  ~deps:(fun ind -> [
+    SchemeIndividualDep (ind, sym_scheme_kind);
+    SchemeIndividualDep (ind, sym_involutive_scheme_kind);
+  ])
   (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
@@ -708,7 +713,7 @@ let rew_l2r_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_dep_scheme_kind =
   declare_individual_scheme_object "_rew_dep"
-  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
+  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in hypotheses                 *)
@@ -718,7 +723,7 @@ let rew_r2l_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_dep"
-  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
+  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
 (* Dependent rewrite from left-to-right in hypotheses                 *)
@@ -728,7 +733,7 @@ let rew_r2l_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_r_dep"
-  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
+  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either left-to-right in conclusion or   *)
@@ -742,7 +747,7 @@ let rew_l2r_forward_dep_scheme_kind =
 let rew_l2r_scheme_kind =
   declare_individual_scheme_object "_rew_r"
   (fun _ ind -> fix_r2l_forward_rew_scheme
-     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Evd.empty_side_effects)
+     (build_r2l_forward_rew_scheme false (Global.env()) ind InType))
 
 (**********************************************************************)
 (* Non-dependent rewrite from either right-to-left in conclusion or   *)
@@ -752,7 +757,7 @@ let rew_l2r_scheme_kind =
 (**********************************************************************)
 let rew_r2l_scheme_kind =
   declare_individual_scheme_object "_rew"
-  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Evd.empty_side_effects)
+  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType)
 
 (* End of rewriting schemes *)
 
@@ -835,5 +840,4 @@ let build_congr env (eq,refl,ctx) ind =
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
   (fun _ ind ->
      (* May fail if equality is not defined *)
-   build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind,
-   Evd.empty_side_effects)
+   build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index d1038f2655..6447708ace 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -27,7 +27,7 @@ val rew_r2l_scheme_kind : individual scheme_kind
 val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family ->
   constr Evd.in_evar_universe_context
 val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family ->
-  constr Evd.in_evar_universe_context * Evd.side_effects
+  constr Evd.in_evar_universe_context
 val build_r2l_forward_rew_scheme :
   bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context
 val build_l2r_forward_rew_scheme :
@@ -39,7 +39,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context
 val sym_scheme_kind : individual scheme_kind
 
 val build_sym_involutive_scheme : env -> inductive ->
-  constr Evd.in_evar_universe_context * Evd.side_effects
+  constr Evd.in_evar_universe_context
 val sym_involutive_scheme_kind : individual scheme_kind
 
 (** Builds a congruence scheme for an equality type *)
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e422366ed6..511cbb8b18 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -32,9 +32,9 @@ type internal_flag =
   | UserIndividualRequest   (* user action, a message is displayed *)
 
 type mutual_scheme_object_function =
-  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context
 
 type 'a scheme_kind = string
 
@@ -46,9 +46,13 @@ let pr_scheme_kind = Pp.str
 type individual
 type mutual
 
+type scheme_dependency =
+| SchemeMutualDep of MutInd.t * mutual scheme_kind
+| SchemeIndividualDep of inductive * individual scheme_kind
+
 type scheme_object_function =
-  | MutualSchemeFunction of mutual_scheme_object_function
-  | IndividualSchemeFunction of individual_scheme_object_function
+  | MutualSchemeFunction of mutual_scheme_object_function * (MutInd.t -> scheme_dependency list) option
+  | IndividualSchemeFunction of individual_scheme_object_function * (inductive -> scheme_dependency list) option
 
 let scheme_object_table =
   (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
@@ -68,11 +72,11 @@ let declare_scheme_object s aux f =
     Hashtbl.add scheme_object_table key (s,f);
     key
 
-let declare_mutual_scheme_object s ?(aux="") f =
-  declare_scheme_object s aux (MutualSchemeFunction f)
+let declare_mutual_scheme_object s ?deps ?(aux="") f =
+  declare_scheme_object s aux (MutualSchemeFunction (f, deps))
 
-let declare_individual_scheme_object s ?(aux="") f =
-  declare_scheme_object s aux (IndividualSchemeFunction f)
+let declare_individual_scheme_object s ?deps ?(aux="") f =
+  declare_scheme_object s aux (IndividualSchemeFunction (f, deps))
 
 (**********************************************************************)
 (* Defining/retrieving schemes *)
@@ -89,6 +93,10 @@ let compute_name internal id =
 let declare_definition_scheme = ref (fun ~internal ~univs ~role ~name c ->
     CErrors.anomaly (Pp.str "scheme declaration not registered"))
 
+let check_scheme kind ind =
+  try let _ = DeclareScheme.lookup_scheme kind ind in true
+  with Not_found -> false
+
 let define internal role id c poly univs =
   let id = compute_name internal id in
   let ctx = UState.minimize univs in
@@ -96,8 +104,9 @@ let define internal role id c poly univs =
   let univs = UState.univ_entry ~poly ctx in
   !declare_definition_scheme ~internal ~univs ~role ~name:id c
 
-let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
-  let (c, ctx), eff = f mode ind in
+(* Assumes that dependencies are already defined *)
+let rec define_individual_scheme_base kind suff f mode idopt (mind,i as ind) eff =
+  let (c, ctx) = f mode ind in
   let mib = Global.lookup_mind mind in
   let id = match idopt with
     | Some id -> id
@@ -105,17 +114,21 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let role = Evd.Schema (ind, kind) in
   let internal = mode == InternalTacticRequest in
   let const, neff = define internal role id c (Declareops.inductive_is_polymorphic mib) ctx in
+  let eff = Evd.concat_side_effects neff eff in
   DeclareScheme.declare_scheme kind [|ind,const|];
-  const, Evd.concat_side_effects neff eff
+  const, eff
 
-let define_individual_scheme kind mode names (mind,i as ind) =
+and define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
-  | _,MutualSchemeFunction f -> assert false
-  | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f mode names ind
-
-let define_mutual_scheme_base kind suff f mode names mind =
-  let (cl, ctx), eff = f mode mind in
+  | _,MutualSchemeFunction _ -> assert false
+  | s,IndividualSchemeFunction (f, deps) ->
+    let deps = match deps with None -> [] | Some deps -> deps ind in
+    let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
+    define_individual_scheme_base kind s f mode names ind eff
+
+(* Assumes that dependencies are already defined *)
+and define_mutual_scheme_base kind suff f mode names mind eff =
+  let (cl, ctx) = f mode mind in
   let mib = Global.lookup_mind mind in
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
       try Int.List.assoc i names
@@ -131,11 +144,25 @@ let define_mutual_scheme_base kind suff f mode names mind =
   DeclareScheme.declare_scheme kind schemes;
   consts, eff
 
-let define_mutual_scheme kind mode names mind =
+and define_mutual_scheme kind mode names mind =
   match Hashtbl.find scheme_object_table kind with
   | _,IndividualSchemeFunction _ -> assert false
-  | s,MutualSchemeFunction f ->
-      define_mutual_scheme_base kind s f mode names mind
+  | s,MutualSchemeFunction (f, deps) ->
+    let deps = match deps with None -> [] | Some deps -> deps mind in
+    let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
+    define_mutual_scheme_base kind s f mode names mind eff
+
+and declare_scheme_dependence mode eff = function
+| SchemeIndividualDep (ind, kind) ->
+  if check_scheme kind ind then eff
+  else
+    let _, eff' = define_individual_scheme kind mode None ind in
+    Evd.concat_side_effects eff' eff
+| SchemeMutualDep (mind, kind) ->
+  if check_scheme kind (mind, 0) then eff
+  else
+    let _, eff' = define_mutual_scheme kind mode [] mind in
+    Evd.concat_side_effects eff' eff
 
 let find_scheme_on_env_too kind ind =
   let s = DeclareScheme.lookup_scheme kind ind in
@@ -145,10 +172,14 @@ let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
-  | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f mode None ind
-  | s,MutualSchemeFunction f ->
-      let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
+  | s,IndividualSchemeFunction (f, deps) ->
+    let deps = match deps with None -> [] | Some deps -> deps ind in
+    let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
+    define_individual_scheme_base kind s f mode None ind eff
+  | s,MutualSchemeFunction (f, deps) ->
+    let deps = match deps with None -> [] | Some deps -> deps mind in
+    let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
+    let ca, eff = define_mutual_scheme_base kind s f mode [] mind eff in
       ca.(i), eff
 
 let define_individual_scheme kind mode names ind =
@@ -157,8 +188,4 @@ let define_individual_scheme kind mode names ind =
 let define_mutual_scheme kind mode names mind =
   ignore (define_mutual_scheme kind mode names mind)
 
-let check_scheme kind ind =
-  try let _ = find_scheme_on_env_too kind ind in true
-  with Not_found -> false
-
 let lookup_scheme = DeclareScheme.lookup_scheme
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 736de2af37..51f7ef9fd3 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -25,19 +25,27 @@ type internal_flag =
   | InternalTacticRequest
   | UserIndividualRequest
 
+type scheme_dependency =
+| SchemeMutualDep of MutInd.t * mutual scheme_kind
+| SchemeIndividualDep of inductive * individual scheme_kind
+
 type mutual_scheme_object_function =
-  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context
 
 (** Main functions to register a scheme builder. Note these functions
    are not safe to be used by plugins as their effects won't be undone
    on backtracking *)
 
-val declare_mutual_scheme_object : string -> ?aux:string ->
+val declare_mutual_scheme_object : string ->
+  ?deps:(MutInd.t -> scheme_dependency list) ->
+  ?aux:string ->
   mutual_scheme_object_function -> mutual scheme_kind
 
-val declare_individual_scheme_object : string -> ?aux:string ->
+val declare_individual_scheme_object : string ->
+  ?deps:(inductive -> scheme_dependency list) ->
+  ?aux:string ->
   individual_scheme_object_function ->
   individual scheme_kind