From ea879916e09cd19287c831152d7ae2a84c61f4b0 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:38:20 +0000 Subject: More Proofview.Goal.enter. Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad. This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics. This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17000 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/btauto/refl_btauto.ml | 70 +++++----- plugins/cc/cctac.ml | 184 ++++++++++++++------------- plugins/omega/coq_omega.ml | 246 ++++++++++++++++++------------------ plugins/quote/quote.ml | 22 ++-- plugins/setoid_ring/newring.ml4 | 44 ++++--- proofs/proofview.ml | 15 ++- proofs/proofview.mli | 18 +-- tactics/auto.ml | 30 +++-- tactics/class_tactics.ml | 18 ++- tactics/contradiction.ml | 80 ++++++------ tactics/eqdecide.ml4 | 44 ++++--- tactics/equality.ml | 115 ++++++++++------- tactics/evar_tactics.ml | 12 +- tactics/extratactics.ml4 | 12 +- tactics/inv.ml | 118 +++++++++-------- tactics/leminv.ml | 24 ++-- tactics/rewrite.ml | 58 +++++---- tactics/tacinterp.ml | 217 +++++++++++++++++++------------ tactics/tacticals.ml | 30 +++-- tactics/tactics.ml | 274 +++++++++++++++++++++------------------- toplevel/auto_ind_decl.ml | 62 ++++----- 21 files changed, 928 insertions(+), 765 deletions(-) diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 440309284..8232604f7 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -217,41 +217,45 @@ module Btauto = struct Tacticals.tclFAIL 0 msg gl let try_unification env = - Proofview.Goal.concl >>= fun concl -> - let eq = Lazy.force eq in - let t = decomp_term concl in - match t with - | Term.App (c, [|typ; p; _|]) when c === eq -> + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let eq = Lazy.force eq in + let t = decomp_term concl in + match t with + | Term.App (c, [|typ; p; _|]) when c === eq -> (* should be an equality [@eq poly ?p (Cst false)] *) - let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in - tac - | _ -> - let msg = str "Btauto: Internal error" in - Tacticals.New.tclFAIL 0 msg + let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in + tac + | _ -> + let msg = str "Btauto: Internal error" in + Tacticals.New.tclFAIL 0 msg + end let tac = - Proofview.Goal.concl >>= fun concl -> - let eq = Lazy.force eq in - let bool = Lazy.force Bool.typ in - let t = decomp_term concl in - match t with - | Term.App (c, [|typ; tl; tr|]) - when typ === bool && c === eq -> - let env = Env.empty () in - let fl = Bool.quote env tl in - let fr = Bool.quote env tr in - let env = Env.to_list env in - let fl = reify env fl in - let fr = reify env fr in - let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (Tactics.change_in_concl None changed_gl); - Proofview.V82.tactic (Tactics.apply (Lazy.force soundness)); - Proofview.V82.tactic (Tactics.normalise_vm_in_concl); - try_unification env - ] - | _ -> - let msg = str "Cannot recognize a boolean equality" in - Tacticals.New.tclFAIL 0 msg + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let eq = Lazy.force eq in + let bool = Lazy.force Bool.typ in + let t = decomp_term concl in + match t with + | Term.App (c, [|typ; tl; tr|]) + when typ === bool && c === eq -> + let env = Env.empty () in + let fl = Bool.quote env tl in + let fr = Bool.quote env tr in + let env = Env.to_list env in + let fl = reify env fl in + let fr = reify env fr in + let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (Tactics.change_in_concl None changed_gl); + Proofview.V82.tactic (Tactics.apply (Lazy.force soundness)); + Proofview.V82.tactic (Tactics.normalise_vm_in_concl); + try_unification env + ] + | _ -> + let msg = str "Cannot recognize a boolean equality" in + Tacticals.New.tclFAIL 0 msg + end end diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c12dd4799..dee57cd04 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -348,25 +348,27 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = simplest_elim false_t] let discriminate_tac cstr p = - let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in - Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) >>= fun intype -> - Proofview.Goal.concl >>= fun concl -> - let outsort = mkType (Termops.new_univ ()) in - Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>= fun xid -> - Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) >>= fun tid -> - let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in - Tacmach.New.of_old (fun gls -> pf_type_of gls identity) >>= fun trivial -> - let outtype = mkType (Termops.new_univ ()) in - let pred=mkLambda(Name xid,outtype,mkRel 1) in - Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>= fun hid -> - Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) >>= fun proj -> - let injt=mkApp (Lazy.force _f_equal, - [|intype;outtype;proj;t1;t2;mkVar hid|]) in - let endt=mkApp (Lazy.force _eq_rect, - [|outtype;trivial;pred;identity;concl;injt|]) in - let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in + Proofview.Goal.enter begin fun gl -> + let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in + Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) >>= fun intype -> + let concl = Proofview.Goal.concl gl in + let outsort = mkType (Termops.new_univ ()) in + Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>= fun xid -> + Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) >>= fun tid -> + let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in + Tacmach.New.of_old (fun gls -> pf_type_of gls identity) >>= fun trivial -> + let outtype = mkType (Termops.new_univ ()) in + let pred=mkLambda(Name xid,outtype,mkRel 1) in + Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>= fun hid -> + Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) >>= fun proj -> + let injt=mkApp (Lazy.force _f_equal, + [|intype;outtype;proj;t1;t2;mkVar hid|]) in + let endt=mkApp (Lazy.force _eq_rect, + [|outtype;trivial;pred;identity;concl;injt|]) in + let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in Tacticals.New.tclTHENS (assert_tac (Name hid) neweq) [proof_tac p; Proofview.V82.tactic (exact_check endt)] + end (* wrap everything *) @@ -378,58 +380,58 @@ let build_term_to_complete uf meta pac = applistc (mkConstruct cinfo.ci_constr) all_args let cc_tactic depth additionnal_terms = - Proofview.tclUNIT () >= fun () -> (* delay for check_required_library *) - Coqlib.check_required_library Coqlib.logic_module_name; - let _ = debug (Pp.str "Reading subgoal ...") in - Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) >>= fun state -> - let _ = debug (Pp.str "Problem built, solving ...") in - let sol = execute true state in - let _ = debug (Pp.str "Computation completed.") in - let uf=forest state in + Proofview.Goal.enter begin fun gl -> + Coqlib.check_required_library Coqlib.logic_module_name; + let _ = debug (Pp.str "Reading subgoal ...") in + Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) >>= fun state -> + let _ = debug (Pp.str "Problem built, solving ...") in + let sol = execute true state in + let _ = debug (Pp.str "Computation completed.") in + let uf=forest state in match sol with - None -> Tacticals.New.tclFAIL 0 (str "congruence failed") - | Some reason -> - debug (Pp.str "Goal solved, generating proof ..."); - match reason with - Discrimination (i,ipac,j,jpac) -> - let p=build_proof uf (`Discr (i,ipac,j,jpac)) in - let cstr=(get_constructor_info uf ipac.cnode).ci_constr in - discriminate_tac cstr p - | Incomplete -> - Proofview.Goal.env >>= fun env -> - let metacnt = ref 0 in - let newmeta _ = incr metacnt; _M !metacnt in - let terms_to_complete = - List.map - (build_term_to_complete uf newmeta) - (epsilons uf) in - Pp.msg_info - (Pp.str "Goal is solvable by congruence but \ + None -> Tacticals.New.tclFAIL 0 (str "congruence failed") + | Some reason -> + debug (Pp.str "Goal solved, generating proof ..."); + match reason with + Discrimination (i,ipac,j,jpac) -> + let p=build_proof uf (`Discr (i,ipac,j,jpac)) in + let cstr=(get_constructor_info uf ipac.cnode).ci_constr in + discriminate_tac cstr p + | Incomplete -> + let env = Proofview.Goal.env gl in + let metacnt = ref 0 in + let newmeta _ = incr metacnt; _M !metacnt in + let terms_to_complete = + List.map + (build_term_to_complete uf newmeta) + (epsilons uf) in + Pp.msg_info + (Pp.str "Goal is solvable by congruence but \ some arguments are missing."); - Pp.msg_info - (Pp.str " Try " ++ - hov 8 - begin - str "\"congruence with (" ++ - prlist_with_sep - (fun () -> str ")" ++ spc () ++ str "(") - (Termops.print_constr_env env) - terms_to_complete ++ - str ")\"," - end ++ - Pp.str " replacing metavariables by arbitrary terms."); - Tacticals.New.tclFAIL 0 (str "Incomplete") - | Contradiction dis -> - let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in - let ta=term uf dis.lhs and tb=term uf dis.rhs in - match dis.rule with - Goal -> proof_tac p - | Hyp id -> refute_tac id ta tb p - | HeqG id -> - convert_to_goal_tac id ta tb p - | HeqnH (ida,idb) -> - convert_to_hyp_tac ida ta idb tb p - + Pp.msg_info + (Pp.str " Try " ++ + hov 8 + begin + str "\"congruence with (" ++ + prlist_with_sep + (fun () -> str ")" ++ spc () ++ str "(") + (Termops.print_constr_env env) + terms_to_complete ++ + str ")\"," + end ++ + Pp.str " replacing metavariables by arbitrary terms."); + Tacticals.New.tclFAIL 0 (str "Incomplete") + | Contradiction dis -> + let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in + let ta=term uf dis.lhs and tb=term uf dis.rhs in + match dis.rule with + Goal -> proof_tac p + | Hyp id -> refute_tac id ta tb p + | HeqG id -> + convert_to_goal_tac id ta tb p + | HeqnH (ida,idb) -> + convert_to_hyp_tac ida ta idb tb p + end let cc_fail gls = errorlabstrm "Congruence" (Pp.str "congruence failed.") @@ -453,32 +455,34 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal) *) let f_equal = - Proofview.Goal.concl >>= fun concl -> - Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> - let cut_eq c1 c2 = - try (* type_of can raise an exception *) - let ty = Termops.refresh_universes (type_of c1) in - Proofview.V82.tactic begin - tclTHENTRY - (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) - (simple_reflexivity ()) - end - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - in - Proofview.tclORELSE - begin match kind_of_term concl with - | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> - begin match kind_of_term t, kind_of_term t' with + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> + let cut_eq c1 c2 = + try (* type_of can raise an exception *) + let ty = Termops.refresh_universes (type_of c1) in + Proofview.V82.tactic begin + tclTHENTRY + (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) + (simple_reflexivity ()) + end + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + in + Proofview.tclORELSE + begin match kind_of_term concl with + | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> + begin match kind_of_term t, kind_of_term t' with | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') -> let rec cuts i = if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 []) else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1)) in cuts (Array.length v - 1) | _ -> Proofview.tclUNIT () - end - | _ -> Proofview.tclUNIT () - end - begin function - | Type_errors.TypeError _ -> Proofview.tclUNIT () - | e -> Proofview.tclZERO e - end + end + | _ -> Proofview.tclUNIT () + end + begin function + | Type_errors.TypeError _ -> Proofview.tclUNIT () + | e -> Proofview.tclZERO e + end + end diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index fbf9334e0..c865639e6 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1647,17 +1647,18 @@ let destructure_hyps = Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> Tacmach.New.of_old decidability >>= fun decidability -> Tacmach.New.of_old pf_nf >>= fun pf_nf -> - let rec loop = function - | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) - | (i,body,t)::lit -> - begin try match destructurate_prop t with + Proofview.Goal.enter begin fun gl -> + let rec loop = function + | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) + | (i,body,t)::lit -> + begin try match destructurate_prop t with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> (Tacticals.New.tclTHENS - (elim_id i) - [ onClearedName i (fun i -> (loop ((i,None,t1)::lit))); - onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ]) + (elim_id i) + [ onClearedName i (fun i -> (loop ((i,None,t1)::lit))); + onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ]) | Kapp(And,[t1;t2]) -> Tacticals.New.tclTHEN (elim_id i) @@ -1676,7 +1677,7 @@ let destructure_hyps = let d1 = decidability t1 in Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp, - [| t1; t2; d1; mkVar i|])]); + [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> (loop ((i,None,mk_or (mk_not t1) t2)::lit)))) ] @@ -1684,113 +1685,115 @@ let destructure_hyps = loop lit | Kapp(Not,[t]) -> begin match destructurate_prop t with - Kapp(Or,[t1;t2]) -> - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac - [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); - (onClearedName i (fun i -> - (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit)))) - ] - | Kapp(And,[t1;t2]) -> - let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac - [mkApp (Lazy.force coq_not_and, - [| t1; t2; d1; mkVar i |])]); - (onClearedName i (fun i -> - (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit)))) - ] - | Kapp(Iff,[t1;t2]) -> - let d1 = decidability t1 in - let d2 = decidability t2 in - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac - [mkApp (Lazy.force coq_not_iff, - [| t1; t2; d1; d2; mkVar i |])]); - (onClearedName i (fun i -> - (loop ((i,None, - mk_or (mk_and t1 (mk_not t2)) - (mk_and (mk_not t1) t2))::lit)))) - ] - | Kimp(t1,t2) -> + Kapp(Or,[t1;t2]) -> + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); + (onClearedName i (fun i -> + (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit)))) + ] + | Kapp(And,[t1;t2]) -> + let d1 = decidability t1 in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force coq_not_and, + [| t1; t2; d1; mkVar i |])]); + (onClearedName i (fun i -> + (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit)))) + ] + | Kapp(Iff,[t1;t2]) -> + let d1 = decidability t1 in + let d2 = decidability t2 in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force coq_not_iff, + [| t1; t2; d1; d2; mkVar i |])]); + (onClearedName i (fun i -> + (loop ((i,None, + mk_or (mk_and t1 (mk_not t2)) + (mk_and (mk_not t1) t2))::lit)))) + ] + | Kimp(t1,t2) -> (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok. For t1, being decidable implies being Prop. *) - let d1 = decidability t1 in - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac - [mkApp (Lazy.force coq_not_imp, - [| t1; t2; d1; mkVar i |])]); - (onClearedName i (fun i -> - (loop ((i,None,mk_and t1 (mk_not t2)) :: lit)))) - ] - | Kapp(Not,[t]) -> - let d = decidability t in - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac - [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); - (onClearedName i (fun i -> (loop ((i,None,t)::lit)))) - ] - | Kapp(op,[t1;t2]) -> - (try - let thm = not_binop op in - Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac - [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); - (onClearedName i (fun _ -> loop lit)) - ] - with Not_found -> loop lit) - | Kapp(Eq,[typ;t1;t2]) -> - if !old_style_flag then begin - match destructurate_type (pf_nf typ) with - | Kapp(Nat,_) -> - Tacticals.New.tclTHENLIST [ - (simplest_elim - (mkApp - (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); - (onClearedName i (fun _ -> loop lit)) - ] - | Kapp(Z,_) -> - Tacticals.New.tclTHENLIST [ - (simplest_elim - (mkApp - (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); - (onClearedName i (fun _ -> loop lit)) - ] - | _ -> loop lit - end else begin - match destructurate_type (pf_nf typ) with - | Kapp(Nat,_) -> - (Tacticals.New.tclTHEN - (Proofview.V82.tactic (convert_hyp_no_check - (i,body, - (mkApp (Lazy.force coq_neq, [| t1;t2|]))))) - (loop lit)) - | Kapp(Z,_) -> - (Tacticals.New.tclTHEN - (Proofview.V82.tactic (convert_hyp_no_check - (i,body, - (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))) - (loop lit)) - | _ -> loop lit - end - | _ -> loop lit + let d1 = decidability t1 in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force coq_not_imp, + [| t1; t2; d1; mkVar i |])]); + (onClearedName i (fun i -> + (loop ((i,None,mk_and t1 (mk_not t2)) :: lit)))) + ] + | Kapp(Not,[t]) -> + let d = decidability t in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); + (onClearedName i (fun i -> (loop ((i,None,t)::lit)))) + ] + | Kapp(op,[t1;t2]) -> + (try + let thm = not_binop op in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac + [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); + (onClearedName i (fun _ -> loop lit)) + ] + with Not_found -> loop lit) + | Kapp(Eq,[typ;t1;t2]) -> + if !old_style_flag then begin + match destructurate_type (pf_nf typ) with + | Kapp(Nat,_) -> + Tacticals.New.tclTHENLIST [ + (simplest_elim + (mkApp + (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); + (onClearedName i (fun _ -> loop lit)) + ] + | Kapp(Z,_) -> + Tacticals.New.tclTHENLIST [ + (simplest_elim + (mkApp + (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); + (onClearedName i (fun _ -> loop lit)) + ] + | _ -> loop lit + end else begin + match destructurate_type (pf_nf typ) with + | Kapp(Nat,_) -> + (Tacticals.New.tclTHEN + (Proofview.V82.tactic (convert_hyp_no_check + (i,body, + (mkApp (Lazy.force coq_neq, [| t1;t2|]))))) + (loop lit)) + | Kapp(Z,_) -> + (Tacticals.New.tclTHEN + (Proofview.V82.tactic (convert_hyp_no_check + (i,body, + (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))) + (loop lit)) + | _ -> loop lit + end + | _ -> loop lit end | _ -> loop lit - with - | Undecidable -> loop lit - | e when catchable_exception e -> loop lit - end - in - Proofview.Goal.hyps >>= fun hyps -> - try (* type_of can raise exceptions *) - loop (Environ.named_context_of_val hyps) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + with + | Undecidable -> loop lit + | e when catchable_exception e -> loop lit + end + in + let hyps = Proofview.Goal.hyps gl in + try (* type_of can raise exceptions *) + loop (Environ.named_context_of_val hyps) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end let destructure_goal = - Proofview.Goal.concl >>= fun concl -> - Tacmach.New.of_old decidability >>= fun decidability -> - let rec loop t = - match destructurate_prop t with + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + Tacmach.New.of_old decidability >>= fun decidability -> + let rec loop t = + match destructurate_prop t with | Kapp(Not,[t]) -> (Tacticals.New.tclTHEN (Tacticals.New.tclTHEN (Proofview.V82.tactic (unfold sp_not)) intro) @@ -1798,18 +1801,19 @@ let destructure_goal = | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b)) | Kapp(False,[]) -> destructure_hyps | _ -> - let goal_tac = - try - let dec = decidability t in - Tacticals.New.tclTHEN - (Proofview.V82.tactic (Tactics.refine - (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))) - intro - with Undecidable -> Proofview.V82.tactic (Tactics.elim_type (build_coq_False ())) - in - Tacticals.New.tclTHEN goal_tac destructure_hyps - in - (loop concl) + let goal_tac = + try + let dec = decidability t in + Tacticals.New.tclTHEN + (Proofview.V82.tactic (Tactics.refine + (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))) + intro + with Undecidable -> Proofview.V82.tactic (Tactics.elim_type (build_coq_False ())) + in + Tacticals.New.tclTHEN goal_tac destructure_hyps + in + (loop concl) + end let destructure_goal = destructure_goal diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index bf061095c..89d161f73 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -453,18 +453,20 @@ let quote_terms ivs lc = yet. *) let quote f lid = - Tacmach.New.pf_global f >>= fun f -> - Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl -> - Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs -> - Proofview.Goal.concl >>= fun concl -> - Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms -> - let (p, vm) = match quoted_terms with - | [p], vm -> (p,vm) - | _ -> assert false - in - match ivs.variable_lhs with + Proofview.Goal.enter begin fun gl -> + Tacmach.New.pf_global f >>= fun f -> + Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl -> + Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs -> + let concl = Proofview.Goal.concl gl in + Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms -> + let (p, vm) = match quoted_terms with + | [p], vm -> (p,vm) + | _ -> assert false + in + match ivs.variable_lhs with | None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast) | Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast) + end let gen_quote cont c f lid = Tacmach.New.pf_global f >>= fun f -> diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 7bd0c7e43..aee7efb76 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -798,16 +798,18 @@ let ltac_ring_structure e = open Proofview.Notations let ring_lookup (f:glob_tactic_expr) lH rl t = - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> - try (* find_ring_strucure can raise an exception *) - let rl = make_args_list rl t in - let e = find_ring_structure env sigma rl in - let rl = carg (make_term_list e.ring_carrier rl) in - let lH = carg (make_hyp_list env lH) in - let ring = ltac_ring_structure e in - ltac_apply f (ring@[lH;rl]) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + try (* find_ring_strucure can raise an exception *) + let rl = make_args_list rl t in + let e = find_ring_structure env sigma rl in + let rl = carg (make_term_list e.ring_carrier rl) in + let lH = carg (make_hyp_list env lH) in + let ring = ltac_ring_structure e in + ltac_apply f (ring@[lH;rl]) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> @@ -1121,16 +1123,18 @@ let ltac_field_structure e = field_simpl_eq_in_ok;cond_ok;pretac;posttac] let field_lookup (f:glob_tactic_expr) lH rl t = - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> - try - let rl = make_args_list rl t in - let e = find_field_structure env sigma rl in - let rl = carg (make_term_list e.field_carrier rl) in - let lH = carg (make_hyp_list env lH) in - let field = ltac_field_structure e in - ltac_apply f (field@[lH;rl]) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + try + let rl = make_args_list rl t in + let e = find_field_structure env sigma rl in + let rl = carg (make_term_list e.field_carrier rl) in + let lH = carg (make_hyp_list env lH) in + let field = ltac_field_structure e in + ltac_apply f (field@[lH;rl]) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end TACTIC EXTEND field_lookup diff --git a/proofs/proofview.ml b/proofs/proofview.ml index dace158ac..364cfeb4b 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -668,7 +668,12 @@ end module Goal = struct - type 'a u = 'a list + type t = Environ.env*Evd.evar_map*Environ.named_context_val*Term.constr + + let env (env,_,_,_) = env + let sigma (_,sigma,_,_) = sigma + let hyps (_,_,hyps,_) = hyps + let concl (_,_,_,concl) = concl let lift s = (* spiwack: convenience notations, waiting for ocaml 3.12 *) @@ -688,15 +693,13 @@ module Goal = struct tclZERO e let return x = lift (Goal.return x) - let concl = lift Goal.concl - let hyps = lift Goal.hyps - let env = lift Goal.env + let enter_t f = Goal.enter (fun env sigma hyps concl -> f (env,sigma,hyps,concl)) let enter f = - lift (Goal.enter f) >= fun ts -> + lift (enter_t f) >= fun ts -> tclDISPATCH ts let enterl f = - lift (Goal.enter f) >= fun ts -> + lift (enter_t f) >= fun ts -> tclDISPATCHL ts >= fun res -> tclUNIT (List.flatten res) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index fa1a8d56f..6d5e9d75d 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -283,6 +283,13 @@ end module Goal : sig + type t + + val concl : t -> Term.constr + val hyps : t -> Environ.named_context_val + val env : t -> Environ.env + val sigma : t -> Evd.evar_map + (* [lift_sensitive s] returns the list corresponding to the evaluation of [s] on each of the focused goals *) val lift : 'a Goal.sensitive -> 'a glist tactic @@ -290,14 +297,9 @@ module Goal : sig (* [lift (Goal.return x)] *) val return : 'a -> 'a glist tactic - val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> unit tactic) -> unit tactic - val enterl : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> 'a glist tactic) -> 'a glist tactic - (* [lift Goal.concl] *) - val concl : Term.constr glist tactic - (* [lift Goal.hyps] *) - val hyps : Environ.named_context_val glist tactic - (* [lift Goal.env] *) - val env : Environ.env glist tactic + val enter : (t -> unit tactic) -> unit tactic + val enterl : (t -> 'a glist tactic) -> 'a glist tactic + end diff --git a/tactics/auto.ml b/tactics/auto.ml index 35b0dc7ff..728eaa3fe 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1275,17 +1275,21 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption let rec trivial_fail_db dbg mod_delta db_list local_db = let intro_tac = Tacticals.New.tclTHEN (dbg_intro dbg) - ( Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> - Tacmach.New.pf_last_hyp >>= fun hyp -> - let hintl = make_resolve_hyp env sigma hyp - in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db)) + ( Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + Tacmach.New.pf_last_hyp >>= fun hyp -> + let hintl = make_resolve_hyp env sigma hyp + in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db) + end) in - Proofview.Goal.concl >>= fun concl -> - Tacticals.New.tclFIRST - ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac:: - (List.map Tacticals.New.tclCOMPLETE - (trivial_resolve dbg mod_delta db_list local_db concl))) + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + Tacticals.New.tclFIRST + ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac:: + (List.map Tacticals.New.tclCOMPLETE + (trivial_resolve dbg mod_delta db_list local_db concl))) + end and my_find_search_nodelta db_list local_db hdc concl = List.map (fun hint -> (None,hint)) @@ -1433,12 +1437,14 @@ let search d n mod_delta db_list local_db = if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else Tacticals.New.tclORELSE0 (Proofview.V82.tactic (dbg_assumption d)) (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) - ( Proofview.Goal.concl >>= fun concl -> + ( Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in let d' = incr_dbg d in Tacticals.New.tclFIRST (List.map (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db)) - (possible_resolve d mod_delta db_list local_db concl)))) + (possible_resolve d mod_delta db_list local_db concl)) + end)) end [] in search d n local_db diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1aaf4af00..c33e5fb7c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -83,13 +83,17 @@ let rec eq_constr_mod_evars x y = | _, _ -> compare_constr eq_constr_mod_evars x y let progress_evars t = - Proofview.Goal.concl >>= fun concl -> - let check = - Proofview.Goal.concl >>= fun newconcl -> - if eq_constr_mod_evars concl newconcl - then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)") - else Proofview.tclUNIT () - in t <*> check + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let check = + Proofview.Goal.enter begin fun gl' -> + let newconcl = Proofview.Goal.concl gl' in + if eq_constr_mod_evars concl newconcl + then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)") + else Proofview.tclUNIT () + end + in t <*> check + end let unify_e_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 74780a8d2..c500a5969 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -44,19 +44,22 @@ let filter_hyp f tac = | [] -> Proofview.tclZERO Not_found | (id,_,t)::rest when f t -> tac id | _::rest -> seek rest in - Proofview.Goal.hyps >>= fun hyps -> - seek (Environ.named_context_of_val hyps) + Proofview.Goal.enter begin fun gl -> + let hyps = Proofview.Goal.hyps gl in + seek (Environ.named_context_of_val hyps) + end let contradiction_context = - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> - let rec seek_neg l = match l with - | [] -> Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction")) - | (id,_,typ)::rest -> - let typ = whd_betadeltaiota env sigma typ in - if is_empty_type typ then - simplest_elim (mkVar id) - else match kind_of_term typ with + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let rec seek_neg l = match l with + | [] -> Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction")) + | (id,_,typ)::rest -> + let typ = whd_betadeltaiota env sigma typ in + if is_empty_type typ then + simplest_elim (mkVar id) + else match kind_of_term typ with | Prod (na,t,u) when is_empty_type u -> (Proofview.tclORELSE begin @@ -69,10 +72,11 @@ let contradiction_context = | e -> Proofview.tclZERO e end) | _ -> seek_neg rest - in - Proofview.Goal.hyps >>= fun hyps -> - let hyps = Environ.named_context_of_val hyps in - seek_neg hyps + in + let hyps = Proofview.Goal.hyps gl in + let hyps = Environ.named_context_of_val hyps in + seek_neg hyps + end let is_negation_of env sigma typ t = match kind_of_term (whd_betadeltaiota env sigma t) with @@ -80,28 +84,30 @@ let is_negation_of env sigma typ t = | _ -> false let contradiction_term (c,lbind as cl) = - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> - Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> - try (* type_of can raise exceptions. *) - let typ = type_of c in - let _, ccl = splay_prod env sigma typ in - if is_empty_type ccl then - Tacticals.New.tclTHEN (elim false cl None) (Proofview.V82.tactic (tclTRY assumption)) - else - Proofview.tclORELSE - begin - if lbind = NoBindings then - filter_hyp (is_negation_of env sigma typ) - (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) - else - Proofview.tclZERO Not_found - end - begin function - | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction.")) - | e -> Proofview.tclZERO e - end - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> + try (* type_of can raise exceptions. *) + let typ = type_of c in + let _, ccl = splay_prod env sigma typ in + if is_empty_type ccl then + Tacticals.New.tclTHEN (elim false cl None) (Proofview.V82.tactic (tclTRY assumption)) + else + Proofview.tclORELSE + begin + if lbind = NoBindings then + filter_hyp (is_negation_of env sigma typ) + (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) + else + Proofview.tclZERO Not_found + end + begin function + | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction.")) + | e -> Proofview.tclZERO e + end + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end let contradiction = function | None -> Tacticals.New.tclTHEN intros contradiction_context diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 0a6e7a072..a0e8fcb88 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -130,16 +130,18 @@ let solveArg eqonleft op a1 a2 tac = let solveEqBranch rectype = Proofview.tclORELSE begin - Proofview.Goal.concl >>= fun concl -> - match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) -> - let (mib,mip) = Global.lookup_inductive rectype in - let nparams = mib.mind_nparams in - let getargs l = List.skipn nparams (snd (decompose_app l)) in - let rargs = getargs rhs - and largs = getargs lhs in - List.fold_right2 - (solveArg eqonleft op) largs rargs - (Tacticals.New.tclTHEN (choose_eq eqonleft) h_reflexivity) + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) -> + let (mib,mip) = Global.lookup_inductive rectype in + let nparams = mib.mind_nparams in + let getargs l = List.skipn nparams (snd (decompose_app l)) in + let rargs = getargs rhs + and largs = getargs lhs in + List.fold_right2 + (solveArg eqonleft op) largs rargs + (Tacticals.New.tclTHEN (choose_eq eqonleft) h_reflexivity) + end end begin function | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!")) @@ -155,16 +157,18 @@ let hd_app c = match kind_of_term c with let decideGralEquality = Proofview.tclORELSE begin - Proofview.Goal.concl >>= fun concl -> - match_eqdec concl >= fun eqonleft,_,c1,c2,typ -> - Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>= fun headtyp -> - begin match kind_of_term headtyp with - | Ind mi -> Proofview.tclUNIT mi - | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects.")) - end >= fun rectype -> - (Tacticals.New.tclTHEN - (mkBranches c1 c2) - (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + match_eqdec concl >= fun eqonleft,_,c1,c2,typ -> + Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>= fun headtyp -> + begin match kind_of_term headtyp with + | Ind mi -> Proofview.tclUNIT mi + | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects.")) + end >= fun rectype -> + (Tacticals.New.tclTHEN + (mkBranches c1 c2) + (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) + end end begin function | PatternMatchingFailure -> diff --git a/tactics/equality.ml b/tactics/equality.ml index ff35b4eeb..782ca67d5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -324,7 +324,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl = | _ -> assert false let type_of_clause = function - | None -> Proofview.Goal.concl + | None -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (Proofview.Goal.concl gl)) | Some id -> Tacmach.New.pf_get_hyp_typ id let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = @@ -359,8 +359,9 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac if occs != AllOccurrences then ( rewrite_side_tac (Hook.get forward_general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac) else - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in match match_with_equality_type t with @@ -391,6 +392,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac | None -> Proofview.tclZERO e (* error "The provided term does not end with an equality or a declared rewrite relation." *) end + end let general_rewrite_ebindings = general_rewrite_ebindings_clause None @@ -465,13 +467,16 @@ type delayed_open_constr_with_bindings = let general_multi_multi_rewrite with_evars l cl tac = let do1 l2r f = - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> - try (* f (an interpretation function) can raise exceptions *) - let sigma,c = f env sigma in - Tacticals.New.tclWITHHOLES with_evars - (general_multi_rewrite l2r with_evars ?tac c) sigma cl - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + try (* f (an interpretation function) can raise exceptions *) + let sigma,c = f env sigma in + Tacticals.New.tclWITHHOLES with_evars + (general_multi_rewrite l2r with_evars ?tac c) sigma cl + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end + in let rec doN l2r c = function | Precisely n when n <= 0 -> Proofview.tclUNIT () | Precisely 1 -> do1 l2r c @@ -848,15 +853,17 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort = let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in - Proofview.Goal.env >>= fun env -> - Proofview.Goal.concl >>= fun concl -> - match find_positions env sigma t1 t2 with + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + match find_positions env sigma t1 t2 with | Inr _ -> Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality.")) | Inl (cpath, (_,dirn), _) -> Tacmach.New.pf_apply get_type_of >>= fun get_type_of -> let sort = get_type_of concl in discr_positions env sigma u eq_clause cpath dirn sort + end let onEquality with_evars tac (c,lbindc) = Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> @@ -877,16 +884,18 @@ let onEquality with_evars tac (c,lbindc) = with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e let onNegatedEquality with_evars tac = - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.concl >>= fun ccl -> - Proofview.Goal.env >>= fun env -> - match kind_of_term (hnf_constr env sigma ccl) with - | Prod (_,t,u) when is_empty_type u -> - Tacticals.New.tclTHEN introf - (Tacticals.New.onLastHypId (fun id -> - onEquality with_evars tac (mkVar id,NoBindings))) - | _ -> - Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality.")) + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let ccl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + match kind_of_term (hnf_constr env sigma ccl) with + | Prod (_,t,u) when is_empty_type u -> + Tacticals.New.tclTHEN introf + (Tacticals.New.onLastHypId (fun id -> + onEquality with_evars tac (mkVar id,NoBindings))) + | _ -> + Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality.")) + end let discrSimpleClause with_evars = function | None -> onNegatedEquality with_evars discrEq @@ -1268,9 +1277,10 @@ let injConcl = injClause None false None let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id))) let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = - Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>= fun sort -> + Proofview.Goal.enter begin fun gl -> + Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>= fun sort -> let sigma = clause.evd in - Proofview.Goal.env >>= fun env -> + let env = Proofview.Goal.env gl in match find_positions env sigma t1 t2 with | Inl (cpath, (_,dirn), _) -> discr_positions env sigma u clause cpath dirn sort @@ -1279,6 +1289,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = | Inr posns -> inject_at_positions env sigma true u clause posns (ntac (clenv_value clause)) + end let dEqThen with_evars ntac = function | None -> onNegatedEquality with_evars (decompEqThen ntac) @@ -1514,9 +1525,10 @@ let is_eq_x gl x (id,_,c) = erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = - Proofview.Goal.env >>= fun env -> - Proofview.Goal.hyps >>= fun hyps -> - Proofview.Goal.concl >>= fun concl -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in let hyps = Environ.named_context_of_val hyps in (* The set of hypotheses using x *) let depdecls = @@ -1551,29 +1563,32 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = else [Proofview.tclUNIT ()]) @ [Proofview.V82.tactic (tclTRY (clear [x;hyp]))]) + end (* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *) let subst_one_var dep_proof_ok x = - Proofview.Goal.hyps >>= fun hyps -> - let hyps = Environ.named_context_of_val hyps in - Tacmach.New.pf_get_hyp x >>= fun (_,xval,_) -> - (* If x has a body, simply replace x with body and clear x *) - if not (Option.is_empty xval) then Proofview.V82.tactic (tclTHEN (unfold_body x) (clear [x])) else - (* x is a variable: *) - let varx = mkVar x in - (* Find a non-recursive definition for x *) - let found gl = - try - let test hyp _ = is_eq_x gl varx hyp in - Context.fold_named_context test ~init:() hyps; - errorlabstrm "Subst" - (str "Cannot find any non-recursive equality over " ++ pr_id x ++ - str".") - with FoundHyp res -> res in - Tacmach.New.of_old found >>= fun (hyp,rhs,dir) -> - subst_one dep_proof_ok x (hyp,rhs,dir) + Proofview.Goal.enter begin fun gl -> + let hyps = Proofview.Goal.hyps gl in + let hyps = Environ.named_context_of_val hyps in + Tacmach.New.pf_get_hyp x >>= fun (_,xval,_) -> + (* If x has a body, simply replace x with body and clear x *) + if not (Option.is_empty xval) then Proofview.V82.tactic (tclTHEN (unfold_body x) (clear [x])) else + (* x is a variable: *) + let varx = mkVar x in + (* Find a non-recursive definition for x *) + let found gl = + try + let test hyp _ = is_eq_x gl varx hyp in + Context.fold_named_context test ~init:() hyps; + errorlabstrm "Subst" + (str "Cannot find any non-recursive equality over " ++ pr_id x ++ + str".") + with FoundHyp res -> res in + Tacmach.New.of_old found >>= fun (hyp,rhs,dir) -> + subst_one dep_proof_ok x (hyp,rhs,dir) + end let subst_gen dep_proof_ok ids = Tacticals.New.tclTHEN (Proofview.V82.tactic tclNORMEVAR) (Tacticals.New.tclMAP (subst_one_var dep_proof_ok) ids) @@ -1651,9 +1666,11 @@ let rewrite_multi_assumption_cond cond_eq_term cl = with | Failure _ | UserError _ -> arec rest end in - Proofview.Goal.hyps >>= fun hyps -> - let hyps = Environ.named_context_of_val hyps in - arec hyps + Proofview.Goal.enter begin fun gl -> + let hyps = Proofview.Goal.hyps gl in + let hyps = Environ.named_context_of_val hyps in + arec hyps + end let replace_multi_term dir_opt c = let cond_eq_fun = diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 0555564bd..20f72b3d5 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -53,8 +53,10 @@ let instantiate n (ist,rawc) ido gl = open Proofview.Notations let let_evar name typ = let src = (Loc.ghost,Evar_kinds.GoalEvar) in - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> - let sigma',evar = Evarutil.new_evar sigma env ~src typ in - Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma')) - (Tactics.letin_tac None name evar None Locusops.nowhere) + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let sigma',evar = Evarutil.new_evar sigma env ~src typ in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma')) + (Tactics.letin_tac None name evar None Locusops.nowhere) + end diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index a4765f22b..fcb131161 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -664,9 +664,9 @@ let mkCaseEq a : unit Proofview.tactic = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) >>= fun type_of_a -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); - begin - Proofview.Goal.concl >>= fun concl -> - Proofview.Goal.env >>= fun env -> + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in Proofview.V82.tactic begin change_in_concl None (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl) @@ -683,8 +683,8 @@ let case_eq_intros_rewrite x = (* Pp.msgnl (Printer.pr_lconstr x); *) Tacticals.New.tclTHENLIST [ mkCaseEq x; - begin - Proofview.Goal.concl >>= fun concl -> + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in Tacmach.New.pf_ids_of_hyps >>= fun hyps -> let n' = nb_prod concl in Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) >>= fun h -> @@ -719,7 +719,7 @@ let destauto_in id = destauto ctype TACTIC EXTEND destauto -| [ "destauto" ] -> [ Proofview.Goal.concl >>= fun concl -> destauto concl ] +| [ "destauto" ] -> [ Proofview.Goal.enter (fun gl -> destauto (Proofview.Goal.concl gl)) ] | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END diff --git a/tactics/inv.ml b/tactics/inv.ml index e4d4fc80e..b3c8b2837 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -443,44 +443,46 @@ let rewrite_equations_tac (gene, othin) id neqns names ba = let raw_inversion inv_kind id status names = - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> - Proofview.Goal.concl >>= fun concl -> - let c = mkVar id in - Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind >>= fun reduce_to_atomic_ind -> - Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> - begin - try - Proofview.tclUNIT (reduce_to_atomic_ind (type_of c)) - with UserError _ -> - Proofview.tclZERO (Errors.UserError ("raw_inversion" , - str ("The type of "^(Id.to_string id)^" is not inductive."))) - end >= fun (ind,t) -> - Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>= fun indclause -> - let ccl = clenv_type indclause in - check_no_metas indclause ccl; - let IndType (indf,realargs) = find_rectype env sigma ccl in - let (elim_predicate,neqns) = - make_inv_predicate env sigma indf realargs id status concl in - let (cut_concl,case_tac) = - if status != NoDep & (dependent c concl) then - Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])), - Tacticals.New.case_then_using - else - Reduction.beta_appvect elim_predicate (Array.of_list realargs), - Tacticals.New.case_nodep_then_using - in - (Tacticals.New.tclTHENS - (assert_tac Anonymous cut_concl) - [case_tac names - (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) - (Some elim_predicate) ([],[]) ind indclause; - Tacticals.New.onLastHypId - (fun id -> - (Tacticals.New.tclTHEN - (Proofview.V82.tactic (apply_term (mkVar id) - (List.init neqns (fun _ -> Evarutil.mk_new_meta())))) - reflexivity))]) + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + let c = mkVar id in + Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind >>= fun reduce_to_atomic_ind -> + Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> + begin + try + Proofview.tclUNIT (reduce_to_atomic_ind (type_of c)) + with UserError _ -> + Proofview.tclZERO (Errors.UserError ("raw_inversion" , + str ("The type of "^(Id.to_string id)^" is not inductive."))) + end >= fun (ind,t) -> + Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>= fun indclause -> + let ccl = clenv_type indclause in + check_no_metas indclause ccl; + let IndType (indf,realargs) = find_rectype env sigma ccl in + let (elim_predicate,neqns) = + make_inv_predicate env sigma indf realargs id status concl in + let (cut_concl,case_tac) = + if status != NoDep & (dependent c concl) then + Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])), + Tacticals.New.case_then_using + else + Reduction.beta_appvect elim_predicate (Array.of_list realargs), + Tacticals.New.case_nodep_then_using + in + (Tacticals.New.tclTHENS + (assert_tac Anonymous cut_concl) + [case_tac names + (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) + (Some elim_predicate) ([],[]) ind indclause; + Tacticals.New.onLastHypId + (fun id -> + (Tacticals.New.tclTHEN + (Proofview.V82.tactic (apply_term (mkVar id) + (List.init neqns (fun _ -> Evarutil.mk_new_meta())))) + reflexivity))]) + end (* Error messages of the inversion tactics *) let wrap_inv_error id = function @@ -523,25 +525,29 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) * back to their places in the hyp-list. *) let invIn k names ids id = - Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps -> - Proofview.Goal.concl >>= fun concl -> - let nb_prod_init = nb_prod concl in - let intros_replace_ids = - Proofview.Goal.concl >>= fun concl -> - let nb_of_new_hyp = - nb_prod concl - (List.length hyps + nb_prod_init) + Proofview.Goal.enter begin fun gl -> + Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps -> + let concl = Proofview.Goal.concl gl in + let nb_prod_init = nb_prod concl in + let intros_replace_ids = + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let nb_of_new_hyp = + nb_prod concl - (List.length hyps + nb_prod_init) + in + if nb_of_new_hyp < 1 then + intros_replacing ids + else + Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids) + end in - if nb_of_new_hyp < 1 then - intros_replacing ids - else - Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids) - in - Proofview.tclORELSE - (Tacticals.New.tclTHENLIST - [Proofview.V82.tactic (bring_hyps hyps); - inversion (false,k) NoDep names id; - intros_replace_ids]) - (wrap_inv_error id) + Proofview.tclORELSE + (Tacticals.New.tclTHENLIST + [Proofview.V82.tactic (bring_hyps hyps); + inversion (false,k) NoDep names id; + intros_replace_ids]) + (wrap_inv_error id) + end let invIn_gen k names idl = try_intros_until (invIn k names idl) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 04819830e..e726e7692 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -284,17 +284,19 @@ let lemInv id c gls = let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id let lemInvIn id c ids = - Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps -> - let intros_replace_ids = - Proofview.Goal.concl >>= fun concl -> - let nb_of_new_hyp = nb_prod concl - List.length ids in - if nb_of_new_hyp < 1 then - intros_replacing ids - else - (Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids)) - in - ((Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTHEN (bring_hyps hyps) (lemInv id c))) - (intros_replace_ids))) + Proofview.Goal.enter begin fun gl -> + Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps -> + let intros_replace_ids = + let concl = Proofview.Goal.concl gl in + let nb_of_new_hyp = nb_prod concl - List.length ids in + if nb_of_new_hyp < 1 then + intros_replacing ids + else + (Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids)) + in + ((Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTHEN (bring_hyps hyps) (lemInv id c))) + (intros_replace_ids))) + end let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 66b2c64b0..14a9eb0ed 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1764,37 +1764,39 @@ let not_declared env ty rel = str ty ++ str" relation. Maybe you need to require the Setoid library") let setoid_proof ty fn fallback = - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> - Proofview.Goal.concl >>= fun concl -> - Proofview.tclORELSE - begin - try - let rel, args = decompose_app_rel env sigma concl in - let evm = sigma in - let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in - fn env evm car rel - with e -> Proofview.tclZERO e - end - begin function - | e -> - Proofview.tclORELSE - fallback - begin function - | Hipattern.NoEquationFound -> + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + Proofview.tclORELSE + begin + try + let rel, args = decompose_app_rel env sigma concl in + let evm = sigma in + let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in + fn env evm car rel + with e -> Proofview.tclZERO e + end + begin function + | e -> + Proofview.tclORELSE + fallback + begin function + | Hipattern.NoEquationFound -> (* spiwack: [Errors.push] here is unlikely to do what it's intended to, or anything meaningful for that matter. *) - let e = Errors.push e in - begin match e with - | Not_found -> - let rel, args = decompose_app_rel env sigma concl in - not_declared env ty rel - | _ -> Proofview.tclZERO e - end - | e' -> Proofview.tclZERO e' - end - end + let e = Errors.push e in + begin match e with + | Not_found -> + let rel, args = decompose_app_rel env sigma concl in + not_declared env ty rel + | _ -> Proofview.tclZERO e + end + | e' -> Proofview.tclZERO e' + end + end + end let setoid_reflexivity = setoid_proof "reflexive" diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index abc1daa5b..83958eca2 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1265,11 +1265,13 @@ and interp_app loc ist fv largs = end >>== fun v -> (* No errors happened, we propagate the trace *) let v = append_trace trace v in - Proofview.Goal.env >>== fun env -> - Proofview.tclLIFT begin - debugging_step ist - (fun () -> - str"evaluation returns"++fnl()++pr_value (Some env) v) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Proofview.tclLIFT begin + debugging_step ist + (fun () -> + str"evaluation returns"++fnl()++pr_value (Some env) v) + end end <*> if List.is_empty lval then (Proofview.Goal.return v) else interp_app loc ist v lval else @@ -1343,9 +1345,13 @@ and interp_letin ist llc u = (* Interprets the Match Context expressions *) and interp_match_goal ist lz lr lmr = - Proofview.Goal.enterl begin fun env sigma hyps concl -> + Proofview.Goal.enterl begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let hyps = Proofview.Goal.hyps gl in let hyps = Environ.named_context_of_val hyps in let hyps = if lr then List.rev hyps else hyps in + let concl = Proofview.Goal.concl gl in let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps = let rec match_next_pattern next = match IStream.peek next with | None -> Proofview.tclZERO PatternMatchingFailure @@ -1428,7 +1434,8 @@ and interp_match_goal ist lz lr lmr = (* Tries to match the hypotheses in a Match Context *) and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps = - Proofview.Goal.env >>== fun env -> + Proofview.Goal.enterl begin fun gl -> + let env = Proofview.Goal.env gl in let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function | hyp_pat::tl -> let (hypname, _, pat as hyp_pat) = @@ -1467,6 +1474,7 @@ and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps = eval_with_fail {ist with lfun=lfun} lz mt in apply_hyps_context_rec lctxt lgmatch hyps mhyps + end and interp_external loc ist gl com req la = assert false (* arnaud: todo @@ -1582,11 +1590,13 @@ and interp_match ist lz constr lmr = in Proofview.tclORELSE begin match matches with | None -> let e = PatternMatchingFailure in - (Proofview.Goal.env >>= fun env -> - Proofview.tclLIFT begin - debugging_exception_step ist false e (fun () -> - str "matching with pattern" ++ fnl () ++ - pr_constr_pattern_env env c) + (Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Proofview.tclLIFT begin + debugging_exception_step ist false e (fun () -> + str "matching with pattern" ++ fnl () ++ + pr_constr_pattern_env env c) + end end) <*> Proofview.tclZERO e | Some lmatch -> Proofview.tclORELSE @@ -1596,12 +1606,14 @@ and interp_match ist lz constr lmr = end begin function | e -> - (Proofview.Goal.env >>= fun env -> - Proofview.tclLIFT begin - debugging_exception_step ist false e (fun () -> - str "rule body for pattern" ++ - pr_constr_pattern_env env c) - end) <*> + (Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Proofview.tclLIFT begin + debugging_exception_step ist false e (fun () -> + str "rule body for pattern" ++ + pr_constr_pattern_env env c) + end + end) <*> Proofview.tclZERO e end end @@ -1635,7 +1647,9 @@ and interp_match ist lz constr lmr = Proofview.tclZERO e end end >>== fun csr -> - Proofview.Goal.enterl begin fun env sigma _ _ -> + Proofview.Goal.enterl begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in Proofview.tclORELSE (apply_match ist csr ilr) @@ -1655,17 +1669,20 @@ and interp_ltac_constr ist e = (val_interp ist e) begin function | Not_found -> - (Proofview.Goal.env >>= fun env -> - Proofview.tclLIFT begin - debugging_step ist (fun () -> - str "evaluation failed for" ++ fnl() ++ - Pptactic.pr_glob_tactic env e) + (Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Proofview.tclLIFT begin + debugging_step ist (fun () -> + str "evaluation failed for" ++ fnl() ++ + Pptactic.pr_glob_tactic env e) + end end) <*> Proofview.tclZERO Not_found | e -> Proofview.tclZERO e end end >>== fun result -> - Proofview.Goal.env >>== fun env -> + Proofview.Goal.enterl begin fun gl -> + let env = Proofview.Goal.env gl in let result = Value.normalize result in try let cresult = coerce_to_closed_constr env result in @@ -1677,11 +1694,13 @@ and interp_ltac_constr ist e = end <*> (Proofview.Goal.return cresult) with CannotCoerceTo _ -> - Proofview.Goal.env >>== fun env -> + let env = Proofview.Goal.env gl in Proofview.tclZERO (UserError ( "", errorlabstrm "" (str "Must evaluate to a closed term" ++ fnl() ++ str "offending expression: " ++ fnl() ++ pr_inspect env e result))) + end + (* Interprets tactic expressions : returns a "tactic" *) and interp_tactic ist tac = @@ -1701,9 +1720,11 @@ and interp_atomic ist tac = with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end | TacIntroMove (ido,hto) -> - Proofview.Goal.env >>= fun env -> - Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>= fun mloc -> - h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>= fun mloc -> + h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc + end | TacAssumption -> Proofview.V82.tactic h_assumption | TacExact c -> Proofview.V82.tactic begin fun gl -> @@ -1730,7 +1751,9 @@ and interp_atomic ist tac = gl end | TacApply (a,ev,cb,cl) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in try (* interp_open_constr_with_bindings_loc can raise exceptions *) let sigma, l = List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb @@ -1745,7 +1768,9 @@ and interp_atomic ist tac = with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end | TacElim (ev,cb,cbo) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in try (* interpretation functions may raise exceptions *) let sigma, cb = interp_constr_with_bindings ist env sigma cb in let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in @@ -1761,7 +1786,9 @@ and interp_atomic ist tac = gl end | TacCase (ev,cb) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in Tacticals.New.tclWITHHOLES ev (h_case ev) sigma cb end @@ -1774,11 +1801,13 @@ and interp_atomic ist tac = gl end | TacFix (idopt,n) -> - Proofview.Goal.env >>= fun env -> - Proofview.V82.tactic (h_fix (Option.map (interp_fresh_ident ist env) idopt) n) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Proofview.V82.tactic (h_fix (Option.map (interp_fresh_ident ist env) idopt) n) + end | TacMutualFix (id,n,l) -> - Proofview.Goal.env >>= fun env -> - Proofview.V82.tactic begin fun gl -> + Proofview.V82.tactic begin fun gl -> + let env = pf_env gl in let f sigma (id,n,c) = let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in sigma , (interp_fresh_ident ist env id,n,c_interp) in @@ -1794,11 +1823,13 @@ and interp_atomic ist tac = gl end | TacCofix idopt -> - Proofview.Goal.env >>= fun env -> - Proofview.V82.tactic (h_cofix (Option.map (interp_fresh_ident ist env) idopt)) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Proofview.V82.tactic (h_cofix (Option.map (interp_fresh_ident ist env) idopt)) + end | TacMutualCofix (id,l) -> - Proofview.Goal.env >>= fun env -> - Proofview.V82.tactic begin fun gl -> + Proofview.V82.tactic begin fun gl -> + let env = pf_env gl in let f sigma (id,c) = let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in sigma , (interp_fresh_ident ist env id,c_interp) in @@ -1822,7 +1853,9 @@ and interp_atomic ist tac = gl end | TacAssert (t,ipat,c) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in try (* intrerpreation function may raise exceptions *) let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>= fun patt -> @@ -1833,11 +1866,11 @@ and interp_atomic ist tac = with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end | TacGeneralize cl -> - Proofview.Goal.enter begin fun env sigma _ _ -> - Proofview.V82.tactic begin fun gl -> - let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in - tclWITHHOLES false (h_generalize_gen) sigma cl gl - end + Proofview.V82.tactic begin fun gl -> + let sigma = project gl in + let env = pf_env gl in + let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in + tclWITHHOLES false (h_generalize_gen) sigma cl gl end | TacGeneralizeDep c -> Proofview.V82.tactic begin fun gl -> @@ -1848,7 +1881,9 @@ and interp_atomic ist tac = gl end | TacLetTac (na,c,clp,b,eqpat) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) >>= fun clp -> Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) >>= fun eqpat -> if Locusops.is_nowhere clp then @@ -1868,13 +1903,17 @@ and interp_atomic ist tac = (* Automation tactics *) | TacTrivial (debug,lems,l) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in Auto.h_trivial ~debug (interp_auto_lemmas ist env sigma lems) (Option.map (List.map (interp_hint_base ist)) l) end | TacAuto (debug,n,lems,l) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n) (interp_auto_lemmas ist env sigma lems) (Option.map (List.map (interp_hint_base ist)) l) @@ -1884,25 +1923,27 @@ and interp_atomic ist tac = | TacSimpleInductionDestruct (isrec,h) -> h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h) | TacInductionDestruct (isrec,ev,(l,el,cls)) -> - Proofview.Goal.env >>= fun env -> - let l = - Goal.sensitive_list_map begin fun (c,(ipato,ipats)) -> - Goal.V82.to_sensitive (fun gl -> interp_induction_arg ist gl c) >- fun c -> - Goal.V82.to_sensitive (fun gl -> interp_intro_pattern ist gl) >- fun interp_intro_pattern -> - Goal.return begin - c, - (Option.map interp_intro_pattern ipato, - Option.map interp_intro_pattern ipats) - end - end l - in - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.lift l >>= fun l -> - let sigma,el = - Option.fold_map (interp_constr_with_bindings ist env) sigma el in - Tacmach.New.of_old (fun gl -> interp_clause ist gl) >>= fun interp_clause -> - let cls = Option.map interp_clause cls in - Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let l = + Goal.sensitive_list_map begin fun (c,(ipato,ipats)) -> + Goal.V82.to_sensitive (fun gl -> interp_induction_arg ist gl c) >- fun c -> + Goal.V82.to_sensitive (fun gl -> interp_intro_pattern ist gl) >- fun interp_intro_pattern -> + Goal.return begin + c, + (Option.map interp_intro_pattern ipato, + Option.map interp_intro_pattern ipats) + end + end l + in + let sigma = Proofview.Goal.sigma gl in + Proofview.Goal.lift l >>= fun l -> + let sigma,el = + Option.fold_map (interp_constr_with_bindings ist env) sigma el in + Tacmach.New.of_old (fun gl -> interp_clause ist gl) >>= fun interp_clause -> + let cls = Option.map interp_clause cls in + Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls) + end | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -1924,7 +1965,9 @@ and interp_atomic ist tac = (Proofview.V82.tclEVARS sigma) (Elim.h_decompose l c_interp) | TacSpecialize (n,cb) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in Proofview.V82.tactic begin fun gl -> let sigma, cb = interp_constr_with_bindings ist env sigma cb in tclWITHHOLES false (h_specialize n) sigma cb gl @@ -1953,8 +1996,8 @@ and interp_atomic ist tac = h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2) gl end | TacRename l -> - Proofview.Goal.env >>= fun env -> - Proofview.V82.tactic begin fun gl -> + Proofview.V82.tactic begin fun gl -> + let env = pf_env gl in h_rename (List.map (fun (id1,id2) -> interp_hyp ist gl id1, interp_fresh_ident ist env (snd id2)) l) @@ -1967,24 +2010,32 @@ and interp_atomic ist tac = (* Constructors *) | TacLeft (ev,bl) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let sigma, bl = interp_bindings ist env sigma bl in Tacticals.New.tclWITHHOLES ev (h_left ev) sigma bl end | TacRight (ev,bl) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let sigma, bl = interp_bindings ist env sigma bl in Tacticals.New.tclWITHHOLES ev (h_right ev) sigma bl end | TacSplit (ev,_,bll) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in Tacticals.New.tclWITHHOLES ev (h_split ev) sigma bll end | TacAnyConstructor (ev,t) -> Tactics.any_constructor ev (Option.map (interp_tactic ist) t) | TacConstructor (ev,n,bl) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let sigma, bl = interp_bindings ist env sigma bl in Tacticals.New.tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl end @@ -2019,7 +2070,9 @@ and interp_atomic ist tac = gl end | TacChange (Some op,c,cl) -> - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in Proofview.V82.tactic begin fun gl -> let sign,op = interp_typed_pattern ist env sigma op in (* spiwack: (2012/04/18) the evar_map output by pf_interp_constr @@ -2104,7 +2157,8 @@ and interp_atomic ist tac = Proofview.V82.tclEVARS sigma <*> tac args ist | TacAlias (loc,s,l,(_,body)) -> - Proofview.Goal.env >>= fun env -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let rec f x = match genarg_tag x with | IntOrVarArgType -> (Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x))) @@ -2195,6 +2249,7 @@ and interp_atomic ist tac = lfun = lfun; extra = TacStore.set ist.extra f_trace trace; } in interp_tactic ist body + end (* Initial call for interpretation *) @@ -2211,7 +2266,9 @@ let eval_tactic t = let interp_tac_gen lfun avoid_ids debug t = - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let extra = TacStore.set TacStore.empty f_debug debug in let extra = TacStore.set extra f_avoid_ids avoid_ids in let ist = { lfun = lfun; extra = extra } in @@ -2232,7 +2289,9 @@ let eval_ltac_constr t = (* Used to hide interpretation for pretty-print, now just launch tactics *) let hide_interp t ot = - Proofview.Goal.enter begin fun env sigma _ _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; gsigma = sigma; genv = env } in let te = intern_pure_tactic ist t in diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 74c31fa38..5d3c8b97a 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -522,27 +522,35 @@ module New = struct | e -> Proofview.tclZERO e end - let nthDecl m = - Proofview.Goal.hyps >>== fun hyps -> + let nthDecl m gl = + let hyps = Proofview.Goal.hyps gl in try let hyps = Environ.named_context_of_val hyps in - (Proofview.Goal.return (List.nth hyps (m-1))) - with Failure _ -> tclZERO (UserError ("" , Pp.str"No such assumption.")) + List.nth hyps (m-1) + with Failure _ -> Errors.error "No such assumption." - let nthHypId m = nthDecl m >>== fun (id,_,_) -> - Proofview.Goal.return id - let nthHyp m = nthHypId m >>== fun id -> - Proofview.Goal.return (mkVar id) + let nthHypId m gl = + let (id,_,_) = nthDecl m gl in + id + let nthHyp m gl = + mkVar (nthHypId m gl) let onNthHypId m tac = - nthHypId m >>= tac + Goal.enter begin fun gl -> + Proofview.tclUNIT (nthHypId m gl) >= tac + end let onNthHyp m tac = - nthHyp m >>= tac + Goal.enter begin fun gl -> + Proofview.tclUNIT (nthHyp m gl) >= tac + end let onLastHypId = onNthHypId 1 let onLastHyp = onNthHyp 1 - let onNthDecl m tac = nthDecl m >>= tac + let onNthDecl m tac = + Proofview.Goal.enter begin fun gl -> + Proofview.tclUNIT (nthDecl m gl) >= tac + end let onLastDecl = onNthDecl 1 let ifOnHyp pred tac1 tac2 id = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index fe605da8e..5e62451f9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -460,8 +460,9 @@ let build_intro_tac id dest tac = match dest with | dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id] let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac = - Proofview.Goal.concl >>= fun concl -> - match kind_of_term concl with + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + match kind_of_term concl with | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) -> find_name loc (name,None,t) name_flag >>= fun name -> build_intro_tac name move_flag tac @@ -476,14 +477,15 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac = (* probably also a pity that intro does zeta *) else Proofview.tclUNIT () end <*> - Proofview.tclORELSE + Proofview.tclORELSE (Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl) - (intro_then_gen loc name_flag move_flag false dep_flag tac)) + (intro_then_gen loc name_flag move_flag false dep_flag tac)) begin function | RefinerError IntroNeedsProduct -> Proofview.tclZERO (Loc.add_loc (Errors.UserError("Intro",str "No product even after head-reduction.")) loc) | e -> Proofview.tclZERO e end + end let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> Proofview.tclUNIT ()) let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) MoveLast true false @@ -1281,18 +1283,20 @@ let check_number_of_constructors expctdnumopt i nconstr = if i > nconstr then error "Not enough constructors." let constructor_tac with_evars expctdnumopt i lbind = - Proofview.Goal.concl >>= fun cl -> - Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind -> - try (* reduce_to_quantified_ind can raise an exception *) - let (mind,redcl) = reduce_to_quantified_ind cl in - let nconstr = - Array.length (snd (Global.lookup_inductive mind)).mind_consnames in - check_number_of_constructors expctdnumopt i nconstr; - let cons = mkConstruct (ith_constructor_of_inductive mind i) in - let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in - (Tacticals.New.tclTHENLIST - [Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac]) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + Proofview.Goal.enter begin fun gl -> + let cl = Proofview.Goal.concl gl in + Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind -> + try (* reduce_to_quantified_ind can raise an exception *) + let (mind,redcl) = reduce_to_quantified_ind cl in + let nconstr = + Array.length (snd (Global.lookup_inductive mind)).mind_consnames in + check_number_of_constructors expctdnumopt i nconstr; + let cons = mkConstruct (ith_constructor_of_inductive mind i) in + let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in + (Tacticals.New.tclTHENLIST + [Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac]) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end let one_constructor i lbind = constructor_tac false None i lbind @@ -1303,18 +1307,20 @@ let one_constructor i lbind = constructor_tac false None i lbind let any_constructor with_evars tacopt = let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in - Proofview.Goal.concl >>= fun cl -> - Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind -> + Proofview.Goal.enter begin fun gl -> + let cl = Proofview.Goal.concl gl in + Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind -> try (* reduce_to_quantified_ind can raise an exception *) - let mind = fst (reduce_to_quantified_ind cl) in - let nconstr = - Array.length (snd (Global.lookup_inductive mind)).mind_consnames in - if Int.equal nconstr 0 then error "The type has no constructors."; - Tacticals.New.tclFIRST - (List.map - (fun i -> Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t) - (List.interval 1 nconstr)) + let mind = fst (reduce_to_quantified_ind cl) in + let nconstr = + Array.length (snd (Global.lookup_inductive mind)).mind_consnames in + if Int.equal nconstr 0 then error "The type has no constructors."; + Tacticals.New.tclFIRST + (List.map + (fun i -> Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t) + (List.interval 1 nconstr)) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2 @@ -1400,29 +1406,31 @@ let rewrite_hyp l2r id = Hook.get forward_subst_one true x (id,rhs,l2r) in let clear_var_and_eq c = tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in - Proofview.Goal.env >>= fun env -> - Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> - Tacmach.New.pf_apply whd_betadeltaiota >>= fun whd_betadeltaiota -> - try (* type_of can raise an exception *) - let t = whd_betadeltaiota (type_of (mkVar id)) in - (* TODO: detect setoid equality? better detect the different equalities *) - match match_with_equality_type t with - | Some (hdcncl,[_;lhs;rhs]) -> - if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then - subst_on l2r (destVar lhs) rhs - else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then - subst_on l2r (destVar rhs) lhs - else - Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id]))) - | Some (hdcncl,[c]) -> - let l2r = not l2r in (* equality of the form eq_true *) - if isVar c then - Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c)) - else - Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id]))) - | _ -> - Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation.")) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> + Tacmach.New.pf_apply whd_betadeltaiota >>= fun whd_betadeltaiota -> + try (* type_of can raise an exception *) + let t = whd_betadeltaiota (type_of (mkVar id)) in + (* TODO: detect setoid equality? better detect the different equalities *) + match match_with_equality_type t with + | Some (hdcncl,[_;lhs;rhs]) -> + if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then + subst_on l2r (destVar lhs) rhs + else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then + subst_on l2r (destVar rhs) lhs + else + Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id]))) + | Some (hdcncl,[c]) -> + let l2r = not l2r in (* equality of the form eq_true *) + if isVar c then + Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c)) + else + Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id]))) + | _ -> + Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation.")) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + end let rec explicit_intro_names = function | (_, IntroIdentifier id) :: l -> @@ -1893,47 +1901,49 @@ let letin_abstract id c (test,out) (occs,check_occs) gl = (depdecls,lastlhyp,ccl,out test) let letin_tac_gen with_eq name (sigmac,c) test ty occs = - Proofview.Goal.env >>= fun env -> - Proofview.Goal.hyps >>= fun hyps -> - let hyps = Environ.named_context_of_val hyps in - let id = - let t = match ty with Some t -> t | None -> typ_of env sigmac c in - let x = id_of_name_using_hdchar (Global.env()) t name in - if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) else - Proofview.Goal.lift begin - if not (mem_named_context x hyps) then Goal.return x else - error ("The variable "^(Id.to_string x)^" is already declared.") - end in - id >>= fun id -> - Tacmach.New.of_old (letin_abstract id c test occs) >>= fun (depdecls,lastlhyp,ccl,c) -> - let t = match ty with Some t -> (Proofview.Goal.return t) | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) in - t >>= fun t -> - let newcl = match with_eq with - | Some (lr,(loc,ido)) -> - let heq = match ido with - | IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id)) - | IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base) - | IntroIdentifier id -> (Proofview.Goal.return id) - | _ -> Proofview.tclZERO (UserError ("" , Pp.str"Expect an introduction pattern naming one hypothesis.")) in - heq >>== fun heq -> - let eqdata = build_coq_eq_data () in - let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in - let eq = applist (eqdata.eq,args) in - let refl = applist (eqdata.refl, [t;mkVar id]) in - Proofview.Goal.return begin - mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)), - Tacticals.New.tclTHEN - (intro_gen loc (IntroMustBe heq) lastlhyp true false) - (Proofview.V82.tactic (thin_body [heq;id])) - end - | None -> - (Proofview.Goal.return (mkNamedLetIn id c t ccl, Proofview.tclUNIT ())) in - newcl >>= fun (newcl,eq_tac) -> - Tacticals.New.tclTHENLIST - [ Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast); - intro_gen dloc (IntroMustBe id) lastlhyp true false; - Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls); - eq_tac ] + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let hyps = Proofview.Goal.hyps gl in + let hyps = Environ.named_context_of_val hyps in + let id = + let t = match ty with Some t -> t | None -> typ_of env sigmac c in + let x = id_of_name_using_hdchar (Global.env()) t name in + if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) else + Proofview.Goal.lift begin + if not (mem_named_context x hyps) then Goal.return x else + error ("The variable "^(Id.to_string x)^" is already declared.") + end in + id >>= fun id -> + Tacmach.New.of_old (letin_abstract id c test occs) >>= fun (depdecls,lastlhyp,ccl,c) -> + let t = match ty with Some t -> (Proofview.Goal.return t) | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) in + t >>= fun t -> + let newcl = match with_eq with + | Some (lr,(loc,ido)) -> + let heq = match ido with + | IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id)) + | IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base) + | IntroIdentifier id -> (Proofview.Goal.return id) + | _ -> Proofview.tclZERO (UserError ("" , Pp.str"Expect an introduction pattern naming one hypothesis.")) in + heq >>== fun heq -> + let eqdata = build_coq_eq_data () in + let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in + let eq = applist (eqdata.eq,args) in + let refl = applist (eqdata.refl, [t;mkVar id]) in + Proofview.Goal.return begin + mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)), + Tacticals.New.tclTHEN + (intro_gen loc (IntroMustBe heq) lastlhyp true false) + (Proofview.V82.tactic (thin_body [heq;id])) + end + | None -> + (Proofview.Goal.return (mkNamedLetIn id c t ccl, Proofview.tclUNIT ())) in + newcl >>= fun (newcl,eq_tac) -> + Tacticals.New.tclTHENLIST + [ Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast); + intro_gen dloc (IntroMustBe id) lastlhyp true false; + Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls); + eq_tac ] + end let make_eq_test c = (make_eq_test c,fun _ -> c) @@ -1942,11 +1952,13 @@ let letin_tac with_eq name c ty occs = letin_tac_gen with_eq name (sigma,c) (make_eq_test c) ty (occs,true) let letin_pat_tac with_eq name c ty occs = - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in letin_tac_gen with_eq name c (make_pattern_test env sigma c) ty (occs,true) + end (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *) let forward usetac ipat c = @@ -2162,6 +2174,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 = let params = List.firstn nparams argl in (* le gl est important pour ne pas préévaluer *) let rec atomize_one i avoid = + Proofview.Goal.enter begin fun gl -> if not (Int.equal i nparams) then Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 -> (* If argl <> [], we expect typ0 not to be quantified, in order to @@ -2170,7 +2183,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 = let indtyp = reduce_to_atomic_ref indref tmptyp0 in let argl = snd (decompose_app indtyp) in let c = List.nth argl (i-1) in - Proofview.Goal.env >>= fun env -> + let env = Proofview.Goal.env gl in match kind_of_term c with | Var id when not (List.exists (occur_var env id) avoid) -> atomize_one (i-1) ((mkVar id)::avoid) @@ -2189,6 +2202,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 = (atomize_one (i-1) ((mkVar x)::avoid)) else Proofview.tclUNIT () + end in atomize_one (List.length argl) params with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e @@ -3121,26 +3135,28 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t hypotheses from the context *) let apply_induction_in_context hyp0 elim indvars names induct_tac = - Proofview.Goal.env >>= fun env -> - Proofview.Goal.concl >>= fun concl -> - let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in - let deps = List.map (on_pi3 refresh_universes_strict) deps in - let tmpcl = it_mkNamedProd_or_LetIn concl deps in - let dephyps = List.map (fun (id,_,_) -> id) deps in - let deps_cstr = - List.fold_left - (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in - Tacticals.New.tclTHENLIST - [ - (* Generalize dependent hyps (but not args) *) - if deps = [] then Proofview.tclUNIT () else Proofview.V82.tactic (apply_type tmpcl deps_cstr); - (* clear dependent hyps *) - Proofview.V82.tactic (thin dephyps); - (* side-conditions in elim (resp case) schemes come last (resp first) *) - apply_induction_with_discharge - induct_tac elim (List.rev indhyps) lhyp0 (List.rev dephyps) names - (re_intro_dependent_hypotheses statuslists) - ] + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in + let deps = List.map (on_pi3 refresh_universes_strict) deps in + let tmpcl = it_mkNamedProd_or_LetIn concl deps in + let dephyps = List.map (fun (id,_,_) -> id) deps in + let deps_cstr = + List.fold_left + (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in + Tacticals.New.tclTHENLIST + [ + (* Generalize dependent hyps (but not args) *) + if deps = [] then Proofview.tclUNIT () else Proofview.V82.tactic (apply_type tmpcl deps_cstr); + (* clear dependent hyps *) + Proofview.V82.tactic (thin dephyps); + (* side-conditions in elim (resp case) schemes come last (resp first) *) + apply_induction_with_discharge + induct_tac elim (List.rev indhyps) lhyp0 (List.rev dephyps) names + (re_intro_dependent_hypotheses statuslists) + ] + end (* Induction with several induction arguments, main differences with induction_from_context is that there is no main induction argument, @@ -3280,22 +3296,26 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = (induction_with_atomization_of_ind_arg isrec with_evars elim names (id,lbind) inhyps) | _ -> - Proofview.tclEVARMAP >= fun defs -> - Proofview.Goal.env >>= fun env -> - let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c) - Anonymous in - Tacmach.New.of_old (fresh_id [] x) >>= fun id -> + Proofview.Goal.enter begin fun gl -> + let defs = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c) + Anonymous in + Tacmach.New.of_old (fresh_id [] x) >>= fun id -> (* We need the equality name now *) - let with_eq = Option.map (fun eq -> (false,eq)) eqname in + let with_eq = Option.map (fun eq -> (false,eq)) eqname in (* TODO: if ind has predicate parameters, use JMeq instead of eq *) - Proofview.Goal.env >>= fun env -> - Tacticals.New.tclTHEN - (* Warning: letin is buggy when c is not of inductive type *) - (letin_tac_gen with_eq (Name id) (sigma,c) - (make_pattern_test env defs (sigma,c)) - None (Option.default allHypsAndConcl cls,false)) - (induction_with_atomization_of_ind_arg - isrec with_evars elim names (id,lbind) inhyps) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + Tacticals.New.tclTHEN + (* Warning: letin is buggy when c is not of inductive type *) + (letin_tac_gen with_eq (Name id) (sigma,c) + (make_pattern_test env defs (sigma,c)) + None (Option.default allHypsAndConcl cls,false)) + (induction_with_atomization_of_ind_arg + isrec with_evars elim names (id,lbind) inhyps) + end + end (* Induction on a list of arguments. First make induction arguments atomic (using letins), then do induction. The specificity here is diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 3976fcf14..bc756eb82 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -594,24 +594,26 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Ci a1 ... an = Ci b1 ... bn replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto *) - Proofview.Goal.concl >>= fun gl -> - match (kind_of_term gl) with - | App (c,ca) -> ( - match (kind_of_term c) with - | Ind indeq -> - if eq_gr (IndRef indeq) Coqlib.glob_eq - then - Tacticals.New.tclTHEN - (do_replace_bl bl_scheme_key ind - (!avoid) - nparrec (ca.(2)) - (ca.(1))) - Auto.default_auto - else - Proofview.tclZERO (UserError ("",str"Failure while solving Boolean->Leibniz.")) + Proofview.Goal.enter begin fun gls -> + let gl = Proofview.Goal.concl gls in + match (kind_of_term gl) with + | App (c,ca) -> ( + match (kind_of_term c) with + | Ind indeq -> + if eq_gr (IndRef indeq) Coqlib.glob_eq + then + Tacticals.New.tclTHEN + (do_replace_bl bl_scheme_key ind + (!avoid) + nparrec (ca.(2)) + (ca.(1))) + Auto.default_auto + else + Proofview.tclZERO (UserError ("",str"Failure while solving Boolean->Leibniz.")) + | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz.")) + ) | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz.")) - ) - | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz.")) + end ] @@ -713,21 +715,23 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclTHENLIST [Proofview.V82.tactic (apply (andb_true_intro())); simplest_split ;Auto.default_auto ] ); - Proofview.Goal.concl >>= fun gl -> - (* assume the goal to be eq (eq_type ...) = true *) + Proofview.Goal.enter begin fun gls -> + let gl = Proofview.Goal.concl gls in + (* assume the goal to be eq (eq_type ...) = true *) match (kind_of_term gl) with - | App(c,ca) -> (match (kind_of_term ca.(1)) with - | App(c',ca') -> - let n = Array.length ca' in - do_replace_lb lb_scheme_key - (!avoid) - nparrec - ca'.(n-2) ca'.(n-1) - | _ -> - Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean.")) - ) + | App(c,ca) -> (match (kind_of_term ca.(1)) with + | App(c',ca') -> + let n = Array.length ca' in + do_replace_lb lb_scheme_key + (!avoid) + nparrec + ca'.(n-2) ca'.(n-1) | _ -> Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean.")) + ) + | _ -> + Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean.")) + end ] let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") -- cgit v1.2.3