Merge PR #11269: Several cleanups and factorization in scheme declarations

Reviewed-by: SkySkimmer
Reviewed-by: ejgallego

7 files changed, 59 insertions, 53 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2998e1c767..ca5c8b30c2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -924,10 +924,10 @@ let reset_env env =
   let env' = Global.env_of_context (Environ.named_context_val env) in
     Environ.push_rel_context (Environ.rel_context env) env'
 
-let fold_match ?(force=false) env sigma c =
+let fold_match env sigma c =
   let (ci, p, c, brs) = destCase sigma c in
   let cty = Retyping.get_type_of env sigma c in
-  let dep, pred, exists, (sk,eff) =
+  let dep, pred, exists, sk =
     let env', ctx, body =
       let ctx, pred = decompose_lam_assum sigma p in
       let env' = push_rel_context ctx env in
@@ -954,8 +954,8 @@ let fold_match ?(force=false) env sigma c =
         else case_scheme_kind_from_type)
     in
     let exists = Ind_tables.check_scheme sk ci.ci_ind in
-      if exists || force then
-        dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind
+      if exists then
+        dep, pred, exists, Ind_tables.lookup_scheme sk ci.ci_ind
       else raise Not_found
   in
   let app =
@@ -964,7 +964,7 @@ let fold_match ?(force=false) env sigma c =
     let meths = List.map (fun br -> br) (Array.to_list brs) in
       applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
   in
-    sk, (if exists then env else reset_env env), app, eff
+    sk, (if exists then env else reset_env env), app
 
 let unfold_match env sigma sk app =
   match EConstr.kind sigma app with
@@ -1222,7 +1222,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
             else
               match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
               | None -> state, c'
-              | Some (cst, _, t', eff (*FIXME*)) ->
+              | Some (cst, _, t') ->
                  let state, res = aux { state ; env ; unfresh ;
                                         term1 = t' ; ty1 = ty ;
                                         cstr = (prop,cstr) ; evars } in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 51f01888aa..d6fda00ad8 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -24,14 +24,14 @@ open Ind_tables
 
 (* Induction/recursion schemes *)
 
-let optimize_non_type_induction_scheme kind dep sort _ ind =
+let optimize_non_type_induction_scheme kind dep sort ind =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   if check_scheme kind ind then
     (* in case the inductive has a type elimination, generates only one
        induction scheme, the other ones share the same code with the
        appropriate type *)
-    let cte, eff = find_scheme kind ind in
+    let cte = lookup_scheme kind ind in
     let sigma, cte = Evd.fresh_constant_instance env sigma cte in
     let c = mkConstU cte in
     let t = type_of_constant_in (Global.env()) cte in
@@ -47,11 +47,11 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
     let sigma, sort = Evd.fresh_sort_in_family sigma sort in
     let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
     let sigma = Evd.minimize_universes sigma in
-    (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff
+    (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma)
   else
     let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
     let sigma, c = build_induction_scheme env sigma pind dep sort in
-      (c, Evd.evar_universe_context sigma), Evd.empty_side_effects
+      (c, Evd.evar_universe_context sigma)
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
@@ -60,17 +60,23 @@ let build_induction_scheme_in_type dep sort ind =
   let sigma, c = build_induction_scheme env sigma pind dep sort in
     c, Evd.evar_universe_context sigma
 
+let declare_individual_scheme_object name ?aux f =
+  let f : individual_scheme_object_function =
+    fun _ ind -> f ind, Evd.empty_side_effects
+  in
+  declare_individual_scheme_object name ?aux f
+
 let rect_scheme_kind_from_type =
   declare_individual_scheme_object "_rect_nodep"
-    (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects)
+    (fun x -> build_induction_scheme_in_type false InType x)
 
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
-    (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects)
+    (fun x -> build_induction_scheme_in_type false InType x)
 
 let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
-    (fun _ x -> build_induction_scheme_in_type true InType x, Evd.empty_side_effects)
+    (fun x -> build_induction_scheme_in_type true InType x)
 
 let rec_scheme_kind_from_type =
   declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
@@ -90,7 +96,7 @@ let ind_scheme_kind_from_type =
 
 let sind_scheme_kind_from_type =
   declare_individual_scheme_object "_sind_nodep"
-  (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects)
+  (fun x -> build_induction_scheme_in_type false InSProp x)
 
 let ind_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
@@ -98,7 +104,7 @@ let ind_dep_scheme_kind_from_type =
 
 let sind_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_sind" ~aux:"_sind_from_type"
-  (fun _ x -> build_induction_scheme_in_type true InSProp x, Evd.empty_side_effects)
+  (fun x -> build_induction_scheme_in_type true InSProp x)
 
 let ind_scheme_kind_from_prop =
   declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
@@ -106,7 +112,7 @@ let ind_scheme_kind_from_prop =
 
 let sind_scheme_kind_from_prop =
   declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop"
-  (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects)
+  (fun x -> build_induction_scheme_in_type false InSProp x)
 
 let nondep_elim_scheme from_kind to_kind =
   match from_kind, to_kind with
@@ -130,24 +136,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
-  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects)
+  (fun x -> build_case_analysis_scheme_in_type false InType x)
 
 let case_scheme_kind_from_prop =
   declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
-  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects)
+  (fun x -> build_case_analysis_scheme_in_type false InType x)
 
 let case_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_case" ~aux:"_case_from_type"
-  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects)
+  (fun x -> build_case_analysis_scheme_in_type true InType x)
 
 let case_dep_scheme_kind_from_type_in_prop =
   declare_individual_scheme_object "_casep_dep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects)
+  (fun x -> build_case_analysis_scheme_in_type true InProp x)
 
 let case_dep_scheme_kind_from_prop =
   declare_individual_scheme_object "_case_dep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects)
+  (fun x -> build_case_analysis_scheme_in_type true InType x)
 
 let case_dep_scheme_kind_from_prop_in_prop =
   declare_individual_scheme_object "_casep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects)
+  (fun x -> build_case_analysis_scheme_in_type true InProp x)
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 093a4c456b..8e167b171c 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -12,14 +12,6 @@ open Ind_tables
 
 (** Induction/recursion schemes *)
 
-val optimize_non_type_induction_scheme :
-  'a Ind_tables.scheme_kind ->
-  Indrec.dep_flag ->
-  Sorts.family ->
-  'b ->
-  Names.inductive ->
-  (Constr.constr * UState.t) * Evd.side_effects
-
 val rect_scheme_kind_from_prop : individual scheme_kind
 val ind_scheme_kind_from_prop : individual scheme_kind
 val sind_scheme_kind_from_prop : individual scheme_kind
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 9c94f3c319..517ccfaf53 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -82,10 +82,9 @@ let is_visible_name id =
   with Not_found -> false
 
 let compute_name internal id =
-  match internal with
-  | UserAutomaticRequest | UserIndividualRequest -> id
-  | InternalTacticRequest ->
-      Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
+  if internal then
+    Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
+  else id
 
 let define internal role id c poly univs =
   let id = compute_name internal id in
@@ -94,10 +93,7 @@ let define internal role id c poly univs =
   let univs = UState.univ_entry ~poly ctx in
   let entry = Declare.pure_definition_entry ~univs c in
   let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
-  let () = match internal with
-    | InternalTacticRequest -> ()
-    | _-> Declare.definition_message id
-  in
+  let () = if internal then () else Declare.definition_message id in
   kn, eff
 
 let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
@@ -107,7 +103,8 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
   let role = Evd.Schema (ind, kind) in
-  let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in
+  let internal = mode == InternalTacticRequest in
+  let const, neff = define internal role id c (Declareops.inductive_is_polymorphic mib) ctx in
   DeclareScheme.declare_scheme kind [|ind,const|];
   const, Evd.concat_side_effects neff eff
 
@@ -125,7 +122,8 @@ let define_mutual_scheme_base kind suff f mode names mind =
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
   let fold i effs id cl =
     let role = Evd.Schema ((mind, i), kind)in
-    let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in
+    let internal = mode == InternalTacticRequest in
+    let cst, neff = define internal role id cl (Declareops.inductive_is_polymorphic mib) ctx in
     (Evd.concat_side_effects neff effs, cst)
   in
   let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in
@@ -153,6 +151,14 @@ let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
       let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
       ca.(i), eff
 
+let define_individual_scheme kind mode names ind =
+  ignore (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 7e544b09dc..d886fb67d3 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -45,15 +45,17 @@ val declare_individual_scheme_object : string -> ?aux:string ->
 
 val define_individual_scheme : individual scheme_kind ->
   internal_flag (** internal *) ->
-  Id.t option -> inductive -> Constant.t * Evd.side_effects
+  Id.t option -> inductive -> unit
 
 val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
-  (int * Id.t) list -> MutInd.t -> Constant.t array * Evd.side_effects
+  (int * Id.t) list -> MutInd.t -> unit
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
 val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects
 
 val check_scheme : 'a scheme_kind -> inductive -> bool
 
+(** Like [find_scheme] but fails when the scheme is not already in the cache *)
+val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t
 
 val pr_scheme_kind : 'a scheme_kind -> Pp.t
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 310ea62a1d..f954915cf8 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -430,7 +430,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
   end
 
 (* used in the bool -> leb side *)
-let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
+let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   let open EConstr in
   let avoid = Array.of_list aavoid in
   let do_arg sigma hd v offset =
@@ -658,7 +658,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                               if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type")
                               then
                                 Tacticals.New.tclTHEN
-                                  (do_replace_bl mode bl_scheme_key ind
+                                  (do_replace_bl bl_scheme_key ind
                                      (!avoid)
                                      nparrec (ca.(2))
                                      (ca.(1)))
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b2e1a5e796..2f0b1062a7 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -210,7 +210,7 @@ let declare_one_case_analysis_scheme ind =
        induction scheme, the other ones share the same code with the
        appropriate type *)
   if Sorts.family_leq InType kelim then
-    ignore (define_individual_scheme dep UserAutomaticRequest None ind)
+    define_individual_scheme dep UserAutomaticRequest None ind
 
 (* Induction/recursion schemes *)
 
@@ -248,7 +248,7 @@ let declare_one_induction_scheme ind =
        else if depelim then kinds_from_type
        else nondep_kinds_from_type)
   in
-  List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
+  List.iter (fun kind -> define_individual_scheme kind UserAutomaticRequest None ind)
     elims
 
 let declare_induction_schemes kn =
@@ -264,7 +264,7 @@ let declare_induction_schemes kn =
 let declare_eq_decidability_gen internal names kn =
   let mib = Global.lookup_mind kn in
   if mib.mind_finite <> Declarations.CoFinite then
-    ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
+    define_mutual_scheme eq_dec_scheme_kind internal names kn
 
 let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
   str "Decidable equality on " ++ quote (Printer.pr_inductive (Global.env()) ind)
@@ -280,14 +280,14 @@ let try_declare_eq_decidability kn =
 let declare_eq_decidability = declare_eq_decidability_scheme_with []
 
 let ignore_error f x =
-  try ignore (f x) with e when CErrors.noncritical e -> ()
+  try f x with e when CErrors.noncritical e -> ()
 
 let declare_rewriting_schemes ind =
   if Hipattern.is_inductive_equality ind then begin
-    ignore (define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind);
-    ignore (define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind);
-    ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
-      UserAutomaticRequest None ind);
+    define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind;
+    define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind;
+    define_individual_scheme rew_r2l_forward_dep_scheme_kind
+      UserAutomaticRequest None ind;
     (* These ones expect the equality to be symmetric; the first one also *)
     (* needs eq *)
     ignore_error (define_individual_scheme rew_l2r_scheme_kind UserAutomaticRequest None) ind;
@@ -310,7 +310,7 @@ let declare_congr_scheme ind =
       try Coqlib.check_required_library Coqlib.logic_module_name; true
       with e when CErrors.noncritical e -> false
     then
-      ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
+      define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind
     else
       warn_cannot_build_congruence ()
   end