Add a global flag for rewrite rules

checker/safe_checking.ml

@@ -12,6 +12,7 @@ open Declarations
 open Environ
 
 let import senv opac clib univs digest =
+  let senv = Safe_typing.check_flags_for_library clib senv in
   let mb = Safe_typing.module_of_library clib in
   let env = Safe_typing.env_of_safe_env senv in
   let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in

checker/values.ml

@@ -376,8 +376,9 @@ and v_modtype =
 
 let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
 let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
+let v_flags = v_tuple "flags" [|v_bool|] (* Allow Rewrite Rules *)
 let v_compiled_lib =
-  v_tuple "compiled" [|v_dp;v_module;v_context_set;v_deps|]
+  v_tuple "compiled" [|v_dp;v_module;v_context_set;v_deps; v_flags|]
 
 (** Library objects *)
 

doc/sphinx/addendum/rewrite-rules.rst

@@ -13,6 +13,20 @@ User-defined rewrite rules
    compilation currently do not understand rewrite rules.
 
 
+The use of rewrite rules is guarded behind a flag, which can be enabled
+either by passing ``-allow-rewrite-rules`` to the
+Coq program or by turning the :flag:`Allow Rewrite Rules` flag on.
+
+.. flag:: Allow Rewrite Rules
+
+   This :term:`flag` enables the use of rewrite rules.
+   It is disabled by default and cannot be disabled once enabled.
+   The command-line flag ``-allow-rewrite-rules`` enables rewrite rules at
+   startup.
+
+   .. exn:: Rewrite rule declaration requires enabling the flag "Allow Rewrite Rules".
+      :undocumented:
+
 Declaring symbols
 -----------------
 
@@ -25,6 +39,7 @@ Rewrite rules operate on symbols, which are their own kind of constants.
 
    .. coqtop:: all
 
+      Set Allow Rewrite Rules.
       Symbol pplus : nat -> nat -> nat.
       Notation "a ++ b" := (pplus a b).
 

kernel/environ.ml

@@ -86,7 +86,10 @@ type env = {
   symb_pats: rewrite_rule list Cmap_env.t;
   env_typing_flags  : typing_flags;
   retroknowledge : Retroknowledge.retroknowledge;
+  rewrite_rules_allowed: bool;
 }
+type rewrule_not_allowed = Symb | Rule
+exception RewriteRulesNotAllowed of rewrule_not_allowed
 
 let empty_named_context_val = {
   env_named_ctx = [];
@@ -116,6 +119,7 @@ let empty_env = {
   symb_pats = Cmap_env.empty;
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
+  rewrite_rules_allowed = false;
 }
 
 
@@ -219,6 +223,7 @@ let lookup_constant kn env =
 let mem_constant kn env = Cmap_env.mem kn env.env_globals.Globals.constants
 
 let add_rewrite_rules l env =
+  if not env.rewrite_rules_allowed then raise (RewriteRulesNotAllowed Rule);
   let add c r = function
     | None -> anomaly Pp.(str "Trying to add a rule to non-symbol " ++ Constant.print c ++ str".")
     | Some rs -> Some (r::rs)
@@ -562,6 +567,11 @@ let set_allow_sprop b env =
 
 let sprop_allowed env = env.env_typing_flags.sprop_allowed
 
+let set_rewrite_rules_allowed b env =
+  { env with rewrite_rules_allowed = env.rewrite_rules_allowed || b }
+
+let rewrite_rules_allowed env = env.rewrite_rules_allowed
+
 (* Global constants *)
 
 let no_link_info = NotLinked
@@ -578,7 +588,11 @@ let add_constant_key kn cb linkinfo env =
     else env.irr_constants
   in
   let symb_pats =
-    match cb.const_body with Symbol _ -> Cmap_env.add kn [] env.symb_pats | _ -> env.symb_pats
+    match cb.const_body with
+    | Symbol _ ->
+      if not env.rewrite_rules_allowed then raise (RewriteRulesNotAllowed Symb);
+      Cmap_env.add kn [] env.symb_pats
+    | _ -> env.symb_pats
   in
   { env with irr_constants; symb_pats; env_globals = new_globals }
 

kernel/environ.mli

@@ -77,8 +77,13 @@ type env = private {
   symb_pats : rewrite_rule list Cmap_env.t;
   env_typing_flags  : typing_flags;
   retroknowledge : Retroknowledge.retroknowledge;
+  rewrite_rules_allowed : bool;
+  (** Allow rewrite rules (breaks e.g. SR) *)
 }
 
+type rewrule_not_allowed = Symb | Rule
+exception RewriteRulesNotAllowed of rewrule_not_allowed
+
 val oracle : env -> Conv_oracle.oracle
 val set_oracle : env -> Conv_oracle.oracle -> env
 
@@ -369,6 +374,8 @@ 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 set_rewrite_rules_allowed : bool -> env -> env
+val rewrite_rules_allowed : env -> bool
 
 val same_flags : typing_flags -> typing_flags -> bool
 

kernel/safe_typing.ml

@@ -115,11 +115,16 @@ type library_info = DirPath.t * vodigest
 (** Functor and funsig parameters, most recent first *)
 type module_parameters = (MBId.t * module_type_body) list
 
+type permanent_flags = {
+  rewrite_rules_allowed : bool;
+}
+
 type compiled_library = {
   comp_name : DirPath.t;
   comp_mod : module_body;
   comp_univs : Univ.ContextSet.t;
   comp_deps : library_info array;
+  comp_flags : permanent_flags;
 }
 
 type reimport = compiled_library * Univ.ContextSet.t * vodigest
@@ -272,6 +277,8 @@ let set_native_compiler b senv =
 
 let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env }
 
+let set_rewrite_rules_allowed b senv = { senv with env = Environ.set_rewrite_rules_allowed b senv.env }
+
 (* Temporary sets custom typing flags *)
 let with_typing_flags ?typing_flags senv ~f =
   match typing_flags with
@@ -483,6 +490,12 @@ let check_required current_libs needed =
   in
   Array.iter check needed
 
+(** When loading a library, the current flags should match
+    those needed for the library *)
+
+let check_flags_for_library lib senv =
+  let { rewrite_rules_allowed } = lib.comp_flags in
+  set_rewrite_rules_allowed rewrite_rules_allowed senv
 
 (** {6 Insertion of section variables} *)
 
@@ -1191,6 +1204,7 @@ let end_module l restype senv =
   let mbids = List.rev_map fst params in
   let mb = build_module_body params restype senv in
   let newenv = Environ.set_universes (Environ.universes senv.env) oldsenv.env in
+  let newenv = Environ.set_rewrite_rules_allowed (Environ.rewrite_rules_allowed senv.env) newenv in
   let senv' = propagate_loads { senv with env = newenv } in
   let newenv = Modops.add_module mb senv'.env in
   let newresolver =
@@ -1215,6 +1229,7 @@ let end_modtype l senv =
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
   let newenv = Environ.set_universes (Environ.universes senv.env) oldsenv.env in
+  let newenv = Environ.set_rewrite_rules_allowed (Environ.rewrite_rules_allowed senv.env) newenv in
   let senv' = propagate_loads {senv with env=newenv} in
   let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in
   let mtb = build_mtb mp auto_tb senv.modresolver in
@@ -1319,17 +1334,22 @@ let export ~output_native_objects senv dir =
       Nativelibrary.dump_library mp senv.env str
     else [], Nativevalues.empty_symbols
   in
+  let permanent_flags = {
+    rewrite_rules_allowed = Environ.rewrite_rules_allowed senv.env;
+  } in
   let lib = {
     comp_name = dir;
     comp_mod = mb;
     comp_univs = senv.univ;
     comp_deps = Array.of_list (DPmap.bindings senv.required);
+    comp_flags = permanent_flags
   } in
   mp, lib, (ast, symbols)
 
 (* cst are the constraints that were computed by the vi2vo step and hence are
  * not part of the [lib.comp_univs] field (but morally should be) *)
 let import lib cst vodigest senv =
+  let senv = check_flags_for_library lib senv in
   check_required senv.required lib.comp_deps;
   if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then
     CErrors.user_err
@@ -1386,6 +1406,7 @@ let close_section senv =
      by {!add_constant_aux}. *)
   let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels;
         rev_reimport; rev_revstruct = revstruct } = revert in
+  let env = Environ.set_rewrite_rules_allowed (Environ.rewrite_rules_allowed env0) env in
   let senv = { senv with env; revstruct; sections; univ; objlabels; } in
   (* Second phase: replay Requires *)
   let senv = List.fold_left (fun senv (lib,cst,vodigest) -> snd (import lib cst vodigest senv))

kernel/safe_typing.mli

@@ -160,6 +160,7 @@ val add_constraints :
 (* val next_universe : int safe_transformer *)
 
 (** Setting the type theory flavor *)
+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
@@ -234,6 +235,7 @@ type compiled_library
 
 val module_of_library : compiled_library -> Declarations.module_body
 val univs_of_library : compiled_library -> Univ.ContextSet.t
+val check_flags_for_library : compiled_library -> safe_transformer0
 
 val start_library : DirPath.t -> ModPath.t safe_transformer
 

library/global.ml

@@ -90,6 +90,8 @@ let set_check_universes c = globalize0 (Safe_typing.set_check_universes c)
 let typing_flags () = Environ.typing_flags (env ())
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
+let set_rewrite_rules_allowed b = globalize0 (Safe_typing.set_rewrite_rules_allowed b)
+let rewrite_rules_allowed () = Environ.rewrite_rules_allowed (env())
 let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
 let add_constant ?typing_flags id d = globalize (Safe_typing.add_constant ?typing_flags (i2l id) d)
 let add_private_constant id u d = globalize (Safe_typing.add_private_constant (i2l id) u d)

library/global.mli

@@ -38,6 +38,8 @@ val set_check_universes : bool -> unit
 val typing_flags : unit -> typing_flags
 val set_allow_sprop : bool -> unit
 val sprop_allowed : unit -> bool
+val set_rewrite_rules_allowed : bool -> unit
+val rewrite_rules_allowed : unit -> bool
 
 (** Variables, Local definitions, constants, inductive types *)
 

printing/printer.ml

@@ -1031,6 +1031,7 @@ module ContextObjectMap = Map.Make (OrderedContextObject)
 
 let pr_assumptionset env sigma s =
   if ContextObjectMap.is_empty s &&
+       not (rewrite_rules_allowed env) &&
        not (is_impredicative_set env) then
     str "Closed under the global context"
   else
@@ -1107,6 +1108,11 @@ let pr_assumptionset env sigma s =
         [str "Set is impredicative"]
       else []
     in
+    let theory =
+      if rewrite_rules_allowed env then
+        str "Rewrite rules are allowed (subject reduction might be broken)" :: theory
+      else theory
+    in
     let theory =
       if type_in_type env then
         str "Type hierarchy is collapsed (logic is inconsistent)" :: theory

sysinit/coqargs.ml

@@ -398,6 +398,8 @@ let parse_args ~usage ~init arglist : t * string list =
       add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None)
     |"-disallow-sprop" ->
       add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
+    |"-allow-rewrite-rules" ->
+      add_set_option oval Vernacentries.allow_rewrite_rules_name (OptionSet None)
     |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
     |"-m"|"--memory" -> { oval with post = { memory_stat = true }}
     |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}

test-suite/success/rewrule.v

@@ -1,3 +1,5 @@
+Set Allow Rewrite Rules.
+
 Symbol pplus : nat -> nat -> nat.
 Notation "a ++ b" := (pplus a b).
 

vernac/comRewriteRule.ml

@@ -59,6 +59,8 @@ let do_symbol ~poly ~unfold_fix udecl (id, typ) =
   declare id entry
 
 let do_symbols ~poly ~unfold_fix l =
+  let env = Global.env () in
+  if not @@ Environ.rewrite_rules_allowed env then raise Environ.(RewriteRulesNotAllowed Symb);
   let udecl, l = preprocess_symbols l in
   List.iter (do_symbol ~poly ~unfold_fix udecl) l
 
@@ -261,5 +263,7 @@ let interp_rule (udecl, lhs, rhs) =
   head_symbol, { lhs_pat = head_umask, elims; rhs }
 
 let do_rules id rules =
+  let env = Global.env () in
+  if not @@ Environ.rewrite_rules_allowed env then raise Environ.(RewriteRulesNotAllowed Rule);
   let body = { rewrules_rules = List.map interp_rule rules } in
   Global.add_rewrite_rules id body

vernac/himsg.ml

@@ -1507,6 +1507,15 @@ let explain_prim_token_notation_error kind env sigma = function
      pr_constr_env env sigma c ++
      strbrk (" while parsing a "^kind^" notation."))
 
+(* Rewrite rules errors *)
+
+let error_not_allowed_rewrite_rules symb_or_rule =
+  str (match symb_or_rule with Rule -> "Rewrite rule" | Symb -> "Symbol") ++ spc () ++
+  str "declaration requires enabling the flag" ++ spc () ++
+  strbrk "\"Allow Rewrite Rules\"" ++
+  str "."
+
+
 (** Registration of generic errors
     Nota: explain_exn does NOT end with a newline anymore!
 *)
@@ -1571,6 +1580,8 @@ let rec vernac_interp_error_handler = function
     if Int.equal i 0 then str "." else str " (level " ++ int i ++ str")."
   | Logic_monad.TacticFailure e ->
     vernac_interp_error_handler e
+  | Environ.RewriteRulesNotAllowed symb_or_rule ->
+    error_not_allowed_rewrite_rules symb_or_rule
   | _ ->
     raise Unhandled
 

vernac/vernacentries.ml

@@ -1558,6 +1558,22 @@ let vernac_generalizable ~local =
   let local = Option.default true local in
   Implicit_quantifiers.declare_generalizable ~local
 
+let allow_rewrite_rules_name = ["Allow"; "Rewrite"; "Rules"]
+
+let set_rewrite_rules_allowed b =
+  let env = Global.env () in
+  if not b && env.rewrite_rules_allowed then CErrors.user_err
+    Pp.(str "This option does not allow the \"Unset\" command.");
+  Global.set_rewrite_rules_allowed b
+
+let () =
+  declare_bool_option
+    { optstage = Summary.Stage.Interp;
+      optdepr  = None;
+      optkey   = allow_rewrite_rules_name;
+      optread  = (fun () -> Global.rewrite_rules_allowed());
+      optwrite = set_rewrite_rules_allowed }
+
 let allow_sprop_opt_name = ["Allow";"StrictProp"]
 
 let () =

vernac/vernacentries.mli

@@ -45,6 +45,7 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
 val command_focus : unit Proof.focus_kind
 
 val allow_sprop_opt_name : string list
+val allow_rewrite_rules_name : string list
 
 (** pre-processing and validation of VernacInductive *)
 module Preprocessed_Mind_decl : sig