diff options
-rw-r--r-- | proofs/tacmach.ml | 6 | ||||
-rw-r--r-- | proofs/tacmach.mli | 8 | ||||
-rw-r--r-- | tactics/equality.ml | 6 | ||||
-rw-r--r-- | tactics/hipattern.ml4 | 4 | ||||
-rw-r--r-- | tactics/hipattern.mli | 2 | ||||
-rw-r--r-- | tactics/inv.ml | 20 | ||||
-rw-r--r-- | tactics/tacticals.ml | 3 | ||||
-rw-r--r-- | tactics/tacticals.mli | 4 | ||||
-rw-r--r-- | tactics/tactics.ml | 9 | ||||
-rw-r--r-- | tactics/tactics.mli | 1 |
10 files changed, 39 insertions, 24 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 943974489..fcba8119d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -271,4 +271,10 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_betadeltaiota gl (pf_get_type_of gl t) + let pf_matches gl pat t = pf_apply ConstrMatching.matches_conv gl pat t + + let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t + + let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t + end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index bf0ce04a1..d122b0941 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -148,5 +148,13 @@ module New : sig val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> inductive * types + val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types + + val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr + + val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map + + val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr + end diff --git a/tactics/equality.ml b/tactics/equality.ml index b16f956d0..de2acaf1d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1461,12 +1461,12 @@ let cutSubstInHyp l2r = if l2r then cutSubstInHyp_LR else cutSubstInHyp_RL let try_rewrite tac = Proofview.tclORELSE tac begin function | ConstrMatching.PatternMatchingFailure -> - Tactics.New.tclZEROMSG (str "Not a primitive equality here.") + Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") | e when catchable_exception e -> - Tactics.New.tclZEROMSG + Tacticals.New.tclZEROMSG (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.") | NothingToRewrite -> - Tactics.New.tclZEROMSG + Tacticals.New.tclZEROMSG (strbrk "Nothing to rewrite.") | e -> Proofview.tclZERO e end diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index cc3c4c297..6cc0af2c6 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -421,10 +421,10 @@ let find_this_eq_data_decompose gl eqn = open Tacmach let match_eq_nf gls eqn eq_pat = - match Id.Map.bindings (pf_matches gls (Lazy.force eq_pat) eqn) with + match Id.Map.bindings (Tacmach.New.pf_matches gls (Lazy.force eq_pat) eqn) with | [(m1,t);(m2,x);(m3,y)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); - (t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y) + (t,Tacmach.New.pf_whd_betadeltaiota gls x,Tacmach.New.pf_whd_betadeltaiota gls y) | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms") let dest_nf_eq gls eqn = diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index f8a4d35a8..fc87fc9ed 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -147,7 +147,7 @@ val match_eqdec : constr -> bool * constr * constr * constr * constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) open Proof_type open Tacmach -val dest_nf_eq : goal sigma -> constr -> (constr * constr * constr) +val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr) (** Match a negation *) val is_matching_not : constr -> bool diff --git a/tactics/inv.ml b/tactics/inv.ml index 7a344eeeb..e2129ce53 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -20,7 +20,7 @@ open Environ open Inductiveops open Printer open Retyping -open Tacmach +open Tacmach.New open Clenv open Tacticals.New open Tactics @@ -192,7 +192,7 @@ let dependent_hyps id idlist gl = | [] -> [] | (id1,_,_)::l -> (* Update the type of id1: it may have been subject to rewriting *) - let d = Tacmach.New.pf_get_hyp id1 gl in + let d = pf_get_hyp id1 gl in if occur_var_in_decl (Global.env()) id d then d :: dep_rec l else dep_rec l @@ -307,10 +307,10 @@ let projectAndApply thin id eqname names depids = (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC)) in let substHypIfVariable tac id = - Proofview.Goal.enter begin fun gl -> - let (t,t1,t2) = - Tacmach.New.of_old (fun gls -> Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id)) gl - in + Proofview.Goal.raw_enter begin fun gl -> + (** We only look at the type of hypothesis "id" *) + let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in + let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in match (kind_of_term t1, kind_of_term t2) with | Var id1, _ -> generalizeRewriteIntros (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2 @@ -461,8 +461,8 @@ let raw_inversion inv_kind id status names = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let c = mkVar id in - let reduce_to_atomic_ind = Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind gl in - let type_of = Tacmach.New.pf_type_of gl in + let reduce_to_atomic_ind = pf_apply Tacred.reduce_to_atomic_ind gl in + let type_of = pf_type_of gl in begin try Proofview.tclUNIT (reduce_to_atomic_ind (type_of c)) @@ -543,12 +543,12 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) let invIn k names ids id = Proofview.Goal.enter begin fun gl -> - let hyps = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) ids in + let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let concl = Proofview.Goal.concl gl in let nb_prod_init = nb_prod concl in let intros_replace_ids = Proofview.Goal.raw_enter begin fun gl -> - let concl = Tacmach.New.pf_nf_concl gl in + let concl = pf_nf_concl gl in let nb_of_new_hyp = nb_prod concl - (List.length hyps + nb_prod_init) in diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 3e35b0a4b..4e42bff7f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -380,6 +380,9 @@ module New = struct let tclFAIL lvl msg = tclZERO (Refiner.FailError (lvl,lazy msg)) + let tclZEROMSG msg = + tclZERO (UserError ("", msg)) + let catch_failerror e = try Refiner.catch_failerror e; diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index ceaa6f27c..0e4c1eb73 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -194,6 +194,10 @@ module New : sig (meaning that it will jump over [n] error catching tacticals FROM THIS MODULE. *) val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic + + val tclZEROMSG : Pp.std_ppcmds -> unit tactic + (** Fail with a [User_Error] containing the given message. *) + val tclOR : unit tactic -> unit tactic -> unit tactic val tclONCE : unit tactic -> unit tactic val tclEXACTLY_ONCE : unit tactic -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c61192031..1f88ed645 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -46,9 +46,6 @@ open Proofview.Notations exception Bound -let tclZEROMSG msg = - Proofview.tclZERO (UserError ("", msg)) - let nb_prod x = let rec count n c = match kind_of_term c with @@ -724,7 +721,7 @@ let cut c = let r = Goal.bind c Goal.refine in Proofview.tclSENSITIVE r else - tclZEROMSG (str "Not a proposition or a type.") + Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") end let cut_intro t = Tacticals.New.tclTHENFIRST (cut t) intro @@ -1188,7 +1185,7 @@ let assumption = if only_eq then let hyps = Proofview.Goal.hyps gl in arec gl false hyps - else tclZEROMSG (str "No such assumption.") + else Tacticals.New.tclZEROMSG (str "No such assumption.") | (id, c, t)::rest -> let concl = Proofview.Goal.concl gl in let is_same_type = @@ -3927,6 +3924,4 @@ module New = struct ) end - let tclZEROMSG = tclZEROMSG - end diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f3c5e7d26..9f4f0e9ce 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -417,5 +417,4 @@ module New : sig open Proofview val exact_proof : Constrexpr.constr_expr -> unit tactic - val tclZEROMSG : Pp.std_ppcmds -> unit tactic end |