[zify] better error reporting

The vernacular command takes a reference instead of a constr.
Moreover, the head symbol is checked i.e
Add Zify InjTyp ref checks that the referenced term has type
Intyp X1 ... Xn

Closes #14054, #13242

Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>

3 files changed, 53 insertions, 27 deletions

diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index 74b0708743..d18065088c 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -24,17 +24,17 @@ let warn_deprecated_Spec =
 DECLARE PLUGIN "zify_plugin"
 
 VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
-| ["Add" "Zify" "InjTyp"    constr(t) ] -> { Zify.InjTable.register t }
-| ["Add" "Zify" "BinOp"     constr(t) ] -> { Zify.BinOp.register t }
-| ["Add" "Zify" "UnOp"      constr(t) ] -> { Zify.UnOp.register t }
-| ["Add" "Zify" "CstOp"     constr(t) ] -> { Zify.CstOp.register t }
-| ["Add" "Zify" "BinRel"    constr(t) ] -> { Zify.BinRel.register t }
-| ["Add" "Zify" "PropOp"    constr(t) ] -> { Zify.PropBinOp.register t }
-| ["Add" "Zify" "PropBinOp"    constr(t) ] -> { Zify.PropBinOp.register t }
-| ["Add" "Zify" "PropUOp"   constr(t) ] -> { Zify.PropUnOp.register t }
-| ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t }
-| ["Add" "Zify" "UnOpSpec"  constr(t) ] -> { Zify.UnOpSpec.register t }
-| ["Add" "Zify" "Saturate"  constr(t) ] -> { Zify.Saturate.register t }
+| ["Add" "Zify" "InjTyp"   reference(t) ] -> { Zify.InjTable.register t }
+| ["Add" "Zify" "BinOp"     reference(t) ] -> { Zify.BinOp.register t }
+| ["Add" "Zify" "UnOp"      reference(t) ] -> { Zify.UnOp.register t }
+| ["Add" "Zify" "CstOp"     reference(t) ] -> { Zify.CstOp.register t }
+| ["Add" "Zify" "BinRel"    reference(t) ] -> { Zify.BinRel.register t }
+| ["Add" "Zify" "PropOp"    reference(t) ] -> { Zify.PropBinOp.register t }
+| ["Add" "Zify" "PropBinOp"    reference(t) ] -> { Zify.PropBinOp.register t }
+| ["Add" "Zify" "PropUOp"   reference(t) ] -> { Zify.PropUnOp.register t }
+| ["Add" "Zify" "BinOpSpec" reference(t) ] -> { Zify.BinOpSpec.register t }
+| ["Add" "Zify" "UnOpSpec"  reference(t) ] -> { Zify.UnOpSpec.register t }
+| ["Add" "Zify" "Saturate"  reference(t) ] -> { Zify.Saturate.register t }
 END
 
 TACTIC EXTEND ITER
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 800dc6cee2..2cb615170b 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -23,6 +23,19 @@ let zify str =
     (UnivGen.constr_of_monomorphic_global
        (Coqlib.lib_ref ("ZifyClasses." ^ str)))
 
+(** classes *)
+let coq_InjTyp = lazy (Coqlib.lib_ref "ZifyClasses.InjTyp")
+
+let coq_BinOp = lazy (Coqlib.lib_ref "ZifyClasses.BinOp")
+let coq_UnOp = lazy (Coqlib.lib_ref "ZifyClasses.UnOp")
+let coq_CstOp = lazy (Coqlib.lib_ref "ZifyClasses.CstOp")
+let coq_BinRel = lazy (Coqlib.lib_ref "ZifyClasses.BinRel")
+let coq_PropBinOp = lazy (Coqlib.lib_ref "ZifyClasses.PropBinOp")
+let coq_PropUOp = lazy (Coqlib.lib_ref "ZifyClasses.PropUOp")
+let coq_BinOpSpec = lazy (Coqlib.lib_ref "ZifyClasses.BinOpSpec")
+let coq_UnOpSpec = lazy (Coqlib.lib_ref "ZifyClasses.UnOpSpec")
+let coq_Saturate = lazy (Coqlib.lib_ref "ZifyClasses.Saturate")
+
 (* morphism like lemma *)
 
 let mkapp2 = lazy (zify "mkapp2")
@@ -46,7 +59,6 @@ let op_iff_morph = lazy (zify "iff_morph")
 let op_not = lazy (zify "not")
 let op_not_morph = lazy (zify "not_morph")
 let op_True = lazy (zify "True")
-let whd = Reductionops.clos_whd_flags CClosure.all
 
 (** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map.
     This is useful for calling Constr.hash *)
@@ -59,6 +71,7 @@ let gl_pr_constr e =
   let evd = Evd.from_env genv in
   pr_constr genv evd e
 
+let whd = Reductionops.clos_whd_flags CClosure.all
 let is_convertible env evd t1 t2 = Reductionops.(is_conv env evd t1 t2)
 
 (** [get_type_of] performs beta reduction ;
@@ -344,6 +357,7 @@ module type Elt = sig
   (** name *)
   val name : string
 
+  val gref : GlobRef.t Lazy.t
   val table : (term_kind * decl_kind) ConstrMap.t ref
   val cast : elt decl -> decl_kind
   val dest : decl_kind -> elt decl option
@@ -375,6 +389,7 @@ module EInj = struct
   type elt = EInjT.t
 
   let name = "EInj"
+  let gref = coq_InjTyp
   let table = table
   let cast x = InjTyp x
   let dest = function InjTyp x -> Some x | _ -> None
@@ -432,6 +447,7 @@ module EBinOp = struct
   open EBinOpT
 
   let name = "BinOp"
+  let gref = coq_BinOp
   let table = table
 
   let mk_elt evd i a =
@@ -473,6 +489,7 @@ module ECstOp = struct
   open ECstOpT
 
   let name = "CstOp"
+  let gref = coq_CstOp
   let table = table
   let cast x = CstOp x
   let dest = function CstOp x -> Some x | _ -> None
@@ -499,6 +516,7 @@ module EUnOp = struct
   open EUnOpT
 
   let name = "UnOp"
+  let gref = coq_UnOp
   let table = table
   let cast x = UnOp x
   let dest = function UnOp x -> Some x | _ -> None
@@ -531,6 +549,7 @@ module EBinRel = struct
   open EBinRelT
 
   let name = "BinRel"
+  let gref = coq_BinRel
   let table = table
   let cast x = BinRel x
   let dest = function BinRel x -> Some x | _ -> None
@@ -557,6 +576,7 @@ module EPropBinOp = struct
   open EPropBinOpT
 
   let name = "PropBinOp"
+  let gref = coq_PropBinOp
   let table = table
   let cast x = PropOp x
   let dest = function PropOp x -> Some x | _ -> None
@@ -569,7 +589,8 @@ module EPropUnOp = struct
 
   open EPropUnOpT
 
-  let name = "PropUnOp"
+  let name = "PropUOp"
+  let gref = coq_PropUOp
   let table = table
   let cast x = PropUnOp x
   let dest = function PropUnOp x -> Some x | _ -> None
@@ -580,7 +601,7 @@ end
 let constr_of_term_kind = function Application c -> c | OtherTerm c -> c
 
 module type S = sig
-  val register : Constrexpr.constr_expr -> unit
+  val register : Libnames.qualid -> unit
   val print : unit -> unit
 end
 
@@ -612,7 +633,7 @@ module MakeTable (E : Elt) = struct
     let c = EConstr.of_constr c in
     let t = get_type_of env evd c in
     match EConstr.kind evd t with
-    | App (intyp, args) ->
+    | App (intyp, args) when EConstr.isRefX evd (Lazy.force E.gref) intyp ->
       let styp = args.(E.get_key) in
       let elt = {decl = c; deriv = make_elt (evd, c)} in
       register_hint evd styp elt
@@ -621,10 +642,11 @@ module MakeTable (E : Elt) = struct
       raise
         (CErrors.user_err
            Pp.(
-             str ": Cannot register term "
-             ++ pr_constr env evd c ++ str ". It has type "
-             ++ pr_constr env evd t
-             ++ str " which should be of the form  [F X1 .. Xn]"))
+             str "Cannot register " ++ pr_constr env evd c
+             ++ str ". It has type " ++ pr_constr env evd t
+             ++ str " instead of type "
+             ++ Printer.pr_global (Lazy.force E.gref)
+             ++ str " X1 ... Xn"))
 
   let register_obj : Constr.constr -> Libobject.obj =
     let cache_constr (_, c) =
@@ -638,17 +660,19 @@ module MakeTable (E : Elt) = struct
          ("register-zify-" ^ E.name)
          ~cache:cache_constr ~subst:(Some subst_constr)
 
-  (** [register c] is called from the VERNACULAR ADD [name] constr(t).
+  (** [register c] is called from the VERNACULAR ADD [name] reference(t).
        The term [c] is interpreted and
        registered as a [superglobal_object_nodischarge].
        TODO: pre-compute [get_type_of] - [cache_constr] is using another environment.
      *)
   let register c =
-    let env = Global.env () in
-    let evd = Evd.from_env env in
-    let evd, c = Constrintern.interp_open_constr env evd c in
-    let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in
-    ()
+    try
+      let c = UnivGen.constr_of_monomorphic_global (Nametab.locate c) in
+      let _ = Lib.add_anonymous_leaf (register_obj c) in
+      ()
+    with Not_found ->
+      raise
+        (CErrors.user_err Pp.(Libnames.pr_qualid c ++ str " does not exist."))
 
   let pp_keys () =
     let env = Global.env () in
@@ -672,6 +696,7 @@ module ESat = struct
   open ESatT
 
   let name = "Saturate"
+  let gref = coq_Saturate
   let table = saturate
   let cast x = Saturate x
   let dest = function Saturate x -> Some x | _ -> None
@@ -685,6 +710,7 @@ module EUnopSpec = struct
   type elt = ESpecT.t
 
   let name = "UnopSpec"
+  let gref = coq_UnOpSpec
   let table = specs
   let cast x = UnOpSpec x
   let dest = function UnOpSpec x -> Some x | _ -> None
@@ -698,6 +724,7 @@ module EBinOpSpec = struct
   type elt = ESpecT.t
 
   let name = "BinOpSpec"
+  let gref = coq_BinOpSpec
   let table = specs
   let cast x = BinOpSpec x
   let dest = function BinOpSpec x -> Some x | _ -> None
diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli
index 555bb4c7fb..68f23393ee 100644
--- a/plugins/micromega/zify.mli
+++ b/plugins/micromega/zify.mli
@@ -7,10 +7,9 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
-open Constrexpr
 
 module type S = sig
-  val register : constr_expr -> unit
+  val register : Libnames.qualid -> unit
   val print : unit -> unit
 end