diff options
| -rw-r--r-- | proofs/clenv.mli | 3 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 12 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 2 | ||||
| -rw-r--r-- | tactics/elim.ml | 11 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 104 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 35 |
7 files changed, 23 insertions, 146 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 9a985a842..e74c4875f 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -85,9 +85,6 @@ val clenv_missing : clausenv -> metavariable list exception NoSuchBinding val clenv_constrain_last_binding : constr -> clausenv -> clausenv -(** defines metas corresponding to the name of the bindings *) -val clenv_match_args : arg_bindings -> clausenv -> clausenv - val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (** start with a clenv to refine with a given term with bindings *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 29211c71a..c0036d192 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -79,18 +79,6 @@ let dft = default_unify_flags let res_pf clenv ?(with_evars=false) ?(flags=dft) gls = clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls -let elim_res_pf_THEN_i clenv tac gls = - let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in - tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls - -let new_elim_res_pf_THEN_i clenv tac = - Proofview.Goal.enter begin fun gl -> - let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) gl in - Proofview.tclTHEN - (Proofview.V82.tactic (clenv_refine false clenv')) - (Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv'))) - end - let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 86d567ef2..f635012fe 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -16,8 +16,6 @@ open Unification val unify : ?flags:unify_flags -> constr -> tactic val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic val res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> tactic -val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic -val new_elim_res_pf_THEN_i : clausenv -> (clausenv -> unit Proofview.tactic array) -> unit Proofview.tactic val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv val clenv_value_cast_meta : clausenv -> constr diff --git a/tactics/elim.ml b/tactics/elim.ml index bbbe62eb5..5eb3dcfe6 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -63,7 +63,7 @@ Another example : *) let elimHypThen tac id = - Tacticals.New.elimination_then tac ([],[]) (mkVar id) + Tacticals.New.elimination_then tac (mkVar id) let rec general_decompose_on_hyp recognizer = Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) @@ -138,8 +138,8 @@ let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) -let simple_elimination c gls = - simple_elimination_then (fun _ -> tclIDTAC) c gls +let simple_elimination c = + Tacticals.New.elimination_then (fun _ -> Tacticals.New.tclIDTAC) c let induction_trailer abs_i abs_j bargs = Tacticals.New.tclTHEN @@ -163,7 +163,7 @@ let induction_trailer abs_i abs_j bargs = let ids = List.rev (ids_of_named_context hyps) in (tclTHENSEQ [Proofview.V82.of_tactic (bring_hyps hyps); tclTRY (clear ids); - simple_elimination (mkVar id)]) gls + Proofview.V82.of_tactic (simple_elimination (mkVar id))]) gls end )) @@ -180,8 +180,7 @@ let double_ind h1 h2 = (Tacticals.New.onLastHypId (fun id -> Tacticals.New.elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) - ([],[]) (mkVar id)))) + (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) end let h_double_induction = double_ind diff --git a/tactics/inv.ml b/tactics/inv.ml index 498addf58..0bc96c19d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -488,7 +488,7 @@ let raw_inversion inv_kind id status names = (assert_tac Anonymous cut_concl) [case_tac names (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) - (Some elim_predicate) ([],[]) ind indclause; + (Some elim_predicate) ind indclause; onLastHypId (fun id -> (tclTHEN diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 82704c3c4..17e49be71 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -224,63 +224,6 @@ let elimination_sort_of_clause = function | None -> elimination_sort_of_goal | Some id -> elimination_sort_of_hyp id -(* Find the right elimination suffix corresponding to the sort of the goal *) -(* c should be of type A1->.. An->B with B an inductive definition *) - -let general_elim_then_using mk_elim - isrec allnames tac predicate (indbindings,elimbindings) - ind indclause gl = - let elim = mk_elim ind gl in - (* applying elimination_scheme just a little modified *) - let indclause' = clenv_match_args indbindings indclause in - let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in - let indmv = - match kind_of_term (last_arg elimclause.templval.Evd.rebus) with - | Meta mv -> mv - | _ -> anomaly (Pp.str "elimination") - in - let pmv = - let p, _ = decompose_app elimclause.templtyp.Evd.rebus in - match kind_of_term p with - | Meta p -> p - | _ -> - let name_elim = - match kind_of_term elim with - | Const kn -> string_of_con kn - | Var id -> Id.to_string id - | _ -> "\b" - in - error ("The elimination combinator " ^ name_elim ^ " is unknown.") - in - let elimclause' = clenv_fchain indmv elimclause indclause' in - let elimclause' = clenv_match_args elimbindings elimclause' in - let branchsigns = compute_construtor_signatures isrec ind in - let brnames = compute_induction_names (Array.length branchsigns) allnames in - let after_tac ce i gl = - let (hd,largs) = decompose_app ce.templtyp.Evd.rebus in - let ba = { branchsign = branchsigns.(i); - branchnames = brnames.(i); - nassums = - List.fold_left - (fun acc b -> if b then acc+2 else acc+1) - 0 branchsigns.(i); - branchnum = i+1; - ity = ind; - largs = List.map (clenv_nf_meta ce) largs; - pred = clenv_nf_meta ce hd } - in - tac ba gl - in - let branchtacs ce = Array.init (Array.length branchsigns) (after_tac ce) in - let elimclause' = - match predicate with - | None -> elimclause' - | Some p -> - clenv_unify ~flags:Unification.elim_flags - Reduction.CONV (mkMeta pmv) p elimclause' - in - elim_res_pf_THEN_i elimclause' branchtacs gl - (* computing the case/elim combinators *) let gl_make_elim ind gl = @@ -294,27 +237,6 @@ let gl_make_case_nodep ind gl = pf_apply Indrec.build_case_analysis_scheme gl ind false (elimination_sort_of_goal gl) -let elimination_then_using tac predicate bindings c gl = - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in - let indclause = mk_clenv_from gl (c,t) in - let isrec,mkelim = - if (Global.lookup_mind (fst ind)).mind_record - then false,gl_make_case_dep - else true,gl_make_elim - in - general_elim_then_using mkelim isrec - None tac predicate bindings ind indclause gl - -let case_then_using = - general_elim_then_using gl_make_case_dep false - -let case_nodep_then_using = - general_elim_then_using gl_make_case_nodep false - -let elimination_then tac = elimination_then_using tac None -let simple_elimination_then tac = elimination_then tac ([],[]) - - let make_elim_branch_assumptions ba gl = let rec makerec (assums,cargs,constargs,recargs,indargs) lb lc = match lb,lc with @@ -622,15 +544,22 @@ module New = struct tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl) end + let elim_res_pf_THEN_i clenv tac = + Proofview.Goal.enter begin fun gl -> + let flags = Unification.elim_flags in + let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv) gl in + Proofview.tclTHEN + (Proofview.V82.tactic (clenv_refine false clenv')) + (Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv'))) + end + (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim - isrec allnames tac predicate (indbindings,elimbindings) - ind indclause = + isrec allnames tac predicate ind indclause = Proofview.Goal.enter begin fun gl -> let elim = Tacmach.New.of_old (mk_elim ind) gl in (* applying elimination_scheme just a little modified *) - let indclause' = clenv_match_args indbindings indclause in let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_type_of gl elim)) gl in let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with @@ -650,8 +579,7 @@ module New = struct in error ("The elimination combinator " ^ name_elim ^ " is unknown.") in - let elimclause' = clenv_fchain indmv elimclause indclause' in - let elimclause' = clenv_match_args elimbindings elimclause' in + let elimclause' = clenv_fchain indmv elimclause indclause in let branchsigns = compute_construtor_signatures isrec ind in let brnames = compute_induction_names (Array.length branchsigns) allnames in let after_tac ce i = @@ -677,10 +605,10 @@ module New = struct clenv_unify ~flags:Unification.elim_flags Reduction.CONV (mkMeta pmv) p elimclause' in - new_elim_res_pf_THEN_i elimclause' branchtacs + elim_res_pf_THEN_i elimclause' branchtacs end - let elimination_then_using tac predicate bindings c = + let elimination_then tac c = Proofview.Goal.enter begin fun gl -> let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) gl in @@ -689,8 +617,7 @@ module New = struct then false,gl_make_case_dep else true,gl_make_elim in - general_elim_then_using mkelim isrec - None tac predicate bindings ind indclause + general_elim_then_using mkelim isrec None tac None ind indclause end let case_then_using = @@ -699,9 +626,6 @@ module New = struct let case_nodep_then_using = general_elim_then_using gl_make_case_nodep false - - let elimination_then tac = elimination_then_using tac None - let elim_on_ba tac ba = Proofview.Goal.enter begin fun gl -> let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 46d62123c..d6c9e87f9 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -137,33 +137,6 @@ val elimination_sort_of_goal : goal sigma -> sorts_family val elimination_sort_of_hyp : Id.t -> goal sigma -> sorts_family val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family -val general_elim_then_using : - (inductive -> goal sigma -> constr) -> rec_flag -> - intro_pattern_expr located option -> (branch_args -> tactic) -> - constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> - tactic - -val elimination_then_using : - (branch_args -> tactic) -> constr option -> - (arg_bindings * arg_bindings) -> constr -> tactic - -val elimination_then : - (branch_args -> tactic) -> - (arg_bindings * arg_bindings) -> constr -> tactic - -val case_then_using : - intro_pattern_expr located option -> (branch_args -> tactic) -> - constr option -> (arg_bindings * arg_bindings) -> - inductive -> clausenv -> tactic - -val case_nodep_then_using : - intro_pattern_expr located option -> (branch_args -> tactic) -> - constr option -> (arg_bindings * arg_bindings) -> - inductive -> clausenv -> tactic - -val simple_elimination_then : - (branch_args -> tactic) -> constr -> tactic - val elim_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic val case_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic @@ -266,17 +239,15 @@ module New : sig val elimination_then : (branch_args -> unit Proofview.tactic) -> - (arg_bindings * arg_bindings) -> constr -> unit Proofview.tactic + constr -> unit Proofview.tactic val case_then_using : intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) -> - constr option -> (arg_bindings * arg_bindings) -> - inductive -> clausenv -> unit Proofview.tactic + constr option -> inductive -> clausenv -> unit Proofview.tactic val case_nodep_then_using : intro_pattern_expr located option -> (branch_args -> unit Proofview.tactic) -> - constr option -> (arg_bindings * arg_bindings) -> - inductive -> clausenv -> unit Proofview.tactic + constr option -> inductive -> clausenv -> unit Proofview.tactic val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic |