Remove dynamic scheme generation

doc/changelog/04-tactics/22192-noforce-scheme-Removed.rst

@@ -0,0 +1,4 @@
+- **Removed:**
+  automatic scheme generation by :tacn:`rewrite`
+  (`#22192 <https://github.com/rocq-prover/rocq/pull/22192>`_,
+  by Gaëtan Gilbert).

engine/evd.ml

@@ -356,15 +356,11 @@ type evar_flags =
     rewrite_rule_evars : Evar.Set.t;
   }
 
-type side_effect_role =
-| Schema of inductive * string
-
 type side_effects = {
   seff_safeenv : Safe_typing.safe_environment option;
   (* If seff_safeenv = Some senv, then senv = Global.safe_env + seff_private *)
   seff_labels : Id.Set.t;
   seff_private : Safe_typing.private_constants;
-  seff_roles : side_effect_role Cmap_env.t;
   seff_univs : UState.named_universes_entry Cmap_env.t;
 }
 
@@ -871,7 +867,6 @@ let empty_side_effects = {
   seff_safeenv = None;
   seff_labels = Id.Set.empty;
   seff_private = Safe_typing.empty_private_constants;
-  seff_roles = Cmap_env.empty;
   seff_univs = Cmap_env.empty;
 }
 
@@ -1259,7 +1254,6 @@ let concat_side_effects eff1 eff2 = {
   seff_safeenv = None;
   seff_labels = Id.Set.fold Id.Set.add eff1.seff_labels eff2.seff_labels;
   seff_private = Safe_typing.concat_private eff1.seff_private eff2.seff_private;
-  seff_roles = Cmap_env.fold Cmap_env.add eff1.seff_roles eff2.seff_roles;
   seff_univs = Cmap_env.fold Cmap_env.add eff1.seff_univs eff2.seff_univs;
 }
 
@@ -1275,7 +1269,7 @@ let set_side_effects eff evd =
 
 let eval_side_effects evd = evd.effects
 
-let push_side_effects ?role ?ts name de ctx effs =
+let push_side_effects ?ts name de ctx effs =
   let senv = get_senv_side_effects effs in
   let senv = match ts with
   | None -> senv
@@ -1287,14 +1281,9 @@ let push_side_effects ?role ?ts name de ctx effs =
     else
       Cmap_env.add kn (UState.Monomorphic_entry ctx, UnivNames.empty_binders) effs.seff_univs
   in
-  let seff_roles = match role with
-  | None -> effs.seff_roles
-  | Some r -> Cmap_env.add kn r effs.seff_roles
-  in
   let effs = {
     seff_private = Safe_typing.concat_private prv effs.seff_private;
     seff_labels = Id.Set.add (Constant.label kn) effs.seff_labels;
-    seff_roles = seff_roles;
     seff_univs = seff_univs;
     seff_safeenv = Some senv;
   } in
@@ -1309,7 +1298,6 @@ let seff_mem_label id effs =
   Id.Set.mem id effs.seff_labels
 
 let seff_private eff = eff.seff_private
-let seff_roles effs = effs.seff_roles
 let seff_univs effs = effs.seff_univs
 
 (* Future goals *)

engine/evd.mli

@@ -396,9 +396,6 @@ val dependent_evar_ident : Evar.t -> evar_map -> Id.t
 
 (** {5 Side-effects} *)
 
-type side_effect_role =
-| Schema of inductive * string
-
 type side_effects
 
 val empty_side_effects : side_effects
@@ -415,7 +412,7 @@ val eval_side_effects : evar_map -> side_effects
 (** Return the effects contained in the evar map. *)
 
 val push_side_effects :
-  ?role:side_effect_role -> ?ts:Conv_oracle.oracle ->
+  ?ts:Conv_oracle.oracle ->
   Id.t -> Safe_typing.side_effect_declaration -> Univ.ContextSet.t ->
   side_effects -> Constant.t * side_effects
 
@@ -425,7 +422,6 @@ val avoid_side_effect_label : Id.t -> evar_map -> evar_map
 
 val seff_mem_label : Id.t -> side_effects -> bool
 val seff_private : side_effects -> Safe_typing.private_constants
-val seff_roles : side_effects -> side_effect_role Cmap_env.t
 val seff_univs : side_effects -> UState.named_universes_entry Names.Cmap_env.t
 
 (** {5 Future goals} *)

tactics/equality.ml

@@ -467,41 +467,30 @@ let lookup_eq_eliminator_opt env sigma eq ~dep het_eq ~inccl l2r ~c_sort ~e_sort
 
 type eq_scheme_kind = Minimality of UnivGen.QualityOrSet.t | Rewriting | Equality
 
-let warn_missing_scheme = CWarnings.create ~name:"missing-scheme" ~category:Deprecation.Version.v9_2
-    Pp.(fun (kind,name,ind) ->
-        let ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) in
-        let cmd () = match kind with
-          | Minimality s ->
-            fmt "Scheme Minimality for %t Sort %t"
-              (const ind) (fun () -> UnivGen.QualityOrSet.raw_pr s)
-          | Rewriting -> fmt "Scheme Rewriting for %t" (const ind)
-          | Equality -> fmt "Scheme Equality for %t" (const ind)
-        in
-        hv 0 @@ fmt "Autogenerated \"%s\" scheme for %t.@ Use \"%t\" to explicitly generate it.@ This will become an error in the future."
-          name (const ind) cmd)
-
-let warn_missing_scheme = function
-  | None -> Proofview.tclUNIT()
-  | Some warn ->
-    Proofview.tclUNIT() >>= fun () ->
-    try warn_missing_scheme warn; Proofview.tclUNIT()
-    with e when CErrors.noncritical e ->
-      let e, info = Exninfo.capture e in
-      Proofview.tclZERO ~info e
+exception MissingScheme of eq_scheme_kind * string * inductive
+
+let () = CErrors.register_handler @@ function
+  | MissingScheme (kind,name,ind) ->
+    let ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) in
+    let cmd () = match kind with
+      | Minimality s ->
+        fmt "Scheme Minimality for %t Sort %t"
+          (const ind) (fun () -> UnivGen.QualityOrSet.raw_pr s)
+      | Rewriting -> fmt "Scheme Rewriting for %t" (const ind)
+      | Equality -> fmt "Scheme Equality for %t" (const ind)
+    in
+    let msg = hv 0 @@ fmt "Missing \"%s\" scheme for %t.@ Use \"%t\" to explicitly generate it.@ This will become an error in the future."
+        name (const ind) cmd
+    in
+    Some msg
+  | _ -> None
 
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. *)
 let find_scheme kind scheme_name ind =
-  find_scheme scheme_name ind >>= function
-    | Some s -> Proofview.tclUNIT (s,None)
-    | None ->
-      force_find_scheme scheme_name ind >>= fun s ->
-      (* We delay the warning to avoid printing it if the rewrite
-         fails (compatible with the future behaviour where the missing
-         scheme is always error). Typically for [rewrite ?lem] where
-         [lem] is sometimes a proof of equality and sometimes not
-         rewriteable. *)
-      Proofview.tclUNIT (s, Some (kind, Ind_tables.scheme_kind_name scheme_name, ind))
+  match lookup_scheme scheme_name ind with
+  | Some s -> Proofview.tclUNIT s
+  | None -> Proofview.tclZERO (MissingScheme (kind,Ind_tables.scheme_kind_name scheme_name,ind))
 
 let find_elim lft2rgt dep inccl type_of_cls (ctx, hdcncl, args) =
   Proofview.Goal.enter_one begin fun gl ->
@@ -510,10 +499,10 @@ let find_elim lft2rgt dep inccl type_of_cls (ctx, hdcncl, args) =
   let gen_elim () =
      match EConstr.kind sigma hdcncl with
     | Ind (ind,u) ->
-      find_scheme Rewriting (scheme_name dep lft2rgt inccl) ind >>= fun (elim,warn) ->
+      find_scheme Rewriting (scheme_name dep lft2rgt inccl) ind >>= fun elim ->
       Proofview.tclEVARMAP >>= fun sigma ->
       let (sigma, gref) = Evd.fresh_global env sigma elim in
-      Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (gref, UnknownPosition, warn)
+      Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (gref, UnknownPosition)
     | _ -> assert false
   in
   let nb_args = List.length args in
@@ -528,7 +517,7 @@ let find_elim lft2rgt dep inccl type_of_cls (ctx, hdcncl, args) =
     let p_sort = Retyping.get_sort_of env sigma type_of_cls in
     match lookup_eq_eliminator_opt env sigma hdcncl maybe_het_eq ~dep ~inccl lft2rgt ~c_sort ~e_sort ~p_sort with
     | Some ((sigma, c),indarg) ->
-        Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (c, indarg, None)
+        Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (c, indarg)
     | None -> gen_elim ()
   else
     gen_elim ()
@@ -542,10 +531,9 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c ((_, hdcncl, _) as t) l w
   | Some id -> Tacmach.pf_get_hyp_typ id gl in
   let dep = dep_proof_ok && dependent_no_evar evd c type_of_cls in
   let inccl = Option.is_empty cls in
-  find_elim lft2rgt dep inccl type_of_cls t >>= fun (elim, indarg, warn) ->
+  find_elim lft2rgt dep inccl type_of_cls t >>= fun (elim, indarg) ->
       general_elim_clause with_evars frzevars tac cls c t l
-        lft2rgt elim indarg >>= fun () ->
-      warn_missing_scheme warn
+        lft2rgt elim indarg
   end
 
 let adjust_rewriting_direction args lft2rgt =
@@ -1395,7 +1383,7 @@ let inject_if_homogenous_dependent_pair ty =
       | Some v -> v
     in
     let new_eq_args = [|Retyping.get_type_of env sigma ar1.(3);ar1.(3);ar2.(3)|] in
-    find_scheme Equality (!eq_dec_scheme_kind_name()) ind >>= fun (c, warn) ->
+    find_scheme Equality (!eq_dec_scheme_kind_name()) ind >>= fun c ->
     let sigma, c = fresh_global env sigma c in
     (* cut with the good equality and prove the requested goal *)
     tclTHENLIST
@@ -1409,7 +1397,7 @@ let inject_if_homogenous_dependent_pair ty =
            Tactics.exact_check
              (mkApp(inj2,[|ar1.(0);c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))
           ]);
-       warn_missing_scheme warn]
+     ]
   with Exit ->
     Proofview.tclUNIT ()
   end

tactics/ind_tables.ml

@@ -24,12 +24,21 @@ open Util
 (**********************************************************************)
 (* Registering schemes in the environment *)
 
-type handle = Evd.side_effects
+type side_effect_role =
+| Schema of inductive * string
+
+type schemes = {
+  sch_eff : Evd.side_effects;
+  sch_roles : side_effect_role Cmap_env.t;
+  sch_reg : (Id.t * Constant.t * Loc.t option * UState.named_universes_entry) list;
+}
+
+type handle = schemes
 
 let push_handle eff =
   let open Proofview.Notations in
   Proofview.tclEVARMAP >>= fun sigma ->
-  let sigma = Evd.emit_side_effects eff sigma in
+  let sigma = Evd.emit_side_effects eff.sch_eff sigma in
   Proofview.Unsafe.tclEVARS sigma
 
 type mutual_scheme_object_function =
@@ -97,7 +106,7 @@ let compute_name internal id avoid =
     Namegen.next_ident_away_from (add_prefix "internal_" id) visible
   else id
 
-let declare_definition_scheme = ref (fun ~univs ~role ~name ~effs c ->
+let declare_definition_scheme = ref (fun ~univs ~name ~effs c ->
     CErrors.anomaly (Pp.str "scheme declaration not registered"))
 
 let register_definition_scheme = ref (fun ~internal ~name ~const ~univs ?loc () ->
@@ -106,43 +115,40 @@ let register_definition_scheme = ref (fun ~internal ~name ~const ~univs ?loc ()
 let lookup_scheme kind ind =
   try Some (DeclareScheme.lookup_scheme kind (GlobRef.IndRef ind)) with Not_found -> None
 
-type schemes = {
-  sch_eff : Evd.side_effects;
-  sch_reg : (Id.t * Constant.t * Loc.t option * UState.named_universes_entry) list;
-}
-
 let empty_schemes eff = {
   sch_eff = eff;
   sch_reg = [];
+  sch_roles = Cmap_env.empty;
 }
 
-let redeclare_schemes { sch_eff = eff } =
+let redeclare_schemes { sch_eff = eff; sch_roles = roles } =
   let fold c role accu = match role with
-  | Evd.Schema (ind, kind) ->
+  | Schema (ind, kind) ->
     try
       let _ = DeclareScheme.lookup_scheme kind (GlobRef.IndRef ind) in
       accu
     with Not_found ->
       let old = try String.Map.find kind accu with Not_found -> [] in
       String.Map.add kind ((GlobRef.IndRef ind, GlobRef.ConstRef c) :: old) accu
   in
-  let schemes = Cmap_env.fold fold (Evd.seff_roles eff) String.Map.empty in
+  let schemes = Cmap_env.fold fold roles String.Map.empty in
   let iter kind defs = List.iter (DeclareScheme.declare_scheme SuperGlobal kind) defs in
   String.Map.iter iter schemes
 
-let local_lookup_scheme eff kind ind = match lookup_scheme kind ind with
+let local_lookup_scheme { sch_roles = roles } kind ind =
+  match lookup_scheme kind ind with
 | Some _ as ans -> ans
 | None ->
   let exception Found of Constant.t in
   let iter c role = match role with
-  | Evd.Schema (i, k) ->
+  | Schema (i, k) ->
     if String.equal k kind && Ind.UserOrd.equal i ind then raise (Found c)
   in
   (* Inefficient O(n), but the number of locally declared schemes is small and
      this is very rarely called *)
-  try let _ = Cmap_env.iter iter (Evd.seff_roles eff) in None with Found c -> Some (GlobRef.ConstRef c)
+  try let _ = Cmap_env.iter iter roles in None with Found c -> Some (GlobRef.ConstRef c)
 
-let local_check_scheme kind ind { sch_eff = eff } =
+let local_check_scheme kind ind eff =
   Option.has_some (local_lookup_scheme eff kind ind)
 
 let define ?loc internal role id c poly uctx sch =
@@ -156,9 +162,10 @@ let define ?loc internal role id c poly uctx sch =
   let uctx = UState.restrict uctx (Vars.universes_of_constr c) in
   let univs = UState.univ_entry ~poly uctx in
   let effs = sch.sch_eff in
-  let cst, effs = !declare_definition_scheme ~univs ~role ~name:id ~effs c in
+  let cst, effs = !declare_definition_scheme ~univs ~name:id ~effs c in
   let reg = (id, cst, loc, univs) :: sch.sch_reg in
-  cst, { sch_eff = effs; sch_reg = reg }
+  let roles = Cmap_env.add cst role sch.sch_roles in
+  cst, { sch_eff = effs; sch_reg = reg; sch_roles = roles  }
 
 module Locmap : sig
 
@@ -209,12 +216,12 @@ let globally_declare_schemes sch =
 (* Assumes that dependencies are already defined *)
 let rec define_individual_scheme_base ?loc kind suff f ~internal idopt (mind,i as ind) eff =
   let env = get_env eff in
-  let (c, ctx) = f env eff.sch_eff ind in
+  let (c, ctx) = f env eff ind in
   let mib = Environ.lookup_mind mind env in
   let id = match idopt with
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename ("_"^suff) in
-  let role = Evd.Schema (ind, kind) in
+  let role = Schema (ind, kind) in
   let poly, cumulative = Declareops.inductive_is_polymorphic mib, Declareops.inductive_is_cumulative mib in
   let poly = PolyFlags.make ~univ_poly:poly ~cumulative ~collapse_sort_variables:true in
   let const, eff = define ?loc internal role id c poly ctx eff in
@@ -233,13 +240,13 @@ and define_individual_scheme ?loc kind ~internal names (mind,i as ind) eff =
 (* Assumes that dependencies are already defined *)
 and define_mutual_scheme_base ?(locmap=Locmap.default None) kind suff f ~internal names mind eff =
   let env = get_env eff in
-  let (cl, ctx) = f env eff.sch_eff mind in
+  let (cl, ctx) = f env eff mind in
   let mib = Environ.lookup_mind mind env in
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
       try Int.List.assoc i names
       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 role = Schema ((mind, i), kind)in
     let loc = Locmap.lookup ~locmap (mind,i) in
     (* FIXME cumulativity not supported? *)
     let poly = PolyFlags.of_univ_poly (Declareops.inductive_is_polymorphic mib) in
@@ -268,44 +275,6 @@ match sd with
   if local_check_scheme kind (mind, 0) eff then eff
   else define_mutual_scheme kind ~internal:true [] mind eff
 
-let find_scheme kind (mind,i as ind) =
-  let open Proofview.Notations in
-  Proofview.tclEVARMAP >>= fun sigma ->
-  let s = local_lookup_scheme (Evd.eval_side_effects sigma) kind ind in
-  Proofview.tclUNIT s
-
-let force_find_scheme kind (mind,i as ind) =
-  let open Proofview.Notations in
-  Proofview.tclEVARMAP >>= fun sigma ->
-  let eff = Evd.eval_side_effects sigma in
-  match local_lookup_scheme eff kind ind with
-  | Some s ->
-    Proofview.tclUNIT s
-  | None ->
-    let senv = Evd.get_senv_side_effects eff in
-    try
-      let eff, ans = match Hashtbl.find scheme_object_table kind with
-      | s,IndividualSchemeFunction (f, deps) ->
-        let env = Safe_typing.env_of_safe_env senv in
-        let deps = match deps with None -> [] | Some deps -> deps env ind in
-        let sch = empty_schemes eff in
-        let eff = List.fold_left (fun eff dep -> declare_scheme_dependence eff dep) sch deps in
-        let c, eff = define_individual_scheme_base kind s f ~internal:true None ind eff in
-        eff, c
-      | s,MutualSchemeFunction (f, deps) ->
-        let env = Safe_typing.env_of_safe_env senv in
-        let deps = match deps with None -> [] | Some deps -> deps env mind in
-        let sch = empty_schemes eff in
-        let eff = List.fold_left (fun eff dep -> declare_scheme_dependence eff dep) sch deps in
-        let ca, eff = define_mutual_scheme_base kind s f ~internal:true [] mind eff in
-        eff, ca.(i)
-      in
-      let sigma = Evd.emit_side_effects eff.sch_eff sigma in
-      Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (GlobRef.ConstRef ans)
-    with Rocqlib.NotFoundRef _ as e ->
-      let e, info = Exninfo.capture e in
-      Proofview.tclZERO ~info e
-
 let register_schemes sch =
   let iter (id, kn, loc, univs) =
     !register_definition_scheme ~internal:false ~name:id ~const:kn ~univs ?loc ()