Enable rewrite rules for only opaque definitions

Author: yannl35133

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

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). *)

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 ->
@@ -52,9 +52,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

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|]
@@ -340,7 +341,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|]|]
 
@@ -526,7 +528,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|];

kernel/constant_typing.ml

@@ -243,7 +243,7 @@ let infer_definition ~sec_univs env entry =
 let infer_opaque ~sec_univs env entry =
   let env, usubst, _, univs = process_universes env entry.opaque_entry_universes in
   let typj = Typeops.infer_type env entry.opaque_entry_type 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 = Vars.subst_univs_level_constr usubst typj.utj_val in
   let hyps = used_section_variables env (Some entry.opaque_entry_secctx) None typ in

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 } *)

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 } *)

kernel/environ.ml

@@ -252,10 +252,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
@@ -271,8 +272,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_body_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
@@ -565,6 +588,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 &&
@@ -577,23 +601,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"Body 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

kernel/environ.mli

@@ -187,6 +187,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_body_flags : RewriteRules.t -> typing_flags -> typing_flags
 val get_enabled_rewrite_rules : env -> RRset.t
 (** [raises RewriteRulesNotAllowed]*)
 
@@ -365,18 +366,25 @@ val push_subgraph : 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
 

kernel/safe_typing.ml

@@ -293,12 +293,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
@@ -308,7 +308,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
@@ -348,12 +348,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 } *)
@@ -1054,7 +1054,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;