diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-03 12:31:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-03 12:31:45 +0000 |
| commit | 1bead2a1ef23f2a281613093d7861815279e336d (patch) | |
| tree | 9eaf1b967dbd270e8525094ae3bed20e1cf260ee | |
| parent | 056af27f37f8fb9a00548c88047a86061a624e8b (diff) | |
Ajout de eelim, ecase, edestruct et einduction (expérimental).
Ajout de l'option with à (e)destruct et (e)induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7
32 files changed, 236 insertions, 200 deletions
@@ -84,6 +84,9 @@ Tactics - The "with" arguments are now typed using informations from the current goal: allows support for coercions and more inference of implicit arguments. - Application of "f_equal"-style lemmas works better. +- Tactics elim, case, destruct and induction now support variants eelim, + ecase, edestruct and einduction. +- Tactics destruct and induction now support option "with". - New intro pattern "?A", which genererates a fresh name based on A. Caveat about a slight loss of compatibility: Some intro patterns don't need space between them. In particular diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 45dee7831..c68304c75 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -910,7 +910,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); - (* observe_tac "h_case" *) (h_case(mkVar rec_id,Rawterm.NoBindings)); + (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Rawterm.NoBindings)); intros_reflexivity] g ) ] diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 0fa73f096..199e01525 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -22,8 +22,8 @@ let is_rec_info scheme_info = let choose_dest_or_ind scheme_info = if is_rec_info scheme_info - then Tactics.new_induct - else Tactics.new_destruct + then Tactics.new_induct false + else Tactics.new_destruct false let functional_induction with_clean c princl pat = @@ -77,7 +77,7 @@ let functional_induction with_clean c princl pat = if princ_infos.Tactics.farg_in_concl then [c] else [] in - List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list) + List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list) in let princ' = Some (princ,bindings) in let princ_vars = diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index fbf72805b..b975c2e93 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -513,7 +513,7 @@ and intros_with_rewrite_aux : tactic = Tauto.tauto g | Case(_,_,v,_) -> tclTHENSEQ[ - h_case (v,Rawterm.NoBindings); + h_case false (v,Rawterm.NoBindings); intros_with_rewrite ] g | LetIn _ -> @@ -550,7 +550,7 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (snd (destApp (pf_concl g))).(2) with | Case(_,_,v,_) -> tclTHENSEQ[ - h_case (v,Rawterm.NoBindings); + h_case false (v,Rawterm.NoBindings); intros; observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] @@ -720,7 +720,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); h_intro graph_principle_id; observe_tac "" (tclTHEN_i - (observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings))))) + (observe_tac "elim" ((elim false (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings))))) (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index d96b63953..be99bdde0 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -175,7 +175,7 @@ let make_pbp_atomic_tactic = function | PbpElim (hyp_name, names) -> let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in TacAtom - (zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None)) + (zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None)) | PbpTryClear l -> TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l))) | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));; diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index ab4da05e3..e3f657202 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1208,11 +1208,12 @@ let rec natural_ntree ig ntree = | TacExtend (_,"CutIntro",[a]) -> let _c = out_gen wit_constr a in natural_cutintro ig lh g gs a ltree - | TacCase (c,_) -> natural_case ig lh g gs ge (snd c) ltree false + | TacCase (_,(c,_)) -> natural_case ig lh g gs ge (snd c) ltree false | TacExtend (_,"CaseIntro",[a]) -> let c = out_gen wit_constr a in natural_case ig lh g gs ge c ltree true - | TacElim ((c,_),_) -> natural_elim ig lh g gs ge (snd c) ltree false + | TacElim (_,(c,_),_) -> + natural_elim ig lh g gs ge (snd c) ltree false | TacExtend (_,"ElimIntro",[a]) -> let c = out_gen wit_constr a in natural_elim ig lh g gs ge c ltree true diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index e2ba05348..4f98b7396 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -663,7 +663,8 @@ let xlate_largs_to_id_opt largs = | _ -> assert false;; let xlate_int_or_constr = function - ElimOnConstr a -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a) + ElimOnConstr (a,NoBindings) -> CT_coerce_FORMULA_to_FORMULA_OR_INT(xlate_formula a) + | ElimOnConstr _ -> xlate_error "TODO: ElimOnConstr with bindings" | ElimOnIdent(_,i) -> CT_coerce_ID_OR_INT_to_FORMULA_OR_INT (CT_coerce_ID_to_ID_OR_INT(xlate_ident i)) @@ -1162,10 +1163,13 @@ and xlate_tac = CT_generalize_dependent (xlate_formula c) | TacElimType c -> CT_elim_type (xlate_formula c) | TacCaseType c -> CT_case_type (xlate_formula c) - | TacElim ((c1,sl), u) -> + | TacElim (false,(c1,sl), u) -> CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u) - | TacCase (c1,sl) -> + | TacCase (false,(c1,sl)) -> CT_casetac (xlate_formula c1, xlate_bindings sl) + | TacElim (true,_,_) | TacCase (true,_) + | TacNewDestruct (true,_,_,_) | TacNewInduction (true,_,_,_) -> + xlate_error "TODO: eelim, ecase, edestruct, einduction" | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h) | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h) | TacCut c -> CT_cut (xlate_formula c) @@ -1207,12 +1211,12 @@ and xlate_tac = CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b) | TacDAuto (a, b, _) -> xlate_error "TODO: dauto using" - | TacNewDestruct(a,b,c) -> - CT_new_destruct (* Julien F. : est-ce correct *) + | TacNewDestruct(false,a,b,c) -> + CT_new_destruct (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) - | TacNewInduction(a,b,c) -> - CT_new_induction (* Pierre C. : est-ce correct *) + | TacNewInduction(false,a,b,c) -> + CT_new_induction (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) (*| TacInstantiate (a, b, cl) -> @@ -27,6 +27,7 @@ install_printer Top_printers.ppenv install_printer Top_printers.ppgoal install_printer Top_printers.ppsigmagoal install_printer Top_printers.pproof +install_printer Top_printers.ppmetas install_printer Top_printers.ppevd install_printer Top_printers.ppevm install_printer Top_printers.ppclenv diff --git a/dev/include b/dev/include index 42d2a0171..1fc82be83 100644 --- a/dev/include +++ b/dev/include @@ -17,6 +17,7 @@ #install_printer (* goal *) ppgoal;; #install_printer (* sigma goal *) ppsigmagoal;; #install_printer (* proof *) pproof;; +#install_printer (* metaset.t *) ppmeta;; #install_printer (* evar_map *) ppevm;; #install_printer (* evar_defs *) ppevd;; #install_printer (* clenv *) ppclenv;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f2b9c996b..cd0fa0c0d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -86,6 +86,7 @@ let ppj j = pp (genppj pr_ljudge j) let prsubst s = pp (Mod_subst.debug_pr_subst s) (* proof printers *) +let ppmetas metas = pp(pr_metaset metas) let ppevm evd = pp(pr_evar_map evd) let ppevd evd = pp(pr_evar_defs evd) let ppclenv clenv = pp(pr_clenv clenv) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 3f7c8c3e8..e8d1be4f6 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -111,9 +111,11 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = (id,CProdN(loc,bl,ty)) (* Functions overloaded by quotifier *) -let induction_arg_of_constr c = - try ElimOnIdent (constr_loc c,snd(coerce_to_id c)) - with _ -> ElimOnConstr c +let induction_arg_of_constr (c,lbind as clbind) = + if lbind = NoBindings then + try ElimOnIdent (constr_loc c,snd(coerce_to_id c)) + with _ -> ElimOnConstr clbind + else ElimOnConstr clbind (* Auxiliary grammar rules *) @@ -147,7 +149,7 @@ GEXTEND Gram ; induction_arg: [ [ n = natural -> ElimOnAnonHyp n - | c = constr -> induction_arg_of_constr c + | c = constr_with_bindings -> induction_arg_of_constr c ] ] ; quantified_hypothesis: @@ -343,9 +345,12 @@ GEXTEND Gram | IDENT "apply"; cl = constr_with_bindings -> TacApply (false,cl) | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,cl) | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator -> - TacElim (cl,el) + TacElim (false,cl,el) + | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator -> + TacElim (true,cl,el) | IDENT "elimtype"; c = constr -> TacElimType c - | IDENT "case"; cl = constr_with_bindings -> TacCase cl + | IDENT "case"; cl = constr_with_bindings -> TacCase (false,cl) + | IDENT "ecase"; cl = constr_with_bindings -> TacCase (true,cl) | IDENT "casetype"; c = constr -> TacCaseType c | "fix"; n = natural -> TacFix (None,n) | "fix"; id = ident; n = natural -> TacFix (Some id,n) @@ -389,13 +394,17 @@ GEXTEND Gram | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis -> TacSimpleInduction h | IDENT "induction"; lc = LIST1 induction_arg; ids = with_names; - el = OPT eliminator -> TacNewInduction (lc,el,ids) + el = OPT eliminator -> TacNewInduction (false,lc,el,ids) + | IDENT "einduction"; lc = LIST1 induction_arg; ids = with_names; + el = OPT eliminator -> TacNewInduction (true,lc,el,ids) | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis; h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) - | IDENT "simple"; IDENT"destruct"; h = quantified_hypothesis -> + | IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis -> TacSimpleDestruct h | IDENT "destruct"; lc = LIST1 induction_arg; ids = with_names; - el = OPT eliminator -> TacNewDestruct (lc,el,ids) + el = OPT eliminator -> TacNewDestruct (false,lc,el,ids) + | IDENT "edestruct"; lc = LIST1 induction_arg; ids = with_names; + el = OPT eliminator -> TacNewDestruct (true,lc,el,ids) | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index c6c168d4e..019063527 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -427,8 +427,8 @@ let pr_clause_pattern pr_id = function let pr_orient b = if b then mt () else str " <-" -let pr_induction_arg prc = function - | ElimOnConstr c -> prc c +let pr_induction_arg prlc prc = function + | ElimOnConstr c -> pr_with_bindings prlc prc c | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) | ElimOnAnonHyp n -> int n @@ -680,11 +680,12 @@ and pr_atom1 = function | TacApply (ev,cb) -> hov 1 (str (if ev then "eapply" else "apply") ++ spc () ++ pr_with_bindings cb) - | TacElim (cb,cbo) -> - hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ + | TacElim (ev,cb,cbo) -> + hov 1 (str (if ev then "eelim" else "elim") ++ pr_arg pr_with_bindings cb ++ pr_opt pr_eliminator cbo) | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c) - | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings cb) + | TacCase (ev,cb) -> + hov 1 (str (if ev then "ecase" else "case") ++ spc () ++ pr_with_bindings cb) | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c) | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> @@ -726,16 +727,16 @@ and pr_atom1 = function (* Derived basic tactics *) | TacSimpleInduction h -> hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h) - | TacNewInduction (h,e,ids) -> - hov 1 (str "induction" ++ spc () ++ - prlist_with_sep spc (pr_induction_arg pr_constr) h ++ + | TacNewInduction (ev,h,e,ids) -> + hov 1 (str (if ev then "einduction" else "induction") ++ spc () ++ + prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ pr_with_names ids ++ pr_opt pr_eliminator e) | TacSimpleDestruct h -> hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) - | TacNewDestruct (h,e,ids) -> - hov 1 (str "destruct" ++ spc () ++ - prlist_with_sep spc (pr_induction_arg pr_constr) h ++ + | TacNewDestruct (ev,h,e,ids) -> + hov 1 (str (if ev then "edestruct" else "destruct") ++ spc () ++ + prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ pr_with_names ids ++ pr_opt pr_eliminator e) | TacDoubleInduction (h1,h2) -> diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 4b1dfd9e3..fbd2e6e07 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -227,19 +227,19 @@ let mlexpr_of_binding_kind = function | Rawterm.NoBindings -> <:expr< Rawterm.NoBindings >> +let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr + +let mlexpr_of_constr_with_binding = + mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind + let mlexpr_of_induction_arg = function | Tacexpr.ElimOnConstr c -> - <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr c$ >> + <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >> | Tacexpr.ElimOnIdent (_,id) -> <:expr< Tacexpr.ElimOnIdent $dloc$ $mlexpr_of_ident id$ >> | Tacexpr.ElimOnAnonHyp n -> <:expr< Tacexpr.ElimOnAnonHyp $mlexpr_of_int n$ >> -let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr - -let mlexpr_of_constr_with_binding = - mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind - let mlexpr_of_clause_pattern _ = failwith "mlexpr_of_clause_pattern: TODO" let mlexpr_of_pattern_ast = mlexpr_of_constr @@ -287,15 +287,15 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacApply (false,cb) -> <:expr< Tacexpr.TacApply False $mlexpr_of_constr_with_binding cb$ >> - | Tacexpr.TacElim (cb,cbo) -> + | Tacexpr.TacElim (false,cb,cbo) -> let cb = mlexpr_of_constr_with_binding cb in let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - <:expr< Tacexpr.TacElim $cb$ $cbo$ >> + <:expr< Tacexpr.TacElim False $cb$ $cbo$ >> | Tacexpr.TacElimType c -> <:expr< Tacexpr.TacElimType $mlexpr_of_constr c$ >> - | Tacexpr.TacCase cb -> + | Tacexpr.TacCase (false,cb) -> let cb = mlexpr_of_constr_with_binding cb in - <:expr< Tacexpr.TacCase $cb$ >> + <:expr< Tacexpr.TacCase False $cb$ >> | Tacexpr.TacCaseType c -> <:expr< Tacexpr.TacCaseType $mlexpr_of_constr c$ >> | Tacexpr.TacFix (ido,n) -> @@ -335,18 +335,18 @@ let rec mlexpr_of_atomic_tactic = function (* Derived basic tactics *) | Tacexpr.TacSimpleInduction h -> <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >> - | Tacexpr.TacNewInduction (cl,cbo,ids) -> + | Tacexpr.TacNewInduction (false,cl,cbo,ids) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in let ids = mlexpr_of_intro_pattern ids in (* let ids = mlexpr_of_option mlexpr_of_intro_pattern ids in *) (* <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>> *) - <:expr< Tacexpr.TacNewInduction $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$>> + <:expr< Tacexpr.TacNewInduction False $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$>> | Tacexpr.TacSimpleDestruct h -> <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >> - | Tacexpr.TacNewDestruct (c,cbo,ids) -> + | Tacexpr.TacNewDestruct (false,c,cbo,ids) -> let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in let ids = mlexpr_of_intro_pattern ids in - <:expr< Tacexpr.TacNewDestruct $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ >> + <:expr< Tacexpr.TacNewDestruct False $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ >> (* Context management *) | Tacexpr.TacClear (b,l) -> diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 2533e64e4..793ac2c32 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -218,7 +218,8 @@ let clenv_wtactic f clenv = {clenv with evd = f clenv.evd } * returns a list of the metavars which appear in the type of * the metavar mv. The list is unordered. *) -let clenv_metavars clenv mv = (meta_ftype clenv mv).freemetas +let clenv_metavars evd mv = + (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas let dependent_metas clenv mvs conclmetas = List.fold_right @@ -269,9 +270,7 @@ let clenv_pose_dependent_evars clenv = clenv dep_mvs -let evar_clenv_unique_resolver clenv gls = - clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls) - +let evar_clenv_unique_resolver = clenv_unique_resolver (******************************************************************) diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index ccaa22f5e..73a171b8d 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -75,9 +75,9 @@ val clenv_unique_resolver : bool -> clausenv -> evar_info sigma -> clausenv (* same as above ([allow_K=false]) but replaces remaining metas - with fresh evars *) + with fresh evars if [evars_flag] is [true] *) val evar_clenv_unique_resolver : - clausenv -> evar_info sigma -> clausenv + bool -> clausenv -> evar_info sigma -> clausenv val clenv_pose_dependent_evars : clausenv -> clausenv diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 300b4c8e6..d0cbeb574 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -659,3 +659,6 @@ let pr_evar_defs evd = if evd.metas = Metamap.empty then mt() else str"METAS:"++brk(0,1)++pr_meta_map evd.metas in v 0 (pp_evm ++ cstrs ++ pp_met) + +let pr_metaset metas = + Metaset.fold (fun mv pp -> pr_meta mv ++ pp) metas (Pp.mt()) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index b5a36c1f3..5d03fbfd3 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -215,3 +215,4 @@ val pr_evar_info : evar_info -> Pp.std_ppcmds val pr_evar_map : evar_map -> Pp.std_ppcmds val pr_evar_defs : evar_defs -> Pp.std_ppcmds val pr_sort_constraints : evar_map -> Pp.std_ppcmds +val pr_metaset : Metaset.t -> Pp.std_ppcmds diff --git a/pretyping/termops.ml b/pretyping/termops.ml index f15ec5166..e52d7c82a 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -517,8 +517,8 @@ let free_rels m = let collect_metas c = let rec collrec acc c = match kind_of_term c with - | Meta mv -> mv::acc - | _ -> fold_constr collrec acc c + | Meta mv -> list_add_set mv acc + | _ -> fold_constr collrec acc c in List.rev (collrec [] c) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 52093e5af..b2190c53c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -32,18 +32,20 @@ let abstract_scheme env c l lname_typ = List.fold_left2 (fun t (locc,a) (na,_,ta) -> let na = match kind_of_term a with Var id -> Name id | _ -> na in +(* [occur_meta ta] test removed for support of eelim/ecase but consequences + are unclear... if occur_meta ta then error "cannot find a type for the generalisation" - else if occur_meta a then lambda_name env (na,ta,t) + else *) if occur_meta a then lambda_name env (na,ta,t) else lambda_name env (na,ta,subst_term_occ locc a t)) c (List.rev l) lname_typ -let abstract_list_all env sigma typ c l = - let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in +let abstract_list_all env evd typ c l = + let ctxt,_ = decomp_n_prod env (evars_of evd) (List.length l) typ in let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in try - if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p + if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p else error "abstract_list_all" with UserError _ -> raise (PretypeError (env,CannotGeneralize typ)) @@ -576,11 +578,10 @@ let w_unify_to_subterm_list env mod_delta allow_K oplist t evd = (evd,[]) let secondOrderAbstraction env mod_delta allow_K typ (p, oplist) evd = - let sigma = evars_of evd in let (evd',cllist) = w_unify_to_subterm_list env mod_delta allow_K oplist typ evd in let typp = Typing.meta_type evd' p in - let pred = abstract_list_all env sigma typp typ cllist in + let pred = abstract_list_all env evd' typp typ cllist in w_unify_0 env topconv mod_delta (mkMeta p) pred evd' let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index f163e95f6..d2cb20550 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -28,8 +28,8 @@ val w_unify_meta_types : env -> evar_defs -> evar_defs (*i This should be in another module i*) -(* [abstract_list_all env sigma t c l] *) +(* [abstract_list_all env evd t c l] *) (* abstracts the terms in l over c to get a term of type t *) (* (exported for inv.ml) *) val abstract_list_all : - env -> evar_map -> constr -> constr -> constr list -> constr + env -> evar_defs -> constr -> constr -> constr list -> constr diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 785316d56..ad19bd9b6 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -60,25 +60,22 @@ let clenv_cast_meta clenv = in crec -let clenv_refine clenv gls = +let clenv_refine with_evars clenv gls = + let clenv = if with_evars then clenv_pose_dependent_evars clenv else clenv in tclTHEN (tclEVARS (evars_of clenv.evd)) (refine (clenv_cast_meta clenv (clenv_value clenv))) gls -let res_pf clenv ?(allow_K=false) gls = - clenv_refine (clenv_unique_resolver allow_K clenv gls) gls +let res_pf clenv ?(with_evars=false) ?(allow_K=false) gls = + clenv_refine with_evars (clenv_unique_resolver allow_K clenv gls) gls let elim_res_pf_THEN_i clenv tac gls = let clenv' = (clenv_unique_resolver true clenv gls) in - tclTHENLASTn (clenv_refine clenv') (tac clenv') gls - - -let e_res_pf clenv gls = - clenv_refine (evar_clenv_unique_resolver clenv gls) gls - + tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls +let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index cc75af0fc..038f84f01 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -16,11 +16,14 @@ open Sign open Evd open Clenv open Proof_type +open Tacexpr (*i*) (* Tactics *) val unify : constr -> tactic -val clenv_refine : clausenv -> tactic -val res_pf : clausenv -> ?allow_K:bool -> tactic -val e_res_pf : clausenv -> tactic +val clenv_refine : evars_flag -> clausenv -> tactic +val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> tactic val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic + +(* Compatibility, use res_pf ?with_evars:true instead *) +val e_res_pf : clausenv -> tactic diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index d68d125bd..cb62c084d 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -124,9 +124,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacExactNoCheck of 'constr | TacVmCastNoCheck of 'constr | TacApply of evars_flag * 'constr with_bindings - | TacElim of 'constr with_bindings * 'constr with_bindings option + | TacElim of evars_flag * 'constr with_bindings * + 'constr with_bindings option | TacElimType of 'constr - | TacCase of 'constr with_bindings + | TacCase of evars_flag * 'constr with_bindings | TacCaseType of 'constr | TacFix of identifier option * int | TacMutualFix of identifier * int * (identifier * int * 'constr) list @@ -140,11 +141,11 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* Derived basic tactics *) | TacSimpleInduction of quantified_hypothesis - | TacNewInduction of 'constr induction_arg list * 'constr with_bindings option - * intro_pattern_expr + | TacNewInduction of evars_flag * 'constr with_bindings induction_arg list * + 'constr with_bindings option * intro_pattern_expr | TacSimpleDestruct of quantified_hypothesis - | TacNewDestruct of 'constr induction_arg list * 'constr with_bindings option - * intro_pattern_expr + | TacNewDestruct of evars_flag * 'constr with_bindings induction_arg list * + 'constr with_bindings option * intro_pattern_expr | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis | TacDecomposeAnd of 'constr diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 62ed700a2..535fd6632 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -77,7 +77,7 @@ let contradiction_term (c,lbind as cl) gl = let typ = pf_type_of gl c in let _, ccl = splay_prod env sigma typ in if is_empty_type ccl then - tclTHEN (elim cl None) (tclTRY assumption) gl + tclTHEN (elim false cl None) (tclTRY assumption) gl else try if lbind = NoBindings then diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 60cedf093..134f018ca 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -762,7 +762,7 @@ let rec consider_match may_intro introduced available expected gls = try conjunction_arity id gls with Not_found -> error "matching hypothesis not found" in tclTHENLIST - [general_case_analysis (mkVar id,NoBindings); + [general_case_analysis false (mkVar id,NoBindings); intron_then nhyps [] (fun l -> consider_match may_intro introduced (List.rev_append l rest_ids) expected)] gls) @@ -1347,7 +1347,7 @@ let end_tac et2 gls = tclSOLVE [simplest_elim pi.per_casee] | ET_Case_analysis,EK_nodep -> tclTHEN - (general_case_analysis (pi.per_casee,NoBindings)) + (general_case_analysis false (pi.per_casee,NoBindings)) (default_justification (List.map mkVar clauses)) | ET_Induction,EK_nodep -> tclTHENLIST diff --git a/tactics/equality.ml b/tactics/equality.ml index 7681a03a4..066bf88d4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -61,7 +61,7 @@ let general_elim_clause with_evars cls c elim = match cls with (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal and did not fail for useless conditional rewritings generating an extra condition *) - tclNOTSAMEGOAL (general_elim c elim ~allow_K:false) + tclNOTSAMEGOAL (general_elim with_evars c elim ~allow_K:false) | Some id -> general_elim_in with_evars id c elim diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 55666a08a..8bb7c5c2c 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -23,7 +23,7 @@ let inj_id id = (dummy_loc,id) let inj_open c = (Evd.empty,c) let inj_open_wb (c,b) = ((Evd.empty,c),b) let inj_ia = function - | ElimOnConstr c -> ElimOnConstr (inj_open c) + | ElimOnConstr c -> ElimOnConstr (inj_open_wb c) | ElimOnIdent id -> ElimOnIdent id | ElimOnAnonHyp n -> ElimOnAnonHyp n let inj_occ (occ,c) = (occ,inj_open c) @@ -42,11 +42,11 @@ let h_vm_cast_no_check c = let h_apply ev cb = abstract_tactic (TacApply (ev,inj_open_wb cb)) (apply_with_ebindings_gen ev cb) -let h_elim cb cbo = - abstract_tactic (TacElim (inj_open_wb cb,option_map inj_open_wb cbo)) - (elim cb cbo) +let h_elim ev cb cbo = + abstract_tactic (TacElim (ev,inj_open_wb cb,option_map inj_open_wb cbo)) + (elim ev cb cbo) let h_elim_type c = abstract_tactic (TacElimType (inj_open c)) (elim_type c) -let h_case cb = abstract_tactic (TacCase (inj_open_wb cb)) (general_case_analysis cb) +let h_case ev cb = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb) let h_case_type c = abstract_tactic (TacCaseType (inj_open c)) (case_type c) let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n) let h_mutual_fix id n l = @@ -77,12 +77,12 @@ let h_simple_induction h = abstract_tactic (TacSimpleInduction h) (simple_induct h) let h_simple_destruct h = abstract_tactic (TacSimpleDestruct h) (simple_destruct h) -let h_new_induction c e idl = - abstract_tactic (TacNewInduction (List.map inj_ia c,option_map inj_open_wb e,idl)) - (new_induct c e idl) -let h_new_destruct c e idl = - abstract_tactic (TacNewDestruct (List.map inj_ia c,option_map inj_open_wb e,idl)) - (new_destruct c e idl) +let h_new_induction ev c e idl = + abstract_tactic (TacNewInduction (ev,List.map inj_ia c,option_map inj_open_wb e,idl)) + (new_induct ev c e idl) +let h_new_destruct ev c e idl = + abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,option_map inj_open_wb e,idl)) + (new_destruct ev c e idl) let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d) let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) @@ -124,8 +124,8 @@ let h_transitivity c = let h_simplest_apply c = h_apply false (c,NoBindings) let h_simplest_eapply c = h_apply true (c,NoBindings) -let h_simplest_elim c = h_elim (c,NoBindings) None -let h_simplest_case c = h_case (c,NoBindings) +let h_simplest_elim c = h_elim false (c,NoBindings) None +let h_simplest_case c = h_case false (c,NoBindings) let h_intro_patterns l = abstract_tactic (TacIntroPattern l) (intro_patterns l) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 8937a37ef..87232988b 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -17,6 +17,7 @@ open Genarg open Tacexpr open Rawterm open Evd +open Clenv (*i*) (* Tactics for the interpreter. They left a trace in the proof tree @@ -35,10 +36,10 @@ val h_vm_cast_no_check : constr -> tactic val h_apply : evars_flag -> constr with_ebindings -> tactic -val h_elim : constr with_ebindings -> +val h_elim : evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic val h_elim_type : constr -> tactic -val h_case : constr with_ebindings -> tactic +val h_case : evars_flag -> constr with_ebindings -> tactic val h_case_type : constr -> tactic val h_mutual_fix : identifier -> int -> @@ -59,11 +60,11 @@ val h_instantiate : int -> Rawterm.rawconstr -> val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic val h_new_induction : - constr induction_arg list -> constr with_ebindings option -> - intro_pattern_expr -> tactic + evars_flag -> constr with_ebindings induction_arg list -> + constr with_ebindings option -> intro_pattern_expr -> tactic val h_new_destruct : - constr induction_arg list -> constr with_ebindings option -> - intro_pattern_expr -> tactic + evars_flag -> constr with_ebindings induction_arg list -> + constr with_ebindings option -> intro_pattern_expr -> tactic val h_specialize : int option -> constr with_ebindings -> tactic val h_lapply : constr -> tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index daa6e2777..bfaa7e5e4 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -111,7 +111,8 @@ let make_inv_predicate env sigma indf realargs id status concl = | None -> let sort = get_sort_of env sigma concl in let p = make_arity env true indf sort in - Unification.abstract_list_all env sigma p concl (realargs@[mkVar id]) in + Unification.abstract_list_all env (Evd.create_evar_defs sigma) + p concl (realargs@[mkVar id]) in let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in (* We lift to make room for the equations *) (hyps,lift nrealargs bodypred) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1a6c18e4d..bff8b1b49 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -492,12 +492,12 @@ let intern_clause_pattern ist (l,occl) = (* TODO: catch ltac vars *) let intern_induction_arg ist = function - | ElimOnConstr c -> ElimOnConstr (intern_constr ist c) + | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c) | ElimOnAnonHyp n as x -> x | ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) - ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id)))) + ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id))),NoBindings) else ElimOnIdent (loc,id) @@ -660,11 +660,11 @@ let rec intern_atomic lf ist x = | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c) | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c) | TacApply (ev,cb) -> TacApply (ev,intern_constr_with_bindings ist cb) - | TacElim (cb,cbo) -> - TacElim (intern_constr_with_bindings ist cb, + | TacElim (ev,cb,cbo) -> + TacElim (ev,intern_constr_with_bindings ist cb, option_map (intern_constr_with_bindings ist) cbo) | TacElimType c -> TacElimType (intern_type ist c) - | TacCase cb -> TacCase (intern_constr_with_bindings ist cb) + | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb) | TacCaseType c -> TacCaseType (intern_type ist c) | TacFix (idopt,n) -> TacFix (option_map (intern_ident lf ist) idopt,n) | TacMutualFix (id,n,l) -> @@ -702,14 +702,14 @@ let rec intern_atomic lf ist x = (* Derived basic tactics *) | TacSimpleInduction h -> TacSimpleInduction (intern_quantified_hypothesis ist h) - | TacNewInduction (lc,cbo,ids) -> - TacNewInduction (List.map (intern_induction_arg ist) lc, + | TacNewInduction (ev,lc,cbo,ids) -> + TacNewInduction (ev,List.map (intern_induction_arg ist) lc, option_map (intern_constr_with_bindings ist) cbo, (intern_intro_pattern lf ist ids)) | TacSimpleDestruct h -> TacSimpleDestruct (intern_quantified_hypothesis ist h) - | TacNewDestruct (c,cbo,ids) -> - TacNewDestruct (List.map (intern_induction_arg ist) c, + | TacNewDestruct (ev,c,cbo,ids) -> + TacNewDestruct (ev,List.map (intern_induction_arg ist) c, option_map (intern_constr_with_bindings ist) cbo, (intern_intro_pattern lf ist ids)) | TacDoubleInduction (h1,h2) -> @@ -1558,14 +1558,6 @@ let interp_declared_or_quantified_hypothesis ist gl = function (coerce_to_decl_or_quant_hyp env) ist (Some env) (dloc,id) with Not_found -> NamedHyp id -let interp_induction_arg ist gl = function - | ElimOnConstr c -> ElimOnConstr (pf_interp_constr ist gl c) - | ElimOnAnonHyp n as x -> x - | ElimOnIdent (loc,id) -> - if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id) - else ElimOnConstr - (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id))))) - let interp_binding ist gl (loc,b,c) = (loc,interp_binding_name ist b,pf_interp_open_constr false ist gl c) @@ -1580,6 +1572,15 @@ let interp_constr_with_bindings ist gl (c,bl) = let interp_open_constr_with_bindings ist gl (c,bl) = (pf_interp_open_constr false ist gl c, interp_bindings ist gl bl) +let interp_induction_arg ist gl = function + | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c) + | ElimOnAnonHyp n as x -> x + | ElimOnIdent (loc,id) -> + if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id) + else ElimOnConstr + (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))), + NoBindings) + let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c) let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c)) let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c) @@ -2085,11 +2086,11 @@ and interp_atomic ist gl = function | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c) | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c) | TacApply (ev,cb) -> h_apply ev (interp_constr_with_bindings ist gl cb) - | TacElim (cb,cbo) -> - h_elim (interp_constr_with_bindings ist gl cb) + | TacElim (ev,cb,cbo) -> + h_elim ev (interp_constr_with_bindings ist gl cb) (option_map (interp_constr_with_bindings ist gl) cbo) | TacElimType c -> h_elim_type (pf_interp_type ist gl c) - | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb) + | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb) | TacCaseType c -> h_case_type (pf_interp_type ist gl c) | TacFix (idopt,n) -> h_fix (option_map (interp_fresh_ident ist gl) idopt) n | TacMutualFix (id,n,l) -> @@ -2130,14 +2131,14 @@ and interp_atomic ist gl = function (* Derived basic tactics *) | TacSimpleInduction h -> h_simple_induction (interp_quantified_hypothesis ist h) - | TacNewInduction (lc,cbo,ids) -> - h_new_induction (List.map (interp_induction_arg ist gl) lc) + | TacNewInduction (ev,lc,cbo,ids) -> + h_new_induction ev (List.map (interp_induction_arg ist gl) lc) (option_map (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist gl ids) | TacSimpleDestruct h -> h_simple_destruct (interp_quantified_hypothesis ist h) - | TacNewDestruct (c,cbo,ids) -> - h_new_destruct (List.map (interp_induction_arg ist gl) c) + | TacNewDestruct (ev,c,cbo,ids) -> + h_new_destruct ev (List.map (interp_induction_arg ist gl) c) (option_map (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist gl ids) | TacDoubleInduction (h1,h2) -> @@ -2337,7 +2338,7 @@ let subst_raw_with_bindings subst (c,bl) = (subst_rawconstr subst c, subst_bindings subst bl) let subst_induction_arg subst = function - | ElimOnConstr c -> ElimOnConstr (subst_rawconstr subst c) + | ElimOnConstr c -> ElimOnConstr (subst_raw_with_bindings subst c) | ElimOnAnonHyp n as x -> x | ElimOnIdent id as x -> x @@ -2413,11 +2414,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c) | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c) | TacApply (ev,cb) -> TacApply (ev,subst_raw_with_bindings subst cb) - | TacElim (cb,cbo) -> - TacElim (subst_raw_with_bindings subst cb, + | TacElim (ev,cb,cbo) -> + TacElim (ev,subst_raw_with_bindings subst cb, option_map (subst_raw_with_bindings subst) cbo) | TacElimType c -> TacElimType (subst_rawconstr subst c) - | TacCase cb -> TacCase (subst_raw_with_bindings subst cb) + | TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb) | TacCaseType c -> TacCaseType (subst_rawconstr subst c) | TacFix (idopt,n) as x -> x | TacMutualFix (id,n,l) -> @@ -2443,12 +2444,12 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Derived basic tactics *) | TacSimpleInduction h as x -> x - | TacNewInduction (lc,cbo,ids) -> (* Pierre C. est-ce correct? *) - TacNewInduction (List.map (subst_induction_arg subst) lc, + | TacNewInduction (ev,lc,cbo,ids) -> + TacNewInduction (ev,List.map (subst_induction_arg subst) lc, option_map (subst_raw_with_bindings subst) cbo, ids) | TacSimpleDestruct h as x -> x - | TacNewDestruct (c,cbo,ids) -> - TacNewDestruct (List.map (subst_induction_arg subst) c, (* Julien F. est-ce correct? *) + | TacNewDestruct (ev,c,cbo,ids) -> + TacNewDestruct (ev,List.map (subst_induction_arg subst) c, option_map (subst_raw_with_bindings subst) cbo, ids) | TacDoubleInduction (h1,h2) as x -> x | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 65610fe27..cffe550af 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -554,8 +554,7 @@ let apply_with_ebindings_gen with_evars (c,lbind) gl = let n = nb_prod thm_ty - nprod in if n<0 then error "Apply: theorem has not enough premisses."; let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in - if with_evars then Clenvtac.e_res_pf clause gl - else Clenvtac.res_pf clause gl in + Clenvtac.res_pf clause ~with_evars:with_evars gl in try try_apply thm_ty0 concl_nprod with PretypeError _|RefinerError _|UserError _|Failure _ as exn -> let rec try_red_apply thm_ty = @@ -824,7 +823,7 @@ let last_arg c = match kind_of_term c with array_last cl | _ -> anomaly "last_arg" -let elimination_clause_scheme allow_K elimclause indclause gl = +let elimination_clause_scheme with_evars allow_K elimclause indclause gl = let indmv = (match kind_of_term (last_arg elimclause.templval.rebus) with | Meta mv -> mv @@ -832,7 +831,7 @@ let elimination_clause_scheme allow_K elimclause indclause gl = (str "The type of elimination clause is not well-formed")) in let elimclause' = clenv_fchain indmv elimclause indclause in - res_pf elimclause' ~allow_K:allow_K gl + res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K gl (* cast added otherwise tactics Case (n1,n2) generates (?f x y) and * refine fails *) @@ -856,8 +855,8 @@ let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl = let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in elimtac elimclause indclause gl -let general_elim c e ?(allow_K=true) = - general_elim_clause (elimination_clause_scheme allow_K) c e +let general_elim with_evars c e ?(allow_K=true) = + general_elim_clause (elimination_clause_scheme with_evars allow_K) c e (* Elimination tactic with bindings but using the default elimination * constant associated with the type. *) @@ -866,22 +865,23 @@ let find_eliminator c gl = let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in lookup_eliminator ind (elimination_sort_of_goal gl) -let default_elim (c,_ as cx) gl = - general_elim cx (find_eliminator c gl,NoBindings) gl +let default_elim with_evars (c,_ as cx) gl = + general_elim with_evars cx (find_eliminator c gl,NoBindings) gl -let elim_in_context c = function - | Some elim -> general_elim c elim ~allow_K:true - | None -> default_elim c +let elim_in_context with_evars c = function + | Some elim -> general_elim with_evars c elim ~allow_K:true + | None -> default_elim with_evars c -let elim (c,lbindc as cx) elim = +let elim with_evars (c,lbindc as cx) elim = match kind_of_term c with | Var id when lbindc = NoBindings -> - tclTHEN (tclTRY (intros_until_id id)) (elim_in_context cx elim) - | _ -> elim_in_context cx elim + tclTHEN (tclTRY (intros_until_id id)) + (elim_in_context with_evars cx elim) + | _ -> elim_in_context with_evars cx elim (* The simplest elimination tactic, with no substitutions at all. *) -let simplest_elim c = default_elim (c,NoBindings) +let simplest_elim c = default_elim false (c,NoBindings) (* Elimination in hypothesis *) (* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y) @@ -915,23 +915,23 @@ let general_elim_in with_evars id = (* Case analysis tactics *) -let general_case_analysis_in_context (c,lbindc) gl = +let general_case_analysis_in_context with_evars (c,lbindc) gl = let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let sort = elimination_sort_of_goal gl in let case = if occur_term c (pf_concl gl) then make_case_dep else make_case_gen in let elim = pf_apply case gl mind sort in - general_elim (c,lbindc) (elim,NoBindings) gl + general_elim with_evars (c,lbindc) (elim,NoBindings) gl -let general_case_analysis (c,lbindc as cx) = +let general_case_analysis with_evars (c,lbindc as cx) = match kind_of_term c with | Var id when lbindc = NoBindings -> tclTHEN (tclTRY (intros_until_id id)) - (general_case_analysis_in_context cx) + (general_case_analysis_in_context with_evars cx) | _ -> - general_case_analysis_in_context cx + general_case_analysis_in_context with_evars cx -let simplest_case c = general_case_analysis (c,NoBindings) +let simplest_case c = general_case_analysis false (c,NoBindings) (*****************************) (* Decomposing introductions *) @@ -1615,16 +1615,15 @@ let empty_scheme = (* Unification between ((elimc:elimt) ?i ?j ?k ?l ... ?m) and the hypothesis on which the induction is made *) -let induction_tac varname typ scheme (*(elimc,lbindelimc),elimt*) gl = +let induction_tac with_evars (varname,lbind) typ scheme gl = let elimc,lbindelimc = match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in let elimt = scheme.elimt in - let c = mkVar varname in - let indclause = make_clenv_binding gl (c,typ) NoBindings in + let indclause = make_clenv_binding gl (mkVar varname,typ) lbind in let elimclause = make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in - elimination_clause_scheme true elimclause indclause gl + elimination_clause_scheme with_evars true elimclause indclause gl let make_base n id = if n=0 or n=1 then id @@ -2134,7 +2133,7 @@ let recolle_clenv scheme lid 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_felim indvars (* (elimc,lbindelimc) elimt *) scheme gl = +let induction_tac_felim with_evars indvars (* (elimc,lbindelimc) elimt *) scheme gl = let elimt = scheme.elimt in let elimc,lbindelimc = match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in @@ -2145,7 +2144,7 @@ let induction_tac_felim indvars (* (elimc,lbindelimc) elimt *) scheme gl = let elimclause' = recolle_clenv scheme indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver true elimclause' gl in - clenv_refine resolved gl + clenv_refine with_evars resolved gl (* Induction with several induction arguments, main differences with induction_from_context is that there is no main induction argument, @@ -2153,7 +2152,7 @@ let induction_tac_felim indvars (* (elimc,lbindelimc) elimt *) scheme gl = all args and params must be given, so we help a bit the unifier by making the "pattern" by hand before calling induction_tac_felim FIXME: REUNIF AVEC induction_tac_felim? *) -let induction_from_context_l isrec elim_info lid names gl = +let induction_from_context_l isrec with_evars elim_info lid names gl = let indsign,scheme = elim_info in (* number of all args, counting farg and indarg if present. *) let nargs_indarg_farg = scheme.nargs @@ -2202,7 +2201,7 @@ let induction_from_context_l isrec elim_info lid names gl = (* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all possible holes using arguments given by the user (but the functional one). *) - induction_tac_felim realindvars scheme; + induction_tac_felim with_evars realindvars scheme; tclTRY (thin (List.rev (indhyps))); ]) (array_map2 @@ -2212,7 +2211,7 @@ let induction_from_context_l isrec elim_info lid names gl = -let induction_from_context isrec elim_info hyp0 names gl = +let induction_from_context isrec with_evars elim_info (hyp0,lbind) names gl = (*test suivant sans doute inutile car refait par le letin_tac*) if List.mem hyp0 (ids_of_named_context (Global.named_context())) then errorlabstrm "induction" @@ -2247,7 +2246,7 @@ let induction_from_context isrec elim_info hyp0 names gl = thin dephyps; (if isrec then tclTHENFIRSTn else tclTHENLASTn) (tclTHENLIST - [ induction_tac hyp0 typ0 scheme (*scheme.elimc,scheme.elimt*); + [ induction_tac with_evars (hyp0,lbind) typ0 scheme; tclTHEN (tclTRY (unfold_body hyp0)) (thin [hyp0]); tclTRY (thin indhyps) ]) (array_map2 @@ -2259,22 +2258,22 @@ let induction_from_context isrec elim_info hyp0 names gl = exception TryNewInduct of exn -let induction_with_atomization_of_ind_arg isrec elim names hyp0 gl = +let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) gl = let (indsign,scheme as elim_info) = find_elim_signature isrec elim hyp0 gl in if scheme.indarg = None then (* This is not a standard induction scheme (the argument is probably a parameter) So try the more general induction mechanism. *) - induction_from_context_l isrec elim_info [hyp0] names gl + induction_from_context_l isrec with_evars elim_info [hyp0] names gl else let indref = match scheme.indref with | None -> assert false | Some x -> x in tclTHEN (atomize_param_of_ind (indref,scheme.nparams) hyp0) - (induction_from_context isrec elim_info hyp0 names) gl + (induction_from_context isrec with_evars elim_info (hyp0,lbind) names) gl (* Induction on a list of induction arguments. Analyse the elim scheme (which is mandatory for multiple ind args), check that all parameters and arguments are given (mandatory too). *) -let induction_without_atomization isrec elim names lid gl = +let induction_without_atomization isrec with_evars elim names lid gl = let (indsign,scheme as elim_info) = find_elim_signature isrec elim (List.hd lid) gl in let awaited_nargs = @@ -2285,26 +2284,29 @@ let induction_without_atomization isrec elim names lid gl = let nlid = List.length lid in if nlid <> awaited_nargs then error "Not the right number of induction arguments" - else induction_from_context_l isrec elim_info lid names gl + else induction_from_context_l isrec with_evars elim_info lid names gl -let new_induct_gen isrec elim names c gl = +let new_induct_gen isrec with_evars elim names (c,lbind) gl = match kind_of_term c with - | Var id when not (mem_named_context id (Global.named_context())) -> - induction_with_atomization_of_ind_arg isrec elim names id gl + | Var id when not (mem_named_context id (Global.named_context())) + & lbind = NoBindings & not with_evars -> + induction_with_atomization_of_ind_arg + isrec with_evars elim names (id,lbind) gl | _ -> let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in let id = fresh_id [] x gl in tclTHEN (letin_tac true (Name id) c allClauses) - (induction_with_atomization_of_ind_arg isrec elim names id) gl + (induction_with_atomization_of_ind_arg + isrec with_evars elim names (id,lbind)) gl (* Induction on a list of arguments. First make induction arguments atomic (using letins), then do induction. The specificity here is that all arguments and parameters of the scheme are given (mandatory for the moment), so we don't need to deal with parameters of the inductive type as in new_induct_gen. *) -let new_induct_gen_l isrec elim names lc gl = +let new_induct_gen_l isrec with_evars elim names lc gl = let newlc = ref [] in let letids = ref [] in let rec atomize_list l gl = @@ -2331,7 +2333,7 @@ let new_induct_gen_l isrec elim names lc gl = [ (atomize_list lc); (fun gl' -> (* recompute each time to have the new value of newlc *) - induction_without_atomization isrec elim names !newlc gl') ; + induction_without_atomization isrec with_evars elim names !newlc gl') ; (* after induction, try to unfold all letins created by atomize_list FIXME: unfold_all does not exist anywhere else? *) (fun gl' -> (* recompute each time to have the new value of letids *) @@ -2340,7 +2342,7 @@ let new_induct_gen_l isrec elim names lc gl = gl -let induct_destruct_l isrec lc elim names = +let induct_destruct_l isrec with_evars lc elim names = (* Several induction hyps: induction scheme is mandatory *) let _ = if elim = None @@ -2351,10 +2353,10 @@ let induct_destruct_l isrec lc elim names = List.map (fun x -> match x with (* FIXME: should we deal with ElimOnIdent? *) - | ElimOnConstr x -> x + | ElimOnConstr (x,NoBindings) -> x | _ -> error "don't know where to find some argument") lc in - new_induct_gen_l isrec elim names newlc + new_induct_gen_l isrec with_evars elim names newlc (* Induction either over a term, over a quantified premisse, or over @@ -2362,24 +2364,27 @@ let induct_destruct_l isrec lc elim names = principles). TODO: really unify induction with one and induction with several args *) -let induct_destruct isrec lc elim names = +let induct_destruct isrec with_evars lc elim names = assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) if List.length lc = 1 then (* induction on one arg: use old mechanism *) try let c = List.hd lc in match c with - | ElimOnConstr c -> new_induct_gen isrec elim names c + | ElimOnConstr c -> new_induct_gen isrec with_evars elim names c | ElimOnAnonHyp n -> tclTHEN (intros_until_n n) - (tclLAST_HYP (new_induct_gen isrec elim names)) + (tclLAST_HYP (fun c -> + new_induct_gen isrec with_evars elim names (c,NoBindings))) (* Identifier apart because id can be quantified in goal and not typable *) | ElimOnIdent (_,id) -> tclTHEN (tclTRY (intros_until_id id)) - (new_induct_gen isrec elim names (mkVar id)) + (new_induct_gen isrec with_evars elim names (mkVar id,NoBindings)) with (* If this fails, try with new mechanism but if it fails too, then the exception is the first one. *) - | x -> (try induct_destruct_l isrec lc elim names with _ -> raise x) - else induct_destruct_l isrec lc elim names + | x -> + (try induct_destruct_l isrec with_evars lc elim names + with _ -> raise x) + else induct_destruct_l isrec with_evars lc elim names diff --git a/tactics/tactics.mli b/tactics/tactics.mli index dfadeb54f..eb62f602a 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -231,27 +231,29 @@ type elim_scheme = { val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme -val general_elim : +val general_elim : evars_flag -> constr with_ebindings -> constr with_ebindings -> ?allow_K:bool -> tactic val general_elim_in : evars_flag -> identifier -> constr with_ebindings -> constr with_ebindings -> tactic -val default_elim : constr with_ebindings -> tactic +val default_elim : evars_flag -> constr with_ebindings -> tactic val simplest_elim : constr -> tactic -val elim : constr with_ebindings -> constr with_ebindings option -> tactic +val elim : + evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic + val simple_induct : quantified_hypothesis -> tactic -val new_induct : constr induction_arg list -> constr with_ebindings option -> - intro_pattern_expr -> tactic +val new_induct : evars_flag -> constr with_ebindings induction_arg list -> + constr with_ebindings option -> intro_pattern_expr -> tactic (*s Case analysis tactics. *) -val general_case_analysis : constr with_ebindings -> tactic +val general_case_analysis : evars_flag -> constr with_ebindings -> tactic val simplest_case : constr -> tactic val simple_destruct : quantified_hypothesis -> tactic -val new_destruct : constr induction_arg list -> constr with_ebindings option -> - intro_pattern_expr -> tactic +val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> + constr with_ebindings option -> intro_pattern_expr -> tactic (*s Eliminations giving the type instead of the proof. *) |