From bda7852cb0896727389935f420eec0e8e3315cf7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Jun 2014 15:04:06 +0200 Subject: Passing some tactics to the new monad type. --- plugins/cc/cctac.ml | 19 ++++++---------- plugins/decl_mode/decl_proof_instr.ml | 6 ++--- plugins/fourier/fourierR.ml | 22 +++++++++---------- plugins/funind/invfun.ml | 4 ++-- plugins/rtauto/refl_tauto.ml | 2 +- tactics/auto.ml | 13 ++++++----- tactics/eauto.ml4 | 2 +- tactics/tactics.ml | 41 +++++++++++++++++++---------------- tactics/tactics.mli | 6 ++--- 9 files changed, 56 insertions(+), 59 deletions(-) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index b85b7995c..2de0fe717 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -249,28 +249,23 @@ let app_global f args k = let new_app_global f args k = Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) -let new_exact_check c = Proofview.V82.tactic (exact_check c) let new_refine c = Proofview.V82.tactic (refine c) let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of t = Tacmach.New.pf_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with - Ax c -> new_exact_check c + Ax c -> exact_check c | SymAx c -> - 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 - (app_global _sym_eq [|typ;r;l;c|] exact_check) gls - end + let typ = (* Termops.refresh_universes *) type_of l in + new_app_global _sym_eq [|typ;r;l;c|] exact_check | Refl t -> - Proofview.V82.tactic begin fun gls -> let lr = constr_of_term t in - let typ = (* Termops.refresh_universes *) (pf_type_of gls lr) in - (app_global _refl_equal [|typ;constr_of_term t|] exact_check) gls - end + let typ = (* Termops.refresh_universes *) type_of lr in + new_app_global _refl_equal [|typ;constr_of_term t|] exact_check | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and @@ -339,7 +334,7 @@ let refute_tac c t1 t2 p = let refine_exact_check c gl = let evm, _ = pf_apply e_type_of gl c in - Tacticals.tclTHEN (Refiner.tclEVARS evm) (exact_check c) gl + Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = Proofview.Goal.enter begin fun gl -> diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 97989e268..c230a9896 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -437,7 +437,7 @@ let thus_tac c ctyp submetas gls = with Not_found -> error "I could not relate this statement to the thesis." in if List.is_empty list then - exact_check proof gls + Proofview.V82.of_tactic (exact_check proof) gls else let refiner = concl_refiner list proof gls in Tactics.refine refiner gls @@ -534,14 +534,14 @@ let instr_rew _thus rew_side cut gls0 = tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq)) [tclTHEN tcl_erase_info (tclTHENS (Proofview.V82.of_tactic (transitivity lhs)) - [just_tac;exact_check (mkVar last_id)]); + [just_tac;Proofview.V82.of_tactic (exact_check (mkVar last_id))]); thus_tac new_eq] gls0 | Rhs -> let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq)) [tclTHEN tcl_erase_info (tclTHENS (Proofview.V82.of_tactic (transitivity rhs)) - [exact_check (mkVar last_id);just_tac]); + [Proofview.V82.of_tactic (exact_check (mkVar last_id));just_tac]); thus_tac new_eq] gls0 diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index d34d50364..1f6ece602 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -422,18 +422,16 @@ let my_cut c gl= let exact = exact_check;; -let tac_use h = match h.htype with - "Rlt" -> exact h.hname - |"Rle" -> exact h.hname - |"Rgt" -> (tclTHEN (apply (get coq_Rfourier_gt_to_lt)) - (exact h.hname)) - |"Rge" -> (tclTHEN (apply (get coq_Rfourier_ge_to_le)) - (exact h.hname)) - |"eqTLR" -> (tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) - (exact h.hname)) - |"eqTRL" -> (tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) - (exact h.hname)) - |_->assert false +let tac_use h = + let tac = Proofview.V82.of_tactic (exact h.hname) in + match h.htype with + "Rlt" -> tac + |"Rle" -> tac + |"Rgt" -> (tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac) + |"Rge" -> (tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac) + |"eqTLR" -> (tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac) + |"eqTRL" -> (tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac) + |_->assert false ;; (* diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 2c153becf..20304b529 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -427,7 +427,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (* replacing [res] with its value *) observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); (* Conclusion *) - observe_tac "exact" (fun g -> exact_check (app_constructor g) g) + observe_tac "exact" (fun g -> Proofview.V82.of_tactic (exact_check (app_constructor g)) g) ] ) g @@ -478,7 +478,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem observe_tac "principle" (Proofview.V82.of_tactic (assert_by (Name principle_id) princ_type - (Proofview.V82.tactic (exact_check f_principle)))); + (exact_check f_principle))); observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.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; diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index bff574a06..6b4be4e2a 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -313,7 +313,7 @@ let rtauto_tac gls= let tac_start_time = System.get_time () in let result= if !check then - Tactics.exact_check term gls + Proofview.V82.of_tactic (Tactics.exact_check term) gls else Tactics.exact_no_check term gls in let tac_end_time = System.get_time () in diff --git a/tactics/auto.ml b/tactics/auto.ml index bcf5e2947..b9c52144e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1172,11 +1172,12 @@ let exact poly (c,clenv) = else let ctx = Evd.evar_universe_context clenv.evd in ctx, c - in - fun gl -> - tclTHEN (Refiner.tclEVARS (Evd.merge_universe_context (project gl) ctx)) - (exact_check c') gl - + in + Proofview.Goal.raw_enter begin fun gl -> + let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in + Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma) (exact_check c') + end + (* Util *) let expand_constructor_hints env sigma lems = @@ -1465,7 +1466,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) match t with | Res_pf (c,cl) -> Proofview.V82.tactic (unify_resolve_gen poly flags (c,cl)) | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf") - | Give_exact (c, cl) -> Proofview.V82.tactic (exact poly (c, cl)) + | Give_exact (c, cl) -> exact poly (c, cl) | Res_pf_THEN_trivial_fail (c,cl) -> Tacticals.New.tclTHEN (Proofview.V82.tactic (unify_resolve_gen poly flags (c,cl))) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 4674bd030..bb7d2f0d2 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -35,7 +35,7 @@ let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_tr let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 || occur_existential t2 then tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl - else exact_check c gl + else Proofview.V82.of_tactic (exact_check c) gl let assumption id = e_give_exact (mkVar id) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ba389faa9..23c37fb65 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -129,18 +129,18 @@ let convert_concl = Tacmach.convert_concl let convert_hyp = Tacmach.convert_hyp let thin_body = Tacmach.thin_body -let convert_gen pb x y gl = - try tclEVARS (pf_apply Evd.conversion gl pb x y) gl - with Reduction.NotConvertible -> - tclFAIL_lazy 0 (lazy (str"Not convertible")) - (* Adding more information in this message, even under the lazy, can result in huge *) - (* blowups, time and spacewise... (see autos used in DoubleCyclic.) 2.3s against 15s. *) - (* ++ Printer.pr_constr_env env x ++ *) - (* str" and " ++ Printer.pr_constr_env env y)) *) - gl - -let convert = convert_gen Reduction.CONV -let convert_leq = convert_gen Reduction.CUMUL +let convert_gen pb x y = + Proofview.Goal.raw_enter begin fun gl -> + try + let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in + Proofview.V82.tclEVARS sigma + with (* Reduction.NotConvertible *) _ -> + (** FIXME: Sometimes an anomaly is raised from conversion *) + Tacticals.New.tclFAIL 0 (str "Not convertible") +end + +let convert x y = convert_gen Reduction.CONV x y +let convert_leq x y = convert_gen Reduction.CUMUL x y let error_clear_dependency env id = function | Evarutil.OccurHypInSimpleClause None -> @@ -1194,16 +1194,19 @@ let cut_and_apply c = (* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *) (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) -let exact_check c gl = - let concl = (pf_concl gl) in - let ct = pf_type_of gl c in - try tclTHEN (convert_leq ct concl) (refine_no_check c) gl - with _ -> error "Not an exact proof." (*FIXME error handling here not the best *) - -let exact_no_check = refine_no_check let new_exact_no_check c = Proofview.Refine.refine (fun h -> (h, c)) +let exact_check c = + Proofview.Goal.raw_enter begin fun gl -> + (** We do not need to normalize the goal because we just check convertibility *) + let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let ct = Tacmach.New.pf_type_of gl c in + Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) + end + +let exact_no_check = refine_no_check + let vm_cast_no_check c gl = let concl = pf_concl gl in refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c1911819b..6574d88c5 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -45,8 +45,8 @@ val fix : Id.t option -> int -> tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic val cofix : Id.t option -> tactic -val convert : constr -> constr -> tactic -val convert_leq : constr -> constr -> tactic +val convert : constr -> constr -> unit Proofview.tactic +val convert_leq : constr -> constr -> unit Proofview.tactic (** {6 Introduction tactics. } *) @@ -110,7 +110,7 @@ val intros_pattern_bound : val assumption : unit Proofview.tactic val exact_no_check : constr -> tactic val vm_cast_no_check : constr -> tactic -val exact_check : constr -> tactic +val exact_check : constr -> unit Proofview.tactic val exact_proof : Constrexpr.constr_expr -> tactic (** {6 Reduction tactics. } *) -- cgit v1.2.3