From 260965dcf60d793ba01110ace8945cf51ef6531f Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:34:01 +0000 Subject: Makes the new Proofview.tactic the basic type of Ltac. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit On the compilation of Coq, we can see an increase of ~20% compile time on my completely non-scientific tests. Hopefully this can be fixed. There are a lot of low hanging fruits, but this is an iso-functionality commit. With a few exceptions which were not necessary for the compilation of the theories: - The declarative mode is not yet ported - The timeout tactical is currently deactivated because it needs some subtle I/O. The framework is ready to handle it, but I haven't done it yet. - For much the same reason, the ltac debugger is unplugged. It will be more difficult, but will eventually be back. A few comments: I occasionnally used a coercion from [unit Proofview.tactic] to the old [Prooftype.tactic]. It should work smoothely, but loses any backtracking information: the coerced tactics has at most one success. - It is used in autorewrite (it shouldn't be a problem there). Autorewrite's code is fairly old and tricky - It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes as we might want to have various success in a "Hint Extern". But it would require a heavy port of eauto.ml4 - It is used in typeclass eauto, but with a little help from Matthieu, it should be easy to port the whole thing to the new tactic engine, actually simplifying the code. - It is used in fourier. I believe it to be inocuous. - It is used in firstorder and congruence. I think it's ok. Their code is somewhat intricate and I'm not sure they would be easy to actually port. - It is used heavily in Function. And honestly, I have no idea whether it can do harm or not. Updates: (11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based architecture for Ltac matching (r16533), which avoid painfully and expensively working around the exception-throwing control flow of the previous API. (11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730) rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma, rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially tclREPEAT, causing rewrites to be tried in the side-conditions of conditional rewrites as well). The new implementation makes Coq faster, but it is pretty much impossible to tell if it is significant at all. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16967 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/btauto/refl_btauto.ml | 28 +- plugins/cc/cctac.ml | 168 +++++---- plugins/cc/cctac.mli | 8 +- plugins/decl_mode/decl_proof_instr.ml | 78 ++-- plugins/decl_mode/decl_proof_instr.mli | 4 +- plugins/firstorder/g_ground.ml4 | 24 +- plugins/firstorder/instances.ml | 14 +- plugins/firstorder/rules.ml | 40 +-- plugins/fourier/fourierR.ml | 18 +- plugins/fourier/g_fourier.ml4 | 2 +- plugins/funind/functional_principles_proofs.ml | 66 ++-- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/g_indfun.ml4 | 20 +- plugins/funind/indfun.ml | 6 +- plugins/funind/indfun_common.ml | 4 +- plugins/funind/invfun.ml | 82 +++-- plugins/funind/recdef.ml | 113 +++--- plugins/micromega/g_micromega.ml4 | 28 +- plugins/nsatz/nsatz.ml4 | 2 +- plugins/omega/coq_omega.ml | 475 +++++++++++++------------ plugins/omega/g_omega.ml4 | 6 +- plugins/quote/quote.ml | 54 +-- plugins/romega/g_romega.ml4 | 10 +- plugins/rtauto/g_rtauto.ml4 | 2 +- plugins/setoid_ring/newring.ml4 | 26 +- 25 files changed, 677 insertions(+), 603 deletions(-) (limited to 'plugins') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index b90e8ddaf..46a7e596c 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,3 +1,5 @@ +open Proofview.Notations + let contrib_name = "btauto" let init_constant dir s = @@ -214,23 +216,23 @@ module Btauto = struct in Tacticals.tclFAIL 0 msg gl - let try_unification env gl = + let try_unification env = + Goal.concl >>- fun concl -> let eq = Lazy.force eq in - let concl = Tacmach.pf_concl gl 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.tclORELSE0 Tactics.reflexivity (print_counterexample p env) in - tac gl + let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in + tac | _ -> let msg = str "Btauto: Internal error" in - Tacticals.tclFAIL 0 msg gl + Tacticals.New.tclFAIL 0 msg - let tac gl = + let tac = + Goal.concl >>- fun concl -> let eq = Lazy.force eq in let bool = Lazy.force Bool.typ in - let concl = Tacmach.pf_concl gl in let t = decomp_term concl in match t with | Term.App (c, [|typ; tl; tr|]) @@ -242,14 +244,14 @@ module Btauto = struct let fl = reify env fl in let fr = reify env fr in let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in - Tacticals.tclTHENLIST [ - Tactics.change_in_concl None changed_gl; - Tactics.apply (Lazy.force soundness); - Tactics.normalise_vm_in_concl; + 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 - ] gl + ] | _ -> let msg = str "Cannot recognize a boolean equality" in - Tacticals.tclFAIL 0 msg gl + Tacticals.New.tclFAIL 0 msg end diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 6c578f1c2..63b6375e1 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -23,6 +23,7 @@ open Ccproof open Pp open Errors open Util +open Proofview.Notations let constant dir s = lazy (Coqlib.gen_constant "CC" dir s) @@ -244,37 +245,42 @@ let build_projection intype outtype (cstr:constructor) special default gls= let _M =mkMeta -let rec proof_tac p gls = +let rec proof_tac p : unit Proofview.tactic = + Tacmach.New.pf_apply Typing.type_of >>- fun type_of -> match p.p_rule with - Ax c -> exact_check c gls + Ax c -> Proofview.V82.tactic (exact_check c) | SymAx c -> - let l=constr_of_term p.p_lhs and - r=constr_of_term p.p_rhs in - let typ = Termops.refresh_universes (pf_type_of gls l) in + Proofview.V82.tactic begin fun gls -> + let l=constr_of_term p.p_lhs and + r=constr_of_term p.p_rhs in + let typ = Termops.refresh_universes (pf_type_of gls l) in exact_check (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls + end | Refl t -> - let lr = constr_of_term t in - let typ = Termops.refresh_universes (pf_type_of gls lr) in - exact_check - (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls + Proofview.V82.tactic begin fun gls -> + let lr = constr_of_term t in + let typ = Termops.refresh_universes (pf_type_of gls lr) in + exact_check + (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls + end | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in - let typ = Termops.refresh_universes (pf_type_of gls t2) in + let typ = Termops.refresh_universes (type_of t2) in let prf = mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in - tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls + Tacticals.New.tclTHENS (Proofview.V82.tactic (refine prf)) [(proof_tac p1);(proof_tac p2)] | Congr (p1,p2)-> let tf1=constr_of_term p1.p_lhs and tx1=constr_of_term p2.p_lhs and tf2=constr_of_term p1.p_rhs and tx2=constr_of_term p2.p_rhs in - let typf = Termops.refresh_universes (pf_type_of gls tf1) in - let typx = Termops.refresh_universes (pf_type_of gls tx1) in - let typfx = Termops.refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in - let id = pf_get_new_id (Id.of_string "f") gls in + let typf = Termops.refresh_universes (type_of tf1) in + let typx = Termops.refresh_universes (type_of tx1) in + let typfx = Termops.refresh_universes (type_of (mkApp (tf1,[|tx1|]))) in + Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) >>- fun id -> let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = mkApp(Lazy.force _f_equal, @@ -288,78 +294,77 @@ let rec proof_tac p gls = mkApp(tf1,[|tx1|]); mkApp(tf2,[|tx1|]); mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in - tclTHENS (refine prf) - [tclTHEN (refine lemma1) (proof_tac p1); - tclFIRST - [tclTHEN (refine lemma2) (proof_tac p2); + Tacticals.New.tclTHENS (Proofview.V82.tactic (refine prf)) + [Tacticals.New.tclTHEN (Proofview.V82.tactic (refine lemma1)) (proof_tac p1); + Tacticals.New.tclFIRST + [Tacticals.New.tclTHEN (Proofview.V82.tactic (refine lemma2)) (proof_tac p2); reflexivity; - fun gls -> - errorlabstrm "Congruence" + Proofview.tclZERO (UserError ("Congruence" , (Pp.str - "I don't know how to handle dependent equality")]] gls + "I don't know how to handle dependent equality")))]] | Inject (prf,cstr,nargs,argind) -> let ti=constr_of_term prf.p_lhs in let tj=constr_of_term prf.p_rhs in let default=constr_of_term p.p_lhs in - let intype = Termops.refresh_universes (pf_type_of gls ti) in - let outtype = Termops.refresh_universes (pf_type_of gls default) in + let intype = Termops.refresh_universes (type_of ti) in + let outtype = Termops.refresh_universes (type_of default) in let special=mkRel (1+nargs-argind) in - let proj=build_projection intype outtype cstr special default gls in + Tacmach.New.of_old (build_projection intype outtype cstr special default) >>- fun proj -> let injt= mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in - tclTHEN (refine injt) (proof_tac prf) gls + Tacticals.New.tclTHEN (Proofview.V82.tactic (refine injt)) (proof_tac prf) -let refute_tac c t1 t2 p gls = +let refute_tac c t1 t2 p = let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let intype = Termops.refresh_universes (pf_type_of gls tt1) in + Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt1)) >>- fun intype -> let neweq= mkApp(Lazy.force _eq, [|intype;tt1;tt2|]) in - let hid=pf_get_new_id (Id.of_string "Heq") gls in + Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>- fun hid -> let false_t=mkApp (c,[|mkVar hid|]) in - tclTHENS (assert_tac (Name hid) neweq) - [proof_tac p; simplest_elim false_t] gls + Tacticals.New.tclTHENS (assert_tac (Name hid) neweq) + [proof_tac p; simplest_elim false_t] -let convert_to_goal_tac c t1 t2 p gls = +let convert_to_goal_tac c t1 t2 p = let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let sort = Termops.refresh_universes (pf_type_of gls tt2) in + Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt2)) >>- fun sort -> let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in - let e=pf_get_new_id (Id.of_string "e") gls in - let x=pf_get_new_id (Id.of_string "X") gls in + Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) >>- fun e -> + Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>- fun x -> let identity=mkLambda (Name x,sort,mkRel 1) in let endt=mkApp (Lazy.force _eq_rect, [|sort;tt1;identity;c;tt2;mkVar e|]) in - tclTHENS (assert_tac (Name e) neweq) - [proof_tac p;exact_check endt] gls + Tacticals.New.tclTHENS (assert_tac (Name e) neweq) + [proof_tac p; Proofview.V82.tactic (exact_check endt)] -let convert_to_hyp_tac c1 t1 c2 t2 p gls = +let convert_to_hyp_tac c1 t1 c2 t2 p = let tt2=constr_of_term t2 in - let h=pf_get_new_id (Id.of_string "H") gls in + Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) >>- fun h -> let false_t=mkApp (c2,[|mkVar h|]) in - tclTHENS (assert_tac (Name h) tt2) + Tacticals.New.tclTHENS (assert_tac (Name h) tt2) [convert_to_goal_tac c1 t1 t2 p; - simplest_elim false_t] gls + simplest_elim false_t] -let discriminate_tac cstr p gls = +let discriminate_tac cstr p = let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in - let intype = Termops.refresh_universes (pf_type_of gls t1) in - let concl=pf_concl gls in + Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) >>- fun intype -> + Goal.concl >>- fun concl -> let outsort = mkType (Termops.new_univ ()) in - let xid=pf_get_new_id (Id.of_string "X") gls in - let tid=pf_get_new_id (Id.of_string "t") gls 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 - let trivial=pf_type_of gls identity 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 - let hid=pf_get_new_id (Id.of_string "Heq") gls in - let proj=build_projection intype outtype cstr trivial concl gls 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 - tclTHENS (assert_tac (Name hid) neweq) - [proof_tac p;exact_check endt] gls + Tacticals.New.tclTHENS (assert_tac (Name hid) neweq) + [proof_tac p; Proofview.V82.tactic (exact_check endt)] (* wrap everything *) @@ -370,24 +375,26 @@ let build_term_to_complete uf meta pac = let all_args = List.rev_append real_args dummy_args in applistc (mkConstruct cinfo.ci_constr) all_args -let cc_tactic depth additionnal_terms gls= +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 - let state = make_prb gls depth additionnal_terms 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 -> tclFAIL 0 (str "congruence failed") gls + 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 gls + discriminate_tac cstr p | Incomplete -> + Goal.env >>- fun env -> let metacnt = ref 0 in let newmeta _ = incr metacnt; _M !metacnt in let terms_to_complete = @@ -404,31 +411,31 @@ let cc_tactic depth additionnal_terms gls= str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(") - (Termops.print_constr_env (pf_env gls)) + (Termops.print_constr_env env) terms_to_complete ++ str ")\"," end ++ Pp.str " replacing metavariables by arbitrary terms."); - tclFAIL 0 (str "Incomplete") gls + 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 gls - | Hyp id -> refute_tac id ta tb p gls + Goal -> proof_tac p + | Hyp id -> refute_tac id ta tb p | HeqG id -> - convert_to_goal_tac id ta tb p gls + convert_to_goal_tac id ta tb p | HeqnH (ida,idb) -> - convert_to_hyp_tac ida ta idb tb p gls + convert_to_hyp_tac ida ta idb tb p let cc_fail gls = errorlabstrm "Congruence" (Pp.str "congruence failed.") let congruence_tac depth l = - tclORELSE - (tclTHEN (tclREPEAT introf) (cc_tactic depth l)) - cc_fail + Tacticals.New.tclORELSE + (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)) + (Proofview.V82.tactic cc_fail) (* Beware: reflexivity = constructor 1 = apply refl_equal might be slow now, let's rather do something equivalent @@ -443,22 +450,31 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal) the fact that congruence is called internally. *) -let f_equal gl = +let f_equal = + Goal.concl >>- fun concl -> + Tacmach.New.pf_apply Typing.type_of >>- fun type_of -> let cut_eq c1 c2 = - let ty = Termops.refresh_universes (pf_type_of gl c1) in - tclTHENTRY - (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) - (simple_reflexivity ()) + 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 in - try match kind_of_term (pf_concl gl) with + 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 tclTRY (congruence_tac 1000 []) - else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1)) - in cuts (Array.length v - 1) gl - | _ -> tclIDTAC gl + 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 - | _ -> tclIDTAC gl - with Type_errors.TypeError _ -> tclIDTAC gl + | _ -> Proofview.tclUNIT () + end + begin function + | Type_errors.TypeError _ -> Proofview.tclUNIT () + | e -> Proofview.tclZERO e + end diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index 365c172c9..a022a07da 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -9,12 +9,12 @@ open Term open Proof_type -val proof_tac: Ccproof.proof -> Proof_type.tactic +val proof_tac: Ccproof.proof -> unit Proofview.tactic -val cc_tactic : int -> constr list -> tactic +val cc_tactic : int -> constr list -> unit Proofview.tactic val cc_fail : tactic -val congruence_tac : int -> constr list -> tactic +val congruence_tac : int -> constr list -> unit Proofview.tactic -val f_equal : tactic +val f_equal : unit Proofview.tactic diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 30ed01c49..3b8487d75 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -121,7 +121,7 @@ let start_proof_tac gls= tcl_change_info info gls let go_to_proof_mode () = - Pfedit.by start_proof_tac; + Pfedit.by (Proofview.V82.tactic start_proof_tac); let p = Proof_global.give_me_the_proof () in Decl_mode.focus p @@ -214,7 +214,8 @@ let filter_hyps f gls = let local_hyp_prefix = Id.of_string "___" -let add_justification_hyps keep items gls = +let add_justification_hyps keep items gls = assert false +(* arnaud: todo let add_aux c gls= match kind_of_term c with Var id -> @@ -226,6 +227,7 @@ let add_justification_hyps keep items gls = tclTHEN (letin_tac None (Names.Name id) c None Locusops.nowhere) (thin_body [id]) gls in tclMAP add_aux items gls +*) let prepare_goal items gls = let tokeep = ref Id.Set.empty in @@ -235,11 +237,11 @@ let prepare_goal items gls = filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls let my_automation_tac = ref - (fun gls -> anomaly (Pp.str "No automation registered")) + (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered"))) let register_automation_tac tac = my_automation_tac:= tac -let automation_tac gls = !my_automation_tac gls +let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac) let justification tac gls= tclORELSE @@ -253,8 +255,10 @@ let justification tac gls= daimon_tac gls end) gls -let default_justification elems gls= +let default_justification elems gls= assert false +(* arnaud: todo justification (tclTHEN (prepare_goal elems) automation_tac) gls +*) (* code for conclusion refining *) @@ -452,7 +456,8 @@ let mk_stat_or_thesis info gls = function error "\"thesis for ...\" is not applicable here." | Thesis Plain -> pf_concl gls -let just_tac _then cut info gls0 = +let just_tac _then cut info gls0 = assert false +(* arnaud: todo let last_item = if _then then try [mkVar (get_last (pf_env gls0))] @@ -471,8 +476,10 @@ let just_tac _then cut info gls0 = | Some tac -> (Tacinterp.eval_tactic tac) gls in justification (tclTHEN items_tac method_tac) gls0 +*) -let instr_cut mkstat _thus _then cut gls0 = +let instr_cut mkstat _thus _then cut gls0 = assert false +(* arnaud: let info = get_its_info gls0 in let stat = cut.cut_stat in let (c_id,_) = match stat.st_label with @@ -487,7 +494,7 @@ let instr_cut mkstat _thus _then cut gls0 = tclTHENS (assert_postpone c_id c_stat) [tclTHEN tcl_erase_info (just_tac _then cut info); thus_tac] gls0 - +*) (* iterated equality *) @@ -505,7 +512,8 @@ let decompose_eq id gls = else error "Previous step is not an equality." | _ -> error "Previous step is not an equality." -let instr_rew _thus rew_side cut gls0 = +let instr_rew _thus rew_side cut gls0 = assert false +(* arnaud: let last_id = try get_last (pf_env gls0) with UserError _ -> error "No previous equality." @@ -546,12 +554,13 @@ let instr_rew _thus rew_side cut gls0 = (tclTHENS (transitivity rhs) [exact_check (mkVar last_id);just_tac]); thus_tac new_eq] gls0 - +*) (* tactics for claim/focus *) -let instr_claim _thus st gls0 = +let instr_claim _thus st gls0 = assert false +(* arnaud: todo let info = get_its_info gls0 in let (id,_) = match st.st_label with Anonymous -> pf_get_new_id (Id.of_string "_claim") gls0,false @@ -565,10 +574,12 @@ let instr_claim _thus st gls0 = tclTHENS (assert_postpone id st.st_it) [thus_tac; tcl_change_info ninfo1] gls0 +*) (* tactics for assume *) -let push_intro_tac coerce nam gls = +let push_intro_tac coerce nam gls = assert false +(* arnaud: todo let (hid,_) = match nam with Anonymous -> pf_get_new_id (Id.of_string "_hyp") gls,false @@ -577,6 +588,7 @@ let push_intro_tac coerce nam gls = [intro_mustbe_force hid; coerce hid] gls +*) let assume_tac hyps gls = List.fold_right @@ -643,7 +655,8 @@ let rec build_applist prod = function let ctx,head = build_applist (prod_applist prod [mkMeta n]) q in (n,typ)::ctx,head -let instr_suffices _then cut gls0 = +let instr_suffices _then cut gls0 = assert false +(* arnaud: todo let info = get_its_info gls0 in let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in let ctx,hd = cut.cut_stat in @@ -659,6 +672,7 @@ let instr_suffices _then cut gls0 = tcl_erase_info; just_tac _then cut info]; thus_tac] gls0 +*) (* tactics for consider/given *) @@ -678,7 +692,8 @@ let conjunction_arity id gls = List.length rc | _ -> raise Not_found -let rec intron_then n ids ltac gls = +let rec intron_then n ids ltac gls = assert false +(* arnaud: if n<=0 then ltac ids gls else @@ -686,9 +701,11 @@ let rec intron_then n ids ltac gls = tclTHEN (intro_mustbe_force id) (intron_then (pred n) (id::ids) ltac) gls +*) -let rec consider_match may_intro introduced available expected gls = +let rec consider_match may_intro introduced available expected gls = assert false +(* arnaud: match available,expected with [],[] -> tclIDTAC gls @@ -731,8 +748,10 @@ let rec consider_match may_intro introduced available expected gls = (List.rev_append l rest_ids) expected)] gls) end gls +*) -let consider_tac c hyps gls = +let consider_tac c hyps gls = assert false +(* arnaud: todo match kind_of_term (strip_outer_cast c) with Var id -> consider_match false [] [id] hyps gls @@ -741,6 +760,7 @@ let consider_tac c hyps gls = tclTHEN (forward None (Some (Loc.ghost, IntroIdentifier id)) c) (consider_match false [] [id] hyps) gls +*) let given_tac hyps gls = @@ -768,9 +788,11 @@ let rec build_function args body = mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun) | [] -> body -let define_tac id args body gls = +let define_tac id args body gls = assert false +(* arnaud: todo: let t = build_function args body in letin_tac None (Name id) t None Locusops.nowhere gls +*) (* tactics for reconsider *) @@ -903,7 +925,8 @@ let register_nodep_subcase id= function end | _ -> anomaly (Pp.str "wrong stack state") -let suppose_tac hyps gls0 = +let suppose_tac hyps gls0 = assert false +(* arnaud: todo let info = get_its_info gls0 in let thesis = pf_concl gls0 in let id = pf_get_new_id (Id.of_string "subcase_") gls0 in @@ -916,6 +939,7 @@ let suppose_tac hyps gls0 = assume_tac hyps; clear old_clauses]; tcl_change_info ninfo2] gls0 +*) (* suppose it is ... *) @@ -1104,7 +1128,8 @@ let rec register_dep_subcase id env per_info pat = function (EK_dep (start_tree env per_info.per_ind per_info.per_wf)) | EK_dep tree -> EK_dep (add_branch id [[pat,per_info.per_wf]] tree) -let case_tac params pat_info hyps gls0 = +let case_tac params pat_info hyps gls0 = assert false +(* arnaud: todo let info = get_its_info gls0 in let id = pf_get_new_id (Id.of_string "subcase_") gls0 in let et,per_info,ek,old_clauses,rest = @@ -1125,6 +1150,7 @@ let case_tac params pat_info hyps gls0 = assume_hyps_or_theses hyps; clear old_clauses]; tcl_change_info ninfo2] gls0 +*) (* end cases *) @@ -1179,7 +1205,8 @@ let hrec_for fix_id per_info gls obj_id = compose_lam rc (whd_beta gls.sigma hd2) -let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = +let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = assert false +(* arnaud: todo match tree, objs with Close_patt t,_ -> let args0 = pop_stacks args in @@ -1272,6 +1299,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = anomaly ~label:"execute_cases " (Pp.str "Nothing to skip") | End_patt (_,_) , _ :: _ -> anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left") +*) let understand_my_constr c gls = let env = pf_env gls in @@ -1283,13 +1311,16 @@ let understand_my_constr c gls = in Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(Pretyping.OfType (pf_concl gls)) (frob rawc) -let my_refine c gls = +let my_refine c gls = assert false +(* arnaud: todo let oc = understand_my_constr c gls in Refine.refine oc gls +*) (* end focus/claim *) -let end_tac et2 gls = +let end_tac et2 gls = assert false +(* arnaud: todo let info = get_its_info gls in let et1,pi,ek,clauses = match info.pm_stack with @@ -1354,6 +1385,7 @@ let end_tac et2 gls = [mkVar c_id] 0 tree] gls0 end end gls +*) (* escape *) @@ -1463,7 +1495,7 @@ let do_instr raw_instr pts = let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) sigma env glob_instr in - Pfedit.by (tclTHEN (eval_instr instr) clean_tmp) + Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) else () end; postprocess pts raw_instr.instr; (* spiwack: this should restore a compatible semantics with diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli index 107b65366..d78ca84d1 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -15,9 +15,9 @@ open Decl_mode val go_to_proof_mode: unit -> unit val return_from_tactic_mode: unit -> unit -val register_automation_tac: tactic -> unit +val register_automation_tac: unit Proofview.tactic -> unit -val automation_tac : tactic +val automation_tac : unit Proofview.tactic val concl_refiner: Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 84060dc9d..c125be65a 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -79,7 +79,7 @@ let gen_ground_tac flag taco ids bases gl= let startseq gl= let seq=empty_seq !ground_depth in extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in - let result=ground_tac solver startseq gl in + let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in qflag:=backup;result with reraise -> qflag:=backup;raise reraise @@ -125,29 +125,31 @@ END TACTIC EXTEND firstorder [ "firstorder" tactic_opt(t) firstorder_using(l) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) l [] ] + [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l []) ] | [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) [] l ] + [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) [] l) ] | [ "firstorder" tactic_opt(t) firstorder_using(l) "with" ne_preident_list(l') ] -> - [ gen_ground_tac true (Option.map eval_tactic t) l l' ] + [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l l') ] END TACTIC EXTEND gintuition [ "gintuition" tactic_opt(t) ] -> - [ gen_ground_tac false (Option.map eval_tactic t) [] [] ] + [ Proofview.V82.tactic (gen_ground_tac false (Option.map eval_tactic t) [] []) ] END +open Proofview.Notations -let default_declarative_automation gls = - tclORELSE - (tclORELSE (Auto.h_trivial [] None) +let default_declarative_automation = + Proofview.tclUNIT () >= fun () -> (* delay for [congruence_depth] *) + Tacticals.New.tclORELSE + (Tacticals.New.tclORELSE (Auto.h_trivial [] None) (Cctac.congruence_tac !congruence_depth [])) - (gen_ground_tac true - (Some (tclTHEN + (Proofview.V82.tactic (gen_ground_tac true + (Some (Tacticals.New.tclTHEN (snd (default_solver ())) (Cctac.congruence_tac !congruence_depth []))) - [] []) gls + [] [])) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index ac612d0cd..0acdc4c80 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -143,11 +143,11 @@ let left_instance_tac (inst,id) continue seq= else tclTHENS (cut dom) [tclTHENLIST - [introf; + [Proofview.V82.of_tactic introf; (fun gls->generalize [mkApp(constr_of_global id, [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); - introf; + Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; tclTRY assumption] @@ -168,7 +168,7 @@ let left_instance_tac (inst,id) continue seq= in tclTHENLIST [special_generalize; - introf; + Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,Some c) seq))]] @@ -177,14 +177,14 @@ let right_instance_tac inst continue seq= Phantom dom -> tclTHENS (cut dom) [tclTHENLIST - [introf; + [Proofview.V82.of_tactic introf; (fun gls-> - split (ImplicitBindings - [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); + Proofview.V82.of_tactic (split (ImplicitBindings + [mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (split (ImplicitBindings [t])) + (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t]))) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 02a0dd20d..99e03cdbe 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -67,24 +67,24 @@ let ll_atom_tac a backtrack id continue seq= [generalize [mkApp(constr_of_global id, [|constr_of_global (find_left a seq)|])]; clear_global id; - intro] + Proofview.V82.of_tactic intro] with Not_found->tclFAIL 0 (Pp.str "No link")) (wrap 1 false continue seq) backtrack (* right connectives rules *) let and_tac backtrack continue seq= - tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack + tclIFTHENELSE (Proofview.V82.of_tactic simplest_split) (wrap 0 true continue seq) backtrack let or_tac backtrack continue seq= tclORELSE - (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq)))) + (Proofview.V82.of_tactic (any_constructor false (Some (Proofview.V82.tactic (tclCOMPLETE (wrap 0 true continue seq)))))) backtrack let arrow_tac backtrack continue seq= - tclIFTHENELSE intro (wrap 1 true continue seq) + tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 1 true continue seq) (tclORELSE - (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq))) + (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 1 true continue seq))) backtrack) (* left connectives rules *) @@ -92,9 +92,9 @@ let left_and_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE (tclTHENLIST - [simplest_elim (constr_of_global id); + [Proofview.V82.of_tactic (simplest_elim (constr_of_global id)); clear_global id; - tclDO n intro]) + tclDO n (Proofview.V82.of_tactic intro)]) (wrap n false continue seq) backtrack gls @@ -103,15 +103,15 @@ let left_or_tac ind backtrack id continue seq gls= let f n= tclTHENLIST [clear_global id; - tclDO n intro; + tclDO n (Proofview.V82.of_tactic intro); wrap n false continue seq] in tclIFTHENSVELSE - (simplest_elim (constr_of_global id)) + (Proofview.V82.of_tactic (simplest_elim (constr_of_global id))) (Array.map f v) backtrack gls let left_false_tac id= - simplest_elim (constr_of_global id) + Proofview.V82.of_tactic (simplest_elim (constr_of_global id)) (* left arrow connective rules *) @@ -135,7 +135,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl= (tclTHENLIST [generalize newhyps; clear_global id; - tclDO lp intro]) + tclDO lp (Proofview.V82.of_tactic intro)]) (wrap lp false continue seq) backtrack gl let ll_arrow_tac a b c backtrack id continue seq= @@ -146,7 +146,7 @@ let ll_arrow_tac a b c backtrack id continue seq= tclORELSE (tclTHENS (cut c) [tclTHENLIST - [introf; + [Proofview.V82.of_tactic introf; clear_global id; wrap 1 false continue seq]; tclTHENS (cut cc) @@ -154,8 +154,8 @@ let ll_arrow_tac a b c backtrack id continue seq= tclTHENLIST [generalize [d]; clear_global id; - introf; - introf; + Proofview.V82.of_tactic introf; + Proofview.V82.of_tactic introf; tclCOMPLETE (wrap 2 true continue seq)]]]) backtrack @@ -163,9 +163,9 @@ let ll_arrow_tac a b c backtrack id continue seq= let forall_tac backtrack continue seq= tclORELSE - (tclIFTHENELSE intro (wrap 0 true continue seq) + (tclIFTHENELSE (Proofview.V82.of_tactic intro) (wrap 0 true continue seq) (tclORELSE - (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq))) + (tclTHEN (Proofview.V82.of_tactic introf) (tclCOMPLETE (wrap 0 true continue seq))) backtrack)) (if !qflag then tclFAIL 0 (Pp.str "reversible in 1st order mode") @@ -175,9 +175,9 @@ let forall_tac backtrack continue seq= let left_exists_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE - (simplest_elim (constr_of_global id)) + (Proofview.V82.of_tactic (simplest_elim (constr_of_global id))) (tclTHENLIST [clear_global id; - tclDO n intro; + tclDO n (Proofview.V82.of_tactic intro); (wrap (n-1) false continue seq)]) backtrack gls @@ -186,13 +186,13 @@ let ll_forall_tac prod backtrack id continue seq= tclORELSE (tclTHENS (cut prod) [tclTHENLIST - [intro; + [Proofview.V82.of_tactic intro; (fun gls-> let id0=pf_nth_hyp_id gls 1 in let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in tclTHEN (generalize [term]) (clear [id0]) gls); clear_global id; - intro; + Proofview.V82.of_tactic intro; tclCOMPLETE (wrap 1 false continue (deepen seq))]; tclCOMPLETE (wrap 0 true continue (deepen seq))]) backtrack diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 3dd384ee8..d49f225e6 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -478,22 +478,22 @@ let rec fourier gl= "Rlt" -> (tclTHEN (tclTHEN (apply (get coq_Rfourier_not_ge_lt)) - (intro_using fhyp)) + (Proofview.V82.of_tactic (intro_using fhyp))) fourier) |"Rle" -> (tclTHEN (tclTHEN (apply (get coq_Rfourier_not_gt_le)) - (intro_using fhyp)) + (Proofview.V82.of_tactic (intro_using fhyp))) fourier) |"Rgt" -> (tclTHEN (tclTHEN (apply (get coq_Rfourier_not_le_gt)) - (intro_using fhyp)) + (Proofview.V82.of_tactic (intro_using fhyp))) fourier) |"Rge" -> (tclTHEN (tclTHEN (apply (get coq_Rfourier_not_lt_ge)) - (intro_using fhyp)) + (Proofview.V82.of_tactic (intro_using fhyp))) fourier) |_-> raise GoalDone) |_-> raise GoalDone @@ -595,16 +595,16 @@ let rec fourier gl= )) (tclTHEN (apply (if sres then get coq_Rnot_lt_lt else get coq_Rnot_le_le)) - (tclTHENS (Equality.replace + (tclTHENS (Proofview.V82.of_tactic (Equality.replace (mkAppL [|get coq_Rminus;!t2;!t1|] ) - tc) + tc)) [tac2; (tclTHENS - (Equality.replace + (Proofview.V82.of_tactic (Equality.replace (mkApp (get coq_Rinv, [|get coq_R1|])) - (get coq_R1)) + (get coq_R1))) (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) [tclORELSE @@ -617,7 +617,7 @@ let rec fourier gl= ])); !tac1]); tac:=(tclTHENS (cut (get coq_False)) - [tclTHEN intro (contradiction None); + [tclTHEN (Proofview.V82.of_tactic intro) (Proofview.V82.of_tactic (contradiction None)); !tac]) |_-> assert false) |_-> assert false ); diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 01166d1db..1635cecc0 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -11,5 +11,5 @@ open FourierR TACTIC EXTEND fourier - [ "fourierz" ] -> [ fourier ] + [ "fourierz" ] -> [ Proofview.V82.tactic fourier ] END diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8edb16850..2da4b6147 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -175,7 +175,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic = fun g -> let prov_id = pf_get_new_id hyp_id g in tclTHENS - ((* observe_tac msg *) (assert_by (Name prov_id) t (tclCOMPLETE tac))) + ((* observe_tac msg *) Proofview.V82.of_tactic (assert_by (Name prov_id) t (Proofview.V82.tactic (tclCOMPLETE tac)))) [tclTHENLIST [ (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); @@ -189,7 +189,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) = let nb_intros = List.length context in tclTHENLIST [ - tclDO nb_intros intro; (* introducing context *) + tclDO nb_intros (Proofview.V82.of_tactic intro); (* introducing context *) (fun g -> let context_hyps = fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) @@ -322,7 +322,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = in let prove_new_hyp : tactic = tclTHEN - (tclDO ctxt_size intro) + (tclDO ctxt_size (Proofview.V82.of_tactic intro)) (fun g -> let all_ids = pf_ids_of_hyps g in let new_ids,_ = list_chop ctxt_size all_ids in @@ -395,7 +395,7 @@ let rewrite_until_var arg_num eq_ids : tactic = | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property"); | eq_id::eq_ids -> tclTHEN - (tclTRY (Equality.rewriteRL (mkVar eq_id))) + (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id)))) (do_rewrite eq_ids) g in @@ -433,7 +433,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let context_length = List.length context in tclTHENLIST [ - tclDO context_length intro; + tclDO context_length (Proofview.V82.of_tactic intro); (fun g -> let context_hyps_ids = fst (list_chop ~msg:"rec hyp : context_hyps" @@ -447,7 +447,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = in (* observe_tac "rec hyp " *) (tclTHENS - (assert_tac (Name rec_pte_id) t_x) + (Proofview.V82.of_tactic (assert_tac (Name rec_pte_id) t_x)) [ (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps); (* observe_tac "prove rec hyp" *) @@ -484,7 +484,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let prove_trivial = let nb_intro = List.length context in tclTHENLIST [ - tclDO nb_intro intro; + tclDO nb_intro (Proofview.V82.of_tactic intro); (fun g -> let context_hyps = fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g)) @@ -583,9 +583,9 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclTHENLIST [ (* We first introduce the variables *) - tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps); + tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding dyn_infos.rec_hyps)); (* Then the equation itself *) - intro_using heq_id; + Proofview.V82.of_tactic (intro_using heq_id); onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) tclMAP introduction_no_check dyn_infos.rec_hyps; @@ -636,7 +636,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = fun g -> let prov_hid = pf_get_new_id hid g in tclTHENLIST[ - pose_proof (Name prov_hid) (mkApp(mkVar hid,args)); + Proofview.V82.of_tactic (pose_proof (Name prov_hid) (mkApp(mkVar hid,args))); thin [hid]; h_rename [prov_hid,hid] ] g @@ -704,7 +704,7 @@ let build_proof thin dyn_infos.rec_hyps; pattern_option [Locus.AllOccurrencesBut [1],t] None; (fun g -> observe_tac "toto" ( - tclTHENSEQ [h_simplest_case t; + tclTHENSEQ [Proofview.V82.of_tactic (h_simplest_case t); (fun g' -> let g'_nb_prod = nb_prod (pf_concl g') in let nb_instanciate_partial = g'_nb_prod - g_nb_prod in @@ -729,7 +729,7 @@ let build_proof match kind_of_term( pf_concl g) with | Prod _ -> tclTHEN - intro + (Proofview.V82.of_tactic intro) (fun g' -> let (id,_,_) = pf_last_hyp g' in let new_term = @@ -965,13 +965,13 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let prove_replacement = tclTHENSEQ [ - tclDO (nb_params + rec_args_num + 1) intro; + tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro); (* observe_tac "" *) (fun g -> let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); - (* observe_tac "h_case" *) (h_case false (mkVar rec_id,NoBindings)); - intros_reflexivity] g + (* observe_tac "h_case" *) (Proofview.V82.of_tactic (h_case false (mkVar rec_id,NoBindings))); + (Proofview.V82.of_tactic intros_reflexivity)] g ) ] in @@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) lemma_type (fun _ _ -> ()); - Pfedit.by (prove_replacement); + Pfedit.by (Proofview.V82.tactic prove_replacement); Lemmas.save_named false @@ -1019,12 +1019,12 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = in let nb_intro_to_do = nb_prod (pf_concl g) in tclTHEN - (tclDO nb_intro_to_do intro) + (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro)) ( fun g' -> let just_introduced = nLastDecls nb_intro_to_do g' in let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in - tclTHEN (Equality.rewriteLR equation_lemma) (revert just_introduced_id) g' + tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) (revert just_introduced_id) g' ) g @@ -1206,9 +1206,9 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let first_tac : tactic = (* every operations until fix creations *) tclTHENSEQ - [ (* observe_tac "introducing params" *) (intros_using (List.rev_map id_of_decl princ_info.params)); - (* observe_tac "introducing predictes" *) (intros_using (List.rev_map id_of_decl princ_info.predicates)); - (* observe_tac "introducing branches" *) (intros_using (List.rev_map id_of_decl princ_info.branches)); + [ (* observe_tac "introducing params" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params)); + (* observe_tac "introducing predictes" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates)); + (* observe_tac "introducing branches" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches)); (* observe_tac "building fixes" *) mk_fixes; ] in @@ -1225,7 +1225,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let nb_args = fix_info.nb_realargs in tclTHENSEQ [ - (* observe_tac ("introducing args") *) (tclDO nb_args intro); + (* observe_tac ("introducing args") *) (tclDO nb_args (Proofview.V82.of_tactic intro)); (fun g -> (* replacement of the function by its body *) let args = nLastDecls nb_args g in let fix_body = fix_info.body_with_param in @@ -1289,7 +1289,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let nb_args = min (princ_info.nargs) (List.length ctxt) in tclTHENSEQ [ - tclDO nb_args intro; + tclDO nb_args (Proofview.V82.of_tactic intro); (fun g -> (* replacement of the function by its body *) let args = nLastDecls nb_args g in let args_id = List.map (fun (id,_,_) -> id) args in @@ -1386,7 +1386,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = fun gls -> let eqs = List.map mkVar eqs in let rewrite = - tclFIRST (List.map Equality.rewriteRL eqs ) + tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs ) in let _,hrec_concl = decompose_prod (pf_type_of gls (mkVar hrec)) in let f_app = Array.last (snd (destApp hrec_concl)) in @@ -1411,8 +1411,8 @@ let rec rewrite_eqs_in_eqs eqs = (fun id gl -> observe_tac (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id)) - (tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences - true (* dep proofs also: *) true id (mkVar eq) false)) + (tclTRY (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences + true (* dep proofs also: *) true id (mkVar eq) false))) gl ) eqs @@ -1543,9 +1543,9 @@ let prove_principle_for_gen ((* observe_tac "prove_rec_arg_acc" *) (tclCOMPLETE (tclTHEN - (assert_by (Name wf_thm_id) + (Proofview.V82.of_tactic (assert_by (Name wf_thm_id) (mkApp (delayed_force well_founded,[|input_type;relation|])) - (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)) + (Proofview.V82.tactic (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))) ( (* observe_tac *) (* "apply wf_thm" *) @@ -1583,8 +1583,8 @@ let prove_principle_for_gen tclTHENSEQ [ generalize [lemma]; - h_intro hid; - Elim.h_decompose_and (mkVar hid); + Proofview.V82.of_tactic (h_intro hid); + Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)); (fun g -> let new_hyps = pf_ids_of_hyps g in tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps)); @@ -1606,10 +1606,10 @@ let prove_principle_for_gen (List.rev_map (fun (na,_,_) -> Nameops.out_name na) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); - (* observe_tac "" *) (assert_by + (* observe_tac "" *) Proofview.V82.of_tactic (assert_by (Name acc_rec_arg_id) (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) - (prove_rec_arg_acc) + (Proofview.V82.tactic prove_rec_arg_acc) ); (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) @@ -1617,7 +1617,7 @@ let prove_principle_for_gen (* observe_tac "h_fix " *) (h_fix (Some fix_id) (List.length args_ids + 1)); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); - Equality.rewriteLR (mkConst eq_ref); + Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); (* observe_tac "finish" *) (fun gl' -> let body = let _,args = destApp (pf_concl gl') in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index e5d8fe4c1..0850d556c 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -297,7 +297,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro (hook new_principle_type) ; (* let _tim1 = System.get_time () in *) - Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); + Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams)); (* let _tim2 = System.get_time () in *) (* begin *) (* let dur1 = System.time_difference tim1 tim2 in *) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index e65ca94f0..b317cec0d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -71,7 +71,7 @@ END TACTIC EXTEND newfuninv [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] -> [ - Invfun.invfun hyp fname + Proofview.V82.tactic (Invfun.invfun hyp fname) ] END @@ -98,7 +98,7 @@ TACTIC EXTEND newfunind | [c] -> c | c::cl -> applist(c,cl) in - Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ] + Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction true c x pat)) princl ] END (***** debug only ***) TACTIC EXTEND snewfunind @@ -109,7 +109,7 @@ TACTIC EXTEND snewfunind | [c] -> c | c::cl -> applist(c,cl) in - Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ] + Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction false c x pat)) princl ] END @@ -318,10 +318,10 @@ let mkEq typ c1 c2 = let poseq_unsafe idunsafe cstr gl = let typ = Tacmach.pf_type_of gl cstr in tclTHEN - (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl) + (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl)) (tclTHENFIRST - (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr)) - Tactics.reflexivity) + (Proofview.V82.of_tactic (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr))) + (Proofview.V82.of_tactic Tactics.reflexivity)) gl @@ -432,7 +432,7 @@ TACTIC EXTEND finduction | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0" | _ -> let heuristic = chose_heuristic oi in - finduction (Some id) heuristic tclIDTAC + Proofview.V82.tactic (finduction (Some id) heuristic tclIDTAC) ] END @@ -442,13 +442,13 @@ TACTIC EXTEND fauto [ "fauto" tactic(tac)] -> [ let heuristic = chose_heuristic None in - finduction None heuristic (Tacinterp.eval_tactic tac) + Proofview.V82.tactic (finduction None heuristic (Proofview.V82.of_tactic (Tacinterp.eval_tactic tac))) ] | [ "fauto" ] -> [ let heuristic = chose_heuristic None in - finduction None heuristic tclIDTAC + Proofview.V82.tactic (finduction None heuristic tclIDTAC) ] END @@ -456,7 +456,7 @@ END TACTIC EXTEND poseq [ "poseq" ident(x) constr(c) ] -> - [ poseq x c ] + [ Proofview.V82.tactic (poseq x c) ] END VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 34814c350..4f32feb24 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -105,18 +105,18 @@ let functional_induction with_clean c princl pat = } in Tacticals.tclTHEN - (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl ) + (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl ) (Hiddentac.h_reduce flag Locusops.allHypsAndConcl) g else Tacticals.tclIDTAC g in Tacticals.tclTHEN - (choose_dest_or_ind + (Proofview.V82.of_tactic (choose_dest_or_ind princ_infos args_as_induction_constr princ' (None,pat) - None) + None)) subst_and_reduce g in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 04cc139c0..e5b975e14 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -484,7 +484,7 @@ let jmeq_refl () = with e when Errors.noncritical e -> raise (ToShow e) let h_intros l = - tclMAP h_intro l + tclMAP (fun x -> Proofview.V82.of_tactic (h_intro x)) l let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" @@ -503,5 +503,5 @@ let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (G let list_rewrite (rev:bool) (eqs: (constr*bool) list) = tclREPEAT (List.fold_right - (fun (eq,b) i -> tclORELSE ((if b then Equality.rewriteLR else Equality.rewriteRL) eq) i) + (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i) (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 4f7a61fbf..ce25f7aaf 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -399,7 +399,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem observe_tac("h_intro_patterns ") (let l = (List.nth intro_pats (pred i)) in match l with | [] -> tclIDTAC - | _ -> h_intro_patterns l); + | _ -> Proofview.V82.of_tactic (h_intro_patterns l)); (* unfolding of all the defined variables introduced by this branch *) (* observe_tac "unfolding" pre_tac; *) (* $zeta$ normalizing of the conclusion *) @@ -414,9 +414,9 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem observe_tac ("toto ") tclIDTAC; (* introducing the the result of the graph and the equality hypothesis *) - observe_tac "introducing" (tclMAP h_intro [res;hres]); + observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (h_intro x)) [res;hres]); (* replacing [res] with its value *) - observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres)); + observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); (* Conclusion *) observe_tac "exact" (fun g -> h_exact (app_constructor g) g) ] @@ -466,11 +466,11 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem in tclTHENSEQ [ - observe_tac "principle" (assert_by + observe_tac "principle" (Proofview.V82.of_tactic (assert_by (Name principle_id) princ_type - (h_exact f_principle)); - observe_tac "intro args_names" (tclMAP h_intro args_names); + (Proofview.V82.tactic (h_exact f_principle)))); + observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) args_names); (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *) observe_tac "idtac" tclIDTAC; tclTHEN_i @@ -741,7 +741,7 @@ and intros_with_rewrite_aux : tactic = if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2) then let id = pf_get_new_id (Id.of_string "y") g in - tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g + tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id); thin [id]; intros_with_rewrite ] g else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) then tclTHENSEQ[ unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]; @@ -759,18 +759,18 @@ and intros_with_rewrite_aux : tactic = else if isVar args.(1) then let id = pf_get_new_id (Id.of_string "y") g in - tclTHENSEQ [ h_intro id; + tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id); generalize_dependent_of (destVar args.(1)) id; - tclTRY (Equality.rewriteLR (mkVar id)); + tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); intros_with_rewrite ] g else if isVar args.(2) then let id = pf_get_new_id (Id.of_string "y") g in - tclTHENSEQ [ h_intro id; + tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id); generalize_dependent_of (destVar args.(2)) id; - tclTRY (Equality.rewriteRL (mkVar id)); + tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id))); intros_with_rewrite ] g @@ -778,16 +778,16 @@ and intros_with_rewrite_aux : tactic = begin let id = pf_get_new_id (Id.of_string "y") g in tclTHENSEQ[ - h_intro id; - tclTRY (Equality.rewriteLR (mkVar id)); + Proofview.V82.of_tactic (h_intro id); + tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); intros_with_rewrite ] g end | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> - Tauto.tauto g + Proofview.V82.of_tactic Tauto.tauto g | Case(_,_,v,_) -> tclTHENSEQ[ - h_case false (v,NoBindings); + Proofview.V82.of_tactic (h_case false (v,NoBindings)); intros_with_rewrite ] g | LetIn _ -> @@ -803,7 +803,7 @@ and intros_with_rewrite_aux : tactic = ] g | _ -> let id = pf_get_new_id (Id.of_string "y") g in - tclTHENSEQ [ h_intro id;intros_with_rewrite] g + tclTHENSEQ [ Proofview.V82.of_tactic (h_intro id);intros_with_rewrite] g end | LetIn _ -> tclTHENSEQ[ @@ -824,12 +824,12 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (snd (destApp (pf_concl g))).(2) with | Case(_,_,v,_) -> tclTHENSEQ[ - h_case false (v,NoBindings); - intros; + Proofview.V82.of_tactic (h_case false (v,NoBindings)); + Proofview.V82.of_tactic intros; observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] - | _ -> reflexivity - with e when Errors.noncritical e -> reflexivity + | _ -> Proofview.V82.of_tactic reflexivity + with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity in let eq_ind = Coqlib.build_coq_eq () in let discr_inject = @@ -841,15 +841,15 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (pf_type_of g (mkVar id)) with | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 - then Equality.discrHyp id g + then Proofview.V82.of_tactic (Equality.discrHyp id) g else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite] g + then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp id);thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) in (tclFIRST - [ observe_tac "reflexivity_with_destruct_cases : reflexivity" reflexivity; + [ observe_tac "reflexivity_with_destruct_cases : reflexivity" (Proofview.V82.of_tactic reflexivity); observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ())); (* We reach this point ONLY if the same value is matched (at least) two times @@ -948,8 +948,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma") in tclTHENSEQ[ - tclMAP h_intro ids; - Equality.rewriteLR (mkConst eq_lemma); + tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) ids; + Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)); (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) h_reduce @@ -996,12 +996,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let params_names = fst (List.chop princ_infos.nparams args_names) in let params = List.map mkVar params_names in tclTHENSEQ - [ tclMAP h_intro (args_names@[res;hres]); + [ tclMAP (fun id -> Proofview.V82.of_tactic (h_intro id)) (args_names@[res;hres]); observe_tac "h_generalize" (h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); - h_intro graph_principle_id; + Proofview.V82.of_tactic (h_intro graph_principle_id); observe_tac "" (tclTHEN_i - (observe_tac "elim" ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) + (observe_tac "elim" (Proofview.V82.of_tactic ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))) (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g @@ -1070,8 +1070,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (fst lemmas_types_infos.(i)) (fun _ _ -> ()); Pfedit.by - (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") - (proving_tac i)); + (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") + (proving_tac i))); do_save (); let finfo = find_Function_infos f_as_constant in let lem_cst = destConst (Constrintern.global_reference lem_id) in @@ -1121,8 +1121,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (fst lemmas_types_infos.(i)) (fun _ _ -> ()); Pfedit.by - (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i)); + (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") + (proving_tac i))); do_save (); let finfo = find_Function_infos f_as_constant in let lem_cst = destConst (Constrintern.global_reference lem_id) in @@ -1162,7 +1162,7 @@ let revert_graph kn post_tac hid g = [ h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; thin [hid]; - h_intro hid; + Proofview.V82.of_tactic (h_intro hid); post_tac hid ] g @@ -1197,7 +1197,7 @@ let functional_inversion kn hid fconst f_correct : tactic = let pre_tac,f_args,res = match kind_of_term args.(1),kind_of_term args.(2) with | App(f,f_args),_ when eq_constr f fconst -> - ((fun hid -> h_symmetry (Locusops.onHyp hid)),f_args,args.(2)) + ((fun hid -> Proofview.V82.of_tactic (h_symmetry (Locusops.onHyp hid))),f_args,args.(2)) |_,App(f,f_args) when eq_constr f fconst -> ((fun hid -> tclIDTAC),f_args,args.(1)) | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2) @@ -1206,8 +1206,8 @@ let functional_inversion kn hid fconst f_correct : tactic = pre_tac hid; h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; thin [hid]; - h_intro hid; - Inv.inv FullInversion None (NamedHyp hid); + Proofview.V82.of_tactic (h_intro hid); + Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid)); (fun g -> let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g @@ -1228,7 +1228,9 @@ let invfun qhyp f = let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in - Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp + Proofview.V82.of_tactic ( + Tactics.try_intros_until (fun hid -> Proofview.V82.tactic (functional_inversion kn hid (mkConst f) f_correct)) qhyp + ) with | Not_found -> error "No graph found" | Option.IsNone -> error "Cannot use equivalence with graph!" @@ -1238,8 +1240,9 @@ let invfun qhyp f g = match f with | Some f -> invfun qhyp f g | None -> + Proofview.V82.of_tactic begin Tactics.try_intros_until - (fun hid g -> + (fun hid -> Proofview.V82.tactic begin fun g -> let hyp_typ = pf_type_of g (mkVar hid) in match kind_of_term hyp_typ with | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> @@ -1276,6 +1279,7 @@ let invfun qhyp f g = else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) end | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ") - ) + end) qhyp + end g diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a77968092..76095cb1c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -383,7 +383,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = tclTHENSEQ [ h_intros (List.rev rev_ids); - intro_using teq_id; + Proofview.V82.of_tactic (intro_using teq_id); onLastHypId (fun heq -> tclTHENSEQ[ thin to_intros; @@ -534,15 +534,16 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = let ids = h'::ids in let def = next_ident_away_in_goal def_id ids in tclTHENLIST[ - split (ImplicitBindings [s_max]); - intro_then + Proofview.V82.of_tactic (split (ImplicitBindings [s_max])); + Proofview.V82.of_tactic (intro_then (fun id -> + Proofview.V82.tactic begin observe_tac (str "destruct_bounds_aux") - (tclTHENS (simplest_case (mkVar id)) + (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id))) [ - tclTHENLIST[intro_using h_id; - simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])); - default_full_auto]; + tclTHENLIST[Proofview.V82.of_tactic (intro_using h_id); + Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]))); + Proofview.V82.of_tactic default_full_auto]; tclTHENLIST[ observe_tac (str "clearing k ") (clear [id]); h_intros [k;h';def]; @@ -564,25 +565,25 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = (observe_tac (str "finishing") (tclORELSE - h_reflexivity + (Proofview.V82.of_tactic h_reflexivity) (observe_tac (str "calling prove_lt") (prove_lt hyple))))]) ] ] - )) + )end)) ] g | (_,v_bound)::l -> tclTHENLIST[ - simplest_elim (mkVar v_bound); + Proofview.V82.of_tactic (simplest_elim (mkVar v_bound)); h_clear false [v_bound]; - tclDO 2 intro; + tclDO 2 (Proofview.V82.of_tactic intro); onNthHypId 1 (fun p_hyp -> (onNthHypId 2 (fun p -> tclTHENLIST[ - simplest_elim - (mkApp(delayed_force max_constr, [| bound; mkVar p|])); - tclDO 3 intro; + Proofview.V82.of_tactic (simplest_elim + (mkApp(delayed_force max_constr, [| bound; mkVar p|]))); + tclDO 3 (Proofview.V82.of_tactic intro); onNLastHypsId 3 (fun lids -> match lids with [hle2;hle1;pmax] -> @@ -606,7 +607,7 @@ let terminate_app f_and_args expr_info continuation_tac infos = tclTHENLIST[ continuation_tac infos; observe_tac (str "first split") - (split (ImplicitBindings [infos.info])); + (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); observe_tac (str "destruct_bounds (1)") (destruct_bounds infos) ] else continuation_tac infos @@ -617,7 +618,7 @@ let terminate_others _ expr_info continuation_tac infos = tclTHENLIST[ continuation_tac infos; observe_tac (str "first split") - (split (ImplicitBindings [infos.info])); + (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); observe_tac (str "destruct_bounds") (destruct_bounds infos) ] else continuation_tac infos @@ -665,7 +666,7 @@ let mkDestructEq : (fun g2 -> change_in_concl None (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2); - simplest_case expr], to_revert + Proofview.V82.of_tactic (simplest_case expr)], to_revert let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = @@ -711,7 +712,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = then tclTHENLIST[ observe_tac (str "first split") - (split (ImplicitBindings [new_infos.info])); + (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); observe_tac (str "destruct_bounds (3)") (destruct_bounds new_infos) ] @@ -720,11 +721,11 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = ] with Not_found -> observe_tac (str "terminate_app_rec not found") (tclTHENS - (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args))) + (Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args)))) [ tclTHENLIST[ - intro_using rec_res_id; - intro; + Proofview.V82.of_tactic (intro_using rec_res_id); + Proofview.V82.of_tactic intro; onNthHypId 1 (fun v_bound -> (onNthHypId 2 @@ -741,7 +742,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = then tclTHENLIST[ observe_tac (str "first split") - (split (ImplicitBindings [new_infos.info])); + (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); observe_tac (str "destruct_bounds (2)") (destruct_bounds new_infos) ] @@ -836,12 +837,12 @@ let rec make_rewrite_list expr_info max = function let def_na,_,_ = destProd t in Nameops.out_name k_na,Nameops.out_name def_na in - general_rewrite_bindings false Locus.AllOccurrences + Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, ExplicitBindings[Loc.ghost,NamedHyp def, expr_info.f_constr;Loc.ghost,NamedHyp k, - (f_S max)]) false g) ) + (f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; tclTHENLIST[ (* x < S max proof *) @@ -863,12 +864,12 @@ let make_rewrite expr_info l hp max = Nameops.out_name k_na,Nameops.out_name def_na in observe_tac (str "general_rewrite_bindings") - (general_rewrite_bindings false Locus.AllOccurrences + (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, ExplicitBindings[Loc.ghost,NamedHyp def, expr_info.f_constr;Loc.ghost,NamedHyp k, - (f_S (f_S max))]) false) g) + (f_S (f_S max))]) false)) g) [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (tclTHENLIST[ @@ -879,7 +880,7 @@ let make_rewrite expr_info l hp max = (list_rewrite true (List.map (fun e -> mkVar e,true) expr_info.eqs)); - (observe_tac (str "h_reflexivity") h_reflexivity)])) + (observe_tac (str "h_reflexivity") (Proofview.V82.of_tactic h_reflexivity))])) ; tclTHENLIST[ (* x < S (S max) proof *) apply (delayed_force le_lt_SS); @@ -893,9 +894,9 @@ let rec compute_max rew_tac max l = | [] -> rew_tac max | (_,p,_)::l -> tclTHENLIST[ - simplest_elim - (mkApp(delayed_force max_constr, [| max; mkVar p|])); - tclDO 3 intro; + Proofview.V82.of_tactic (simplest_elim + (mkApp(delayed_force max_constr, [| max; mkVar p|]))); + tclDO 3 (Proofview.V82.of_tactic intro); onNLastHypsId 3 (fun lids -> match lids with | [hle2;hle1;pmax] -> compute_max rew_tac (mkVar pmax) l @@ -913,9 +914,9 @@ let rec destruct_hex expr_info acc l = end | (v,hex)::l -> tclTHENLIST[ - simplest_case (mkVar hex); + Proofview.V82.of_tactic (simplest_case (mkVar hex)); clear [hex]; - tclDO 2 intro; + tclDO 2 (Proofview.V82.of_tactic intro); onNthHypId 1 (fun hp -> onNthHypId 2 (fun p -> observe_tac @@ -928,7 +929,7 @@ let rec destruct_hex expr_info acc l = let rec intros_values_eq expr_info acc = tclORELSE( tclTHENLIST[ - tclDO 2 intro; + tclDO 2 (Proofview.V82.of_tactic intro); onNthHypId 1 (fun hex -> (onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc))) ) @@ -960,13 +961,13 @@ let equation_app_rec (f,args) expr_info continuation_tac info = if expr_info.is_final && expr_info.is_main_branch then tclTHENLIST - [ simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)); + [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}; observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info []) ] else tclTHENLIST[ - simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)); + Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}) ] end @@ -1049,22 +1050,22 @@ let termination_proof_header is_mes input_type ids args_id relation (tclTHENS (observe_tac (str "first assert") - (assert_tac + (Proofview.V82.of_tactic (assert_tac (Name wf_rec_arg) (mkApp (delayed_force acc_rel, [|input_type;relation;mkVar rec_arg_id|]) ) - ) + )) ) [ (* accesibility proof *) tclTHENS (observe_tac (str "second assert") - (assert_tac + (Proofview.V82.of_tactic (assert_tac (Name wf_thm) (mkApp (delayed_force well_founded,[|input_type;relation|])) - ) + )) ) [ (* interactive proof that the relation is well_founded *) @@ -1086,7 +1087,7 @@ let termination_proof_header is_mes input_type ids args_id relation ; observe_tac (str "h_fix") (h_fix (Some hrec) (nargs+1)); h_intros args_id; - h_intro wf_rec_arg; + Proofview.V82.of_tactic (h_intro wf_rec_arg); observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) ] ] @@ -1271,11 +1272,11 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ tclTHENSEQ [ h_generalize [lemma]; - h_intro hid; + Proofview.V82.of_tactic (h_intro hid); (fun g -> let ids = pf_ids_of_hyps g in tclTHEN - (Elim.h_decompose_and (mkVar hid)) + (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid))) (fun g -> let ids' = pf_ids_of_hyps g in lid := List.rev (List.subtract Id.equal ids' ids); @@ -1288,7 +1289,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (fun g -> match kind_of_term (pf_concl g) with | App(f,_) when eq_constr f (well_founded ()) -> - Auto.h_auto None [] (Some []) g + Proofview.V82.of_tactic (Auto.h_auto None [] (Some [])) g | _ -> incr h_num; (observe_tac (str "finishing using") @@ -1318,10 +1319,10 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ hook; if Indfun_common.is_strict_tcc () then - by (tclIDTAC) + by (Proofview.V82.tactic (tclIDTAC)) else begin - by ( + by (Proofview.V82.tactic begin fun g -> tclTHEN (decompose_and_tac) @@ -1330,17 +1331,17 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (List.map (fun c -> tclTHENSEQ - [intros; + [Proofview.V82.of_tactic intros; h_simplest_apply (interp_constr Evd.empty (Global.env()) c); - tclCOMPLETE Auto.default_auto + tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto) ] ) using_lemmas) ) tclIDTAC) - g) + g end) end; try - by tclIDTAC; (* raises UserError _ if the proof is complete *) + by (Proofview.V82.tactic tclIDTAC); (* raises UserError _ if the proof is complete *) with UserError _ -> defined () @@ -1363,9 +1364,9 @@ let com_terminate (Global, Proof Lemma) (Environ.named_context_val env) (compute_terminate_type nb_args fonctional_ref) hook; - by (observe_tac (str "starting_tac") tac_start); - by (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref - input_type relation rec_arg_num )) + by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)); + by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref + input_type relation rec_arg_num ))) in start_proof tclIDTAC tclIDTAC; try @@ -1391,8 +1392,8 @@ let start_equation (f:global_reference) (term_f:global_reference) h_intros x; unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]; observe_tac (str "simplest_case") - (simplest_case (mkApp (terminate_constr, - Array.of_list (List.map mkVar x)))); + (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr, + Array.of_list (List.map mkVar x))))); observe_tac (str "prove_eq") (cont_tactic x)] g;; let (com_eqn : int -> Id.t -> @@ -1410,7 +1411,7 @@ let (com_eqn : int -> Id.t -> (start_proof eq_name (Global, Proof Lemma) (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); by - (start_equation f_ref terminate_ref + (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> prove_eq (fun _ -> tclIDTAC) {nb_arg=nb_arg; @@ -1436,7 +1437,7 @@ let (com_eqn : int -> Id.t -> ih = Id.of_string "______"; } ) - ); + )); (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) (* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) Flags.silently (fun () -> Lemmas.save_named opacity) () ; diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index a17c62eba..78d1e1756 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -24,52 +24,52 @@ let out_arg = function | ArgArg x -> x TACTIC EXTEND PsatzZ -| [ "psatz_Z" int_or_var(i) ] -> [ Coq_micromega.psatz_Z (out_arg i) ] -| [ "psatz_Z" ] -> [ Coq_micromega.psatz_Z (-1) ] +| [ "psatz_Z" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Z (out_arg i)) ] +| [ "psatz_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Z (-1)) ] END TACTIC EXTEND ZOmicron -[ "xlia" ] -> [ Coq_micromega.xlia] +[ "xlia" ] -> [ Proofview.V82.tactic (Coq_micromega.xlia) ] END TACTIC EXTEND Nlia -[ "xnlia" ] -> [ Coq_micromega.xnlia] +[ "xnlia" ] -> [ Proofview.V82.tactic (Coq_micromega.xnlia) ] END TACTIC EXTEND Sos_Z -| [ "sos_Z" ] -> [ Coq_micromega.sos_Z] +| [ "sos_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.sos_Z) ] END TACTIC EXTEND Sos_Q -| [ "sos_Q" ] -> [ Coq_micromega.sos_Q] +| [ "sos_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.sos_Q) ] END TACTIC EXTEND Sos_R -| [ "sos_R" ] -> [ Coq_micromega.sos_R] +| [ "sos_R" ] -> [ Proofview.V82.tactic (Coq_micromega.sos_R) ] END TACTIC EXTEND Omicron -[ "psatzl_Z" ] -> [ Coq_micromega.psatzl_Z] +[ "psatzl_Z" ] -> [ Proofview.V82.tactic (Coq_micromega.psatzl_Z) ] END TACTIC EXTEND QOmicron -[ "psatzl_Q" ] -> [ Coq_micromega.psatzl_Q] +[ "psatzl_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.psatzl_Q) ] END TACTIC EXTEND ROmicron -[ "psatzl_R" ] -> [ Coq_micromega.psatzl_R] +[ "psatzl_R" ] -> [ Proofview.V82.tactic (Coq_micromega.psatzl_R) ] END TACTIC EXTEND RMicromega -| [ "psatz_R" int_or_var(i) ] -> [ Coq_micromega.psatz_R (out_arg i) ] -| [ "psatz_R" ] -> [ Coq_micromega.psatz_R (-1) ] +| [ "psatz_R" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_R (out_arg i)) ] +| [ "psatz_R" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_R (-1)) ] END TACTIC EXTEND QMicromega -| [ "psatz_Q" int_or_var(i) ] -> [ Coq_micromega.psatz_Q (out_arg i) ] -| [ "psatz_Q" ] -> [ Coq_micromega.psatz_Q (-1) ] +| [ "psatz_Q" int_or_var(i) ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Q (out_arg i)) ] +| [ "psatz_Q" ] -> [ Proofview.V82.tactic (Coq_micromega.psatz_Q (-1)) ] END diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 286fa6335..6fd8ab8e9 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -590,7 +590,7 @@ let nsatz_compute t = return_term lpol TACTIC EXTEND nsatz_compute -| [ "nsatz_compute" constr(lt) ] -> [ nsatz_compute lt ] +| [ "nsatz_compute" constr(lt) ] -> [ Proofview.V82.tactic (nsatz_compute lt) ] END diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4f96d7209..512e372bb 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -27,13 +27,16 @@ open Globnames open Nametab open Contradiction open Misctypes +open Proofview.Notations module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver (* Added by JCF, 09/03/98 *) -let elim_id id gl = simplest_elim (pf_global gl id) gl +let elim_id id = + Tacmach.New.pf_global id >>- fun c -> + simplest_elim c let resolve_id id gl = apply (pf_global gl id) gl let timing timer_name f arg = f arg @@ -76,13 +79,6 @@ let _ = optwrite = write old_style_flag } -let all_time = timing "Omega " -let solver_time = timing "Solver " -let exact_time = timing "Rewrites " -let elim_time = timing "Elim " -let simpl_time = timing "Simpl " -let generalize_time = timing "Generalize" - let new_identifier = let cpt = ref 0 in (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s) @@ -124,9 +120,9 @@ let mk_then = tclTHENLIST let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) -let generalize_tac t = generalize_time (generalize t) -let elim t = elim_time (simplest_elim t) -let exact t = exact_time (Tactics.refine t) +let generalize_tac t = generalize t +let elim t = simplest_elim t +let exact t = Tactics.refine t let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] let rev_assoc k = @@ -536,7 +532,7 @@ let focused_simpl path gl = let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in convert_concl_no_check newc DEFAULTcast gl -let focused_simpl path = simpl_time (focused_simpl path) +let focused_simpl path = focused_simpl path type oformula = | Oplus of oformula * oformula @@ -1015,12 +1011,12 @@ let replay_history tactic_normalisation = let aux1 = Id.of_string "auxiliary_1" in let aux2 = Id.of_string "auxiliary_2" in let izero = mk_integer zero in - let rec loop t = + let rec loop t : unit Proofview.tactic = match t with | HYP e :: l -> begin try - tclTHEN + Tacticals.New.tclTHEN (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation) (loop l) with Not_found -> loop l end @@ -1032,16 +1028,16 @@ let replay_history tactic_normalisation = let k = if b then negone else one in let p_initial = [P_APP 1;P_TYPE] in let tac= shuffle_mult_right p_initial e1.body k e2.body in - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA17, [| val_of eq1; val_of eq2; mk_integer k; mkVar id1; mkVar id2 |])]); - (mk_then tac); + Proofview.V82.tactic (mk_then tac); (intros_using [aux]); - (resolve_id aux); + Proofview.V82.tactic (resolve_id aux); reflexivity ] | CONTRADICTION (e1,e2) :: l -> @@ -1055,13 +1051,13 @@ let replay_history tactic_normalisation = Lazy.force coq_Gt; Lazy.force coq_Gt |]) in - tclTHENS - (tclTHENLIST [ - (unfold sp_Zle); - (simpl_in_concl); + Tacticals.New.tclTHENS + (Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zle); + Proofview.V82.tactic (simpl_in_concl); intro; (absurd not_sup_sup) ]) - [ assumption ; reflexivity ] + [ Proofview.V82.tactic assumption ; reflexivity ] in let theorem = mkApp (Lazy.force coq_OMEGA2, [| @@ -1069,7 +1065,7 @@ let replay_history tactic_normalisation = mkVar (hyp_of_tag e1.id); mkVar (hyp_of_tag e2.id) |]) in - tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) (solve_le) + Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (generalize_tac [theorem]) (mk_then tac))) (solve_le) | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> let id = hyp_of_tag e1.id in let eq1 = val_of(decompile e1) @@ -1079,34 +1075,34 @@ let replay_history tactic_normalisation = let rhs = mk_plus (mk_times eq2 kk) dd in let state_eg = mk_eq eq1 rhs in let tac = scalar_norm_add [P_APP 3] e2.body in - tclTHENS - (cut state_eg) - [ tclTHENS - (tclTHENLIST [ + Tacticals.New.tclTHENS + (Proofview.V82.tactic (cut state_eg)) + [ Tacticals.New.tclTHENS + (Tacticals.New.tclTHENLIST [ (intros_using [aux]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA1, [| eq1; rhs; mkVar aux; mkVar id |])]); - (clear [aux;id]); + Proofview.V82.tactic (clear [aux;id]); (intros_using [id]); - (cut (mk_gt kk dd)) ]) - [ tclTHENS - (cut (mk_gt kk izero)) - [ tclTHENLIST [ + Proofview.V82.tactic (cut (mk_gt kk dd)) ]) + [ Tacticals.New.tclTHENS + (Proofview.V82.tactic (cut (mk_gt kk izero))) + [ Tacticals.New.tclTHENLIST [ (intros_using [aux1; aux2]); - (generalize_tac + (Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_Zmult_le_approx, - [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]); - (clear [aux1;aux2;id]); + [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])])); + Proofview.V82.tactic (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; - tclTHENLIST [ - (unfold sp_Zgt); - (simpl_in_concl); + Tacticals.New.tclTHENLIST [ + (Proofview.V82.tactic (unfold sp_Zgt)); + (Proofview.V82.tactic simpl_in_concl); reflexivity ] ]; - tclTHENLIST [ (unfold sp_Zgt); simpl_in_concl; reflexivity ] + Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (unfold sp_Zgt); Proofview.V82.tactic simpl_in_concl; reflexivity ] ]; - tclTHEN (mk_then tac) reflexivity ] + Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] | NOT_EXACT_DIVIDE (e1,k) :: l -> let c = floor_div e1.constant k in @@ -1117,27 +1113,27 @@ let replay_history tactic_normalisation = let kk = mk_integer k and dd = mk_integer d in let tac = scalar_norm_add [P_APP 2] e2.body in - tclTHENS - (cut (mk_gt dd izero)) - [ tclTHENS (cut (mk_gt kk dd)) - [tclTHENLIST [ + Tacticals.New.tclTHENS + (Proofview.V82.tactic (cut (mk_gt dd izero))) + [ Tacticals.New.tclTHENS (Proofview.V82.tactic (cut (mk_gt kk dd))) + [Tacticals.New.tclTHENLIST [ (intros_using [aux2;aux1]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA4, [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); - (clear [aux1;aux2]); - (unfold sp_not); + Proofview.V82.tactic (clear [aux1;aux2]); + Proofview.V82.tactic (unfold sp_not); (intros_using [aux]); - (resolve_id aux); - (mk_then tac); - assumption ] ; - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; + Proofview.V82.tactic (resolve_id aux); + Proofview.V82.tactic (mk_then tac); + Proofview.V82.tactic assumption ] ; + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zgt); + Proofview.V82.tactic simpl_in_concl; reflexivity ] ]; - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zgt); + Proofview.V82.tactic simpl_in_concl; reflexivity ] ] | EXACT_DIVIDE (e1,k) :: l -> let id = hyp_of_tag e1.id in @@ -1148,36 +1144,36 @@ let replay_history tactic_normalisation = let state_eq = mk_eq eq1 (mk_times eq2 kk) in if e1.kind == DISE then let tac = scalar_norm [P_APP 3] e2.body in - tclTHENS - (cut state_eq) - [tclTHENLIST [ + Tacticals.New.tclTHENS + (Proofview.V82.tactic (cut state_eq)) + [Tacticals.New.tclTHENLIST [ (intros_using [aux1]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA18, [| eq1;eq2;kk;mkVar aux1; mkVar id |])]); - (clear [aux1;id]); + Proofview.V82.tactic (clear [aux1;id]); (intros_using [id]); (loop l) ]; - tclTHEN (mk_then tac) reflexivity ] + Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] else let tac = scalar_norm [P_APP 3] e2.body in - tclTHENS (cut state_eq) + Tacticals.New.tclTHENS (Proofview.V82.tactic (cut state_eq)) [ - tclTHENS - (cut (mk_gt kk izero)) - [tclTHENLIST [ + Tacticals.New.tclTHENS + (Proofview.V82.tactic (cut (mk_gt kk izero))) + [Tacticals.New.tclTHENLIST [ (intros_using [aux2;aux1]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA3, [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]); - (clear [aux1;aux2;id]); + Proofview.V82.tactic (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zgt); + Proofview.V82.tactic simpl_in_concl; reflexivity ] ]; - tclTHEN (mk_then tac) reflexivity ] + Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] | (MERGE_EQ(e3,e1,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1190,16 +1186,16 @@ let replay_history tactic_normalisation = (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: scalar_norm [P_APP 3] e1.body in - tclTHENS - (cut (mk_eq eq1 (mk_inv eq2))) - [tclTHENLIST [ + Tacticals.New.tclTHENS + (Proofview.V82.tactic (cut (mk_eq eq1 (mk_inv eq2)))) + [Tacticals.New.tclTHENLIST [ (intros_using [aux]); - (generalize_tac [mkApp (Lazy.force coq_OMEGA8, + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); - (clear [id1;id2;aux]); + Proofview.V82.tactic (clear [id1;id2;aux]); (intros_using [id]); (loop l) ]; - tclTHEN (mk_then tac) reflexivity] + Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity] | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l -> let id = new_identifier () @@ -1223,21 +1219,21 @@ let replay_history tactic_normalisation = [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) :: shuffle_mult_right p_initial orig.body m ({c= negone;v= v}::def.body) in - tclTHENS - (cut theorem) - [tclTHENLIST [ + Tacticals.New.tclTHENS + (Proofview.V82.tactic (cut theorem)) + [Tacticals.New.tclTHENLIST [ (intros_using [aux]); (elim_id aux); - (clear [aux]); + Proofview.V82.tactic (clear [aux]); (intros_using [vid; aux]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA9, [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); - (mk_then tac); - (clear [aux]); + Proofview.V82.tactic (mk_then tac); + Proofview.V82.tactic (clear [aux]); (intros_using [id]); (loop l) ]; - tclTHEN (exists_tac eq1) reflexivity ] + Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in @@ -1246,10 +1242,10 @@ let replay_history tactic_normalisation = let tac1 = norm_add [P_APP 2;P_TYPE] e.body in let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in let eq = val_of(decompile e) in - tclTHENS + Tacticals.New.tclTHENS (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))) - [tclTHENLIST [ (mk_then tac1); (intros_using [id1]); (loop act1) ]; - tclTHENLIST [ (mk_then tac2); (intros_using [id2]); (loop act2) ]] + [Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac1); (intros_using [id1]); (loop act1) ]; + Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac2); (intros_using [id2]); (loop act2) ]] | SUM(e3,(k1,e1),(k2,e2)) :: l -> let id = new_identifier () in tag_hypothesis id e3; @@ -1268,10 +1264,10 @@ let replay_history tactic_normalisation = let p_initial = if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in let tac = shuffle_mult_right p_initial e1.body k2 e2.body in - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); - (mk_then tac); + Proofview.V82.tactic (mk_then tac); (intros_using [id]); (loop l) ] @@ -1280,43 +1276,43 @@ let replay_history tactic_normalisation = and kk2 = mk_integer k2 in let p_initial = [P_APP 2;P_TYPE] in let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in - tclTHENS (cut (mk_gt kk1 izero)) - [tclTHENS - (cut (mk_gt kk2 izero)) - [tclTHENLIST [ + Tacticals.New.tclTHENS (Proofview.V82.tactic (cut (mk_gt kk1 izero))) + [Tacticals.New.tclTHENS + (Proofview.V82.tactic (cut (mk_gt kk2 izero))) + [Tacticals.New.tclTHENLIST [ (intros_using [aux2;aux1]); - (generalize_tac + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA7, [| eq1;eq2;kk1;kk2; mkVar aux1;mkVar aux2; mkVar id1;mkVar id2 |])]); - (clear [aux1;aux2]); - (mk_then tac); + Proofview.V82.tactic (clear [aux1;aux2]); + Proofview.V82.tactic (mk_then tac); (intros_using [id]); (loop l) ]; - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zgt); + Proofview.V82.tactic simpl_in_concl; reflexivity ] ]; - tclTHENLIST [ - (unfold sp_Zgt); - simpl_in_concl; + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (unfold sp_Zgt); + Proofview.V82.tactic simpl_in_concl; reflexivity ] ] | CONSTANT_NOT_NUL(e,k) :: l -> - tclTHEN (generalize_tac [mkVar (hyp_of_tag e)]) Equality.discrConcl + Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl | CONSTANT_NUL(e) :: l -> - tclTHEN (resolve_id (hyp_of_tag e)) reflexivity + Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity | CONSTANT_NEG(e,k) :: l -> - tclTHENLIST [ - (generalize_tac [mkVar (hyp_of_tag e)]); - (unfold sp_Zle); - simpl_in_concl; - (unfold sp_not); + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]); + Proofview.V82.tactic (unfold sp_Zle); + Proofview.V82.tactic simpl_in_concl; + Proofview.V82.tactic (unfold sp_not); (intros_using [aux]); - (resolve_id aux); + Proofview.V82.tactic (resolve_id aux); reflexivity ] - | _ -> tclIDTAC + | _ -> Proofview.tclUNIT () in loop @@ -1336,7 +1332,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) = in if not (List.is_empty tac) then let id' = new_identifier () in - ((id',(tclTHENLIST [ (shift_left); (mk_then tac); (intros_using [id']) ])) + ((id',(Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (shift_left); Proofview.V82.tactic (mk_then tac); (intros_using [id']) ])) :: tactic, compile id' flag t' :: defs) else @@ -1377,12 +1373,18 @@ let destructure_omega gl tac_def (id,c) = let reintroduce id = (* [id] cannot be cleared if dependent: protect it by a try *) - tclTHEN (tclTRY (clear [id])) (intro_using id) + Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTRY (clear [id]))) (intro_using id) + + +open Proofview.Notations -let coq_omega gl = +let coq_omega = + Proofview.tclUNIT () >= fun () -> (* delay for the effects in [clear_tables] *) clear_tables (); + Tacmach.New.pf_hyps_types >>- fun hyps_types -> + Tacmach.New.of_old destructure_omega >>- fun destructure_omega -> let tactic_normalisation, system = - List.fold_left (destructure_omega gl) ([],[]) (pf_hyps_types gl) in + List.fold_left destructure_omega ([],[]) hyps_types in let prelude,sys = List.fold_left (fun (tac,sys) (t,(v,th,b)) -> @@ -1390,78 +1392,79 @@ let coq_omega gl = let id = new_identifier () in let i = new_id () in tag_hypothesis id i; - (tclTHENLIST [ + (Tacticals.New.tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); (intros_using [v; id]); (elim_id id); - (clear [id]); + Proofview.V82.tactic (clear [id]); (intros_using [th;id]); tac ]), {kind = INEQ; body = [{v=intern_id v; c=one}]; constant = zero; id = i} :: sys else - (tclTHENLIST [ + (Tacticals.New.tclTHENLIST [ (simplest_elim (applist (Lazy.force coq_new_var, [t]))); (intros_using [v;th]); tac ]), sys) - (tclIDTAC,[]) (dump_tables ()) + (Proofview.tclUNIT (),[]) (dump_tables ()) in let system = system @ sys in if !display_system_flag then display_system display_var system; if !old_style_flag then begin try let _ = simplify (new_id,new_var_num,display_var) false system in - tclIDTAC gl + Proofview.tclUNIT () with UNSOLVABLE -> let _,path = depend [] [] (history ()) in if !display_action_flag then display_action display_var path; - (tclTHEN prelude (replay_history tactic_normalisation path)) gl + (Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path)) end else begin try let path = simplify_strong (new_id,new_var_num,display_var) system in if !display_action_flag then display_action display_var path; - (tclTHEN prelude (replay_history tactic_normalisation path)) gl - with NO_CONTRADICTION -> error "Omega can't solve this system" + Tacticals.New.(tclTHEN prelude (replay_history tactic_normalisation path)) + with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system")) end -let coq_omega = solver_time coq_omega +let coq_omega = coq_omega -let nat_inject gl = - let rec explore p t = +let nat_inject = + Tacmach.New.pf_apply Reductionops.is_conv >>- fun is_conv -> + let rec explore p t : unit Proofview.tactic = try match destructurate_term t with | Kapp(Plus,[t1;t2]) -> - tclTHENLIST [ - (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_plus),[t1;t2])); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ] | Kapp(Mult,[t1;t2]) -> - tclTHENLIST [ - (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_mult),[t1;t2])); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ] | Kapp(Minus,[t1;t2]) -> let id = new_identifier () in - tclTHENS - (tclTHEN + Tacticals.New.tclTHENS + (Tacticals.New.tclTHEN (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1]))) (intros_using [id])) [ - tclTHENLIST [ - (clever_rewrite_gen p + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (clever_rewrite_gen p (mk_minus (mk_inj t1) (mk_inj t2)) ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id])); (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]); (explore (P_APP 1 :: p) t1); (explore (P_APP 2 :: p) t2) ]; - (tclTHEN - (clever_rewrite_gen p (mk_integer zero) - ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id])) + (Tacticals.New.tclTHEN + (Proofview.V82.tactic (clever_rewrite_gen p (mk_integer zero) + ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))) (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])])) ] | Kapp(S,[t']) -> @@ -1472,37 +1475,37 @@ let nat_inject gl = | _ -> false with e when catchable_exception e -> false in - let rec loop p t = + let rec loop p t : unit Proofview.tactic = try match destructurate_term t with Kapp(S,[t]) -> - (tclTHEN - (clever_rewrite_gen p + (Tacticals.New.tclTHEN + (Proofview.V82.tactic (clever_rewrite_gen p (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |])) - ((Lazy.force coq_inj_S),[t])) + ((Lazy.force coq_inj_S),[t]))) (loop (P_APP 1 :: p) t)) | _ -> explore p t with e when catchable_exception e -> explore p t in - if is_number t' then focused_simpl p else loop p t + if is_number t' then Proofview.V82.tactic (focused_simpl p) else loop p t | Kapp(Pred,[t]) -> let t_minus_one = mkApp (Lazy.force coq_minus, [| t; mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in - tclTHEN - (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one - ((Lazy.force coq_pred_of_minus),[t])) + Tacticals.New.tclTHEN + (Proofview.V82.tactic (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one + ((Lazy.force coq_pred_of_minus),[t]))) (explore p t_minus_one) - | Kapp(O,[]) -> focused_simpl p - | _ -> tclIDTAC - with e when catchable_exception e -> tclIDTAC + | Kapp(O,[]) -> Proofview.V82.tactic (focused_simpl p) + | _ -> Proofview.tclUNIT () + with e when catchable_exception e -> Proofview.tclUNIT () and loop = function - | [] -> tclIDTAC + | [] -> Proofview.tclUNIT () | (i,t)::lit -> begin try match destructurate_prop t with Kapp(Le,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1510,8 +1513,8 @@ let nat_inject gl = (loop lit) ] | Kapp(Lt,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1519,8 +1522,8 @@ let nat_inject gl = (loop lit) ] | Kapp(Ge,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1528,8 +1531,8 @@ let nat_inject gl = (loop lit) ] | Kapp(Gt,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1537,8 +1540,8 @@ let nat_inject gl = (loop lit) ] | Kapp(Neq,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 1; P_TYPE] t1); (explore [P_APP 2; P_TYPE] t2); @@ -1546,9 +1549,9 @@ let nat_inject gl = (loop lit) ] | Kapp(Eq,[typ;t1;t2]) -> - if pf_conv_x gl typ (Lazy.force coq_nat) then - tclTHENLIST [ - (generalize_tac + if is_conv typ (Lazy.force coq_nat) then + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]); (explore [P_APP 2; P_TYPE] t1); (explore [P_APP 3; P_TYPE] t2); @@ -1559,7 +1562,8 @@ let nat_inject gl = | _ -> loop lit with e when catchable_exception e -> loop lit end in - loop (List.rev (pf_hyps_types gl)) gl + Tacmach.New.pf_hyps_types >>- fun hyps_types -> + loop (List.rev hyps_types) let dec_binop = function | Zne -> coq_dec_Zne @@ -1627,50 +1631,51 @@ let rec decidability gl t = let onClearedName id tac = (* We cannot ensure that hyps can be cleared (because of dependencies), *) (* so renaming may be necessary *) - tclTHEN - (tclTRY (clear [id])) - (fun gl -> - let id = fresh_id [] id gl in - tclTHEN (introduction id) (tac id) gl) + Tacticals.New.tclTHEN + (Proofview.V82.tactic (tclTRY (clear [id]))) + (Tacmach.New.of_old (fresh_id [] id) >>- fun id -> + Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id)) let onClearedName2 id tac = - tclTHEN - (tclTRY (clear [id])) - (fun gl -> - let id1 = fresh_id [] (add_suffix id "_left") gl in - let id2 = fresh_id [] (add_suffix id "_right") gl in - tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] gl) - -let destructure_hyps gl = + Tacticals.New.tclTHEN + (Proofview.V82.tactic (tclTRY (clear [id]))) + (Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) >>- fun id1 -> + Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) >>- fun id2 -> + Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (introduction id1); Proofview.V82.tactic (introduction id2); tac id1 id2 ]) + +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 - | [] -> (tclTHEN nat_inject coq_omega) + | [] -> (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]) -> - (tclTHENS + (Tacticals.New.tclTHENS (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]) -> - tclTHEN + Tacticals.New.tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> loop ((i1,None,t1)::(i2,None,t2)::lit))) | Kapp(Iff,[t1;t2]) -> - tclTHEN + Tacticals.New.tclTHEN (elim_id i) (onClearedName2 i (fun i1 i2 -> loop ((i1,None,mkArrow t1 t2)::(i2,None,mkArrow t2 t1)::lit))) | Kimp(t1,t2) -> (* t1 and t2 might be in Type rather than Prop. For t1, the decidability check will ensure being Prop. *) - if is_Prop (pf_type_of gl t2) + if is_Prop (type_of t2) then - let d1 = decidability gl t1 in - tclTHENLIST [ - (generalize_tac [mkApp (Lazy.force coq_imp_simp, + let d1 = decidability t1 in + Tacticals.New.tclTHENLIST [ + Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> (loop ((i,None,mk_or (mk_not t1) t2)::lit)))) @@ -1680,26 +1685,26 @@ let destructure_hyps gl = | Kapp(Not,[t]) -> begin match destructurate_prop t with Kapp(Or,[t1;t2]) -> - tclTHENLIST [ - (generalize_tac + 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 gl t1 in - tclTHENLIST [ - (generalize_tac + 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 gl t1 in - let d2 = decidability gl t2 in - tclTHENLIST [ - (generalize_tac + 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 -> @@ -1710,42 +1715,42 @@ let destructure_hyps gl = | 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 gl t1 in - tclTHENLIST [ - (generalize_tac + 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 gl t in - tclTHENLIST [ - (generalize_tac + 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 - tclTHENLIST [ - (generalize_tac + 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 gl typ) with + match destructurate_type (pf_nf typ) with | Kapp(Nat,_) -> - tclTHENLIST [ + Tacticals.New.tclTHENLIST [ (simplest_elim (mkApp (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))); (onClearedName i (fun _ -> loop lit)) ] | Kapp(Z,_) -> - tclTHENLIST [ + Tacticals.New.tclTHENLIST [ (simplest_elim (mkApp (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))); @@ -1753,18 +1758,18 @@ let destructure_hyps gl = ] | _ -> loop lit end else begin - match destructurate_type (pf_nf gl typ) with + match destructurate_type (pf_nf typ) with | Kapp(Nat,_) -> - (tclTHEN - (convert_hyp_no_check + (Tacticals.New.tclTHEN + (Proofview.V82.tactic (convert_hyp_no_check (i,body, - (mkApp (Lazy.force coq_neq, [| t1;t2|])))) + (mkApp (Lazy.force coq_neq, [| t1;t2|]))))) (loop lit)) | Kapp(Z,_) -> - (tclTHEN - (convert_hyp_no_check + (Tacticals.New.tclTHEN + (Proofview.V82.tactic (convert_hyp_no_check (i,body, - (mkApp (Lazy.force coq_Zne, [| t1;t2|])))) + (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))) (loop lit)) | _ -> loop lit end @@ -1776,37 +1781,37 @@ let destructure_hyps gl = | e when catchable_exception e -> loop lit end in - loop (pf_hyps gl) gl + Goal.hyps >>- fun hyps -> + loop (Environ.named_context_of_val hyps) -let destructure_goal gl = - let concl = pf_concl gl in +let destructure_goal = + Goal.concl >>- fun concl -> + Tacmach.New.of_old decidability >>- fun decidability -> let rec loop t = match destructurate_prop t with | Kapp(Not,[t]) -> - (tclTHEN - (tclTHEN (unfold sp_not) intro) + (Tacticals.New.tclTHEN + (Tacticals.New.tclTHEN (Proofview.V82.tactic (unfold sp_not)) intro) destructure_hyps) - | Kimp(a,b) -> (tclTHEN intro (loop b)) + | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b)) | Kapp(False,[]) -> destructure_hyps | _ -> let goal_tac = try - let dec = decidability gl t in - tclTHEN - (Tactics.refine - (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))) + 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 -> Tactics.elim_type (build_coq_False ()) + with Undecidable -> Proofview.V82.tactic (Tactics.elim_type (build_coq_False ())) in - tclTHEN goal_tac destructure_hyps + Tacticals.New.tclTHEN goal_tac destructure_hyps in - (loop concl) gl + (loop concl) -let destructure_goal = all_time (destructure_goal) +let destructure_goal = destructure_goal -let omega_solver gl = +let omega_solver = + Proofview.tclUNIT () >= fun () -> (* delay for [check_required_library] *) Coqlib.check_required_library ["Coq";"omega";"Omega"]; - let result = destructure_goal gl in - (* if !display_time_flag then begin text_time (); - flush Pervasives.stdout end; *) - result + destructure_goal diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 082eac422..0aad364c1 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -28,9 +28,9 @@ let omega_tactic l = | s -> Errors.error ("No Omega knowledge base for type "^s)) (Util.List.sort_uniquize String.compare l) in - tclTHEN - (tclREPEAT (tclPROGRESS (tclTHENLIST tacs))) - omega_solver + Tacticals.New.tclTHEN + (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) + (omega_solver) TACTIC EXTEND omega diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 92b27c3e8..0cf4d3bb4 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -109,6 +109,7 @@ open Pattern open Patternops open Matching open Tacmach +open Proofview.Notations (*i*) (*s First, we need to access some Coq constants @@ -219,14 +220,16 @@ let compute_rhs bodyi index_of_f = (*s Now the function [compute_ivs] itself *) -let compute_ivs gl f cs = +let compute_ivs f cs = let cst = try destConst f with DestKO -> i_can't_do_that () in let body = Environ.constant_value (Global.env()) cst in match decomp_term body with | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> let (args3, body3) = decompose_lam body2 in let nargs3 = List.length args3 in - begin match decomp_term body3 with + Tacmach.New.pf_apply Reductionops.is_conv >- fun is_conv -> + Goal.return + begin match decomp_term body3 with | Case(_,p,c,lci) -> (*

Case c of c1 ... cn end *) let n_lhs_rhs = ref [] and v_lhs = ref (None : constr option) @@ -245,8 +248,7 @@ let compute_ivs gl f cs = (* Then we test if the RHS is the RHS for variables *) else begin match decompose_app bodyi with | vmf, [_; _; a3; a4 ] - when isRel a3 && isRel a4 && - pf_conv_x gl vmf + when isRel a3 && isRel a4 && is_conv vmf (Lazy.force coq_varmap_find)-> v_lhs := Some (compute_lhs (snd (List.hd args3)) @@ -389,7 +391,10 @@ module Constrhash = Hashtbl.Make [ivs : inversion_scheme]\\ [lc: constr list]\\ [gl: goal sigma]\\ *) -let quote_terms ivs lc gl = +let quote_terms ivs lc = + (* spiwack: [Goal.return () >- fun () -> … ] suspends the effects in + [Coqlib.check_required_library]. *) + Goal.return () >- fun () -> Coqlib.check_required_library ["Coq";"quote";"Quote"]; let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) @@ -436,36 +441,41 @@ let quote_terms ivs lc gl = auxl ivs.normal_lhs_rhs in let lp = List.map aux lc in - (lp, (btree_of_array (Array.of_list (List.rev !varlist)) - ivs.return_type )) + Goal.return begin + (lp, (btree_of_array (Array.of_list (List.rev !varlist)) + ivs.return_type )) + end (*s actually we could "quote" a list of terms instead of a single term. Ring for example needs that, but Ring doesn't use Quote yet. *) -let quote f lid gl = - let f = pf_global gl f in - let cl = List.map (pf_global gl) lid in - let ivs = compute_ivs gl f cl in - let (p, vm) = match quote_terms ivs [(pf_concl gl)] gl with +let quote f lid = + Tacmach.New.pf_global f >>- fun f -> + Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl -> + compute_ivs f cl >>- fun ivs -> + Goal.concl >>- fun concl -> + 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 -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl - | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl - -let gen_quote cont c f lid gl = - let f = pf_global gl f in - let cl = List.map (pf_global gl) lid in - let ivs = compute_ivs gl f cl in - let (p, vm) = match quote_terms ivs [c] gl with + | None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast) + | Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast) + +let gen_quote cont c f lid = + Tacmach.New.pf_global f >>- fun f -> + Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl -> + compute_ivs f cl >>- fun ivs -> + quote_terms ivs [c] >>- fun quoted_terms -> + let (p, vm) = match quoted_terms with | [p], vm -> (p,vm) | _ -> assert false in match ivs.variable_lhs with - | None -> cont (mkApp (f, [| p |])) gl - | Some _ -> cont (mkApp (f, [| vm; p |])) gl + | None -> cont (mkApp (f, [| p |])) + | Some _ -> cont (mkApp (f, [| vm; p |])) (*i diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 055546c8b..efe11b99c 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -21,14 +21,14 @@ let romega_tactic l = | s -> Errors.error ("No ROmega knowledge base for type "^s)) (Util.List.sort_uniquize String.compare l) in - tclTHEN - (tclREPEAT (tclPROGRESS (tclTHENLIST tacs))) - (tclTHEN + Tacticals.New.tclTHEN + (Tacticals.New.tclREPEAT (Proofview.tclPROGRESS (Tacticals.New.tclTHENLIST tacs))) + (Tacticals.New.tclTHEN (* because of the contradiction process in (r)omega, we'd better leave as little as possible in the conclusion, for an easier decidability argument. *) - Tactics.intros - total_reflexive_omega_tactic) + (Tactics.intros) + (Proofview.V82.tactic total_reflexive_omega_tactic)) TACTIC EXTEND romega diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index af4e33964..7d0b7a1bc 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -9,6 +9,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) TACTIC EXTEND rtauto - [ "rtauto" ] -> [ Refl_tauto.rtauto_tac ] + [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ] END diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 74ad34eff..907cd474c 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -97,9 +97,9 @@ let protect_tac_in map id = TACTIC EXTEND protect_fv [ "protect_fv" string(map) "in" ident(id) ] -> - [ protect_tac_in map id ] + [ Proofview.V82.tactic (protect_tac_in map id) ] | [ "protect_fv" string(map) ] -> - [ protect_tac map ] + [ Proofview.V82.tactic (protect_tac map) ] END;; (****************************************************************************) @@ -112,7 +112,7 @@ let closed_term t l = TACTIC EXTEND closed_term [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> - [ closed_term t l ] + [ Proofview.V82.tactic (closed_term t l) ] END ;; @@ -192,7 +192,7 @@ let exec_tactic env n f args = Tacexp(TacFun(List.map(fun id -> Some id) lid, Tacintern.glob_tactic(tacticIn get_res))) in let _ = - Tacinterp.eval_tactic(ltac_call f (args@[getter])) (dummy_goal env) in + Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) (dummy_goal env) in !res let constr_of v = match Value.to_constr v with @@ -795,15 +795,17 @@ let ltac_ring_structure e = [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] -let ring_lookup (f:glob_tactic_expr) lH rl t gl = - let env = pf_env gl in - let sigma = project gl in +open Proofview.Notations + +let ring_lookup (f:glob_tactic_expr) lH rl t = + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> 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]) gl + ltac_apply f (ring@[lH;rl]) TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> @@ -1116,15 +1118,15 @@ let ltac_field_structure e = [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac] -let field_lookup (f:glob_tactic_expr) lH rl t gl = - let env = pf_env gl in - let sigma = project gl in +let field_lookup (f:glob_tactic_expr) lH rl t = + Goal.env >>- fun env -> + Goal.defs >>- fun sigma -> 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]) gl + ltac_apply f (field@[lH;rl]) TACTIC EXTEND field_lookup -- cgit v1.2.3