aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/zify.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/zify.ml')
-rw-r--r--plugins/micromega/zify.ml168
1 files changed, 112 insertions, 56 deletions
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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:00:33 +0000