aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/mlutil.ml3
-rw-r--r--plugins/funind/gen_principle.ml7
-rw-r--r--plugins/funind/glob_termops.ml2
-rw-r--r--plugins/micromega/certificate.ml8
-rw-r--r--plugins/micromega/g_zify.mlg22
-rw-r--r--plugins/micromega/zify.ml168
-rw-r--r--plugins/micromega/zify.mli3
7 files changed, 135 insertions, 78 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index cfdaac710b..268d4bf9e9 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1525,8 +1525,7 @@ let inline_test r t =
else
let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in
let has_body =
- try constant_has_body (Global.lookup_constant c)
- with Not_found -> false
+ Environ.mem_constant c (Global.env()) && constant_has_body (Global.lookup_constant c)
in
has_body &&
(let t1 = eta_red t in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 5980446508..f1a3cb6af8 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -2058,13 +2058,12 @@ let make_graph (f_ref : GlobRef.t) =
let sigma = Evd.from_env env in
let c, c_body =
match f_ref with
- | GlobRef.ConstRef c -> (
- try (c, Global.lookup_constant c)
- with Not_found ->
+ | GlobRef.ConstRef c ->
+ if Environ.mem_constant c (Global.env ()) then (c, Global.lookup_constant c) else
CErrors.user_err
Pp.(
str "Cannot find "
- ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c)) )
+ ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c))
| _ -> CErrors.user_err Pp.(str "Not a function reference")
in
match Global.body_of_constant_body Library.indirect_accessor c_body with
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 164a446fe3..fb00d2f202 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -342,7 +342,7 @@ let is_free_in id =
| GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ -> false
| GHole _ -> false
| GCast (b, (CastConv t | CastVM t | CastNative t)) ->
- is_free_in b || is_free_in t | GCast (b, CastCoerce) -> is_free_in b
+ is_free_in b || is_free_in t
| GInt _ | GFloat _ -> false
| GArray (_u, t, def, ty) ->
Array.exists is_free_in t || is_free_in def || is_free_in ty)
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..3ea7408067 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")
@@ -33,6 +46,7 @@ let mkrel = lazy (zify "mkrel")
let iff_refl = lazy (zify "iff_refl")
let eq_iff = lazy (zify "eq_iff")
let rew_iff = lazy (zify "rew_iff")
+let rew_iff_rev = lazy (zify "rew_iff_rev")
(* propositional logic *)
@@ -46,7 +60,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 +73,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 +359,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 +391,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 +449,7 @@ module EBinOp = struct
open EBinOpT
let name = "BinOp"
+ let gref = coq_BinOp
let table = table
let mk_elt evd i a =
@@ -473,6 +491,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 +518,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 +551,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 +578,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 +591,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 +603,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
@@ -599,20 +622,26 @@ module MakeTable (E : Elt) = struct
failwith ("Cannot register term " ^ t)
| Some a -> E.mk_elt evd i a
+ let safe_ref evd c =
+ try
+ fst (EConstr.destRef evd c)
+ with DestKO -> CErrors.user_err Pp.(str "Add Zify "++str E.name ++ str ": the term "++
+ gl_pr_constr c ++ str " should be a global reference")
+
let register_hint evd t elt =
match EConstr.kind evd t with
| App (c, _) ->
- let gr = fst (EConstr.destRef evd c) in
- E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table
+ let gr = safe_ref evd c in
+ E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table
| _ ->
- let gr = fst (EConstr.destRef evd t) in
- E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table
+ let gr = safe_ref evd t in
+ E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table
let register_constr env evd c =
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 +650,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 +668,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 +704,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 +718,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 +732,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
@@ -1337,7 +1372,15 @@ let trans_concl prfp =
Tactics.change_concl t')
| TProof (t, prf) ->
Proofview.Goal.enter (fun gl ->
- Equality.general_rewrite true Locus.AllOccurrences true false prf)
+ let env = Tacmach.New.pf_env gl in
+ let evd = Tacmach.New.project gl in
+ let typ = get_type_of env evd prf in
+ match EConstr.kind evd typ with
+ | App (c, a) when Array.length a = 2 ->
+ Tactics.apply
+ (EConstr.mkApp (Lazy.force rew_iff_rev, [|a.(0); a.(1); prf|]))
+ | _ ->
+ raise (CErrors.anomaly Pp.(str "zify cannot transform conclusion")))
let tclTHENOpt e tac tac' =
match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac'
@@ -1511,41 +1554,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 +1622,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 +1634,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-05-01 12:39:45 +0000