aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/micromega/g_zify.mlg22
-rw-r--r--plugins/micromega/zify.ml55
-rw-r--r--plugins/micromega/zify.mli3
-rw-r--r--test-suite/micromega/bug_14054.v46
-rw-r--r--theories/micromega/ZifyClasses.v10
5 files changed, 109 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
diff --git a/test-suite/micromega/bug_14054.v b/test-suite/micromega/bug_14054.v
new file mode 100644
index 0000000000..d97e13375f
--- /dev/null
+++ b/test-suite/micromega/bug_14054.v
@@ -0,0 +1,46 @@
+(* bug 13242 *)
+
+Require Import Lia.
+Fail Add Zify InjTyp id.
+
+(* bug 14054 *)
+
+Require Import Coq.ZArith.ZArith. Open Scope Z_scope.
+Require Coq.Init.Byte .
+Require Import Coq.micromega.ZifyClasses Coq.micromega.Lia.
+
+Notation byte := Coq.Init.Byte.byte.
+
+Module byte.
+ Definition unsigned(b: byte): Z := Z.of_N (Byte.to_N b).
+End byte.
+
+Section WithA.
+ Context (A: Type).
+ Fixpoint tuple(n: nat): Type :=
+ match n with
+ | O => unit
+ | S m => A * tuple m
+ end.
+End WithA.
+
+Module LittleEndian.
+ Fixpoint combine (n : nat) : forall (bs : tuple byte n), Z :=
+ match n with
+ | O => fun _ => 0
+ | S n => fun bs => Z.lor (byte.unsigned (fst bs))
+ (Z.shiftl (combine n (snd bs)) 8)
+ end.
+ Lemma combine_bound: forall {n: nat} (t: tuple byte n),
+ 0 <= LittleEndian.combine n t < 2 ^ (8 * Z.of_nat n).
+ Admitted.
+End LittleEndian.
+
+Instance InjByteTuple{n: nat}: InjTyp (tuple byte n) Z := {|
+ inj := LittleEndian.combine n;
+ pred x := 0 <= x < 2 ^ (8 * Z.of_nat n);
+ cstr := @LittleEndian.combine_bound n;
+|}.
+Fail Add Zify InjTyp InjByteTuple.
+Fail Add Zify UnOp InjByteTuple.
+Fail Add Zify UnOp X.
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index f6ade67c5f..a08a56b20e 100644
--- a/theories/micromega/ZifyClasses.v
+++ b/theories/micromega/ZifyClasses.v
@@ -250,8 +250,18 @@ Register rew_iff as ZifyClasses.rew_iff.
Register source_prop as ZifyClasses.source_prop.
Register injprop_ok as ZifyClasses.injprop_ok.
Register iff as ZifyClasses.iff.
+
+Register InjTyp as ZifyClasses.InjTyp.
+Register BinOp as ZifyClasses.BinOp.
+Register UnOp as ZifyClasses.UnOp.
+Register CstOp as ZifyClasses.CstOp.
+Register BinRel as ZifyClasses.BinRel.
+Register PropOp as ZifyClasses.PropOp.
+Register PropUOp as ZifyClasses.PropUOp.
Register BinOpSpec as ZifyClasses.BinOpSpec.
Register UnOpSpec as ZifyClasses.UnOpSpec.
+Register Saturate as ZifyClasses.Saturate.
+
(** Propositional logic *)
Register and as ZifyClasses.and.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:13:31 +0000