aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-02 15:34:01 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-02 15:34:01 +0000
commit260965dcf60d793ba01110ace8945cf51ef6531f (patch)
treed07323383e16bb5a63492e2721cf0502ba931716 /plugins/firstorder
parent328279514e65f47a689e2d23f132c43c86870c05 (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 'plugins/firstorder')
-rw-r--r--plugins/firstorder/g_ground.ml424
-rw-r--r--plugins/firstorder/instances.ml14
-rw-r--r--plugins/firstorder/rules.ml40
3 files changed, 40 insertions, 38 deletions
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