aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/micromega/certificate.ml8
-rw-r--r--plugins/micromega/g_zify.mlg22
-rw-r--r--plugins/micromega/zify.ml143
-rw-r--r--plugins/micromega/zify.mli3
4 files changed, 110 insertions, 66 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 53aa619d10..1018271751 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -449,6 +449,8 @@ let bound_monomials (sys : WithProof.t list) =
in
List.map snd (List.filter has_mon bounds) @ snd l
+let bound_monomials = tr_sys "bound_monomials" bound_monomials
+
let develop_constraints prfdepth n_spec sys =
LinPoly.MonT.clear ();
max_nb_cstr := compute_max_nb_cstr sys prfdepth;
@@ -1181,10 +1183,12 @@ let nlia enum prfdepth sys =
It would only be safe if the variable is linear...
*)
let sys1 =
- elim_simple_linear_equality (WithProof.subst_constant true sys)
+ normalise
+ (elim_simple_linear_equality (WithProof.subst_constant true sys))
in
+ let bnd1 = bound_monomials sys1 in
let sys2 = saturate_by_linear_equalities sys1 in
- let sys3 = nlinear_preprocess (sys1 @ sys2) in
+ let sys3 = nlinear_preprocess (rev_concat [bnd1; sys1; sys2]) in
let sys4 = make_cstr_system (*sys2@*) sys3 in
(* [reduction_equations] is too brutal - there should be some non-linear reasoning *)
xlia (List.map fst sys) enum reduction_equations sys4
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..b780c1833e 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,7 @@ 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
+let op_I = lazy (zify "I")
(** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map.
This is useful for calling Constr.hash *)
@@ -59,6 +72,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 +358,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 +390,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 +448,7 @@ module EBinOp = struct
open EBinOpT
let name = "BinOp"
+ let gref = coq_BinOp
let table = table
let mk_elt evd i a =
@@ -473,6 +490,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 +517,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 +550,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 +577,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 +590,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 +602,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 +634,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 +643,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 +661,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 +697,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 +711,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 +725,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
@@ -1511,41 +1539,51 @@ let spec_of_hyps =
let iter_specs = spec_of_hyps
let find_hyp evd t l =
- try Some (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l))
+ try
+ Some
+ (EConstr.mkVar
+ (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l)))
with Not_found -> None
-let sat_constr c d =
- Proofview.Goal.enter (fun gl ->
- let evd = Tacmach.New.project gl in
- let env = Tacmach.New.pf_env gl in
- let hyps = Tacmach.New.pf_hyps_types gl in
- match EConstr.kind evd c with
- | App (c, args) ->
- if Array.length args = 2 then
- let h1 =
- Tacred.cbv_beta env evd
- (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|]))
- in
- let h2 =
- Tacred.cbv_beta env evd
- (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|]))
- in
- match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with
- | Some h1, Some h2 ->
- let n =
- Tactics.fresh_id_in_env Id.Set.empty
- (Names.Id.of_string "__sat")
- env
- in
- let trm =
- EConstr.mkApp
- ( d.ESatT.satOK
- , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] )
- in
- Tactics.pose_proof (Names.Name n) trm
- | _, _ -> Tacticals.New.tclIDTAC
- else Tacticals.New.tclIDTAC
- | _ -> Tacticals.New.tclIDTAC)
+let find_proof evd t l =
+ if EConstr.eq_constr evd t (Lazy.force op_True) then Some (Lazy.force op_I)
+ else find_hyp evd t l
+
+(** [sat_constr env evd sub taclist hyps c d]= (sub',taclist',hyps') where
+ - sub' is a fresh subscript obtained from sub
+ - taclist' is obtained from taclist by posing the lemma 'd' applied to 'c'
+ - hyps' is obtained from hyps'
+ taclist and hyps are threaded to avoid adding duplicates
+ *)
+let sat_constr env evd (sub,taclist, hyps) c d =
+ match EConstr.kind evd c with
+ | App (c, args) ->
+ if Array.length args = 2 then
+ let h1 =
+ Tacred.cbv_beta env evd
+ (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|]))
+ in
+ let h2 =
+ Tacred.cbv_beta env evd
+ (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|]))
+ in
+ let n = Nameops.add_subscript (Names.Id.of_string "__sat") sub in
+ let trm =
+ match (find_proof evd h1 hyps, find_proof evd h2 hyps) with
+ | Some h1, Some h2 ->
+ (EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1; h2|]))
+ | Some h1, _ ->
+ EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1|])
+ | _, _ -> EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1)|])
+ in
+ let rtrm = Tacred.cbv_beta env evd trm in
+ let typ = Retyping.get_type_of env evd rtrm in
+ match find_hyp evd typ hyps with
+ | None -> (Nameops.Subscript.succ sub, (Tactics.pose_proof (Names.Name n) rtrm :: taclist) , (n,typ)::hyps)
+ | Some _ -> (sub, taclist, hyps)
+ else (sub,taclist,hyps)
+ | _ -> (sub,taclist,hyps)
+
let get_all_sat env evd c =
List.fold_left
@@ -1569,8 +1607,10 @@ let saturate =
Array.iter sat args;
if Array.length args = 2 then
let ds = get_all_sat env evd c in
- if ds = [] then ()
- else List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds
+ if ds = [] || CstrTable.HConstr.mem table t
+ then ()
+ else List.iter (fun x ->
+ CstrTable.HConstr.add table t x.deriv) ds
else ()
| Prod (a, t1, t2) when a.Context.binder_name = Names.Anonymous ->
sat t1; sat t2
@@ -1579,5 +1619,6 @@ let saturate =
(* Collect all the potential saturation lemma *)
sat concl;
List.iter (fun (_, t) -> sat t) hyps;
- Tacticals.New.tclTHENLIST
- (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table []))
+ let s0 = fresh_subscript env in
+ let (_,tacs,_) = CstrTable.HConstr.fold (fun c d acc -> sat_constr env evd acc c d) table (s0,[],hyps) in
+ Tacticals.New.tclTHENLIST tacs)
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:50:59 +0000