From 4c6a5f56ef5ab248d9e816b4d7bee3001cab9a2e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 3 Apr 2014 15:55:27 +0200 Subject: Removing tactic compatibility layer from Elim. --- tactics/elim.ml | 84 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 41 insertions(+), 43 deletions(-) (limited to 'tactics/elim.ml') diff --git a/tactics/elim.ml b/tactics/elim.ml index 5eb3dcfe6..845c4eee1 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -12,8 +12,8 @@ open Term open Termops open Inductiveops open Hipattern -open Tacmach -open Tacticals +open Tacmach.New +open Tacticals.New open Tactics open Misctypes open Proofview.Notations @@ -22,27 +22,27 @@ let introElimAssumsThen tac ba = let nassums = List.fold_left (fun acc b -> if b then acc+2 else acc+1) - 0 ba.branchsign + 0 ba.Tacticals.branchsign in - let introElimAssums = Tacticals.New.tclDO nassums intro in - (Tacticals.New.tclTHEN introElimAssums (Tacticals.New.elim_on_ba tac ba)) + let introElimAssums = tclDO nassums intro in + (tclTHEN introElimAssums (elim_on_ba tac ba)) let introCaseAssumsThen tac ba = let case_thin_sign = List.flatten (List.map (function b -> if b then [false;true] else [false]) - ba.branchsign) + ba.Tacticals.branchsign) in let n1 = List.length case_thin_sign in - let n2 = List.length ba.branchnames in + let n2 = List.length ba.Tacticals.branchnames in let (l1,l2),l3 = - if n1 < n2 then List.chop n1 ba.branchnames, [] + if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, [] else - (ba.branchnames, []), + (ba.Tacticals.branchnames, []), if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in let introCaseAssums = - Tacticals.New.tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in - (Tacticals.New.tclTHEN introCaseAssums (Tacticals.New.case_on_ba (tac l2) ba)) + tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in + (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) (* The following tactic Decompose repeatedly applies the elimination(s) rule(s) of the types satisfying the predicate @@ -63,18 +63,18 @@ Another example : *) let elimHypThen tac id = - Tacticals.New.elimination_then tac (mkVar id) + elimination_then tac (mkVar id) let rec general_decompose_on_hyp recognizer = - Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) + ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) and general_decompose_aux recognizer id = elimHypThen (introElimAssumsThen (fun bas -> - Tacticals.New.tclTHEN (Proofview.V82.tactic (clear [id])) - (Tacticals.New.tclMAP (general_decompose_on_hyp recognizer) - (ids_of_named_context bas.assums)))) + tclTHEN (Proofview.V82.tactic (clear [id])) + (tclMAP (general_decompose_on_hyp recognizer) + (ids_of_named_context bas.Tacticals.assums)))) id (* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste @@ -85,17 +85,15 @@ let tmphyp_name = Id.of_string "_TmpHyp" let up_to_delta = ref false (* true *) let general_decompose recognizer c = - Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_type_of gl in - try (* type_of can raise exceptions *) + Proofview.Goal.raw_enter begin fun gl -> + let type_of = pf_type_of gl in let typc = type_of c in - Tacticals.New.tclTHENS (cut typc) - [ Tacticals.New.tclTHEN (intro_using tmphyp_name) - (Tacticals.New.onLastHypId - (Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer) + tclTHENS (cut typc) + [ tclTHEN (intro_using tmphyp_name) + (onLastHypId + (ifOnHyp recognizer (general_decompose_aux recognizer) (fun id -> Proofview.V82.tactic (clear [id])))); Proofview.V82.tactic (exact_no_check c) ] - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end let head_in indl t gl = @@ -110,7 +108,7 @@ let head_in indl t gl = with Not_found -> false let decompose_these c l = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.raw_enter begin fun gl -> let indl = (*List.map inductive_of*) l in general_decompose (fun (_,t) -> head_in indl t gl) c end @@ -139,47 +137,47 @@ let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) let simple_elimination c = - Tacticals.New.elimination_then (fun _ -> Tacticals.New.tclIDTAC) c + elimination_then (fun _ -> tclIDTAC) c let induction_trailer abs_i abs_j bargs = - Tacticals.New.tclTHEN - (Tacticals.New.tclDO (abs_j - abs_i) intro) - (Tacticals.New.onLastHypId + tclTHEN + (tclDO (abs_j - abs_i) intro) + (onLastHypId (fun id -> - Proofview.V82.tactic begin fun gls -> - let idty = pf_type_of gls (mkVar id) in - let fvty = global_vars (pf_env gls) idty in + Proofview.Goal.enter begin fun gl -> + let idty = pf_type_of gl (mkVar id) in + let fvty = global_vars (pf_env gl) idty in let possible_bring_hyps = - (List.tl (nLastDecls (abs_j - abs_i) gls)) @ bargs.assums + (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums in let (hyps,_) = List.fold_left - (fun (bring_ids,leave_ids) (cid,_,cidty as d) -> + (fun (bring_ids,leave_ids) (cid,_,_ as d) -> if not (List.mem cid leave_ids) then (d::bring_ids,leave_ids) else (bring_ids,cid::leave_ids)) ([],fvty) possible_bring_hyps in let ids = List.rev (ids_of_named_context hyps) in - (tclTHENSEQ - [Proofview.V82.of_tactic (bring_hyps hyps); tclTRY (clear ids); - Proofview.V82.of_tactic (simple_elimination (mkVar id))]) gls + (tclTHENLIST + [bring_hyps hyps; tclTRY (Proofview.V82.tactic (clear ids)); + simple_elimination (mkVar id)]) end )) let double_ind h1 h2 = Proofview.Goal.enter begin fun gl -> - let abs_i = Tacmach.New.of_old (depth_of_quantified_hypothesis true h1) gl in - let abs_j = Tacmach.New.of_old (depth_of_quantified_hypothesis true h2) gl in + let abs_i = of_old (depth_of_quantified_hypothesis true h1) gl in + let abs_j = of_old (depth_of_quantified_hypothesis true h2) gl in let abs = if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else - Proofview.tclZERO (Errors.UserError ("", Pp.str"Both hypotheses are the same.")) in + tclZEROMSG (Pp.str "Both hypotheses are the same.") in abs >>= fun (abs_i,abs_j) -> - (Tacticals.New.tclTHEN (Tacticals.New.tclDO abs_i intro) - (Tacticals.New.onLastHypId + (tclTHEN (tclDO abs_i intro) + (onLastHypId (fun id -> - Tacticals.New.elimination_then + elimination_then (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) end -- cgit v1.2.3