List used rewrite rules in Print Assumptions

Author: yannl35133

kernel/names.ml

@@ -1052,6 +1052,8 @@ module RewriteRules = struct
 
   let to_string { library = d ; id } =
     DirPath.to_string d ^ "." ^ Label.to_string id
+
+  let print kn = str (to_string kn)
 end
 
 module RRmap = HMap.Make(RewriteRules)

kernel/names.mli

@@ -669,6 +669,7 @@ module RewriteRules : sig
   val hash : t -> int
   val compare : t -> t -> int
   val to_string : t -> string
+  val print : t -> Pp.t
 end
 
 module RRset : CSig.USetS with type elt = RewriteRules.t

printing/printer.ml

@@ -1035,6 +1035,7 @@ type axiom =
   | Guarded of GlobRef.t
   | TypeInType of GlobRef.t
   | UIP of MutInd.t
+  | RewriteRules of GlobRef.t * RRset.t * RRset.t option
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
@@ -1057,6 +1058,8 @@ struct
     | Guarded k1 , Guarded k2
     | TypeInType k1, TypeInType k2 ->
       GlobRef.CanOrd.compare k1 k2
+    | RewriteRules (kn, _, _), RewriteRules (kn2, _, _) ->
+      GlobRef.CanOrd.compare kn kn2
     | Constant _, _ -> -1
     | _, Constant _ -> 1
     | Positive _, _ -> -1
@@ -1065,6 +1068,8 @@ struct
     | _, Guarded _ -> 1
     | TypeInType _, _ -> -1
     | _, TypeInType _ -> 1
+    | RewriteRules _, _ -> -1
+    | _, RewriteRules _ -> 1
 
   let compare x y =
     match x , y with
@@ -1117,6 +1122,17 @@ let pr_assumptionset env sigma s =
       try str " " ++ pr_ltype_env env sigma typ
       with e when CErrors.noncritical e -> mt ()
     in
+    let pr_rrs rrs =
+      prlist_with_sep spc RewriteRules.print (RRset.elements rrs)
+    in
+    let pr_rrs_pair rrs rtso =
+      let rrs, rps_text = match rtso with
+      | None -> rrs, mt()
+      | Some rts ->
+          rts, spc() ++ str "and its proof additionally relies on" ++ spc() ++ pr_rrs (RRset.diff rrs rts)
+      in
+      str "relies on" ++ spc() ++ pr_rrs rrs ++ rps_text ++ strbrk"."
+    in
     let pr_axiom env ax typ =
       match ax with
       | Constant kn ->
@@ -1129,6 +1145,8 @@ let pr_assumptionset env sigma s =
           hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
       | UIP mind ->
           hov 2 (safe_pr_inductive env mind ++ spc () ++ strbrk"relies on definitional UIP.")
+      | RewriteRules (gr, rrs, rtso) ->
+          hov 2 (safe_pr_global env gr ++ spc () ++ pr_rrs_pair rrs rtso)
     in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
@@ -1164,7 +1182,10 @@ let pr_assumptionset env sigma s =
     in
     let theory =
       if rewrite_rules_allowed env then
-        str "Rewrite rules are allowed (subject reduction might be broken)" :: theory
+        let rrs = get_enabled_rewrite_rules env in
+        str "Rewrite rules are allowed (subject reduction might be broken);" ++
+        spc() ++ str "enabled rules: " ++ (if RRset.is_empty rrs then str"(none)" else pr_rrs rrs)
+        :: theory
       else theory
     in
     let theory =

printing/printer.mli

@@ -213,6 +213,7 @@ type axiom =
   | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
   | TypeInType of GlobRef.t (* a constant which relies on type in type *)
   | UIP of MutInd.t (* An inductive using the special reduction rule. *)
+  | RewriteRules of GlobRef.t * RRset.t * RRset.t option (* A constant which relies on typing rules (and possibly proof-only rules) *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)

vernac/assumptions.ml

@@ -375,6 +375,13 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st gr t =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
       in
+      let accu =
+        match cb.const_typing_flags.enabled_rewrite_rules with
+        | Some rrs when not (RRset.is_empty rrs) ->
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (RewriteRules (obj, rrs, cb.const_typing_flags.enabled_rewrite_rules_type), l)) Constr.mkProp accu
+        | Some _ | None -> accu
+      in
     if not (Option.has_some contents) then
       let t = type_of_constant cb in
       let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in