diff options
author | 2013-11-02 15:34:01 +0000 | |
---|---|---|
committer | 2013-11-02 15:34:01 +0000 | |
commit | 260965dcf60d793ba01110ace8945cf51ef6531f (patch) | |
tree | d07323383e16bb5a63492e2721cf0502ba931716 /tactics/elim.ml | |
parent | 328279514e65f47a689e2d23f132c43c86870c05 (diff) |
Makes the new Proofview.tactic the basic type of Ltac.
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
Diffstat (limited to 'tactics/elim.ml')
-rw-r--r-- | tactics/elim.ml | 117 |
1 files changed, 64 insertions, 53 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index faa32ab86..0e30daf6d 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -17,6 +17,7 @@ open Tacmach open Tacticals open Tactics open Misctypes +open Proofview.Notations let introElimAssumsThen tac ba = let nassums = @@ -24,8 +25,8 @@ let introElimAssumsThen tac ba = (fun acc b -> if b then acc+2 else acc+1) 0 ba.branchsign in - let introElimAssums = tclDO nassums intro in - (tclTHEN introElimAssums (elim_on_ba tac ba)) + let introElimAssums = Tacticals.New.tclDO nassums intro in + (Tacticals.New.tclTHEN introElimAssums (Tacticals.New.elim_on_ba tac ba)) let introCaseAssumsThen tac ba = let case_thin_sign = @@ -41,8 +42,8 @@ let introCaseAssumsThen tac ba = (ba.branchnames, []), if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in let introCaseAssums = - tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in - (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) + Tacticals.New.tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in + (Tacticals.New.tclTHEN introCaseAssums (Tacticals.New.case_on_ba (tac l2) ba)) (* The following tactic Decompose repeatedly applies the elimination(s) rule(s) of the types satisfying the predicate @@ -62,18 +63,18 @@ Another example : Qed. *) -let elimHypThen tac id gl = - elimination_then tac ([],[]) (mkVar id) gl +let elimHypThen tac id = + Tacticals.New.elimination_then tac ([],[]) (mkVar id) let rec general_decompose_on_hyp recognizer = - ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> tclIDTAC) + Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) and general_decompose_aux recognizer id = elimHypThen (introElimAssumsThen (fun bas -> - tclTHEN (clear [id]) - (tclMAP (general_decompose_on_hyp recognizer) + Tacticals.New.tclTHEN (Proofview.V82.tactic (clear [id])) + (Tacticals.New.tclMAP (general_decompose_on_hyp recognizer) (ids_of_named_context bas.assums)))) id @@ -84,42 +85,49 @@ and general_decompose_aux recognizer id = let tmphyp_name = Id.of_string "_TmpHyp" let up_to_delta = ref false (* true *) -let general_decompose recognizer c gl = - let typc = pf_type_of gl c in - tclTHENSV (cut typc) - [| tclTHEN (intro_using tmphyp_name) - (onLastHypId - (ifOnHyp recognizer (general_decompose_aux recognizer) - (fun id -> clear [id]))); - exact_no_check c |] gl - -let head_in gls indl t = - try - let ity,_ = - if !up_to_delta - then find_mrectype (pf_env gls) (project gls) t - else extract_mrectype t - in List.mem ity indl - with Not_found -> false - -let decompose_these c l gls = +let general_decompose recognizer c = + Tacmach.New.pf_apply Typing.type_of >>- fun type_of -> + let typc = type_of c in + Tacticals.New.tclTHENS (Proofview.V82.tactic (cut typc)) + [ Tacticals.New.tclTHEN (intro_using tmphyp_name) + (Tacticals.New.onLastHypId + (Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer) + (fun id -> Proofview.V82.tactic (clear [id])))); + Proofview.V82.tactic (exact_no_check c) ] + +let head_in = + Goal.env >- fun env -> + Goal.defs >- fun sigma -> + Goal.return begin + fun indl t -> + try + let ity,_ = + if !up_to_delta + then find_mrectype env sigma t + else extract_mrectype t + in List.mem ity indl + with Not_found -> false + end + +let decompose_these c l = let indl = (*List.map inductive_of*) l in - general_decompose (fun (_,t) -> head_in gls indl t) c gls + head_in >>- fun head_in -> + general_decompose (fun (_,t) -> head_in indl t) c -let decompose_nonrec c gls = +let decompose_nonrec c = general_decompose (fun (_,t) -> is_non_recursive_type t) - c gls + c -let decompose_and c gls = +let decompose_and c = general_decompose (fun (_,t) -> is_record t) - c gls + c -let decompose_or c gls = +let decompose_or c = general_decompose (fun (_,t) -> is_disjunction t) - c gls + c let h_decompose l c = decompose_these c l @@ -133,10 +141,11 @@ let simple_elimination c gls = simple_elimination_then (fun _ -> tclIDTAC) c gls let induction_trailer abs_i abs_j bargs = - tclTHEN - (tclDO (abs_j - abs_i) intro) - (onLastHypId - (fun id gls -> + Tacticals.New.tclTHEN + (Tacticals.New.tclDO (abs_j - abs_i) intro) + (Tacticals.New.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 let possible_bring_hyps = @@ -153,22 +162,24 @@ let induction_trailer abs_i abs_j bargs = let ids = List.rev (ids_of_named_context hyps) in (tclTHENSEQ [bring_hyps hyps; tclTRY (clear ids); - simple_elimination (mkVar id)]) - gls)) - -let double_ind h1 h2 gls = - let abs_i = depth_of_quantified_hypothesis true h1 gls in - let abs_j = depth_of_quantified_hypothesis true h2 gls in - let (abs_i,abs_j) = - if abs_i < abs_j then (abs_i,abs_j) else - if abs_i > abs_j then (abs_j,abs_i) else - error "Both hypotheses are the same." in - (tclTHEN (tclDO abs_i intro) - (onLastHypId + simple_elimination (mkVar id)]) gls + end + )) + +let double_ind h1 h2 = + Tacmach.New.of_old (depth_of_quantified_hypothesis true h1) >>- fun abs_i -> + Tacmach.New.of_old (depth_of_quantified_hypothesis true h2) >>- fun abs_j -> + 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 + abs >= fun (abs_i,abs_j) -> + (Tacticals.New.tclTHEN (Tacticals.New.tclDO abs_i intro) + (Tacticals.New.onLastHypId (fun id -> - elimination_then + Tacticals.New.elimination_then (introElimAssumsThen (induction_trailer abs_i abs_j)) - ([],[]) (mkVar id)))) gls + ([],[]) (mkVar id)))) let h_double_induction = double_ind |