aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
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/omega
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/omega')
-rw-r--r--plugins/omega/coq_omega.ml475
-rw-r--r--plugins/omega/g_omega.ml46
2 files changed, 243 insertions, 238 deletions
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