diff options
Diffstat (limited to 'plugins/omega/coq_omega.ml')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 475 |
1 files changed, 240 insertions, 235 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 |