Merge PR #10732: Make `Print Rings` and `Print Fields` more reliable

Reviewed-by: thery

3 files changed, 26 insertions, 77 deletions

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b456d2eed2..76c393450b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -18,7 +18,6 @@ open EConstr
 open Vars
 open CClosure
 open Environ
-open Libnames
 open Globnames
 open Glob_term
 open Locus
@@ -326,19 +325,18 @@ let _ = add_map "ring"
 module Cmap = Map.Make(Constr)
 
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
-let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
 
 let print_rings () =
   Feedback.msg_notice (strbrk "The following ring structures have been declared:");
-  Spmap.iter (fun fn fi ->
+  Cmap.iter (fun _carrier ring ->
       let env = Global.env () in
       let sigma = Evd.from_env env in
       Feedback.msg_notice
         (hov 2
-           (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-            str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
-            str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
-    ) !from_name
+           (Ppconstr.pr_id ring.ring_name ++ spc() ++
+            str"with carrier "++ pr_constr_env env sigma ring.ring_carrier++spc()++
+            str"and equivalence relation "++ pr_constr_env env sigma ring.ring_req))
+    ) !from_carrier
 
 let ring_for_carrier r = Cmap.find r !from_carrier
 
@@ -361,9 +359,7 @@ let find_ring_structure env sigma l =
     | [] -> assert false
 
 let add_entry (sp,_kn) e =
-  from_carrier := Cmap.add e.ring_carrier e !from_carrier;
-  from_name := Spmap.add sp e !from_name
-
+  from_carrier := Cmap.add e.ring_carrier e !from_carrier
 
 let subst_th (subst,th) =
   let c' = subst_mps subst th.ring_carrier in
@@ -391,7 +387,8 @@ let subst_th (subst,th) =
      pretac' == th.ring_pre_tac &&
      posttac' == th.ring_post_tac then th
   else
-    { ring_carrier = c';
+    { ring_name = th.ring_name;
+      ring_carrier = c';
       ring_req = eq';
       ring_setoid = set';
       ring_ext = ext';
@@ -428,59 +425,6 @@ let op_morph r add mul opp req m1 m2 m3 =
 let op_smorph r add mul req m1 m2 =
   lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
 
-(* let default_ring_equality (r,add,mul,opp,req) = *)
-(*   let is_setoid = function *)
-(*       {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *)
-(*         eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *)
-(*     | _ -> false in *)
-(*   match default_relation_for_carrier ~filter:is_setoid r with *)
-(*       Leibniz _ -> *)
-(*         let setoid = lapp coq_eq_setoid [|r|] in *)
-(*         let op_morph = *)
-(*           match opp with *)
-(*               Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *)
-(*             | None -> lapp coq_eq_smorph [|r;add;mul|] in *)
-(*         (setoid,op_morph) *)
-(*     | Relation rel -> *)
-(*         let setoid = setoid_of_relation rel in *)
-(*         let is_endomorphism = function *)
-(*             { args=args } -> List.for_all *)
-(*                 (function (var,Relation rel) -> *)
-(*                   var=None && eq_constr_nounivs req rel *)
-(*                   | _ -> false) args in *)
-(*         let add_m = *)
-(*           try default_morphism ~filter:is_endomorphism add *)
-(*           with Not_found -> *)
-(*             error "ring addition should be declared as a morphism" in *)
-(*         let mul_m = *)
-(*           try default_morphism ~filter:is_endomorphism mul *)
-(*           with Not_found -> *)
-(*             error "ring multiplication should be declared as a morphism" in *)
-(*         let op_morph = *)
-(*           match opp with *)
-(*             | Some opp -> *)
-(*             (let opp_m = *)
-(*               try default_morphism ~filter:is_endomorphism opp *)
-(*               with Not_found -> *)
-(*                 error "ring opposite should be declared as a morphism" in *)
-(*              let op_morph = *)
-(*                op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *)
-(*              msgnl *)
-(*                (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++   *)
-(*                str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
-(*                str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *)
-(*                str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *)
-(*                str"\""); *)
-(*              op_morph) *)
-(*             | None -> *)
-(*             (msgnl *)
-(*               (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++   *)
-(*                str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
-(*                str"\""++spc()++str"and \""++ *)
-(*                pr_constr mul_m.morphism_theory++str"\""); *)
-(*             op_smorph r add mul req add_m.lem mul_m.lem) in *)
-(*         (setoid,op_morph) *)
-
 let ring_equality env evd (r,add,mul,opp,req) =
   match EConstr.kind !evd req with
     | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
@@ -657,7 +601,8 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div
   let _ =
     Lib.add_leaf name
       (theory_to_obj
-        { ring_carrier = r;
+        { ring_name = name;
+          ring_carrier = r;
           ring_req = req;
           ring_setoid = sth;
           ring_ext = params.(1);
@@ -835,19 +780,18 @@ let dest_field env evd th_spec =
     | _ -> error "bad field structure"
 
 let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
-let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
 
 let print_fields () =
   Feedback.msg_notice (strbrk "The following field structures have been declared:");
-  Spmap.iter (fun fn fi ->
+  Cmap.iter (fun _carrier fi ->
       let env = Global.env () in
       let sigma = Evd.from_env env in
       Feedback.msg_notice
         (hov 2
-           (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+           (Id.print fi.field_name ++ spc() ++
             str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
             str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
-    ) !field_from_name
+    ) !field_from_carrier
 
 let field_for_carrier r = Cmap.find r !field_from_carrier
 
@@ -871,8 +815,7 @@ let find_field_structure env sigma l =
     | [] -> assert false
 
 let add_field_entry (sp,_kn) e =
-  field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier;
-  field_from_name := Spmap.add sp e !field_from_name
+  field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier
 
 let subst_th (subst,th) =
   let c' = subst_mps subst th.field_carrier in
@@ -898,7 +841,8 @@ let subst_th (subst,th) =
      pretac' == th.field_pre_tac &&
      posttac' == th.field_post_tac then th
   else
-    { field_carrier = c';
+    { field_name = th.field_name;
+      field_carrier = c';
       field_req = eq';
       field_cst_tac = tac';
       field_pow_tac = pow_tac';
@@ -983,7 +927,8 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od
   let _ =
     Lib.add_leaf name
       (ftheory_to_obj
-        { field_carrier = r;
+        { field_name = name;
+          field_carrier = r;
           field_req = req;
           field_cst_tac = cst_tac;
           field_pow_tac = pow_tac;
diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml
index 0a3e7bd9ca..b81f5f7d14 100644
--- a/plugins/setoid_ring/newring_ast.ml
+++ b/plugins/setoid_ring/newring_ast.ml
@@ -40,7 +40,8 @@ type 'constr field_mod =
   | Inject of constr_expr
 
 type ring_info =
-    { ring_carrier : types;
+    { ring_name : Names.Id.t;
+      ring_carrier : types;
       ring_req : constr;
       ring_setoid : constr;
       ring_ext : constr;
@@ -54,7 +55,8 @@ type ring_info =
       ring_post_tac : glob_tactic_expr }
 
 type field_info =
-    { field_carrier : types;
+    { field_name : Names.Id.t;
+      field_carrier : types;
       field_req : constr;
       field_cst_tac : glob_tactic_expr;
       field_pow_tac : glob_tactic_expr;
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index 0a3e7bd9ca..b81f5f7d14 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -40,7 +40,8 @@ type 'constr field_mod =
   | Inject of constr_expr
 
 type ring_info =
-    { ring_carrier : types;
+    { ring_name : Names.Id.t;
+      ring_carrier : types;
       ring_req : constr;
       ring_setoid : constr;
       ring_ext : constr;
@@ -54,7 +55,8 @@ type ring_info =
       ring_post_tac : glob_tactic_expr }
 
 type field_info =
-    { field_carrier : types;
+    { field_name : Names.Id.t;
+      field_carrier : types;
       field_req : constr;
       field_cst_tac : glob_tactic_expr;
       field_pow_tac : glob_tactic_expr;