Non syntactic matching when reifying for ring

plugins/ltac/g_auto.mlg

@@ -155,6 +155,7 @@ TACTIC EXTEND unify
       let state = Hints.Hint_db.transparent_state t in
       Tactics.unify ~state x y
   }
+| ["convert" constr(x) constr(y) ] -> { Tactics.convert x y }
 END
 
 {

theories/setoid_ring/Ncring_tac.v

@@ -26,7 +26,7 @@ Set Implicit Arguments.
 Ltac reify_as_var_aux n lvar term :=
   lazymatch lvar with
   | @cons _ ?t0 ?tl =>
-      match constr:(ltac:((constr_eq term t0; exact true) || exact false)) with
+      match constr:(ltac:((convert term t0; exact true) || exact false)) with
       | true => n
       | false => reify_as_var_aux open_constr:(S n) tl term
       end
@@ -46,54 +46,66 @@ Ltac close_varlist lvar :=
 
 Ltac extra_reify term := open_constr:((false,tt)).
 
+(* "convert x y; open_constr:(foo)" doesn't work so instead we do "let _ := open_constr:(do_convert x y) in foo" *)
+Local Notation do_convert x y := ltac:(convert x y;exact tt) (only parsing).
+
 Ltac reify_term Tring lvar term :=
-  lazymatch open_constr:((Tring, term)) with
+  match open_constr:((Tring, term)) with
+  (* int literals *)
   | (_, Z0) => open_constr:(PEc 0%Z)
   | (_, Zpos ?p) => open_constr:(PEc (Zpos p))
   | (_, Zneg ?p) => open_constr:(PEc (Zneg p))
-  | (Ring (ring0:=?op), ?op) => open_constr:(PEc 0%Z)
-  | (_, zero) => open_constr:(PEc 0%Z)
-  | (Ring (ring1:=?op), ?op) => open_constr:(PEc 1%Z)
-  | (_, one) => open_constr:(PEc 1%Z)
-  | (Ring (add:=?op), ?op ?t1 ?t2) =>
-      let et1 := reify_term Tring lvar t1 in
-      let et2 := reify_term Tring lvar t2 in
-      open_constr:(PEadd et1 et2)
-  | (_, addition ?t1 ?t2) =>
-      let et1 := reify_term Tring lvar t1 in
-      let et2 := reify_term Tring lvar t2 in
-      open_constr:(PEadd et1 et2)
-  | (Ring (mul:=?op), ?op ?t1 ?t2) =>
-      let et1 := reify_term Tring lvar t1 in
-      let et2 := reify_term Tring lvar t2 in
-      open_constr:(PEmul et1 et2)
-  | (Ring (T:=?R), multiplication (A:=?R) ?t1 ?t2) =>
-      let et1 := reify_term Tring lvar t1 in
-      let et2 := reify_term Tring lvar t2 in
-      open_constr:(PEmul et1 et2)
-  | (_, @multiplication Z _ _ ?z ?t) =>
-      let et := reify_term Tring lvar t in
-      open_constr:(PEmul (PEc z) et)
-  | (Ring (sub:=?op), ?op ?t1 ?t2) =>
-      let et1 := reify_term Tring lvar t1 in
-      let et2 := reify_term Tring lvar t2 in
-      open_constr:(PEsub et1 et2)
-  | (_, subtraction ?t1 ?t2) =>
-      let et1 := reify_term Tring lvar t1 in
-      let et2 := reify_term Tring lvar t2 in
-      open_constr:(PEsub et1 et2)
-  | (Ring (opp:=?op), ?op ?t) =>
+
+  (* ring constants *)
+  | (Ring (ring0:=?op), _) =>
+      let _ := open_constr:(do_convert op term) in
+      open_constr:(PEc 0%Z)
+  | (Ring (ring1:=?op), _) =>
+      let _ := open_constr:(do_convert op term) in
+      open_constr:(PEc 1%Z)
+
+  (* binary operators *)
+  | (Ring (T:=?R) (add:=?add) (mul:=?mul) (sub:=?sub), ?op ?t1 ?t2) =>
+      (* quick(?) check op is of th right type? TODO try without this check *)
+      let _ := open_constr:(t1 : R) in
+      let _ := open_constr:(t2 : R) in
+      match tt with
+      | _ =>
+          let _ := open_constr:(do_convert add op) in
+          (* NB: don't reify before we recognize the operator in case we can't recognire it *)
+          let et1 := reify_term Tring lvar t1 in
+          let et2 := reify_term Tring lvar t2 in
+          open_constr:(PEadd et1 et2)
+      | _ =>
+          let _ := open_constr:(do_convert mul op) in
+          let et1 := reify_term Tring lvar t1 in
+          let et2 := reify_term Tring lvar t2 in
+          open_constr:(PEmul et1 et2)
+      | _ =>
+          let _ := open_constr:(do_convert sub op) in
+          let et1 := reify_term Tring lvar t1 in
+          let et2 := reify_term Tring lvar t2 in
+          open_constr:(PEsub et1 et2)
+      end
+
+  (* unary operator (opposite) *)
+  | (Ring (T:=?R) (opp:=?opp), ?op ?t) =>
+      let _ := open_constr:(do_convert opp op) in
       let et := reify_term Tring lvar t in
       open_constr:(PEopp et)
-  | (_, opposite ?t) =>
+
+  (* special cases (XXX can/should we be less syntactic?) *)
+  | (_, @multiplication Z _ _ ?z ?t) =>
       let et := reify_term Tring lvar t in
-      open_constr:(PEopp et)
+      open_constr:(PEmul (PEc z) et)
   | (_, pow_N ?t ?n) =>
       let et := reify_term Tring lvar t in
       open_constr:(PEpow et n)
   | (_, @power _ _ power_ring ?t ?n) =>
       let et := reify_term Tring lvar t in
       open_constr:(PEpow et (ZN n))
+
+  (* extensibility and variable case *)
   | _ =>
       let extra := extra_reify term in
       lazymatch extra with