Enable rewrite rules for only opaque definitions

yannl35133 · yannl35133 · commit 55fa1175616b · 2026-01-21T15:21:23.000+01:00
diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml
@@ -10,7 +10,7 @@
 
 open Declarations
 
-let set_local_flags flags env =
+let set_local_flags ?type_mode flags env =
   (* Explicitly ignored flags are set to not change *)
   let envflags = Environ.typing_flags env in
   let flags = {
@@ -22,6 +22,7 @@ let set_local_flags flags env =
     share_reduction = flags.share_reduction;
     allow_uip = flags.allow_uip;
     enabled_rewrite_rules = flags.enabled_rewrite_rules;
+    enabled_rewrite_rules_type = flags.enabled_rewrite_rules_type;
     (* These flags may not *)
     enable_VM = envflags.enable_VM;
     enable_native_compiler = envflags.enable_native_compiler;
@@ -30,4 +31,4 @@ let set_local_flags flags env =
     sprop_allowed = envflags.sprop_allowed;
   }
   in
-  Environ.set_typing_flags flags env
+  Environ.set_typing_flags ?type_mode flags env
diff --git a/checker/checkFlags.mli b/checker/checkFlags.mli
@@ -8,5 +8,5 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val set_local_flags : Declarations.typing_flags -> Environ.env -> Environ.env
+val set_local_flags : ?type_mode:bool -> Declarations.typing_flags -> Environ.env -> Environ.env
 (** Set flags except for those ignored by the checker (see .ml file for those). *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
@@ -35,7 +35,7 @@ exception BadConstant of Constant.t * Pp.t
 
 let check_constant_declaration env opac kn cb opacify =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
-  let env = CheckFlags.set_local_flags cb.const_typing_flags env in
+  let env = CheckFlags.set_local_flags ~type_mode:true cb.const_typing_flags env in
   let poly, env =
     match cb.const_universes with
     | Monomorphic ->
@@ -53,9 +53,11 @@ let check_constant_declaration env opac kn cb opacify =
   let jty = Typeops.infer_type env ty in
   if not (Sorts.relevance_equal cb.const_relevance (Sorts.relevance_of_sort jty.utj_type))
   then raise Pp.(BadConstant (kn, str "incorrect const_relevance"));
+  let env = Environ.resync_rewrite_rules_body env in
+  let b = Environ.rewrite_rules_type_different env in
   let body, env = match cb.const_body with
-    | Undef _ | Primitive _ | Symbol _ -> None, env
-    | Def c -> Some c, env
+    | Undef _ | Primitive _ | Symbol _ -> assert (not b); None, env
+    | Def c -> assert (not b); Some c, env
     | OpaqueDef o ->
       let c, u = !indirect_accessor o in
       let env = match u, cb.const_universes with
diff --git a/checker/values.ml b/checker/values.ml
@@ -176,6 +176,7 @@ let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|]
 let v_ind = v_tuple "inductive" [|v_cst;v_int|]
 let v_cons = v_tuple "constructor" [|v_ind;v_int|]
 
+let v_rules = v_tuple "rewrite rule" [|v_dp; v_id|]
 
 (** kernel/univ *)
 let v_level_global = v_tuple "Level.Global.t" [|v_dp;v_string;v_int|]
@@ -357,7 +358,8 @@ let v_typing_flags =
   v_tuple "typing_flags"
     [|v_bool; v_bool; v_bool;
       v_oracle; v_bool; v_bool;
-      v_bool; v_bool; v_bool; v_bool; v_bool|]
+      v_bool; v_bool; v_bool; v_bool; v_bool;
+      v_opt (v_hset v_rules); v_opt (v_hset v_rules)|]
 
 let v_univs = v_sum "universes" 1 [|[|v_abs_context|]|]
 
@@ -543,7 +545,7 @@ let [_v_hpattern;v_elimination;_v_head_elim;_v_patarg] : _ Vector.t =
 let v_rewrule = v_tuple "rewrite_rule"
   [| v_tuple "nvars" [| v_int; v_int; v_int |]; v_pair v_instance_mask (v_list v_elimination); v_constr |]
 let v_rrb = v_tuple "rewrite_rules_body"
-  [| v_list (v_pair v_cst v_rewrule) |]
+  [| v_list (v_pair v_cst v_rewrule); v_bool |]
 
 let v_module_with_decl = v_sum "with_declaration" 0 [|
     [|v_list v_id; v_mp|];
diff --git a/kernel/constant_typing.ml b/kernel/constant_typing.ml
@@ -248,7 +248,7 @@ let infer_opaque ~sec_univs env entry =
   let env, usubst, _, univs = process_universes env entry.opaque_entry_universes in
   let typ = Vars.subst_univs_level_constr usubst entry.opaque_entry_type in
   let typj = Typeops.infer_type env typ in
-  let context = TyCtx (env, typj, entry.opaque_entry_secctx, usubst, univs) in
+  let context = TyCtx (Environ.resync_rewrite_rules_body env, typj, entry.opaque_entry_secctx, usubst, univs) in
   let def = OpaqueDef () in
   let typ = typj.utj_val in
   let hyps = used_section_variables env (Some entry.opaque_entry_secctx) None typ in
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
@@ -104,6 +104,9 @@ type typing_flags = {
   enabled_rewrite_rules: RRset.t option;
   (** Enabled rewrite rules ([None] means rewrite rules are not allowed) *)
 
+  enabled_rewrite_rules_type: RRset.t option;
+  (** Enabled rewrite rules for the type
+      ([None] means same as normal, must be [None] except for constants) *)
 }
 
 (** {6 Representation of definitions/assumptions in the kernel } *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
@@ -32,6 +32,7 @@ let safe_flags oracle = {
   sprop_allowed = true;
   allow_uip = false;
   enabled_rewrite_rules = None;
+  enabled_rewrite_rules_type = None;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
@@ -260,10 +260,11 @@ let register_rewrite_rules rules env =
     symb_pats = List.fold_left (fun symb_pats (c, r) -> Cmap_env.update c (add c r) symb_pats) env.symb_pats rules.rewrules_rules
   }
 
-let sync_rewrite_rules prev_rules env =
+let sync_rewrite_rules ~type_mode prev_rules env =
   let rrset = match get_enabled_rewrite_rules env with rrset -> rrset | exception RewriteRulesNotAllowed _ ->
     anomaly Pp.(str"Trying to remove \"-allowed-rewrite-rules\" flag")
   in
+  let rrset = if type_mode then Option.default rrset env.env_typing_flags.enabled_rewrite_rules_type else rrset in
   let prev_rules = Option.default RRset.empty prev_rules in
   (* Efficient symmetric difference function ? *)
   let new_rules, removed_rules = RRset.diff rrset prev_rules, RRset.diff prev_rules rrset in
@@ -279,8 +280,30 @@ let sync_rewrite_rules prev_rules env =
     register_rewrite_rules rr env)
     rules_to_add env
 
+let rewrite_rules_type_different env = Option.has_some env.env_typing_flags.enabled_rewrite_rules_type
+
+let resync_rewrite_rules_type env =
+  if rewrite_rules_type_different env then
+    sync_rewrite_rules ~type_mode:false None env
+  else
+    env
+
+let resync_rewrite_rules_body env =
+  let type_rr = env.env_typing_flags.enabled_rewrite_rules_type in
+  if Option.has_some type_rr then
+    sync_rewrite_rules ~type_mode:false type_rr env
+  else
+    env
+
 let enable_rewrite_rules_flags kn flags =
-  { flags with enabled_rewrite_rules = Some (RRset.add kn (get_enabled_rewrite_rules_flags flags)) }
+  { flags with
+    enabled_rewrite_rules = Some (RRset.add kn (get_enabled_rewrite_rules_flags flags));
+    enabled_rewrite_rules_type = Option.map (RRset.add kn) flags.enabled_rewrite_rules_type; }
+
+let enable_rewrite_rules_proof_flags kn flags =
+  { flags with
+    enabled_rewrite_rules = Some (RRset.add kn (get_enabled_rewrite_rules_flags flags));
+    enabled_rewrite_rules_type = Some (get_enabled_rewrite_rules_flags flags) }
 
 let enable_rewrite_rules kn env =
   let env = { env with env_typing_flags = enable_rewrite_rules_flags kn env.env_typing_flags } in
@@ -582,6 +605,7 @@ let same_flags {
      sprop_allowed;
      allow_uip;
      enabled_rewrite_rules;
+     enabled_rewrite_rules_type;
   } alt =
   check_guarded == alt.check_guarded &&
   check_positive == alt.check_positive &&
@@ -594,23 +618,29 @@ let same_flags {
   impredicative_set == alt.impredicative_set &&
   sprop_allowed == alt.sprop_allowed &&
   allow_uip == alt.allow_uip &&
-  enabled_rewrite_rules == alt.enabled_rewrite_rules
+  enabled_rewrite_rules == alt.enabled_rewrite_rules &&
+  enabled_rewrite_rules_type == alt.enabled_rewrite_rules_type
 [@warning "+9"]
 
 let set_type_in_type b = map_universes (UGraph.set_type_in_type b)
 
-let set_typing_flags c env =
+let set_typing_flags ?type_mode c env =
   if same_flags env.env_typing_flags c then env
   else
+    let () = if Option.is_empty type_mode && Option.has_some c.enabled_rewrite_rules_type then
+      CErrors.user_err Pp.(str"Proof rewrite rules are only supported for opaque definitions")
+    in
+    let type_mode = Option.default false type_mode in
     let newenv = { env with env_typing_flags = c } in
     let newenv = set_type_in_type (not c.check_universes) newenv in
-    if env.env_typing_flags.enabled_rewrite_rules == c.enabled_rewrite_rules then
+    if env.env_typing_flags.enabled_rewrite_rules == c.enabled_rewrite_rules &&
+      env.env_typing_flags.enabled_rewrite_rules_type == c.enabled_rewrite_rules_type then
       newenv
     else
-      sync_rewrite_rules env.env_typing_flags.enabled_rewrite_rules newenv
+      sync_rewrite_rules ~type_mode (if type_mode then env.env_typing_flags.enabled_rewrite_rules_type else env.env_typing_flags.enabled_rewrite_rules) newenv
 
-let update_typing_flags ?typing_flags env =
-  Option.cata (fun flags -> set_typing_flags flags env) env typing_flags
+let update_typing_flags ?type_mode ?typing_flags env =
+  Option.cata (fun flags -> set_typing_flags ?type_mode flags env) env typing_flags
 
 let set_impredicative_set b env =
   set_typing_flags {env.env_typing_flags with impredicative_set=b} env
diff --git a/kernel/environ.mli b/kernel/environ.mli
@@ -190,6 +190,7 @@ val add_rewrite_rules : RewriteRules.t -> rewrite_rules_body -> env -> env
 
 val enable_rewrite_rules : RewriteRules.t -> env -> env
 val enable_rewrite_rules_flags : RewriteRules.t -> typing_flags -> typing_flags
+val enable_rewrite_rules_proof_flags : RewriteRules.t -> typing_flags -> typing_flags
 val get_enabled_rewrite_rules : env -> RRset.t
 (** [raises RewriteRulesNotAllowed]*)
 
@@ -411,18 +412,25 @@ val push_subgraph : Univ.ContextSet.t -> env -> env
    also checks that they do not imply new transitive constraints
    between pre-existing universes in [env]. *)
 
-val set_typing_flags : typing_flags -> env -> env
+val set_typing_flags : ?type_mode:bool -> typing_flags -> env -> env
 val set_impredicative_set : bool -> env -> env
 val set_type_in_type : bool -> env -> env
 val set_allow_sprop : bool -> env -> env
 val sprop_allowed : env -> bool
 val allow_rewrite_rules : env -> env
 val rewrite_rules_allowed : env -> bool
+val rewrite_rules_type_different : env -> bool
 
 val same_flags : typing_flags -> typing_flags -> bool
 
 (** [update_typing_flags ?typing_flags] may update env with optional typing flags *)
-val update_typing_flags : ?typing_flags:typing_flags -> env -> env
+val update_typing_flags : ?type_mode:bool -> ?typing_flags:typing_flags -> env -> env
+
+(** Sets active rewrite rules to the regular list *)
+val resync_rewrite_rules_body : env -> env
+
+(** Sets active rewrite rules to the type list *)
+val resync_rewrite_rules_type : env -> env
 
 val universes_of_global : env -> GlobRef.t -> AbstractContext.t
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
@@ -295,12 +295,12 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 
 (** {6 Typing flags } *)
 
-let set_typing_flags c senv =
-  let env = Environ.set_typing_flags c senv.env in
+let set_typing_flags ?type_mode c senv =
+  let env = Environ.set_typing_flags ?type_mode c senv.env in
   if env == senv.env then senv
   else { senv with env }
 
-let set_typing_flags flags senv =
+let set_typing_flags ?type_mode flags senv =
   (* NB: we allow changing the conv_oracle inside sections because it
      doesn't matter for consistency. *)
   if Option.has_some senv.sections
@@ -310,7 +310,7 @@ let set_typing_flags flags senv =
              share_reduction = flags.share_reduction;
             })
   then CErrors.user_err Pp.(str "Changing typing flags inside sections is not allowed.");
-  set_typing_flags flags senv
+  set_typing_flags ?type_mode flags senv
 
 let set_impredicative_set b senv =
   let flags = Environ.typing_flags senv.env in
@@ -350,12 +350,12 @@ let set_rewrite_rules_allowed b senv =
   else senv
 
 (* Temporary sets custom typing flags *)
-let with_typing_flags ?typing_flags senv ~f =
+let with_typing_flags ?type_mode ?typing_flags senv ~f =
   match typing_flags with
   | None -> f senv
   | Some typing_flags ->
     let orig_typing_flags = Environ.typing_flags senv.env in
-    let res, senv = f (set_typing_flags typing_flags senv) in
+    let res, senv = f (set_typing_flags ?type_mode typing_flags senv) in
     res, set_typing_flags orig_typing_flags senv
 
 (** {6 Stm machinery } *)
@@ -1118,7 +1118,8 @@ let add_constant l decl senv =
   kn, senv
 
 let add_constant ?typing_flags l decl senv =
-  with_typing_flags ?typing_flags senv ~f:(add_constant l decl)
+  let type_mode = match decl with Entries.OpaqueEntry _ -> Some true | _ -> None in
+  with_typing_flags ?type_mode ?typing_flags senv ~f:(add_constant l decl)
 
 type opaque_certificate = {
   opq_body : Constr.t;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
@@ -166,7 +166,7 @@ val push_qualities : rigid:bool -> Sorts.QContextSet.t -> safe_transformer0
 val set_rewrite_rules_allowed : bool -> safe_transformer0
 val set_impredicative_set : bool -> safe_transformer0
 val set_indices_matter : bool -> safe_transformer0
-val set_typing_flags : Declarations.typing_flags -> safe_transformer0
+val set_typing_flags : ?type_mode:bool -> Declarations.typing_flags -> safe_transformer0
 val set_share_reduction : bool -> safe_transformer0
 val set_check_guarded : bool -> safe_transformer0
 val set_check_positive : bool -> safe_transformer0
diff --git a/proofs/proof.ml b/proofs/proof.ml
@@ -443,7 +443,7 @@ let solve ?with_end_tac env gi info_lvl tac pr =
         Proofview.tclTHEN tac solve_constraints
       else tac
     in
-    let env = Environ.update_typing_flags ?typing_flags:pr.typing_flags env in
+    let env = Environ.update_typing_flags ~type_mode:false ?typing_flags:pr.typing_flags env in
     let (p, (env, status, info), ()) = run_tactic env tac pr in
     let sigma = (data p).sigma in
     let () =
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
@@ -512,30 +512,37 @@ let typing_flags_parser : Declarations.typing_flags key_parser = fun ?loc orig a
   | att ->
     CErrors.user_err ?loc Pp.(str "Ill-formed “typing” attribute: " ++ pr_vernac_flag_value att)
 
-let enabled_rewrite_rules ?loc orig = function
+let enabled_rewrite_rules ~proof ?loc orig = function
   | VernacFlagEmpty | VernacFlagLeaf _ ->
     CErrors.user_err ?loc
-      Pp.(str "Attribute enabled_rewrite_rules only accepts lists of values.")
+      Pp.(str "Attribute rewrite_rules only accepts lists of values.")
   | VernacFlagList atts ->
     let rec one res = function
       | [] -> res
       | {CAst.v=key, value; loc} :: rem ->
           if List.exists (fun {CAst.v=k, _} -> String.equal key k) rem then
             error_twice ?loc ~name:key;
           let qid = Libnames.qualid_of_string ?loc key in
-          let rrl = Nametab.locate_rewrite_rules qid in
+          let rrl =
+            match Nametab.locate_rewrite_rules qid with
+            | rrl -> rrl
+            | exception Not_found ->
+                CErrors.user_err ?loc Pp.(str "Unknown rewrite rule set")
+            in
           if not (get_bool_value ?loc ~key ~default:true value) then
             CErrors.user_err ?loc
-              Pp.(str "Attribute enabled_rewrite_rules can only enable rules.");
+              Pp.(str "Attribute rewrite_rules can only enable rules.");
           one (rrl :: res) rem
     in
     let rules = one [] atts in
     let typing_flags = Option.default (Global.typing_flags ()) orig in
-    List.fold_left (fun env kn -> Environ.enable_rewrite_rules_flags kn env) typing_flags rules
+    List.fold_left (fun env kn -> (if proof then Environ.enable_rewrite_rules_proof_flags else Environ.enable_rewrite_rules_flags) kn env) typing_flags rules
 
 
 let typing_flags : Declarations.typing_flags option attribute =
-  attribute_of_list ["bypass_check", typing_flags_parser; "enabled_rewrite_rules", enabled_rewrite_rules]
+  attribute_of_list
+    ["bypass_check", typing_flags_parser;
+     "rewrite_rules", enabled_rewrite_rules ~proof:true]
 
 let bind_scope_where =
   let name = "where to bind scope" in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
@@ -136,7 +136,7 @@ let do_definition ?loc ?hook ~name ?scope ?clearbody ~poly ?typing_flags ~kind ?
 
 let do_definition_program ?loc ?hook ~pm ~name ~scope ?clearbody ~poly ?typing_flags ~kind ?using ?user_warns udecl bl red_option c ctypopt =
   let env = Global.env() in
-  let env = Environ.update_typing_flags ?typing_flags env in
+  let env = Environ.update_typing_flags ~type_mode:true ?typing_flags env in
   (* Explicitly bound universes and constraints *)
   let evd, udecl = interp_univ_decl_opt env udecl in
   let evd, (body, types), impargs =
@@ -150,7 +150,7 @@ let do_definition_program ?loc ?hook ~pm ~name ~scope ?clearbody ~poly ?typing_f
 
 let do_definition_interactive ?loc ~program_mode ?hook ~name ~scope ?clearbody ~poly ~typing_flags ~kind ?using ?user_warns udecl bl t =
   let env = Global.env () in
-  let env = Environ.update_typing_flags ?typing_flags env in
+  let env = Environ.update_typing_flags ~type_mode:true ?typing_flags env in
   let flags = Pretyping.{ all_no_fail_flags with program_mode; poly } in
   let evd, udecl = Constrintern.interp_univ_decl_opt env udecl in
   let evd, args, typ,impargs = interp_statement ~program_mode ~flags ~scope env evd name bl t in
@@ -169,7 +169,7 @@ let do_definition_interactive ?loc ~program_mode ?hook ~name ~scope ?clearbody ~
 
 let do_definition_refine ?loc ?hook ~name ~scope ?clearbody ~poly ~typing_flags ~kind ?using ?user_warns udecl bl c ctypopt =
   let env = Global.env() in
-  let env = Environ.update_typing_flags ?typing_flags env in
+  let env = Environ.update_typing_flags ~type_mode:true ?typing_flags env in
   (* Explicitly bound universes and constraints *)
   let evd, udecl = interp_univ_decl_opt env udecl in
   let evd, (body, typ), impargs =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
@@ -458,6 +458,8 @@ let interp_mutual_definition env ~program_mode ~poly ~function_mode rec_order fi
   let fixrecimps = List.map3 (fun ctximps wfimps cclimps -> ctximps @ wfimps @ cclimps) fixctximps fixwfimps fixcclimps in
   let fiximps = List.map2 (fun ctximps cclimps -> ctximps @ cclimps) fixctximps fixcclimps in
 
+  let env = Environ.resync_rewrite_rules_body env in
+
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in
   let sigma, fixdefs =
@@ -564,7 +566,7 @@ let finish_regular env sigma use_inference_hook fix =
 let do_mutually_recursive ?pm ~refine ~program_mode ?(use_inference_hook=false) ?scope ?clearbody ~kind ~poly ?typing_flags ?user_warns ?using (rec_order, fixl)
   : Declare.OblState.t option * Declare.Proof.t option =
   let env = Global.env () in
-  let env = Environ.update_typing_flags ?typing_flags env in
+  let env = Environ.update_typing_flags ~type_mode:true ?typing_flags env in
   let (env,rec_sign,sigma),(fix,possible_guard,udecl) = interp_mutual_definition env ~program_mode ~poly ~function_mode:false rec_order fixl in
   check_recursive ~kind env sigma fix;
 
diff --git a/vernac/declare.ml b/vernac/declare.ml

Original file line number	Diff line number	Diff line change
`@@ -104,6 +104,9 @@ type typing_flags = {`
`104`	`104`	`enabled_rewrite_rules: RRset.t option;`
`105`	`105`	`(** Enabled rewrite rules ([None] means rewrite rules are not allowed) *)`
`106`	`106`
	`107`	`+ enabled_rewrite_rules_type: RRset.t option;`
	`108`	`+ (** Enabled rewrite rules for the type`
	`109`	`+ ([None] means same as normal, must be [None] except for constants) *)`
`107`	`110`	`}`
`108`	`111`
`109`	`112`	`(** {6 Representation of definitions/assumptions in the kernel } *)`
Original file line number	Diff line number	Diff line change
`@@ -32,6 +32,7 @@ let safe_flags oracle = {`
`32`	`32`	`sprop_allowed = true;`
`33`	`33`	`allow_uip = false;`
`34`	`34`	`enabled_rewrite_rules = None;`
	`35`	`+ enabled_rewrite_rules_type = None;`
`35`	`36`	`}`
`36`	`37`
`37`	`38`	`(** {6 Arities } *)`