From 73cdb000ec07ec484557839c4b94fcf779df2f06 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 13 May 2016 00:16:09 +0200 Subject: Put the "clear" tactic into the monad. --- ltac/coretactics.ml4 | 2 +- ltac/tauto.ml | 2 +- plugins/decl_mode/decl_proof_instr.ml | 16 +++++ plugins/firstorder/rules.ml | 4 +- plugins/funind/functional_principles_proofs.ml | 5 +- plugins/funind/invfun.ml | 1 + plugins/funind/recdef.ml | 14 ++-- plugins/omega/coq_omega.ml | 28 ++++---- printing/printer.ml | 3 - proofs/logic.ml | 10 --- proofs/proof_type.mli | 1 - proofs/tacmach.ml | 5 -- proofs/tacmach.mli | 2 - tactics/autorewrite.ml | 2 +- tactics/elim.ml | 4 +- tactics/eqdecide.ml | 1 - tactics/equality.ml | 2 - tactics/inv.ml | 2 - tactics/tactics.ml | 96 ++++++++++++++------------ tactics/tactics.mli | 3 +- toplevel/vernacentries.ml | 2 +- 21 files changed, 100 insertions(+), 105 deletions(-) diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 8b5f527cd0..4e2dfafb52 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -247,7 +247,7 @@ END TACTIC EXTEND clear [ "clear" hyp_list(ids) ] -> [ if List.is_empty ids then Tactics.keep [] - else Proofview.V82.tactic (Tactics.clear ids) + else Tactics.clear ids ] | [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ] END diff --git a/ltac/tauto.ml b/ltac/tauto.ml index 655bfd5f52..c0cae84c02 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -102,7 +102,7 @@ let assert_ ?by c = let apply c = Tactics.apply c -let clear id = Proofview.V82.tactic (fun gl -> Tactics.clear [id] gl) +let clear id = Tactics.clear [id] let assumption = Tactics.assumption diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 090b293f5c..4f22703130 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -34,6 +34,22 @@ open Context.Named.Declaration (* Strictness option *) +let clear ids { it = goal; sigma } = + let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in + let env = Goal.V82.env sigma goal in + let sign = Goal.V82.hyps sigma goal in + let cl = Goal.V82.concl sigma goal in + let evdref = ref (Evd.clear_metas sigma) in + let (hyps, concl) = + try Evarutil.clear_hyps_in_evi env evdref sign cl ids + with Evarutil.ClearDependencyError (id, _) -> + errorlabstrm "" (str "Cannot clear " ++ pr_id id) + in + let sigma = !evdref in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + let sigma = Goal.V82.partial_solution_to sigma goal gl ev in + { it = [gl]; sigma } + let get_its_info gls = get_info gls.sigma gls.it let get_strictness,set_strictness = diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index c05015c538..f19cdd2ccc 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -52,7 +52,7 @@ let basename_of_global=function | _->assert false let clear_global=function - VarRef id->clear [id] + VarRef id-> Proofview.V82.of_tactic (clear [id]) | _->tclIDTAC (* connection rules *) @@ -192,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq= (fun gls-> let id0=pf_nth_hyp_id gls 1 in let term=mkApp(idc,[|mkVar(id0)|]) in - tclTHEN (generalize [term]) (clear [id0]) gls)); + tclTHEN (generalize [term]) (Proofview.V82.of_tactic (clear [id0])) gls)); clear_global id; Proofview.V82.of_tactic intro; tclCOMPLETE (wrap 1 false continue (deepen seq))]; diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8395865286..fdb112ba01 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -127,8 +127,7 @@ let finish_proof dynamic_infos g = let refine c = Tacmach.refine c -let thin l = - Tacmach.thin_no_check l +let thin l = Proofview.V82.of_tactic (Tactics.clear l) let eq_constr u v = eq_constr_nounivs u v @@ -1565,7 +1564,7 @@ let prove_principle_for_gen Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) in let revert l = - tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l) + tclTHEN (Tactics.generalize (List.map mkVar l)) (Proofview.V82.of_tactic (clear l)) in let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 6a5a5ad533..fde1b7e707 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -94,6 +94,7 @@ let nf_zeta = Environ.empty_env Evd.empty +let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl (* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *) (* let id_to_constr id = *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e98ac5fb5e..ac81366bb5 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -267,8 +267,8 @@ let observe_tclTHENLIST s tacl = let tclUSER tac is_mes l g = let clear_tac = match l with - | None -> clear [] - | Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l) + | None -> tclIDTAC + | Some l -> tclMAP (fun id -> tclTRY (Proofview.V82.of_tactic (clear [id]))) (List.rev l) in observe_tclTHENLIST (str "tclUSER1") [ @@ -399,7 +399,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = Proofview.V82.of_tactic (intro_using teq_id); onLastHypId (fun heq -> observe_tclTHENLIST (str "treat_case2")[ - thin to_intros; + Proofview.V82.of_tactic (clear to_intros); h_intros to_intros; (fun g' -> let ty_teq = pf_unsafe_type_of g' (mkVar heq) in @@ -560,7 +560,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]))); Proofview.V82.of_tactic default_full_auto]; observe_tclTHENLIST (str "destruct_bounds_aux2")[ - observe_tac (str "clearing k ") (clear [id]); + observe_tac (str "clearing k ") (Proofview.V82.of_tactic (clear [id])); h_intros [k;h';def]; observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl)); observe_tac (str "unfold functional") @@ -589,7 +589,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = | (_,v_bound)::l -> observe_tclTHENLIST (str "destruct_bounds_aux3")[ Proofview.V82.of_tactic (simplest_elim (mkVar v_bound)); - clear [v_bound]; + Proofview.V82.of_tactic (clear [v_bound]); tclDO 2 (Proofview.V82.of_tactic intro); onNthHypId 1 (fun p_hyp -> @@ -948,7 +948,7 @@ let rec destruct_hex expr_info acc l = | (v,hex)::l -> observe_tclTHENLIST (str "destruct_hex")[ Proofview.V82.of_tactic (simplest_case (mkVar hex)); - clear [hex]; + Proofview.V82.of_tactic (clear [hex]); tclDO 2 (Proofview.V82.of_tactic intro); onNthHypId 1 (fun hp -> onNthHypId 2 (fun p -> @@ -1116,7 +1116,7 @@ let termination_proof_header is_mes input_type ids args_id relation [observe_tac (str "generalize") (onNLastHypsId (nargs+1) (tclMAP (fun id -> - tclTHEN (Tactics.generalize [mkVar id]) (clear [id])) + tclTHEN (Tactics.generalize [mkVar id]) (Proofview.V82.of_tactic (clear [id]))) )) ; observe_tac (str "fix") (fix (Some hrec) (nargs+1)); diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 1f420cf6ae..fc50540805 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1122,7 +1122,7 @@ let replay_history tactic_normalisation = Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA1, [| eq1; rhs; mkVar aux; mkVar id |])]); - Proofview.V82.tactic (clear [aux;id]); + (clear [aux;id]); (intros_using [id]); (cut (mk_gt kk dd)) ]) [ Tacticals.New.tclTHENS @@ -1132,7 +1132,7 @@ let replay_history tactic_normalisation = (Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_Zmult_le_approx, [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])])); - Proofview.V82.tactic (clear [aux1;aux2;id]); + (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; Tacticals.New.tclTHENLIST [ @@ -1160,7 +1160,7 @@ let replay_history tactic_normalisation = Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA4, [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); - Proofview.V82.tactic (clear [aux1;aux2]); + (clear [aux1;aux2]); unfold sp_not; (intros_using [aux]); Proofview.V82.tactic (resolve_id aux); @@ -1190,7 +1190,7 @@ let replay_history tactic_normalisation = Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA18, [| eq1;eq2;kk;mkVar aux1; mkVar id |])]); - Proofview.V82.tactic (clear [aux1;id]); + (clear [aux1;id]); (intros_using [id]); (loop l) ]; Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ] @@ -1205,7 +1205,7 @@ let replay_history tactic_normalisation = Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA3, [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]); - Proofview.V82.tactic (clear [aux1;aux2;id]); + (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; Tacticals.New.tclTHENLIST [ @@ -1231,7 +1231,7 @@ let replay_history tactic_normalisation = (intros_using [aux]); Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); - Proofview.V82.tactic (clear [id1;id2;aux]); + (clear [id1;id2;aux]); (intros_using [id]); (loop l) ]; Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity] @@ -1263,13 +1263,13 @@ let replay_history tactic_normalisation = [Tacticals.New.tclTHENLIST [ (intros_using [aux]); (elim_id aux); - Proofview.V82.tactic (clear [aux]); + (clear [aux]); (intros_using [vid; aux]); Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA9, [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); Proofview.V82.tactic (mk_then tac); - Proofview.V82.tactic (clear [aux]); + (clear [aux]); (intros_using [id]); (loop l) ]; Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ] @@ -1325,7 +1325,7 @@ let replay_history tactic_normalisation = eq1;eq2;kk1;kk2; mkVar aux1;mkVar aux2; mkVar id1;mkVar id2 |])]); - Proofview.V82.tactic (clear [aux1;aux2]); + (clear [aux1;aux2]); Proofview.V82.tactic (mk_then tac); (intros_using [id]); (loop l) ]; @@ -1367,7 +1367,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) = let shift_left = tclTHEN (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]) - (tclTRY (clear [id])) + (tclTRY (Proofview.V82.of_tactic (clear [id]))) in if not (List.is_empty tac) then let id' = new_identifier () in @@ -1412,7 +1412,7 @@ let destructure_omega gl tac_def (id,c) = let reintroduce id = (* [id] cannot be cleared if dependent: protect it by a try *) - Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTRY (clear [id]))) (intro_using id) + Tacticals.New.tclTHEN (Tacticals.New.tclTRY (clear [id])) (intro_using id) open Proofview.Notations @@ -1435,7 +1435,7 @@ let coq_omega = (simplest_elim (applist (Lazy.force coq_intro_Z, [t]))); (intros_using [v; id]); (elim_id id); - Proofview.V82.tactic (clear [id]); + (clear [id]); (intros_using [th;id]); tac ]), {kind = INEQ; @@ -1674,7 +1674,7 @@ let onClearedName id tac = (* We cannot ensure that hyps can be cleared (because of dependencies), *) (* so renaming may be necessary *) Tacticals.New.tclTHEN - (Proofview.V82.tactic (tclTRY (clear [id]))) + (Tacticals.New.tclTRY (clear [id])) (Proofview.Goal.nf_enter { enter = begin fun gl -> let id = Tacmach.New.of_old (fresh_id [] id) gl in Tacticals.New.tclTHEN (introduction id) (tac id) @@ -1682,7 +1682,7 @@ let onClearedName id tac = let onClearedName2 id tac = Tacticals.New.tclTHEN - (Proofview.V82.tactic (tclTRY (clear [id]))) + (Tacticals.New.tclTRY (clear [id])) (Proofview.Goal.nf_enter { enter = begin fun gl -> let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in diff --git a/printing/printer.ml b/printing/printer.ml index a16a92d0a5..401f5f99e9 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -711,9 +711,6 @@ let pr_prim_rule = function str(if Termops.occur_meta c then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c - | Thin ids -> - (str"clear " ++ pr_sequence pr_id ids) - | Move (id1,id2) -> (str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2) diff --git a/proofs/logic.ml b/proofs/logic.ml index 09f308abef..df5a12473b 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -636,16 +636,6 @@ let prim_refiner r sigma goal = let sigma = Goal.V82.partial_solution sigma goal oterm in (sgl, sigma) - (* And now the structural rules *) - | Thin ids -> - let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in - let (hyps,concl,nsigma) = clear_hyps env sigma ids sign cl in - let (gl,ev,sigma) = - Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal) - in - let sigma = Goal.V82.partial_solution_to sigma goal gl ev in - ([gl], sigma) - | Move (hfrom, hto) -> let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index b4c9dae2a3..48ad50c7a0 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -22,7 +22,6 @@ type prim_rule = | FixRule of Id.t * int * (Id.t * int * constr) list * int | Cofix of Id.t * (Id.t * constr) list * int | Refine of constr - | Thin of Id.t list | Move of Id.t * Id.t move_location (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 33cef7486b..67daccb81d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -121,10 +121,6 @@ let internal_cut_rev_no_check replace id t gl = let refine_no_check c gl = refiner (Refine c) gl -(* This does not check dependencies *) -let thin_no_check ids gl = - if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl - let move_hyp_no_check id1 id2 gl = refiner (Move (id1,id2)) gl @@ -139,7 +135,6 @@ let mutual_cofix f others j gl = let internal_cut b d t = with_check (internal_cut_no_check b d t) let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) -let thin c = with_check (thin_no_check c) let move_hyp id id' = with_check (move_hyp_no_check id id') (* Pretty-printers *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f786b5f218..fef205f823 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -86,7 +86,6 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool val refiner : rule -> tactic val internal_cut_no_check : bool -> Id.t -> types -> tactic val refine_no_check : constr -> tactic -val thin_no_check : Id.t list -> tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic @@ -96,7 +95,6 @@ val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic val internal_cut : bool -> Id.t -> types -> tactic val internal_cut_rev : bool -> Id.t -> types -> tactic val refine : constr -> tactic -val thin : Id.t list -> tactic val move_hyp : Id.t -> Id.t move_location -> tactic (** {6 Pretty-printing functions (debug only). } *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 6d6e51536c..9ae0ab90b2 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -151,7 +151,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = begin let gl'' = if !to_be_cleared then - tclTHEN (fun _ -> gl') (tclTRY (clear [!id])) gl + tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl else gl' in id := lastid ; to_be_cleared := true ; diff --git a/tactics/elim.ml b/tactics/elim.ml index d441074f6a..33eb80c280 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -63,7 +63,7 @@ and general_decompose_aux recognizer id = elimHypThen (introElimAssumsThen (fun bas -> - tclTHEN (Proofview.V82.tactic (clear [id])) + tclTHEN (clear [id]) (tclMAP (general_decompose_on_hyp recognizer) (ids_of_named_context bas.Tacticals.assums)))) id @@ -83,7 +83,7 @@ let general_decompose recognizer c = [ tclTHEN (intro_using tmphyp_name) (onLastHypId (ifOnHyp recognizer (general_decompose_aux recognizer) - (fun id -> Proofview.V82.tactic (clear [id])))); + (fun id -> clear [id]))); Proofview.V82.tactic (exact_no_check c) ] end } diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index ef361d3265..01ebaa7b72 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -49,7 +49,6 @@ open Coqlib Eduardo Gimenez (30/3/98). *) -let clear ids = Proofview.V82.tactic (clear ids) let clear_last = (onLastHyp (fun c -> (clear [destVar c]))) let choose_eq eqonleft = diff --git a/tactics/equality.ml b/tactics/equality.ml index cb1d82ae6b..eecc2b787c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -79,8 +79,6 @@ let _ = (* Rewriting tactics *) -let clear ids = Proofview.V82.tactic (clear ids) - let tclNOTSAMEGOAL tac = Proofview.V82.tactic (Tacticals.tclNOTSAMEGOAL (Proofview.V82.of_tactic tac)) diff --git a/tactics/inv.ml b/tactics/inv.ml index 89c6beb321..3707ef90b4 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -30,8 +30,6 @@ open Sigma.Notations open Proofview.Notations open Context.Named.Declaration -let clear hyps = Proofview.V82.tactic (clear hyps) - let var_occurs_in_pf gl id = let env = Proofview.Goal.env gl in occur_var env id (Proofview.Goal.concl gl) || diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2fe4d620ed..b266438f94 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -271,25 +271,45 @@ let replacing_dependency_msg env sigma id = function let error_replacing_dependency env sigma id err = errorlabstrm "" (replacing_dependency_msg env sigma id err) -let thin l gl = - try Tacmach.thin l gl - with Evarutil.ClearDependencyError (id,err) -> - error_clear_dependency (pf_env gl) (project gl) id err +(* This tactic enables the user to remove hypotheses from the signature. + * Some care is taken to prevent him from removing variables that are + * subsequently used in other hypotheses or in the conclusion of the + * goal. *) -let thin_for_replacing l gl = - try Tacmach.thin l gl - with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency (pf_env gl) (project gl) id err +let clear_gen fail = function +| [] -> Proofview.tclUNIT () +| ids -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> + let ids = List.fold_right Id.Set.add ids Id.Set.empty in + (** clear_hyps_in_evi does not require nf terms *) + let gl = Proofview.Goal.assume gl in + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let concl = Proofview.Goal.concl gl in + let evdref = ref sigma in + let (hyps, concl) = + try clear_hyps_in_evi env evdref (named_context_val env) concl ids + with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err + in + let env = reset_with_named_context hyps env in + let tac = Refine.refine ~unsafe:true { run = fun sigma -> + Evarutil.new_evar env sigma ~principal:true concl + } in + Sigma.Unsafe.of_pair (tac, !evdref) + end } + +let clear ids = clear_gen error_clear_dependency ids +let clear_for_replacing ids = clear_gen error_replacing_dependency ids let apply_clear_request clear_flag dft c = let check_isvar c = if not (isVar c) then error "keep/clear modifiers apply only to hypothesis names." in - let clear = match clear_flag with + let doclear = match clear_flag with | None -> dft && isVar c | Some true -> check_isvar c; true | Some false -> false in - if clear then Proofview.V82.tactic (thin [destVar c]) + if doclear then clear [destVar c] else Tacticals.New.tclIDTAC (* Moving hypotheses *) @@ -890,7 +910,7 @@ let intro_replacing id = Proofview.Goal.enter { enter = begin fun gl -> let next_hyp = get_next_hyp_position id gl in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (thin_for_replacing [id]); + clear_for_replacing [id]; introduction id; Proofview.V82.tactic (move_hyp id next_hyp); ] @@ -910,7 +930,7 @@ let intros_possibly_replacing ids = let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> - Tacticals.New.tclTRY (Proofview.V82.tactic (thin_for_replacing [id]))) + Tacticals.New.tclTRY (clear_for_replacing [id])) (if suboptimal then ids else List.rev ids)) (Tacticals.New.tclMAP (fun (id,pos) -> Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id)) @@ -922,7 +942,7 @@ let intros_replacing ids = Proofview.Goal.enter { enter = begin fun gl -> let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in Tacticals.New.tclTHEN - (Proofview.V82.tactic (thin_for_replacing ids)) + (clear_for_replacing ids) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) end } @@ -1563,7 +1583,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) (fun b id -> Tacticals.New.tclTHEN (try_main_apply b (mkVar id)) - (Proofview.V82.tactic (thin [id]))) + (clear [id])) (exn0, info) c else Proofview.tclZERO ~info exn0 in @@ -1690,7 +1710,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming (fun id -> Tacticals.New.tclTHENLIST [ apply_clear_request clear_flag false c; - Proofview.V82.tactic (thin idstoclear); + clear idstoclear; tac id ]) with e when with_destruct && Errors.noncritical e -> @@ -1823,14 +1843,6 @@ let assumption = (* Modification of a local context *) (*****************************************************************) -(* This tactic enables the user to remove hypotheses from the signature. - * Some care is taken to prevent him from removing variables that are - * subsequently used in other hypotheses or in the conclusion of the - * goal. *) - -let clear ids = (* avant seul dyn_clear n'echouait pas en [] *) - if List.is_empty ids then tclIDTAC else thin ids - let on_the_bodies = function | [] -> assert false | [id] -> str " depends on the body of " ++ pr_id id @@ -1912,13 +1924,7 @@ let clear_body ids = end } let clear_wildcards ids = - Proofview.V82.tactic (tclMAP (fun (loc,id) gl -> - try with_check (Tacmach.thin_no_check [id]) gl - with ClearDependencyError (id,err) -> - (* Intercept standard [thin] error message *) - Loc.raise loc - (error_clear_dependency (pf_env gl) (project gl) (Id.of_string "_") err)) - ids) + Tacticals.New.tclMAP (fun (loc, id) -> clear [id]) ids (* Takes a list of booleans, and introduces all the variables * quantified in the goal which are associated with a value @@ -1929,7 +1935,7 @@ let rec intros_clearing = function | (false::tl) -> Tacticals.New.tclTHEN intro (intros_clearing tl) | (true::tl) -> Tacticals.New.tclTHENLIST - [ intro; Tacticals.New.onLastHypId (fun id -> Proofview.V82.tactic (clear [id])); intros_clearing tl] + [ intro; Tacticals.New.onLastHypId (fun id -> clear [id]); intros_clearing tl] (* Keeping only a few hypotheses *) @@ -1948,7 +1954,7 @@ let keep hyps = else (hyp::clear,keep)) ~init:([],[]) (Proofview.Goal.env gl) in - Proofview.V82.tactic (fun gl -> thin cl gl) + clear cl end } (*********************************) @@ -1995,7 +2001,7 @@ let revert hyps = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in - (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps)) + (bring_hyps ctx) <*> (clear hyps) end } (************************) @@ -2137,7 +2143,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id = let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in let ll = get_and_check_or_and_pattern loc ll branchsigns in Tacticals.New.tclTHENLASTn - (Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id]))) + (Tacticals.New.tclTHEN (simplest_case c) (clear [id])) (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) nv_with_let ll) end } @@ -2164,20 +2170,20 @@ let rewrite_hyp_then assert_style thin l2r id tac = let id' = destVar rhs in subst_on l2r id' lhs, early_clear id' thin else - Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])), + Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]), thin | Some (hdcncl,[c]) -> let l2r = not l2r in (* equality of the form eq_true *) if isVar c then let id' = destVar c in Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) - (Proofview.V82.tactic (clear_var_and_eq id')), + (clear_var_and_eq id'), early_clear id' thin else - Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])), + Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]), thin | _ -> - Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id])), + Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]), thin in (* Skip the side conditions of the rewriting step *) Tacticals.New.tclTHENFIRST eqtac (tac thin) @@ -2314,7 +2320,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with if naming = NamingMustBe (loc,id) then Proofview.tclUNIT () (* apply_in_once do a replacement *) else - Proofview.V82.tactic (clear [id]) in + clear [id] in let f = { delayed = fun env sigma -> let Sigma (c, sigma, p) = f.delayed env sigma in Sigma ((c, NoBindings), sigma, p) @@ -2653,7 +2659,7 @@ let generalize_dep ?(with_let=false) c gl = tclTHENLIST [tclEVARS evd; Proofview.V82.of_tactic (apply_type cl'' (if Option.is_empty body then c::args else args)); - thin (List.rev tothin')] + Proofview.V82.of_tactic (clear (List.rev tothin'))] gl (** *) @@ -2789,7 +2795,7 @@ let unfold_body x = end } (* Either unfold and clear if defined or simply clear if not a definition *) -let expand_hyp id = Tacticals.New.tclTHEN (Tacticals.New.tclTRY (unfold_body id)) (Proofview.V82.tactic (clear [id])) +let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] (*****************************) (* High-level induction *) @@ -3523,7 +3529,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))] else Tacticals.New.tclTHENLIST [ tac; - Proofview.V82.tactic (clear [id]); + clear [id]; Tacticals.New.tclDO n intro] in if List.is_empty vars then tac @@ -3590,7 +3596,7 @@ let specialize_eqs id gl = let specialize_eqs id gl = if - (try ignore(clear [id] gl); false + (try ignore(Proofview.V82.of_tactic (clear [id]) gl); false with e when Errors.noncritical e -> true) then tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl @@ -4044,7 +4050,7 @@ let clear_unselected_context id inhyps cls gl = let test id = occur_var_in_decl (pf_env gl) id d in if List.exists test (id::inhyps) then Some id' else None in let ids = List.map_filter to_erase (pf_hyps gl) in - thin ids gl + Proofview.V82.of_tactic (clear ids) gl | None -> tclIDTAC gl let use_bindings env sigma elim must_be_closed (c,lbind) typ = @@ -4148,7 +4154,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim end }; if with_evars then Proofview.shelve_unifiable else guard_no_unifiable; if is_arg_pure_hyp - then Tacticals.New.tclTRY (Proofview.V82.tactic (thin [destVar c0])) + then Tacticals.New.tclTRY (clear [destVar c0]) else Proofview.tclUNIT (); if isrec then Proofview.cycle (-1) else Proofview.tclUNIT () ]) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 4c4a96ec07..87400bfdff 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -35,7 +35,6 @@ val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic -val thin : Id.t list -> tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> tactic val fix : Id.t option -> int -> tactic @@ -163,7 +162,7 @@ val unfold_constr : global_reference -> unit Proofview.tactic (** {6 Modification of the local context. } *) -val clear : Id.t list -> tactic +val clear : Id.t list -> unit Proofview.tactic val clear_body : Id.t list -> unit Proofview.tactic val unfold_body : Id.t -> unit Proofview.tactic val keep : Id.t list -> unit Proofview.tactic diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b40f61b15e..0e5cef828b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -861,7 +861,7 @@ let vernac_set_used_variables e = Proof_global.with_current_proof begin fun _ p -> if List.is_empty to_clear then (p, ()) else - let tac = Proofview.V82.tactic (Tactics.clear to_clear) in + let tac = Tactics.clear to_clear in fst (solve SelectAll None tac p), () end -- cgit v1.2.3 From dc8750d166cffd846619d2de20e02a4e31c6357f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 18:10:36 +0200 Subject: Put the "exact_constr" tactic in the monad. --- tactics/tactics.ml | 15 +++++++++++---- tactics/tactics.mli | 4 +--- toplevel/vernacentries.ml | 2 +- 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b266438f94..a47ee96a0a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1806,9 +1806,16 @@ let native_cast_no_check c gl = Tacmach.refine_no_check (Term.mkCast(c,Term.NATIVEcast,concl)) gl -let exact_proof c gl = - let c,ctx = Constrintern.interp_casted_constr (Tacmach.pf_env gl) (Tacmach.project gl) c (Tacmach.pf_concl gl) - in tclTHEN (tclEVARUNIVCONTEXT ctx) (Tacmach.refine_no_check c) gl +let exact_proof c = + let open Tacmach.New in + Proofview.Goal.nf_enter { enter = begin fun gl -> + Refine.refine { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in + let sigma = Evd.merge_universe_context sigma ctx in + Sigma.Unsafe.of_pair (c, sigma) + end } + end } let assumption = let open Context.Named.Declaration in @@ -4802,7 +4809,7 @@ end module New = struct open Proofview.Notations - let exact_proof c = Proofview.V82.tactic (exact_proof c) + let exact_proof c = exact_proof c open Genredexpr open Locus diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 87400bfdff..f6c001941c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -118,7 +118,7 @@ val exact_no_check : constr -> tactic val vm_cast_no_check : constr -> tactic val native_cast_no_check : constr -> tactic val exact_check : constr -> unit Proofview.tactic -val exact_proof : Constrexpr.constr_expr -> tactic +val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic (** {6 Reduction tactics. } *) @@ -436,6 +436,4 @@ module New : sig val reduce_after_refine : unit Proofview.tactic (** The reducing tactic called after {!refine}. *) - open Proofview - val exact_proof : Constrexpr.constr_expr -> unit tactic end diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0e5cef828b..23755dac1d 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -504,7 +504,7 @@ let vernac_end_proof ?proof = function let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) - let status = by (Tactics.New.exact_proof c) in + let status = by (Tactics.exact_proof c) in save_proof (Vernacexpr.(Proved(Opaque None,None))); if not status then Pp.feedback Feedback.AddedAxiom -- cgit v1.2.3 From 12f4c8ed277fa8368cab2e99f173339a64bcef3d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 18:34:21 +0200 Subject: Put the "fix" tactic in the monad. --- ltac/coretactics.ml4 | 4 +- ltac/tacinterp.ml | 2 +- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 8 ++-- plugins/funind/recdef.ml | 2 +- printing/printer.ml | 12 ----- proofs/logic.ml | 45 ------------------ proofs/proof_type.mli | 1 - proofs/tacmach.ml | 3 -- proofs/tacmach.mli | 2 - stm/lemmas.ml | 4 +- tactics/tactics.ml | 63 ++++++++++++++++++++++++-- tactics/tactics.mli | 4 +- 13 files changed, 72 insertions(+), 80 deletions(-) diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 4e2dfafb52..98b77ab357 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -231,8 +231,8 @@ END (* Fix *) TACTIC EXTEND fix - [ "fix" natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix None n) ] -| [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ] + [ "fix" natural(n) ] -> [ Tactics.fix None n ] +| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ] END (* Cofix *) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index d650cb5c6f..5e0153fcee 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1714,7 +1714,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in - let tac = Proofview.V82.tactic (Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0) in + let tac = Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0 in Sigma.Unsafe.of_pair (tac, sigma) end } end diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 4f22703130..a6b3381648 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1385,7 +1385,7 @@ let end_tac et2 gls = let c_id = pf_get_new_id (Id.of_string "_main_arg") gls0 in tclTHENLIST - [fix (Some fix_id) (succ nargs); + [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs)); tclDO nargs (Proofview.V82.of_tactic introf); Proofview.V82.of_tactic (intro_mustbe_force c_id); execute_cases (Name fix_id) pi diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index fdb112ba01..0b7a1e6468 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1227,10 +1227,10 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam if this_fix_info.idx + 1 = 0 then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) else - observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (fix (Some this_fix_info.name) (this_fix_info.idx +1)) + observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1))) else - Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) - other_fix_infos 0 + Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) + other_fix_infos 0) | _ -> anomaly (Pp.str "Not a valid information") in let first_tac : tactic = (* every operations until fix creations *) @@ -1642,7 +1642,7 @@ let prove_principle_for_gen (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) (* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) - (* observe_tac "h_fix " *) (fix (Some fix_id) (List.length args_ids + 1)); + (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ac81366bb5..c1c3801b45 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1119,7 +1119,7 @@ let termination_proof_header is_mes input_type ids args_id relation tclTHEN (Tactics.generalize [mkVar id]) (Proofview.V82.of_tactic (clear [id]))) )) ; - observe_tac (str "fix") (fix (Some hrec) (nargs+1)); + observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1))); h_intros args_id; Proofview.V82.of_tactic (Simple.intro wf_rec_arg); observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) diff --git a/printing/printer.ml b/printing/printer.ml index 401f5f99e9..4c8e806f43 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -685,18 +685,6 @@ let pr_prim_rule = function (str"cut " ++ pr_constr t ++ str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - | FixRule (f,n,[],_) -> - (str"fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others,j) -> - if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\""); - let rec print_mut = function - | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth - | [] -> mt () in - (str"fix " ++ pr_id f ++ str"/" ++ int n ++ - str" with " ++ print_mut others) - | Cofix (f,[],_) -> (str"cofix " ++ pr_id f) diff --git a/proofs/logic.ml b/proofs/logic.ml index df5a12473b..ec1b7ca869 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -543,51 +543,6 @@ let prim_refiner r sigma goal = let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) - | FixRule (f,n,rest,j) -> - let rec check_ind env k cl = - match kind_of_term (strip_outer_cast cl) with - | Prod (na,c1,b) -> - if Int.equal k 1 then - try - fst (find_inductive env sigma c1) - with Not_found -> - error "Cannot do a fixpoint on a non inductive type." - else - let open Context.Rel.Declaration in - check_ind (push_rel (LocalAssum (na,c1)) env) (k-1) b - | _ -> error "Not enough products." - in - let ((sp,_),u) = check_ind env n cl in - let firsts,lasts = List.chop j rest in - let all = firsts@(f,n,cl)::lasts in - let rec mk_sign sign = function - | (f,n,ar)::oth -> - let ((sp',_),u') = check_ind env n ar in - if not (eq_mind sp sp') then - error "Fixpoints should be on the same mutual inductive declaration."; - if !check && mem_named_context f (named_context_of_val sign) then - errorlabstrm "Logic.prim_refiner" - (str "Name " ++ pr_id f ++ str " already used in the environment"); - mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth - | [] -> - Evd.Monad.List.map (fun (_,_,c) sigma -> - let gl,ev,sig' = - Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in - (gl,ev),sig') - all sigma - in - let (gls_evs,sigma) = mk_sign sign all in - let (gls,evs) = List.split gls_evs in - let ids = List.map pi1 all in - let evs = List.map (Vars.subst_vars (List.rev ids)) evs in - let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in - let funnames = Array.of_list (List.map (fun i -> Name i) ids) in - let typarray = Array.of_list (List.map pi3 all) in - let bodies = Array.of_list evs in - let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in - let sigma = Goal.V82.partial_solution sigma goal oterm in - (gls,sigma) - | Cofix (f,others,j) -> let rec check_is_coind env cl = let b = whd_betadeltaiota env sigma cl in diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 48ad50c7a0..ea3b5242da 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -19,7 +19,6 @@ open Misctypes type prim_rule = | Cut of bool * bool * Id.t * types - | FixRule of Id.t * int * (Id.t * int * constr) list * int | Cofix of Id.t * (Id.t * constr) list * int | Refine of constr | Move of Id.t * Id.t move_location diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 67daccb81d..8eb8b2cec6 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -124,9 +124,6 @@ let refine_no_check c gl = let move_hyp_no_check id1 id2 gl = refiner (Move (id1,id2)) gl -let mutual_fix f n others j gl = - with_check (refiner (FixRule (f,n,others,j))) gl - let mutual_cofix f others j gl = with_check (refiner (Cofix (f,others,j))) gl diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index fef205f823..e2d8bfc6ef 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -86,8 +86,6 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool val refiner : rule -> tactic val internal_cut_no_check : bool -> Id.t -> types -> tactic val refine_no_check : constr -> tactic -val mutual_fix : - Id.t -> int -> (Id.t * int * constr) list -> int -> tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic (** {6 The most primitive tactics with consistency and type checking } *) diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 80b3fef196..8db8de9927 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -385,7 +385,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_ let rec_tac_initializer finite guard thms snl = if finite then match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with - | (id,_)::l -> Tactics.mutual_cofix id l 0 + | (id,_)::l -> Proofview.V82.tactic (Tactics.mutual_cofix id l 0) | _ -> assert false else (* nl is dummy: it will be recomputed at Qed-time *) @@ -403,7 +403,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = | Anonymous -> Tactics.intro) (List.rev ids) in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> - let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in + let rec_tac = rec_tac_initializer finite guard thms snl in Some (match init_tac with | None -> if Flags.is_auto_intros () then diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a47ee96a0a..01af30049b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -472,14 +472,69 @@ let assert_after_replacing id = assert_after_gen true (NamingMustBe (dloc,id)) (* Fixpoints and CoFixpoints *) (**************************************************************) +let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) with +| Prod (na, c1, b) -> + if Int.equal k 1 then + try + let ((sp, _), u), _ = find_inductive env sigma c1 in + (sp, u) + with Not_found -> error "Cannot do a fixpoint on a non inductive type." + else + let open Context.Rel.Declaration in + check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b +| _ -> error "Not enough products." + (* Refine as a fixpoint *) -let mutual_fix = Tacmach.mutual_fix +let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let concl = Proofview.Goal.concl gl in + let (sp, u) = check_mutind env sigma n concl in + let firsts, lasts = List.chop j rest in + let all = firsts @ (f, n, concl) :: lasts in + let rec mk_sign sign = function + | [] -> sign + | (f, n, ar) :: oth -> + let open Context.Named.Declaration in + let (sp', u') = check_mutind env sigma n ar in + if not (eq_mind sp sp') then + error "Fixpoints should be on the same mutual inductive declaration."; + if mem_named_context f (named_context_of_val sign) then + errorlabstrm "Logic.prim_refiner" + (str "Name " ++ pr_id f ++ str " already used in the environment"); + mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth + in + let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in + Refine.refine { run = begin fun sigma -> + let rec map : type r s. r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma = + fun sigma p -> function + | [] -> Sigma ([], sigma, p) + | (_, _, arg) :: rem -> + let Sigma (arg, sigma, q) = Evarutil.new_evar nenv sigma arg in + let Sigma (rem, sigma, r) = map sigma (p +> q) rem in + Sigma (arg :: rem, sigma, r) + in + let Sigma (evs, sigma, p) = map sigma Sigma.refl all in + let ids = List.map pi1 all in + let evs = List.map (Vars.subst_vars (List.rev ids)) evs in + let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in + let funnames = Array.of_list (List.map (fun i -> Name i) ids) in + let typarray = Array.of_list (List.map pi3 all) in + let bodies = Array.of_list evs in + let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in + Sigma (oterm, sigma, p) + end } +end } -let fix ido n gl = match ido with +let fix ido n = match ido with | None -> - mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] 0 gl + Proofview.Goal.enter { enter = begin fun gl -> + let name = Pfedit.get_current_proof_name () in + let id = new_fresh_id [] name gl in + mutual_fix id n [] 0 + end } | Some id -> - mutual_fix id n [] 0 gl + mutual_fix id n [] 0 (* Refine as a cofixpoint *) let mutual_cofix = Tacmach.mutual_cofix diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f6c001941c..47ff197a05 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -36,8 +36,8 @@ val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofvi val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic val mutual_fix : - Id.t -> int -> (Id.t * int * constr) list -> int -> tactic -val fix : Id.t option -> int -> tactic + Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic +val fix : Id.t option -> int -> unit Proofview.tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic val cofix : Id.t option -> tactic -- cgit v1.2.3 From 9ae9ac00b6882a9918eea3cb7d809424695d37ff Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 20:57:34 +0200 Subject: Put the "exact" family of tactic in the monad. --- ltac/coretactics.ml4 | 2 +- ltac/tacinterp.ml | 2 +- plugins/firstorder/rules.ml | 4 ++-- plugins/rtauto/refl_tauto.ml | 2 +- tactics/class_tactics.ml | 2 +- tactics/eauto.ml | 2 +- tactics/elim.ml | 2 +- tactics/equality.ml | 2 +- tactics/tactics.ml | 17 +++++++---------- tactics/tactics.mli | 2 +- 10 files changed, 17 insertions(+), 20 deletions(-) diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 98b77ab357..3849a84405 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -39,7 +39,7 @@ TACTIC EXTEND cut END TACTIC EXTEND exact_no_check - [ "exact_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.exact_no_check c) ] + [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ] END TACTIC EXTEND vm_cast_no_check diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 5e0153fcee..7acdff9acf 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1659,7 +1659,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Trace.name_tactic (fun () -> Pp.str"") begin Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let (sigma, c_interp) = pf_interp_casted_constr ist gl c in - Sigma.Unsafe.of_pair (Proofview.V82.tactic (Tactics.exact_no_check c_interp), sigma) + Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma) end } end | TacApply (a,ev,cb,cl) -> diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index f19cdd2ccc..d05e9484ab 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -58,7 +58,7 @@ let clear_global=function (* connection rules *) let axiom_tac t seq= - try pf_constr_of_global (find_left t seq) exact_no_check + try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c)) with Not_found->tclFAIL 0 (Pp.str "No axiom link") let ll_atom_tac a backtrack id continue seq= @@ -151,7 +151,7 @@ let ll_arrow_tac a b c backtrack id continue seq= clear_global id; wrap 1 false continue seq]; tclTHENS (Proofview.V82.of_tactic (cut cc)) - [pf_constr_of_global id exact_no_check; + [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c)); tclTHENLIST [pf_constr_of_global id (fun idc -> generalize [d idc]); clear_global id; diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 2f3a3e5514..73dc13e72e 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -316,7 +316,7 @@ let rtauto_tac gls= if !check then Proofview.V82.of_tactic (Tactics.exact_check term) gls else - Tactics.exact_no_check term gls in + Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in let tac_end_time = System.get_time () in let _ = if !check then msg_info (str "Proof term type-checking is on"); diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 4855598989..cfbcc47505 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -164,7 +164,7 @@ let e_give_exact flags poly (c,clenv) gl = else c, gl in let t1 = pf_unsafe_type_of gl c in - tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl + Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl let unify_e_resolve poly flags = { enter = begin fun gls (c,clenv) -> let clenv', c = connect_hint_clenv poly c clenv gls in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 6bbd9b2e8a..f0f408c24d 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -33,7 +33,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c = let t1 = Tacmach.New.pf_unsafe_type_of gl c in let t2 = Tacmach.New.pf_concl gl in if occur_existential t1 || occur_existential t2 then - Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c)) + Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) else exact_check c end } diff --git a/tactics/elim.ml b/tactics/elim.ml index 33eb80c280..d59c2fba49 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -84,7 +84,7 @@ let general_decompose recognizer c = (onLastHypId (ifOnHyp recognizer (general_decompose_aux recognizer) (fun id -> clear [id]))); - Proofview.V82.tactic (exact_no_check c) ] + exact_no_check c ] end } let head_in indl t gl = diff --git a/tactics/equality.ml b/tactics/equality.ml index eecc2b787c..572d4b7ab7 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1582,7 +1582,7 @@ let substClause l2r c cls = Proofview.Goal.enter { enter = begin fun gl -> let eq = pf_apply get_type_of gl c in tclTHENS (cutSubstClause l2r eq cls) - [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)] + [Proofview.tclUNIT (); exact_no_check c] end } let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 01af30049b..6bf5831f78 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1833,7 +1833,7 @@ let cut_and_apply c = (* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *) (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) -let new_exact_no_check c = +let exact_no_check c = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h } let exact_check c = @@ -1845,13 +1845,11 @@ let exact_check c = let sigma = Sigma.to_evar_map sigma in let sigma, ct = Typing.type_of env sigma c in let tac = - Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) + Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c) in Sigma.Unsafe.of_pair (tac, sigma) end } -let exact_no_check = Tacmach.refine_no_check - let vm_cast_no_check c gl = let concl = Tacmach.pf_concl gl in Tacmach.refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl @@ -2626,8 +2624,7 @@ let forward b usetac ipat c = Proofview.Goal.enter { enter = begin fun gl -> let t = Tacmach.New.pf_unsafe_type_of gl c in let hd = head_ident c in - Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) - (Proofview.V82.tactic (exact_no_check c)) + Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c) end } | Some tac -> if b then @@ -2820,14 +2817,14 @@ let specialize (c,lbind) = (Proofview.Unsafe.tclEVARS sigma) (Tacticals.New.tclTHENFIRST (assert_before_replacing id typ) - (new_exact_no_check term)) + (exact_no_check term)) | _ -> (* To deprecate in favor of generalize? *) Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tacticals.New.tclTHENLAST (cut typ) - (new_exact_no_check term)) + (exact_no_check term)) end } (*****************************) @@ -3652,7 +3649,7 @@ let specialize_eqs id gl = let ty' = Evarutil.nf_evar !evars ty' in if worked then tclTHENFIRST (Tacmach.internal_cut true id ty') - (exact_no_check ((* refresh_universes_strict *) acc')) gl + (Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl @@ -4798,7 +4795,7 @@ let abstract_subproof id gk tac = Entries.(snd (Future.force const.const_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> - new_exact_no_check (applist (lem, args)) + exact_no_check (applist (lem, args)) in let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in Sigma.Unsafe.of_pair (tac, evd) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 47ff197a05..2ffedf81ac 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -114,7 +114,7 @@ val intros_patterns : intro_patterns -> unit Proofview.tactic (** {6 Exact tactics. } *) val assumption : unit Proofview.tactic -val exact_no_check : constr -> tactic +val exact_no_check : constr -> unit Proofview.tactic val vm_cast_no_check : constr -> tactic val native_cast_no_check : constr -> tactic val exact_check : constr -> unit Proofview.tactic -- cgit v1.2.3 From 1394bab8ba40dd4714e941586109fd88a79ef653 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 21:14:12 +0200 Subject: Put the "*_cast_no_check" tactics in the monad. --- ltac/coretactics.ml4 | 4 ++-- tactics/tactics.ml | 16 +++++++++------- tactics/tactics.mli | 4 ++-- 3 files changed, 13 insertions(+), 11 deletions(-) diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 3849a84405..4893e40973 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -43,11 +43,11 @@ TACTIC EXTEND exact_no_check END TACTIC EXTEND vm_cast_no_check - [ "vm_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.vm_cast_no_check c) ] + [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ] END TACTIC EXTEND native_cast_no_check - [ "native_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.native_cast_no_check c) ] + [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ] END TACTIC EXTEND casetype diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6bf5831f78..dc018a6703 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1850,14 +1850,16 @@ let exact_check c = Sigma.Unsafe.of_pair (tac, sigma) end } -let vm_cast_no_check c gl = - let concl = Tacmach.pf_concl gl in - Tacmach.refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl - -let native_cast_no_check c gl = - let concl = Tacmach.pf_concl gl in - Tacmach.refine_no_check (Term.mkCast(c,Term.NATIVEcast,concl)) gl +let cast_no_check cast c = + Proofview.Goal.enter { enter = begin fun gl -> + let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + Refine.refine ~unsafe:true { run = begin fun sigma -> + Sigma.here (Term.mkCast (c, cast, concl)) sigma + end } + end } +let vm_cast_no_check c = cast_no_check Term.VMcast c +let native_cast_no_check c = cast_no_check Term.NATIVEcast c let exact_proof c = let open Tacmach.New in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 2ffedf81ac..12364d2110 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -115,8 +115,8 @@ val intros_patterns : intro_patterns -> unit Proofview.tactic val assumption : unit Proofview.tactic val exact_no_check : constr -> unit Proofview.tactic -val vm_cast_no_check : constr -> tactic -val native_cast_no_check : constr -> tactic +val vm_cast_no_check : constr -> unit Proofview.tactic +val native_cast_no_check : constr -> unit Proofview.tactic val exact_check : constr -> unit Proofview.tactic val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic -- cgit v1.2.3 From a4bd166bd2119a5290276f0ded44f8186ba1ecee Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 21:21:42 +0200 Subject: Put the "cofix" tactic in the monad. --- ltac/coretactics.ml4 | 4 +-- ltac/tacinterp.ml | 2 +- printing/printer.ml | 10 -------- proofs/logic.ml | 41 ------------------------------- proofs/proof_type.mli | 1 - proofs/tacmach.ml | 3 --- proofs/tacmach.mli | 1 - stm/lemmas.ml | 2 +- tactics/tactics.ml | 68 +++++++++++++++++++++++++++++++++++++++++---------- tactics/tactics.mli | 4 +-- 10 files changed, 61 insertions(+), 75 deletions(-) diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 4893e40973..766f0714d2 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -238,8 +238,8 @@ END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ] -| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ] + [ "cofix" ] -> [ Tactics.cofix None ] +| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ] END (* Clear *) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 7acdff9acf..5aff262aa5 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1729,7 +1729,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in - let tac = Proofview.V82.tactic (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0) in + let tac = Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0 in Sigma.Unsafe.of_pair (tac, sigma) end } end diff --git a/printing/printer.ml b/printing/printer.ml index 4c8e806f43..cb075c64fb 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -685,16 +685,6 @@ let pr_prim_rule = function (str"cut " ++ pr_constr t ++ str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - | Cofix (f,[],_) -> - (str"cofix " ++ pr_id f) - - | Cofix (f,others,j) -> - if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\""); - let rec print_mut = function - | (f,ar)::oth -> - (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) - | [] -> mt () in - (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) | Refine c -> str(if Termops.occur_meta c then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c diff --git a/proofs/logic.ml b/proofs/logic.ml index ec1b7ca869..36ae5554fe 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -543,47 +543,6 @@ let prim_refiner r sigma goal = let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) - | Cofix (f,others,j) -> - let rec check_is_coind env cl = - let b = whd_betadeltaiota env sigma cl in - match kind_of_term b with - | Prod (na,c1,b) -> let open Context.Rel.Declaration in - check_is_coind (push_rel (LocalAssum (na,c1)) env) b - | _ -> - try - let _ = find_coinductive env sigma b in () - with Not_found -> - error "All methods must construct elements in coinductive types." - in - let firsts,lasts = List.chop j others in - let all = firsts@(f,cl)::lasts in - List.iter (fun (_,c) -> check_is_coind env c) all; - let rec mk_sign sign = function - | (f,ar)::oth -> - (try - (let _ = lookup_named_val f sign in - error "Name already used in the environment.") - with - | Not_found -> - mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth) - | [] -> - Evd.Monad.List.map (fun (_,c) sigma -> - let gl,ev,sigma = - Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in - (gl,ev),sigma) - all sigma - in - let (gls_evs,sigma) = mk_sign sign all in - let (gls,evs) = List.split gls_evs in - let (ids,types) = List.split all in - let evs = List.map (Vars.subst_vars (List.rev ids)) evs in - let funnames = Array.of_list (List.map (fun i -> Name i) ids) in - let typarray = Array.of_list types in - let bodies = Array.of_list evs in - let oterm = Term.mkCoFix (0,(funnames,typarray,bodies)) in - let sigma = Goal.V82.partial_solution sigma goal oterm in - (gls,sigma) - | Refine c -> check_meta_variables c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index ea3b5242da..ef0d52b62d 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -19,7 +19,6 @@ open Misctypes type prim_rule = | Cut of bool * bool * Id.t * types - | Cofix of Id.t * (Id.t * constr) list * int | Refine of constr | Move of Id.t * Id.t move_location diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 8eb8b2cec6..8c0b4ba98a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -124,9 +124,6 @@ let refine_no_check c gl = let move_hyp_no_check id1 id2 gl = refiner (Move (id1,id2)) gl -let mutual_cofix f others j gl = - with_check (refiner (Cofix (f,others,j))) gl - (* Versions with consistency checks *) let internal_cut b d t = with_check (internal_cut_no_check b d t) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e2d8bfc6ef..182433cb3a 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -86,7 +86,6 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool val refiner : rule -> tactic val internal_cut_no_check : bool -> Id.t -> types -> tactic val refine_no_check : constr -> tactic -val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic (** {6 The most primitive tactics with consistency and type checking } *) diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 8db8de9927..ce5ef01699 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -385,7 +385,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_ let rec_tac_initializer finite guard thms snl = if finite then match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with - | (id,_)::l -> Proofview.V82.tactic (Tactics.mutual_cofix id l 0) + | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else (* nl is dummy: it will be recomputed at Qed-time *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index dc018a6703..c3d6a65eb8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -472,6 +472,14 @@ let assert_after_replacing id = assert_after_gen true (NamingMustBe (dloc,id)) (* Fixpoints and CoFixpoints *) (**************************************************************) +let rec mk_holes : type r s. _ -> r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma = +fun env sigma p -> function +| [] -> Sigma ([], sigma, p) +| arg :: rem -> + let Sigma (arg, sigma, q) = Evarutil.new_evar env sigma arg in + let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in + Sigma (arg :: rem, sigma, r) + let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) with | Prod (na, c1, b) -> if Int.equal k 1 then @@ -506,15 +514,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl -> in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in Refine.refine { run = begin fun sigma -> - let rec map : type r s. r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma = - fun sigma p -> function - | [] -> Sigma ([], sigma, p) - | (_, _, arg) :: rem -> - let Sigma (arg, sigma, q) = Evarutil.new_evar nenv sigma arg in - let Sigma (rem, sigma, r) = map sigma (p +> q) rem in - Sigma (arg :: rem, sigma, r) - in - let Sigma (evs, sigma, p) = map sigma Sigma.refl all in + let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl (List.map pi3 all) in let ids = List.map pi1 all in let evs = List.map (Vars.subst_vars (List.rev ids)) evs in let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in @@ -536,14 +536,56 @@ let fix ido n = match ido with | Some id -> mutual_fix id n [] 0 +let rec check_is_mutcoind env sigma cl = + let b = whd_betadeltaiota env sigma cl in + match kind_of_term b with + | Prod (na, c1, b) -> + let open Context.Rel.Declaration in + check_is_mutcoind (push_rel (LocalAssum (na,c1)) env) sigma b + | _ -> + try + let _ = find_coinductive env sigma b in () + with Not_found -> + error "All methods must construct elements in coinductive types." + (* Refine as a cofixpoint *) -let mutual_cofix = Tacmach.mutual_cofix +let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let concl = Proofview.Goal.concl gl in + let firsts,lasts = List.chop j others in + let all = firsts @ (f, concl) :: lasts in + List.iter (fun (_, c) -> check_is_mutcoind env sigma c) all; + let rec mk_sign sign = function + | [] -> sign + | (f, ar) :: oth -> + let open Context.Named.Declaration in + if mem_named_context f (named_context_of_val sign) then + error "Name already used in the environment."; + mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth + in + let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in + Refine.refine { run = begin fun sigma -> + let (ids, types) = List.split all in + let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl types in + let evs = List.map (Vars.subst_vars (List.rev ids)) evs in + let funnames = Array.of_list (List.map (fun i -> Name i) ids) in + let typarray = Array.of_list types in + let bodies = Array.of_list evs in + let oterm = Term.mkCoFix (0, (funnames, typarray, bodies)) in + Sigma (oterm, sigma, p) + end } +end } -let cofix ido gl = match ido with +let cofix ido = match ido with | None -> - mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] 0 gl + Proofview.Goal.enter { enter = begin fun gl -> + let name = Pfedit.get_current_proof_name () in + let id = new_fresh_id [] name gl in + mutual_cofix id [] 0 + end } | Some id -> - mutual_cofix id [] 0 gl + mutual_cofix id [] 0 (**************************************************************) (* Reduction and conversion tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 12364d2110..f730dd6c40 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -38,8 +38,8 @@ val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic val fix : Id.t option -> int -> unit Proofview.tactic -val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic -val cofix : Id.t option -> tactic +val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic +val cofix : Id.t option -> unit Proofview.tactic val convert : constr -> constr -> unit Proofview.tactic val convert_leq : constr -> constr -> unit Proofview.tactic -- cgit v1.2.3 From b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 21:41:55 +0200 Subject: Put the "generalize" tactic in the monad. --- ltac/extratactics.ml4 | 2 +- ltac/tacinterp.ml | 2 +- plugins/decl_mode/decl_proof_instr.ml | 6 +-- plugins/firstorder/instances.ml | 8 ++-- plugins/firstorder/rules.ml | 8 ++-- plugins/funind/functional_principles_proofs.ml | 10 ++--- plugins/funind/invfun.ml | 10 ++--- plugins/funind/recdef.ml | 6 +-- plugins/micromega/coq_micromega.ml | 8 ++-- plugins/nsatz/g_nsatz.ml4 | 2 +- plugins/omega/coq_omega.ml | 58 +++++++++++++------------- plugins/romega/refl_omega.ml | 4 +- tactics/eqdecide.ml | 2 +- tactics/tactics.ml | 18 ++++---- tactics/tactics.mli | 5 +-- 15 files changed, 73 insertions(+), 76 deletions(-) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 1f3eb13355..e03cc675e7 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -728,7 +728,7 @@ let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in Tacticals.New.tclTHENLIST - [Proofview.V82.tactic (Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); + [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 5aff262aa5..7ec1b2ca0c 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1755,7 +1755,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Tacticals.New.tclWITHHOLES false (name_atomic ~env (TacGeneralize cl) - (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma + (Tactics.generalize_gen cl)) sigma end } | TacLetTac (na,c,clp,b,eqpat) -> Proofview.V82.nf_evar_goals <*> diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index a6b3381648..de06af0053 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1289,7 +1289,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = (fun id -> hrec_for (out_name fix_name) per_info gls1 id) recs in - generalize hrecs gls1 + Proofview.V82.of_tactic (generalize hrecs) gls1 end; match bro with None -> @@ -1365,7 +1365,7 @@ let end_tac et2 gls = (default_justification (List.map mkVar clauses)) | ET_Induction,EK_nodep -> tclTHENLIST - [generalize (pi.per_args@[pi.per_casee]); + [Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])); Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args)))); default_justification (List.map mkVar clauses)] | ET_Case_analysis,EK_dep tree -> @@ -1377,7 +1377,7 @@ let end_tac et2 gls = (initial_instance_stack clauses) [pi.per_casee] 0 tree | ET_Induction,EK_dep tree -> let nargs = (List.length pi.per_args) in - tclTHEN (generalize (pi.per_args@[pi.per_casee])) + tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]))) begin fun gls0 -> let fix_id = diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 0e2a40245b..5eff2f2774 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -135,9 +135,9 @@ let left_instance_tac (inst,id) continue seq= [tclTHENLIST [Proofview.V82.of_tactic introf; pf_constr_of_global id (fun idc -> - (fun gls->generalize + (fun gls-> Proofview.V82.of_tactic (generalize [mkApp(idc, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls)); + [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls)); Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; @@ -158,10 +158,10 @@ let left_instance_tac (inst,id) continue seq= try Typing.type_of (pf_env gl) evmap gt with e when Errors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in - tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl) + tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl) else pf_constr_of_global id (fun idc -> - generalize [mkApp(idc,[|t|])]) + Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])])) in tclTHENLIST [special_generalize; diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index d05e9484ab..92b6e828e8 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -67,7 +67,7 @@ let ll_atom_tac a backtrack id continue seq= tclTHENLIST [pf_constr_of_global (find_left a seq) (fun left -> pf_constr_of_global id (fun id -> - generalize [mkApp(id, [|left|])])); + Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])]))); clear_global id; Proofview.V82.of_tactic intro] with Not_found->tclFAIL 0 (Pp.str "No link")) @@ -135,7 +135,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= let newhyps idc =List.init lp (myterm idc) in tclIFTHENELSE (tclTHENLIST - [pf_constr_of_global id (fun idc -> generalize (newhyps idc)); + [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc))); clear_global id; tclDO lp (Proofview.V82.of_tactic intro)]) (wrap lp false continue seq) backtrack gl @@ -153,7 +153,7 @@ let ll_arrow_tac a b c backtrack id continue seq= tclTHENS (Proofview.V82.of_tactic (cut cc)) [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c)); tclTHENLIST - [pf_constr_of_global id (fun idc -> generalize [d idc]); + [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc])); clear_global id; Proofview.V82.of_tactic introf; Proofview.V82.of_tactic introf; @@ -192,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq= (fun gls-> let id0=pf_nth_hyp_id gls 1 in let term=mkApp(idc,[|mkVar(id0)|]) in - tclTHEN (generalize [term]) (Proofview.V82.of_tactic (clear [id0])) gls)); + tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls)); clear_global id; Proofview.V82.of_tactic intro; tclCOMPLETE (wrap 1 false continue (deepen seq))]; diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 0b7a1e6468..879145c2fa 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -704,7 +704,7 @@ let build_proof in tclTHENSEQ [ - generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); + Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps))); thin dyn_infos.rec_hyps; Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None); (fun g -> observe_tac "toto" ( @@ -934,7 +934,7 @@ let generalize_non_dep hyp g = in (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *) tclTHEN - ((* observe_tac "h_generalize" *) (generalize (List.map mkVar to_revert) )) + ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize (List.map mkVar to_revert) ))) ((* observe_tac "thin" *) (thin to_revert)) g @@ -942,7 +942,7 @@ let id_of_decl decl = Nameops.out_name (get_name decl) let var_of_decl decl = mkVar (id_of_decl decl) let revert idl = tclTHEN - (generalize (List.map mkVar idl)) + (Proofview.V82.of_tactic (generalize (List.map mkVar idl))) (thin idl) let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num = @@ -1564,7 +1564,7 @@ let prove_principle_for_gen Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) in let revert l = - tclTHEN (Tactics.generalize (List.map mkVar l)) (Proofview.V82.of_tactic (clear l)) + tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l)) in let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = @@ -1610,7 +1610,7 @@ let prove_principle_for_gen in tclTHENSEQ [ - generalize [lemma]; + Proofview.V82.of_tactic (generalize [lemma]); Proofview.V82.of_tactic (Simple.intro hid); Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)); (fun g -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index fde1b7e707..72529fbbe3 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -465,7 +465,7 @@ let generalize_dependent_of x hyp g = tclMAP (function | LocalAssum (id,t) when not (Id.equal id hyp) && - (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id]) + (Termops.occur_var (pf_env g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id]) | _ -> tclIDTAC ) (pf_hyps g) @@ -715,7 +715,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = }) Locusops.onConcl) ; - generalize (List.map mkVar ids); + Proofview.V82.of_tactic (generalize (List.map mkVar ids)); thin ids ] else @@ -754,7 +754,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = tclTHENSEQ [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]); observe_tac "h_generalize" - (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); + (Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)])); Proofview.V82.of_tactic (Simple.intro graph_principle_id); observe_tac "" (tclTHEN_i (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) @@ -937,7 +937,7 @@ let revert_graph kn post_tac hid g = let f_args,res = Array.chop (Array.length args - 1) args in tclTHENSEQ [ - generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; + Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]); thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); post_tac hid @@ -981,7 +981,7 @@ let functional_inversion kn hid fconst f_correct : tactic = in tclTHENSEQ[ pre_tac hid; - generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; + Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]); thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid)); diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c1c3801b45..10f08d3d13 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -689,7 +689,7 @@ let mkDestructEq : to_revert_constr in pf_typel new_hyps (fun _ -> observe_tclTHENLIST (str "mkDestructEq") - [generalize new_hyps; + [Proofview.V82.of_tactic (generalize new_hyps); (fun g2 -> let changefun patvars = { run = fun sigma -> let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in @@ -1116,7 +1116,7 @@ let termination_proof_header is_mes input_type ids args_id relation [observe_tac (str "generalize") (onNLastHypsId (nargs+1) (tclMAP (fun id -> - tclTHEN (Tactics.generalize [mkVar id]) (Proofview.V82.of_tactic (clear [id]))) + tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id]))) )) ; observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1))); @@ -1306,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in observe_tclTHENLIST (str "") [ - generalize [lemma]; + Proofview.V82.of_tactic (generalize [lemma]); Proofview.V82.of_tactic (Simple.intro hid); (fun g -> let ids = pf_ids_of_hyps g in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 5c0a8226a7..0fcfbfc711 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1464,7 +1464,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* ] (Tacmach.pf_concl gl)) ; - Tactics.new_generalize env ; + Tactics.generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] end } @@ -1726,7 +1726,7 @@ let micromega_gen | Some (ids,ff',res') -> (Tacticals.New.tclTHENLIST [ - Tactics.new_generalize (List.map Term.mkVar ids) ; + Tactics.generalize (List.map Term.mkVar ids) ; micromega_order_change spec res' (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff' ]) @@ -1774,7 +1774,7 @@ let micromega_order_changer cert env ff = ("__wit", cert, cert_typ) ] (Tacmach.pf_concl gl))); - Tactics.new_generalize env ; + Tactics.generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] end } @@ -1812,7 +1812,7 @@ let micromega_genr prover = (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in (Tacticals.New.tclTHENLIST [ - Tactics.new_generalize (List.map Term.mkVar ids) ; + Tactics.generalize (List.map Term.mkVar ids) ; micromega_order_changer res' env (abstract_wrt_formula ff' ff) ]) with diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 0da6305304..5f906a8dad 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -13,5 +13,5 @@ DECLARE PLUGIN "nsatz_plugin" DECLARE PLUGIN "nsatz_plugin" TACTIC EXTEND nsatz_compute -| [ "nsatz_compute" constr(lt) ] -> [ Proofview.V82.tactic (Nsatz.nsatz_compute lt) ] +| [ "nsatz_compute" constr(lt) ] -> [ Nsatz.nsatz_compute lt ] END diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index fc50540805..ab33a5d2c6 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1067,12 +1067,12 @@ let replay_history tactic_normalisation = let p_initial = [P_APP 1;P_TYPE] in let tac= shuffle_mult_right p_initial e1.body k e2.body in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + generalize_tac [mkApp (Lazy.force coq_OMEGA17, [| val_of eq1; val_of eq2; mk_integer k; - mkVar id1; mkVar id2 |])]); + mkVar id1; mkVar id2 |])]; Proofview.V82.tactic (mk_then tac); (intros_using [aux]); Proofview.V82.tactic (resolve_id aux); @@ -1104,7 +1104,7 @@ let replay_history tactic_normalisation = mkVar (hyp_of_tag e1.id); mkVar (hyp_of_tag e2.id) |]) in - Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (generalize_tac [theorem]) (mk_then tac))) (solve_le) + Proofview.tclTHEN (Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (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) @@ -1119,7 +1119,7 @@ let replay_history tactic_normalisation = [ Tacticals.New.tclTHENS (Tacticals.New.tclTHENLIST [ (intros_using [aux]); - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_OMEGA1, [| eq1; rhs; mkVar aux; mkVar id |])]); (clear [aux;id]); @@ -1129,9 +1129,9 @@ let replay_history tactic_normalisation = (cut (mk_gt kk izero)) [ Tacticals.New.tclTHENLIST [ (intros_using [aux1; aux2]); - (Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_Zmult_le_approx, - [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])])); + [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]); (clear [aux1;aux2;id]); (intros_using [id]); (loop l) ]; @@ -1157,7 +1157,7 @@ let replay_history tactic_normalisation = [ Tacticals.New.tclTHENS (cut (mk_gt kk dd)) [Tacticals.New.tclTHENLIST [ (intros_using [aux2;aux1]); - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_OMEGA4, [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]); (clear [aux1;aux2]); @@ -1187,7 +1187,7 @@ let replay_history tactic_normalisation = (cut state_eq) [Tacticals.New.tclTHENLIST [ (intros_using [aux1]); - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_OMEGA18, [| eq1;eq2;kk;mkVar aux1; mkVar id |])]); (clear [aux1;id]); @@ -1202,7 +1202,7 @@ let replay_history tactic_normalisation = (cut (mk_gt kk izero)) [Tacticals.New.tclTHENLIST [ (intros_using [aux2;aux1]); - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_OMEGA3, [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]); (clear [aux1;aux2;id]); @@ -1229,7 +1229,7 @@ let replay_history tactic_normalisation = (cut (mk_eq eq1 (mk_inv eq2))) [Tacticals.New.tclTHENLIST [ (intros_using [aux]); - Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_OMEGA8, + (generalize_tac [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]); (clear [id1;id2;aux]); (intros_using [id]); @@ -1265,7 +1265,7 @@ let replay_history tactic_normalisation = (elim_id aux); (clear [aux]); (intros_using [vid; aux]); - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_OMEGA9, [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]); Proofview.V82.tactic (mk_then tac); @@ -1304,7 +1304,7 @@ let replay_history tactic_normalisation = 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 Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]); Proofview.V82.tactic (mk_then tac); (intros_using [id]); @@ -1320,7 +1320,7 @@ let replay_history tactic_normalisation = (cut (mk_gt kk2 izero)) [Tacticals.New.tclTHENLIST [ (intros_using [aux2;aux1]); - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_OMEGA7, [| eq1;eq2;kk1;kk2; mkVar aux1;mkVar aux2; @@ -1338,12 +1338,12 @@ let replay_history tactic_normalisation = simpl_in_concl; reflexivity ] ] | CONSTANT_NOT_NUL(e,k) :: l -> - Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl + Tacticals.New.tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl | CONSTANT_NUL(e) :: l -> Tacticals.New.tclTHEN (Proofview.V82.tactic (resolve_id (hyp_of_tag e))) reflexivity | CONSTANT_NEG(e,k) :: l -> Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]); + (generalize_tac [mkVar (hyp_of_tag e)]); unfold sp_Zle; simpl_in_concl; unfold sp_not; @@ -1366,7 +1366,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) = let (tac,t') = normalize p_initial t in let shift_left = tclTHEN - (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ]) + (Proofview.V82.of_tactic (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])) (tclTRY (Proofview.V82.of_tactic (clear [id]))) in if not (List.is_empty tac) then @@ -1546,7 +1546,7 @@ let nat_inject = begin try match destructurate_prop t with Kapp(Le,[t1;t2]) -> Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (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); @@ -1555,7 +1555,7 @@ let nat_inject = ] | Kapp(Lt,[t1;t2]) -> Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (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); @@ -1564,7 +1564,7 @@ let nat_inject = ] | Kapp(Ge,[t1;t2]) -> Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (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); @@ -1573,7 +1573,7 @@ let nat_inject = ] | Kapp(Gt,[t1;t2]) -> Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (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); @@ -1582,7 +1582,7 @@ let nat_inject = ] | Kapp(Neq,[t1;t2]) -> Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (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); @@ -1592,7 +1592,7 @@ let nat_inject = | Kapp(Eq,[typ;t1;t2]) -> if is_conv typ (Lazy.force coq_nat) then Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (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); @@ -1723,7 +1723,7 @@ let destructure_hyps = then let d1 = decidability t1 in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp, + (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| t1; t2; d1; mkVar i|])]); (onClearedName i (fun i -> (loop (LocalAssum (i,mk_or (mk_not t1) t2) :: lit)))) @@ -1734,7 +1734,7 @@ let destructure_hyps = begin match destructurate_prop t with Kapp(Or,[t1;t2]) -> Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]); (onClearedName i (fun i -> (loop (LocalAssum (i,mk_and (mk_not t1) (mk_not t2)) :: lit)))) @@ -1742,7 +1742,7 @@ let destructure_hyps = | Kapp(And,[t1;t2]) -> let d1 = decidability t1 in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_not_and, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> @@ -1752,7 +1752,7 @@ let destructure_hyps = let d1 = decidability t1 in let d2 = decidability t2 in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_not_iff, [| t1; t2; d1; d2; mkVar i |])]); (onClearedName i (fun i -> @@ -1764,7 +1764,7 @@ let destructure_hyps = For t1, being decidable implies being Prop. *) let d1 = decidability t1 in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_not_imp, [| t1; t2; d1; mkVar i |])]); (onClearedName i (fun i -> @@ -1773,7 +1773,7 @@ let destructure_hyps = | Kapp(Not,[t]) -> let d = decidability t in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]); (onClearedName i (fun i -> (loop (LocalAssum (i,t) :: lit)))) ] @@ -1781,7 +1781,7 @@ let destructure_hyps = (try let thm = not_binop op in Tacticals.New.tclTHENLIST [ - Proofview.V82.tactic (generalize_tac + (generalize_tac [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]); (onClearedName i (fun _ -> loop lit)) ] diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 177c870b3c..dca46cbcf7 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1280,8 +1280,8 @@ let resolution env full_reified_goal systems_list = CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in let decompose_tactic = decompose_tree env context solution_tree in - Tactics.generalize - (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >> + Proofview.V82.of_tactic (Tactics.generalize + (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >> Proofview.V82.of_tactic (Tactics.change_concl reified) >> Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 01ebaa7b72..b1d3290aac 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -64,7 +64,7 @@ let choose_noteq eqonleft = let mkBranches c1 c2 = tclTHENLIST - [Proofview.V82.tactic (generalize [c2]); + [generalize [c2]; Simple.elim c1; intros; onLastHyp Simple.case; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c3d6a65eb8..d4589154f8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2766,14 +2766,15 @@ let generalize_dep ?(with_let=false) c gl = gl (** *) -let generalize_gen_let lconstr gl = +let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let newcl, evd = - List.fold_right_i (generalize_goal gl) 0 lconstr - (Tacmach.pf_concl gl,Tacmach.project gl) + List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr + (Tacmach.New.pf_concl gl,Tacmach.New.project gl) in - Proofview.V82.of_tactic (Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) - (apply_type newcl (List.map_filter (fun ((_,c,b),_) -> - if Option.is_empty b then Some c else None) lconstr))) gl + let map ((_, c, b),_) = if Option.is_empty b then Some c else None in + let tac = apply_type newcl (List.map_filter map lconstr) in + Sigma.Unsafe.of_pair (tac, evd) +end } let new_generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl -> @@ -2809,11 +2810,8 @@ let generalize_gen lconstr = let new_generalize_gen lconstr = new_generalize_gen_let (List.map (fun ((occs,c),na) -> (occs,c,None),na) lconstr) - -let generalize l = - generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l) -let new_generalize l = +let generalize l = new_generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l) (* Faudra-t-il une version avec plusieurs args de generalize_dep ? diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f730dd6c40..9d02d3f6d3 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -383,10 +383,9 @@ val letin_pat_tac : (bool * intro_pattern_naming) option -> (** {6 Generalize tactics. } *) -val generalize : constr list -> tactic -val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic +val generalize : constr list -> unit Proofview.tactic +val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> unit Proofview.tactic -val new_generalize : constr list -> unit Proofview.tactic val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic -- cgit v1.2.3 From c6a16e8cc607f70f519f3ebbd5856b8ff501d782 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 22:18:12 +0200 Subject: Put the "generalize dependent" tactic in the monad. --- ltac/coretactics.ml4 | 2 +- tactics/tactics.ml | 9 ++++++--- tactics/tactics.mli | 2 +- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 766f0714d2..b7fc63cd56 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -261,7 +261,7 @@ END (* Generalize dependent *) TACTIC EXTEND generalize_dependent - [ "generalize" "dependent" constr(c) ] -> [ Proofview.V82.tactic (Tactics.generalize_dep c) ] + [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ] END (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d4589154f8..547c361642 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2727,7 +2727,7 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = let sigma, t = Typing.type_of env sigma c in generalize_goal_gen env sigma ids i o t cl -let generalize_dep ?(with_let=false) c gl = +let old_generalize_dep ?(with_let=false) c gl = let open Context.Named.Declaration in let env = pf_env gl in let sign = pf_hyps gl in @@ -2765,6 +2765,9 @@ let generalize_dep ?(with_let=false) c gl = Proofview.V82.of_tactic (clear (List.rev tothin'))] gl +let generalize_dep ?(with_let = false) c = + Proofview.V82.tactic (old_generalize_dep ~with_let c) + (** *) let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let newcl, evd = @@ -3627,7 +3630,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = Tacticals.New.tclTHENLIST [ tac; rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro; - Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))] + generalize_dep ~with_let:true (mkVar oldid)] else Tacticals.New.tclTHENLIST [ tac; clear [id]; @@ -3638,7 +3641,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = (Tacticals.New.tclFIRST [revert vars ; Proofview.V82.tactic (fun gl -> tclMAP (fun id -> - tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)]) + tclTRY (Proofview.V82.of_tactic (generalize_dep ~with_let:true (mkVar id)))) vars gl)]) end } let rec compare_upto_variables x y = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 9d02d3f6d3..eb041e2a0b 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -388,7 +388,7 @@ val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> unit Proo val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic -val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic +val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> unit Proofview.tactic (** {6 Other tactics. } *) -- cgit v1.2.3 From fd5898afa9a89ca61f87cdeca4ae982a024e4d4b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 22:24:45 +0200 Subject: Put the "specialize_eq" tactic in the monad. --- ltac/extratactics.ml4 | 2 +- tactics/tactics.ml | 13 ++++++------- tactics/tactics.mli | 2 +- 3 files changed, 8 insertions(+), 9 deletions(-) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e03cc675e7..451e0987b0 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -582,7 +582,7 @@ END during dependent induction. For internal use. *) TACTIC EXTEND specialize_eqs -[ "specialize_eqs" hyp(id) ] -> [ Proofview.V82.tactic (specialize_eqs id) ] +[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ] END (**********************************************************************) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 547c361642..59e6a1c82a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3698,13 +3698,12 @@ let specialize_eqs id gl = else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl -let specialize_eqs id gl = - if - (try ignore(Proofview.V82.of_tactic (clear [id]) gl); false - with e when Errors.noncritical e -> true) - then - tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl - else specialize_eqs id gl +let specialize_eqs id = Proofview.Goal.nf_enter { enter = begin fun gl -> + let msg = str "Specialization not allowed on dependent hypotheses" in + Proofview.tclOR (clear [id]) + (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () -> + Proofview.V82.tactic (specialize_eqs id) +end } let occur_rel n c = let res = not (noccurn n c) in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index eb041e2a0b..6987e5b70e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -397,7 +397,7 @@ val unify : ?state:Names.transparent_state -> constr -> constr -> unit val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic -val specialize_eqs : Id.t -> tactic +val specialize_eqs : Id.t -> unit Proofview.tactic val general_rewrite_clause : (bool -> evars_flag -> constr with_bindings -> clause -> unit Proofview.tactic) Hook.t -- cgit v1.2.3 From ed1c4d01388bf11710b38f1c302d405233c24647 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 22:58:07 +0200 Subject: Put the "change" tactic in the monad. --- ltac/tacinterp.ml | 37 +++++++++++++++++-------------------- tactics/tactics.ml | 10 ++++++---- tactics/tactics.mli | 2 +- 3 files changed, 24 insertions(+), 25 deletions(-) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 7ec1b2ca0c..5d282a6936 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1879,7 +1879,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in Sigma.Unsafe.of_pair (c, sigma) end } in - Proofview.V82.tactic (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)) + Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl) end } end | TacChange (Some op,c,cl) -> @@ -1889,25 +1889,22 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - Proofview.V82.tactic begin fun gl -> - let op = interp_typed_pattern ist env sigma op in - let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in - let c_interp patvars = { Sigma.run = begin fun sigma -> - let lfun' = Id.Map.fold (fun id c lfun -> - Id.Map.add id (Value.of_constr c) lfun) - patvars ist.lfun - in - let ist = { ist with lfun = lfun' } in - try - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_constr ist env sigma c in - Sigma.Unsafe.of_pair (c, sigma) - with e when to_catch e (* Hack *) -> - errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") - end } in - (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) - gl - end + let op = interp_typed_pattern ist env sigma op in + let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in + let c_interp patvars = { Sigma.run = begin fun sigma -> + let lfun' = Id.Map.fold (fun id c lfun -> + Id.Map.add id (Value.of_constr c) lfun) + patvars ist.lfun + in + let ist = { ist with lfun = lfun' } in + try + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = interp_constr ist env sigma c in + Sigma.Unsafe.of_pair (c, sigma) + with e when to_catch e (* Hack *) -> + errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") + end } in + Tactics.change (Some op) c_interp (interp_clause ist env sigma cl) end } end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 59e6a1c82a..83b8aacfea 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -825,14 +825,16 @@ let change_option occl t = function | Some id -> change_in_hyp occl t id | None -> change_in_concl occl t -let change chg c cls gl = - let cls = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps gl) cls in - Proofview.V82.of_tactic (Tacticals.New.tclMAP (function +let change chg c cls = + Proofview.Goal.enter { enter = begin fun gl -> + let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in + Tacticals.New.tclMAP (function | OnHyp (id,occs,where) -> change_option (bind_change_occurrences occs chg) c (Some (id,where)) | OnConcl occs -> change_option (bind_change_occurrences occs chg) c None) - cls) gl + cls + end } let change_concl t = change_in_concl None (make_change_arg t) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6987e5b70e..046a15d148 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -154,7 +154,7 @@ val unfold_in_hyp : val unfold_option : (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic val change : - constr_pattern option -> change_arg -> clause -> tactic + constr_pattern option -> change_arg -> clause -> unit Proofview.tactic val pattern_option : (occurrences * constr) list -> goal_location -> unit Proofview.tactic val reduce : red_expr -> clause -> unit Proofview.tactic -- cgit v1.2.3 From cddddce068bc0482f62ffab8e412732a307b90bb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 May 2016 10:47:53 +0200 Subject: Put the "move" tactic in the monad. --- ltac/coretactics.ml4 | 8 ++++---- tactics/tactics.ml | 11 +++++------ tactics/tactics.mli | 2 +- 3 files changed, 10 insertions(+), 11 deletions(-) diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index b7fc63cd56..ce28eacc09 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -200,10 +200,10 @@ END (** Move *) TACTIC EXTEND move - [ "move" hyp(id) "at" "top" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveFirst) ] -| [ "move" hyp(id) "at" "bottom" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveLast) ] -| [ "move" hyp(id) "after" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveAfter h)) ] -| [ "move" hyp(id) "before" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveBefore h)) ] + [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ] +| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ] +| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ] +| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ] END (** Revert *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 83b8aacfea..15f465ae2b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -313,7 +313,7 @@ let apply_clear_request clear_flag dft c = else Tacticals.New.tclIDTAC (* Moving hypotheses *) -let move_hyp id dest gl = Tacmach.move_hyp id dest gl +let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest) (* Renaming hypotheses *) let rename_hyp repl = @@ -908,9 +908,8 @@ let find_intro_names ctxt gl = let build_intro_tac id dest tac = match dest with | MoveLast -> Tacticals.New.tclTHEN (introduction id) (tac id) | dest -> Tacticals.New.tclTHENLIST - [introduction id; - Proofview.V82.tactic (move_hyp id dest); tac id] - + [introduction id; move_hyp id dest; tac id] + let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let open Context.Rel.Declaration in Proofview.Goal.enter { enter = begin fun gl -> @@ -1011,7 +1010,7 @@ let intro_replacing id = Tacticals.New.tclTHENLIST [ clear_for_replacing [id]; introduction id; - Proofview.V82.tactic (move_hyp id next_hyp); + move_hyp id next_hyp; ] end } @@ -2437,7 +2436,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with and prepare_intros_loc loc dft destopt = function | IntroNaming ipat -> prepare_naming loc ipat, - (fun id -> Proofview.V82.tactic (move_hyp id destopt)) + (fun id -> move_hyp id destopt) | IntroAction ipat -> prepare_naming loc dft, (let tac thin bound = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 046a15d148..24aca2a689 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -170,7 +170,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic val specialize : constr with_bindings -> unit Proofview.tactic -val move_hyp : Id.t -> Id.t move_location -> tactic +val move_hyp : Id.t -> Id.t move_location -> unit Proofview.tactic val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic val revert : Id.t list -> unit Proofview.tactic -- cgit v1.2.3 From 43343c1f79d9f373104ae5174baf41e2257e2b8d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 May 2016 11:02:58 +0200 Subject: Removing the old refine tactic from the Tactics module. It is indeed confusing, as it has little to do with the proper refine defined in the New submodule. Legacy code relying on it should call the Logic or Tacmach modules instead. --- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/omega/coq_omega.ml | 4 ++-- tactics/equality.ml | 6 +++--- tactics/tactics.mli | 1 - 4 files changed, 6 insertions(+), 7 deletions(-) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index de06af0053..be6ce59bd3 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -485,7 +485,7 @@ let thus_tac c ctyp submetas gls = Proofview.V82.of_tactic (exact_check proof) gls else let refiner = concl_refiner list proof gls in - Tactics.refine refiner gls + Tacmach.refine refiner gls (* general forward step *) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ab33a5d2c6..0bf30e7fd8 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -150,7 +150,7 @@ let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) let generalize_tac t = generalize t let elim t = simplest_elim t -let exact t = Tactics.refine t +let exact t = Tacmach.refine t let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] let rev_assoc k = @@ -1847,7 +1847,7 @@ let destructure_goal = try let dec = decidability t in Tacticals.New.tclTHEN - (Proofview.V82.tactic (Tactics.refine + (Proofview.V82.tactic (Tacmach.refine (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))) intro with Undecidable -> Tactics.elim_type (build_coq_False ()) diff --git a/tactics/equality.ml b/tactics/equality.ml index 572d4b7ab7..12d31d0f31 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -974,7 +974,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS eff <*> tclTHENS (assert_after Anonymous absurd_term) - [onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))] + [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in @@ -1316,7 +1316,7 @@ let inject_if_homogenous_dependent_pair ty = onLastHyp (fun hyp -> tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar hyp]; - Proofview.V82.tactic (refine + Proofview.V82.tactic (Tacmach.refine (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) ])] with Exit -> @@ -1362,7 +1362,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) [inject_if_homogenous_dependent_pair ty; - Proofview.V82.tactic (refine pf)]) + Proofview.V82.tactic (Tacmach.refine pf)]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 24aca2a689..df41951c32 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -30,7 +30,6 @@ val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) val introduction : ?check:bool -> Id.t -> unit Proofview.tactic -val refine : constr -> tactic val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic -- cgit v1.2.3 From dadd4003b6607ccc103658f842b5efbd6d8ab57f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 May 2016 20:50:47 +0200 Subject: Removing some compatibility layers in Tactics. --- proofs/logic.ml | 6 ++--- tactics/tactics.ml | 70 +++++++++++++++++++++++++++++------------------------- 2 files changed, 40 insertions(+), 36 deletions(-) diff --git a/proofs/logic.ml b/proofs/logic.ml index 36ae5554fe..fd8a70c650 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -77,10 +77,10 @@ let with_check = Flags.with_option check (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and returns [tail::(f head (id,_,_) (rev tail))] *) -let apply_to_hyp sign id f = +let apply_to_hyp check sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if !check then error_no_such_hypothesis id + if check then error_no_such_hypothesis id else sign let check_typability env sigma c = @@ -493,7 +493,7 @@ let convert_hyp check sign sigma d = let env = Global.env() in let reorder = ref [] in let sign' = - apply_to_hyp sign id + apply_to_hyp check sign id (fun _ d' _ -> let _,c,ct = to_tuple d' in let env = Global.env_of_context sign in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 15f465ae2b..15e9d3a943 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -708,11 +708,11 @@ let pf_e_reduce_decl redfun where decl gl = let Sigma (ty', sigma, q) = if where != InHypValueOnly then redfun sigma ty else Sigma.here ty sigma in Sigma (LocalDef (id, b', ty'), sigma, p +> q) -let e_reduct_in_concl (redfun, sty) = +let e_reduct_in_concl ~check (redfun, sty) = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in - Sigma (convert_concl_no_check c' sty, sigma, p) + Sigma (convert_concl ~check c' sty, sigma, p) end } let e_reduct_in_hyp ?(check=false) redfun (id, where) = @@ -723,7 +723,7 @@ let e_reduct_in_hyp ?(check=false) redfun (id, where) = let e_reduct_option ?(check=false) redfun = function | Some id -> e_reduct_in_hyp ~check (fst redfun) id - | None -> e_reduct_in_concl (revert_cast redfun) + | None -> e_reduct_in_concl ~check (revert_cast redfun) (** Versions with evars to maintain the unification of universes resulting from conversions. *) @@ -873,10 +873,9 @@ let reduce redexp cl = let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in let redexps = reduction_clause redexp cl in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in - let tac = Tacticals.New.tclMAP (fun (where,redexp) -> + Tacticals.New.tclMAP (fun (where,redexp) -> e_reduct_option ~check - (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps in - if check then Proofview.V82.tactic (fun gl -> with_check (Proofview.V82.of_tactic tac) gl) else tac (** FIXME *) + (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps end } (* Unfolding occurrences of a constant *) @@ -1097,10 +1096,14 @@ let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) let intros_until = intros_until_gen true let intros_until_n = intros_until_n_gen true -let tclCHECKVAR id gl = ignore (Tacmach.pf_get_hyp gl id); tclIDTAC gl +let tclCHECKVAR id = + Proofview.Goal.enter { enter = begin fun gl -> + let _ = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in + Proofview.tclUNIT () + end } let try_intros_until_id_check id = - Tacticals.New.tclORELSE (intros_until_id id) (Proofview.V82.tactic (tclCHECKVAR id)) + Tacticals.New.tclORELSE (intros_until_id id) (tclCHECKVAR id) let try_intros_until tac = function | NamedHyp id -> Tacticals.New.tclTHEN (try_intros_until_id_check id) (tac id) @@ -1620,9 +1623,7 @@ let solve_remaining_apply_goals = let concl = Proofview.Goal.concl gl in if Typeclasses.is_class_type evd concl then let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in - let tac = - (Proofview.V82.tactic (Tacmach.refine_no_check c')) - in + let tac = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c' h } in Sigma.Unsafe.of_pair (tac, evd') else Sigma.here (Proofview.tclUNIT ()) sigma with Not_found -> Sigma.here (Proofview.tclUNIT ()) sigma @@ -3641,8 +3642,8 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = else Tacticals.New.tclTHEN tac (Tacticals.New.tclFIRST [revert vars ; - Proofview.V82.tactic (fun gl -> tclMAP (fun id -> - tclTRY (Proofview.V82.of_tactic (generalize_dep ~with_let:true (mkVar id)))) vars gl)]) + Tacticals.New.tclMAP (fun id -> + Tacticals.New.tclTRY (generalize_dep ~with_let:true (mkVar id))) vars]) end } let rec compare_upto_variables x y = @@ -4003,10 +4004,10 @@ let recolle_clenv i params args elimclause gl = let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in (* parameters correspond to first elts of lid. *) let clauses_params = - List.map_i (fun i id -> mkVar id , Tacmach.pf_get_hyp_typ gl id , lindmv.(i)) + List.map_i (fun i id -> mkVar id , pf_get_hyp_typ id gl, lindmv.(i)) 0 params in let clauses_args = - List.map_i (fun i id -> mkVar id , Tacmach.pf_get_hyp_typ gl id , lindmv.(k+i)) + List.map_i (fun i id -> mkVar id , pf_get_hyp_typ id gl, lindmv.(k+i)) 0 args in let clauses = clauses_params@clauses_args in (* iteration of clenv_fchain with all infos we have. *) @@ -4016,7 +4017,7 @@ let recolle_clenv i params args elimclause gl = (* from_n (Some 0) means that x should be taken "as is" without trying to unify (which would lead to trying to apply it to evars if y is a product). *) - let indclause = mk_clenv_from_n gl (Some 0) (x,y) in + let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from_n gl (Some 0) (x,y)) gl in let elimclause' = clenv_fchain ~with_univs:false i acc indclause in elimclause') (List.rev clauses) @@ -4026,19 +4027,20 @@ let recolle_clenv i params args elimclause gl = (elimc ?i ?j ?k...?l). This solves partly meta variables (and may produce new ones). Then refine with the resulting term with holes. *) -let induction_tac with_evars params indvars elim gl = +let induction_tac with_evars params indvars elim = + Proofview.Goal.nf_enter { enter = begin fun gl -> let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in let i = match i with None -> index_of_ind_arg elimt | Some i -> i in (* elimclause contains this: (elimc ?i ?j ?k...?l) *) let elimc = contract_letin_in_lam_header elimc in let elimc = mkCast (elimc, DEFAULTcast, elimt) in - let elimclause = - Tacmach.pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in + let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in (* elimclause' is built from elimclause by instanciating all args and params. *) let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) - let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - Proofview.V82.of_tactic (enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved)) gl + let resolved = Tacmach.New.of_old (clenv_unique_resolver ~flags:(elim_flags ()) elimclause') gl in + enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved) + end } (* Apply induction "in place" taking into account dependent hypotheses from the context, replacing the main hypothesis on which @@ -4085,7 +4087,7 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyp let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in atomize_param_of_ind_then elim_info hyp0 (fun indvars -> apply_induction_in_context (Some hyp0) inhyps (pi3 elim_info) indvars names - (fun elim -> Proofview.V82.tactic (induction_tac with_evars [] [hyp0] elim))) + (fun elim -> induction_tac with_evars [] [hyp0] elim)) end } let msg_not_right_number_induction_arguments scheme = @@ -4123,23 +4125,24 @@ let induction_without_atomization isrec with_evars elim names lid = but by chance, because of the addition of at least hyp0 for cook_sign, it behaved as if there was a real induction arg. *) if indvars = [] then [List.hd lid_params] else indvars in - let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [ + let induct_tac elim = Tacticals.New.tclTHENLIST [ (* pattern to make the predicate appear. *) - Proofview.V82.of_tactic (reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl); + reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl; (* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all possible holes using arguments given by the user (but the functional one). *) (* FIXME: Tester ca avec un principe dependant et non-dependant *) - induction_tac with_evars params realindvars elim - ]) in + induction_tac with_evars params realindvars elim; + ] in let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in apply_induction_in_context None [] elim indvars names induct_tac end } (* assume that no occurrences are selected *) -let clear_unselected_context id inhyps cls gl = +let clear_unselected_context id inhyps cls = + Proofview.Goal.nf_enter { enter = begin fun gl -> let open Context.Named.Declaration in - if occur_var (Tacmach.pf_env gl) id (Tacmach.pf_concl gl) && + if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) && cls.concl_occs == NoOccurrences then errorlabstrm "" (str "Conclusion must be mentioned: it depends on " ++ pr_id id @@ -4151,11 +4154,12 @@ let clear_unselected_context id inhyps cls gl = if Id.List.mem id' inhyps then (* if selected, do not erase *) None else (* erase if not selected and dependent on id or selected hyps *) - let test id = occur_var_in_decl (pf_env gl) id d in + let test id = occur_var_in_decl (Tacmach.New.pf_env gl) id d in if List.exists test (id::inhyps) then Some id' else None in - let ids = List.map_filter to_erase (pf_hyps gl) in - Proofview.V82.of_tactic (clear ids) gl - | None -> tclIDTAC gl + let ids = List.map_filter to_erase (Proofview.Goal.hyps gl) in + clear ids + | None -> Proofview.tclUNIT () + end } let use_bindings env sigma elim must_be_closed (c,lbind) typ = let sigma = Sigma.to_evar_map sigma in @@ -4312,7 +4316,7 @@ let induction_gen clear_flag isrec with_evars elim and w/o equality kept: no need to generalize *) let id = destVar c in Tacticals.New.tclTHEN - (Proofview.V82.tactic (clear_unselected_context id inhyps cls)) + (clear_unselected_context id inhyps cls) (induction_with_atomization_of_ind_arg isrec with_evars elim names id inhyps) else -- cgit v1.2.3