From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- tactics/auto.ml | 26 +++-- tactics/auto.mli | 2 +- tactics/autorewrite.ml | 2 +- tactics/autorewrite.mli | 2 +- tactics/btermdn.ml | 2 +- tactics/btermdn.mli | 2 +- tactics/class_tactics.ml4 | 2 +- tactics/contradiction.ml | 2 +- tactics/contradiction.mli | 2 +- tactics/eauto.ml4 | 2 +- tactics/eauto.mli | 2 +- tactics/elim.ml | 2 +- tactics/elim.mli | 2 +- tactics/elimschemes.ml | 2 +- tactics/elimschemes.mli | 2 +- tactics/eqdecide.ml4 | 2 +- tactics/eqschemes.ml | 2 +- tactics/eqschemes.mli | 2 +- tactics/equality.ml | 2 +- tactics/equality.mli | 2 +- tactics/evar_tactics.ml | 2 +- tactics/evar_tactics.mli | 2 +- tactics/extraargs.ml4 | 2 +- tactics/extraargs.mli | 2 +- tactics/extratactics.ml4 | 8 +- tactics/extratactics.mli | 2 +- tactics/hiddentac.ml | 25 ++--- tactics/hiddentac.mli | 21 ++-- tactics/hipattern.ml4 | 2 +- tactics/hipattern.mli | 2 +- tactics/inv.ml | 2 +- tactics/inv.mli | 2 +- tactics/leminv.ml | 2 +- tactics/nbtermdn.ml | 2 +- tactics/nbtermdn.mli | 2 +- tactics/refine.ml | 2 +- tactics/refine.mli | 2 +- tactics/rewrite.ml4 | 247 ++++++++++++++++++++++++++++++++-------------- tactics/tacinterp.ml | 65 +++++++----- tactics/tacinterp.mli | 3 +- tactics/tactic_option.ml | 2 +- tactics/tactic_option.mli | 2 +- tactics/tacticals.ml | 2 +- tactics/tacticals.mli | 2 +- tactics/tactics.ml | 21 ++-- tactics/tactics.mli | 6 +- tactics/tauto.ml4 | 2 +- tactics/termdn.ml | 2 +- tactics/termdn.mli | 2 +- 49 files changed, 324 insertions(+), 178 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 8a0de08b..041bb44b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* str"Ø" | PathEpsilon -> str"ε" -let rec subst_hints_path subst hp = - match hp with - | PathAtom PathAny -> hp - | PathAtom (PathHints grs) -> +let subst_path_atom subst p = + match p with + | PathAny -> p + | PathHints grs -> let gr' gr = fst (subst_global subst gr) in let grs' = list_smartmap gr' grs in - if grs' == grs then hp else PathAtom (PathHints grs') + if grs' == grs then p else PathHints grs' + +let rec subst_hints_path subst hp = + match hp with + | PathAtom p -> + let p' = subst_path_atom subst p in + if p' == p then hp else PathAtom p' | PathStar p -> let p' = subst_hints_path subst p in if p' == p then hp else PathStar p' | PathSeq (p, q) -> @@ -386,7 +392,7 @@ module Hint_db = struct let db = if db.use_dn && rebuild then rebuild_db st' db else db in addkv k (next_hint_id db) v db - let add_list l db = List.fold_right add_one l db + let add_list l db = List.fold_left (fun db k -> add_one k db) db l let remove_sdl p sdl = list_smartfilter p sdl let remove_he st p (sl1, sl2, dn as he) = @@ -672,9 +678,10 @@ let subst_autohint (subst,(local,name,hintlist as obj)) = let tac' = !forward_subst_tactic subst tac in if tac==tac' then data.code else Extern tac' in + let name' = subst_path_atom subst data.name in let data' = - if data.pat==pat' && data.code==code' then data - else { data with pat = pat'; code = code' } + if data.pat==pat' && data.name == name' && data.code==code' then data + else { data with pat = pat'; name = name'; code = code' } in if k' == k && data' == data then hint else (k',data') in @@ -848,6 +855,7 @@ let interp_hints h = | HintsConstructors lqid -> let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in + Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind"; list_tabulate (fun i -> let c = (ind,i+1) in None, true, PathHints [ConstructRef c], mkConstruct c) (nconstructors ind) in diff --git a/tactics/auto.mli b/tactics/auto.mli index 87786e5b..7daebb36 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* tclFAIL 0 (str "Not a variable or hypothesis") ] END +TACTIC EXTEND is_fix +| [ "is_fix" constr(x) ] -> + [ match kind_of_term x with + | Fix _ -> Tacticals.tclIDTAC + | _ -> Tacticals.tclFAIL 0 (Pp.str "not a fix definition") ] +END;; (* Command to grab the evars left unresolved at the end of a proof. *) (* spiwack: I put it in extratactics because it is somewhat tied with diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 66f46722..3f30ddb4 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ElimOnAnonHyp n let h_induction_destruct isrec ev lcl = - let lcl' = on_fst (List.map (fun (a,b,c) ->(List.map out_indarg a,b,c))) lcl in + let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in abstract_tactic (TacInductionDestruct (isrec,ev,lcl')) (induction_destruct isrec ev lcl) -let h_new_induction ev c e idl cl = - h_induction_destruct true ev ([c,e,idl],cl) -let h_new_destruct ev c e idl cl = h_induction_destruct false ev ([c,e,idl],cl) +let h_new_induction ev c idl e cl = + h_induction_destruct true ev ([c,idl],e,cl) +let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl) let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d) let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 96e7e3f0..f31b3a80 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* tactic val h_generalize : constr list -> tactic val h_generalize_gen : (constr with_occurrences * name) list -> tactic val h_generalize_dep : constr -> tactic -val h_let_tac : letin_flag -> name -> constr -> - Tacticals.clause -> tactic +val h_let_tac : letin_flag -> name -> constr -> Tacticals.clause -> + intro_pattern_expr located option -> tactic val h_let_pat_tac : letin_flag -> name -> evar_map * constr -> - Tacticals.clause -> tactic + Tacticals.clause -> intro_pattern_expr located option -> + tactic (** Derived basic tactics *) @@ -66,19 +67,19 @@ val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic val h_new_induction : evars_flag -> - (evar_map * constr with_bindings) induction_arg list -> - constr with_bindings option -> + (evar_map * constr with_bindings) induction_arg -> intro_pattern_expr located option * intro_pattern_expr located option -> + constr with_bindings option -> Tacticals.clause option -> tactic val h_new_destruct : evars_flag -> - (evar_map * constr with_bindings) induction_arg list -> - constr with_bindings option -> + (evar_map * constr with_bindings) induction_arg -> intro_pattern_expr located option * intro_pattern_expr located option -> + constr with_bindings option -> Tacticals.clause option -> tactic val h_induction_destruct : rec_flag -> evars_flag -> - ((evar_map * constr with_bindings) induction_arg list * - constr with_bindings option * + ((evar_map * constr with_bindings) induction_arg * (intro_pattern_expr located option * intro_pattern_expr located option)) list + * constr with_bindings option * Tacticals.clause option -> tactic val h_specialize : int option -> constr with_bindings -> tactic diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 9057c60d..8a1b5996 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* assert false) | _ -> assert false +let arrow_morphism ta tb a b = + let ap = is_Prop ta and bp = is_Prop tb in + if ap && bp then mkApp (Lazy.force impl, [| a; b |]), unfold_impl + else if ap then (* Domain in Prop, CoDomain in Type *) + mkProd (Anonymous, a, b), (fun x -> x) + else if bp then (* Dummy forall *) + mkApp (Lazy.force coq_all, [| a; mkLambda (Anonymous, a, b) |]), unfold_forall + else (* None in Prop, use arrow *) + mkApp (Lazy.force arrow, [| a; b |]), unfold_impl + let rec decomp_pointwise n c = if n = 0 then c else @@ -814,9 +819,10 @@ let subterm all flags (s : strategy) : strategy = | Prod (n, x, b) when noccurn 1 b -> let b = subst1 mkProp b in let tx = Typing.type_of env (goalevars evars) x and tb = Typing.type_of env (goalevars evars) b in - let res = aux env avoid (mkApp (arrow_morphism tx tb, [| x; b |])) ty cstr evars in + let mor, unfold = arrow_morphism tx tb x b in + let res = aux env avoid mor ty cstr evars in (match res with - | Some (Some r) -> Some (Some { r with rew_to = unfold_impl r.rew_to }) + | Some (Some r) -> Some (Some { r with rew_to = unfold r.rew_to }) | _ -> res) (* if x' = None && flags.under_lambdas then *) @@ -1048,6 +1054,22 @@ module Strategies = rew_prf = RewCast DEFAULTcast; rew_evars = sigma, cstrevars evars }) with _ -> None + + let fold_glob c : strategy = + fun env avoid t ty cstr evars -> +(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *) + let sigma, c = Pretyping.Default.understand_tcc (goalevars evars) env c in + let unfolded = + try Tacred.try_red_product env sigma c + with _ -> error "fold: the term is not unfoldable !" + in + try + let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in + let c' = Evarutil.nf_evar sigma c in + Some (Some { rew_car = ty; rew_from = t; rew_to = c'; + rew_prf = RewCast DEFAULTcast; + rew_evars = sigma, cstrevars evars }) + with _ -> None end @@ -1096,8 +1118,6 @@ let map_rewprf f = function | RewPrf (rel, prf) -> RewPrf (f rel, f prf) | RewCast c -> RewCast c -exception RewriteFailure - type result = (evar_map * constr option * types) option option let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result = @@ -1162,9 +1182,9 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl = let evartac evd = Refiner.tclEVARS evd in let treat res = match res with - | None -> raise RewriteFailure + | None -> tclFAIL 0 (str "Nothing to rewrite") | Some None -> - tclFAIL 0 (str"setoid rewrite failed: no progress made") + tclFAIL 0 (str"No progress made") | Some (Some (undef, p, newt)) -> let tac = match clause, p with @@ -1195,7 +1215,7 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl = | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> Refiner.tclFAIL_lazy 0 - (lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints." + (lazy (str"Unable to satisfy the rewriting constraints." ++ fnl () ++ Himsg.explain_typeclass_error env e)) in tac gl @@ -1243,12 +1263,15 @@ let assert_replacing id newt tac = in Proofview.tclTHEN (Proofview.tclSENSITIVE sens) (Proofview.tclFOCUS 2 2 tac) +let newfail n s = + Proofview.tclZERO (Refiner.FailError (n, lazy s)) + let cl_rewrite_clause_newtac ?abs strat clause = let treat (res, is_hyp) = match res with - | None -> raise RewriteFailure + | None -> newfail 0 (str "Nothing to rewrite") | Some None -> - fail 0 (str"setoid rewrite failed: no progress made") + newfail 0 (str"No progress made") | Some (Some res) -> match is_hyp, res with | Some id, (undef, Some p, newt) -> @@ -1288,22 +1311,25 @@ let cl_rewrite_clause_newtac ?abs strat clause = let cl_rewrite_clause_new_strat ?abs strat clause = init_setoid (); - try cl_rewrite_clause_newtac ?abs strat clause - with RewriteFailure -> - fail 0 (str"setoid rewrite failed: strategy failed") + cl_rewrite_clause_newtac ?abs strat clause let cl_rewrite_clause_newtac' l left2right occs clause = Proof_global.run_tactic (Proofview.tclFOCUS 1 1 (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)) -let cl_rewrite_clause_strat strat clause gl = - init_setoid (); - let meta = Evarutil.new_meta() in -(* let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in *) + +let tactic_init_setoid () = + init_setoid (); tclIDTAC + +let cl_rewrite_clause_strat strat clause = + tclTHEN (tactic_init_setoid ()) + (fun gl -> + let meta = Evarutil.new_meta() in try cl_rewrite_clause_tac strat (mkMeta meta) clause gl - with RewriteFailure -> - tclFAIL 0 (str"setoid rewrite failed: strategy failed") gl + with + | Refiner.FailError (n, pp) -> + tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl) let cl_rewrite_clause l left2right occs clause gl = cl_rewrite_clause_strat (rewrite_with (general_rewrite_unif_flags ()) l left2right occs) clause gl @@ -1329,13 +1355,25 @@ let apply_constr_expr c l2r occs = fun env avoid t ty cstr evars -> apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings)) l2r occs env avoid t ty cstr (evd, cstrevars evars) +let apply_glob_constr c l2r occs = fun env avoid t ty cstr evars -> + let evd, c = (Pretyping.Default.understand_tcc (goalevars evars) env c) in + apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings)) + l2r occs env avoid t ty cstr (evd, cstrevars evars) + let interp_constr_list env sigma = List.map (fun c -> let evd, c = Constrintern.interp_open_constr sigma env c in (evd, (c, NoBindings)), true) +let interp_glob_constr_list env sigma = + List.map (fun c -> + let evd, c = Pretyping.Default.understand_tcc sigma env c in + (evd, (c, NoBindings)), true) + open Pcoq +(* Syntax for rewriting with strategies *) + type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings @@ -1364,58 +1402,127 @@ ARGUMENT EXTEND glob_constr_with_bindings [ constr_with_bindings(bl) ] -> [ bl ] END -let _ = - (Genarg.create_arg None "strategy" : - ((strategy, Genarg.tlevel) Genarg.abstract_argument_type * - (strategy, Genarg.glevel) Genarg.abstract_argument_type * - (strategy, Genarg.rlevel) Genarg.abstract_argument_type)) - - +type ('constr,'redexpr) strategy_ast = + | StratId | StratFail | StratRefl + | StratUnary of string * ('constr,'redexpr) strategy_ast + | StratBinary of string * ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast + | StratConstr of 'constr * bool + | StratTerms of 'constr list + | StratHints of bool * string + | StratEval of 'redexpr + | StratFold of 'constr + +let rec map_strategy (f : 'a -> 'a2) (g : 'b -> 'b2) : ('a,'b) strategy_ast -> ('a2,'b2) strategy_ast = function + | StratId | StratFail | StratRefl as s -> s + | StratUnary (s, str) -> StratUnary (s, map_strategy f g str) + | StratBinary (s, str, str') -> StratBinary (s, map_strategy f g str, map_strategy f g str') + | StratConstr (c, b) -> StratConstr (f c, b) + | StratTerms l -> StratTerms (List.map f l) + | StratHints (b, id) -> StratHints (b, id) + | StratEval r -> StratEval (g r) + | StratFold c -> StratFold (f c) + +let rec strategy_of_ast = function + | StratId -> Strategies.id + | StratFail -> Strategies.fail + | StratRefl -> Strategies.refl + | StratUnary (f, s) -> + let s' = strategy_of_ast s in + let f' = match f with + | "subterms" -> all_subterms + | "subterm" -> one_subterm + | "innermost" -> Strategies.innermost + | "outermost" -> Strategies.outermost + | "bottomup" -> Strategies.bu + | "topdown" -> Strategies.td + | "progress" -> Strategies.progress + | "try" -> Strategies.try_ + | "any" -> Strategies.any + | "repeat" -> Strategies.repeat + | _ -> anomalylabstrm "strategy_of_ast" (str"Unkwnon strategy: " ++ str f) + in f' s' + | StratBinary (f, s, t) -> + let s' = strategy_of_ast s in + let t' = strategy_of_ast t in + let f' = match f with + | "compose" -> Strategies.seq + | "choice" -> Strategies.choice + | _ -> anomalylabstrm "strategy_of_ast" (str"Unkwnon strategy: " ++ str f) + in f' s' t' + | StratConstr (c, b) -> apply_glob_constr (fst c) b all_occurrences + | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id + | StratTerms l -> + (fun env avoid t ty cstr evars -> + let l' = interp_glob_constr_list env (goalevars evars) (List.map fst l) in + Strategies.lemmas rewrite_unif_flags l' env avoid t ty cstr evars) + | StratEval r -> + (fun env avoid t ty cstr evars -> + let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in + Strategies.reduce r_interp env avoid t ty cstr (sigma,cstrevars evars)) + | StratFold c -> Strategies.fold_glob (fst c) + + +type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast +type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast + +let interp_strategy ist gl s = + let sigma = project gl in + sigma, strategy_of_ast s +let glob_strategy ist s = map_strategy (Tacinterp.intern_constr ist) (fun c -> c) s +let subst_strategy s str = str let pr_strategy _ _ _ (s : strategy) = Pp.str "" +let pr_raw_strategy _ _ _ (s : raw_strategy) = Pp.str "" +let pr_glob_strategy _ _ _ (s : glob_strategy) = Pp.str "" -let interp_strategy ist gl c = project gl , c -let glob_strategy ist l = l -let subst_strategy evm l = l - - -ARGUMENT EXTEND rewstrategy TYPED AS strategy +ARGUMENT EXTEND rewstrategy PRINTED BY pr_strategy + INTERPRETED BY interp_strategy GLOBALIZED BY glob_strategy SUBSTITUTED BY subst_strategy - [ constr(c) ] -> [ apply_constr_expr c true all_occurrences ] - | [ "<-" constr(c) ] -> [ apply_constr_expr c false all_occurrences ] - | [ "subterms" rewstrategy(h) ] -> [ all_subterms h ] - | [ "subterm" rewstrategy(h) ] -> [ one_subterm h ] - | [ "innermost" rewstrategy(h) ] -> [ Strategies.innermost h ] - | [ "outermost" rewstrategy(h) ] -> [ Strategies.outermost h ] - | [ "bottomup" rewstrategy(h) ] -> [ Strategies.bu h ] - | [ "topdown" rewstrategy(h) ] -> [ Strategies.td h ] - | [ "id" ] -> [ Strategies.id ] - | [ "refl" ] -> [ Strategies.refl ] - | [ "progress" rewstrategy(h) ] -> [ Strategies.progress h ] - | [ "fail" ] -> [ Strategies.fail ] - | [ "try" rewstrategy(h) ] -> [ Strategies.try_ h ] - | [ "any" rewstrategy(h) ] -> [ Strategies.any h ] - | [ "repeat" rewstrategy(h) ] -> [ Strategies.repeat h ] - | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ Strategies.seq h h' ] + RAW_TYPED AS raw_strategy + RAW_PRINTED BY pr_raw_strategy + + GLOB_TYPED AS glob_strategy + GLOB_PRINTED BY pr_glob_strategy + + [ glob(c) ] -> [ StratConstr (c, true) ] + | [ "<-" constr(c) ] -> [ StratConstr (c, false) ] + | [ "subterms" rewstrategy(h) ] -> [ StratUnary ("all_subterms", h) ] + | [ "subterm" rewstrategy(h) ] -> [ StratUnary ("one_subterm", h) ] + | [ "innermost" rewstrategy(h) ] -> [ StratUnary("innermost", h) ] + | [ "outermost" rewstrategy(h) ] -> [ StratUnary("outermost", h) ] + | [ "bottomup" rewstrategy(h) ] -> [ StratUnary("bottomup", h) ] + | [ "topdown" rewstrategy(h) ] -> [ StratUnary("topdown", h) ] + | [ "id" ] -> [ StratId ] + | [ "fail" ] -> [ StratFail ] + | [ "refl" ] -> [ StratRefl ] + | [ "progress" rewstrategy(h) ] -> [ StratUnary ("progress", h) ] + | [ "try" rewstrategy(h) ] -> [ StratUnary ("try", h) ] + | [ "any" rewstrategy(h) ] -> [ StratUnary ("any", h) ] + | [ "repeat" rewstrategy(h) ] -> [ StratUnary ("repeat", h) ] + | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ StratBinary ("compose", h, h') ] | [ "(" rewstrategy(h) ")" ] -> [ h ] - | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ Strategies.choice h h' ] - | [ "old_hints" preident(h) ] -> [ Strategies.old_hints h ] - | [ "hints" preident(h) ] -> [ Strategies.hints h ] - | [ "terms" constr_list(h) ] -> [ fun env avoid t ty cstr evars -> - Strategies.lemmas rewrite_unif_flags (interp_constr_list env (goalevars evars) h) env avoid t ty cstr evars ] - | [ "eval" red_expr(r) ] -> [ fun env avoid t ty cstr evars -> - let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in - Strategies.reduce r_interp env avoid t ty cstr (sigma,cstrevars evars) ] - | [ "fold" constr(c) ] -> [ Strategies.fold c ] + | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ StratBinary ("choice", h, h') ] + | [ "old_hints" preident(h) ] -> [ StratHints (true, h) ] + | [ "hints" preident(h) ] -> [ StratHints (false, h) ] + | [ "terms" constr_list(h) ] -> [ StratTerms h ] + | [ "eval" red_expr(r) ] -> [ StratEval r ] + | [ "fold" constr(c) ] -> [ StratFold c ] END +(* By default the strategy for "rewrite_db" is top-down *) + +let db_strat db = Strategies.td (Strategies.hints db) +let cl_rewrite_clause_db db cl = cl_rewrite_clause_strat (db_strat db) cl + TACTIC EXTEND rewrite_strat | [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ] | [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ] +| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ] +| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ] END let clsubstitute o c = @@ -1841,16 +1948,10 @@ let apply_lemma gl (c,l) cl l2r occs = let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = let meta = Evarutil.new_meta() in let hypinfo, strat = apply_lemma gl (c,l) cl l2r occs in - try - tclWEAK_PROGRESS - (tclTHEN - (Refiner.tclEVARS hypinfo.cl.evd) - (cl_rewrite_clause_tac ~abs:hypinfo.abs strat (mkMeta meta) cl)) gl - with RewriteFailure -> - let {l2r=l2r; c1=x; c2=y} = hypinfo in - raise (Pretype_errors.PretypeError - (pf_env gl,project gl, - Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl))) + tclWEAK_PROGRESS + (tclTHEN + (Refiner.tclEVARS hypinfo.cl.evd) + (cl_rewrite_clause_tac ~abs:hypinfo.abs strat (mkMeta meta) cl)) gl let general_s_rewrite_clause x = init_setoid (); @@ -1948,7 +2049,7 @@ let implify id gl = let sigma = project gl in let tyhd = Typing.type_of env sigma ty and tyconcl = Typing.type_of (Environ.push_rel hd env) sigma concl in - let app = mkApp (arrow_morphism tyhd (subst1 mkProp tyconcl), [| ty; (subst1 mkProp concl) |]) in + let app, unfold = arrow_morphism tyhd (subst1 mkProp tyconcl) ty (subst1 mkProp concl) in it_mkProd_or_LetIn app tl | _ -> ctype in convert_hyp_no_check (id, b, ctype') gl diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3efff8fa..3ff0cf93 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* List.iter (fun (_, r) -> + try + Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) + (Smartlocate.smart_global r) + with _ -> ()) occs + | Cbv grf | Lazy grf -> + List.iter (fun r -> + try + Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) + (Smartlocate.smart_global r) + with _ -> ()) grf.rConst + | _ -> () + let intern_red_expr ist = function | Unfold l -> Unfold (List.map (intern_unfold ist) l) | Fold l -> Fold (List.map (intern_constr ist) l) @@ -707,10 +723,11 @@ let rec intern_atomic lf ist x = intern_constr_with_occurrences ist c, intern_name lf ist na) cl) | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c) - | TacLetTac (na,c,cls,b) -> + | TacLetTac (na,c,cls,b,eqpat) -> let na = intern_name lf ist na in TacLetTac (na,intern_constr ist c, - (clause_app (intern_hyp_location ist) cls),b) + (clause_app (intern_hyp_location ist) cls),b, + (Option.map (intern_intro_pattern lf ist) eqpat)) (* Automation tactics *) | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l) @@ -721,12 +738,12 @@ let rec intern_atomic lf ist x = (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) -> TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h) - | TacInductionDestruct (ev,isrec,(l,cls)) -> - TacInductionDestruct (ev,isrec,(List.map (fun (lc,cbo,(ipato,ipats)) -> - (List.map (intern_induction_arg ist) lc, - Option.map (intern_constr_with_bindings ist) cbo, + | TacInductionDestruct (ev,isrec,(l,el,cls)) -> + TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats)) -> + (intern_induction_arg ist c, (Option.map (intern_intro_pattern lf ist) ipato, Option.map (intern_intro_pattern lf ist) ipats))) l, + Option.map (intern_constr_with_bindings ist) el, Option.map (clause_app (intern_hyp_location ist)) cls)) | TacDoubleInduction (h1,h2) -> let h1 = intern_quantified_hypothesis ist h1 in @@ -759,6 +776,7 @@ let rec intern_atomic lf ist x = (* Conversion *) | TacReduce (r,cl) -> + dump_glob_red_expr r; TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) | TacChange (None,c,cl) -> TacChange (None, @@ -2384,18 +2402,18 @@ and interp_atomic ist gl tac = tclTHEN (tclEVARS sigma) (h_generalize_dep c_interp) - | TacLetTac (na,c,clp,b) -> + | TacLetTac (na,c,clp,b,eqpat) -> let clp = interp_clause ist gl clp in if clp = nowhere then - (* We try to fully-typechect the term *) + (* We try to fully-typecheck the term *) let (sigma,c_interp) = pf_interp_constr ist gl c in tclTHEN (tclEVARS sigma) - (h_let_tac b (interp_fresh_name ist env na) c_interp clp) + (h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat) else (* We try to keep the pattern structure as much as possible *) h_let_pat_tac b (interp_fresh_name ist env na) - (interp_pure_open_constr ist env sigma c) clp + (interp_pure_open_constr ist env sigma c) clp eqpat (* Automation tactics *) | TacTrivial (debug,lems,l) -> @@ -2410,17 +2428,17 @@ and interp_atomic ist gl tac = (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) -> h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h) - | TacInductionDestruct (isrec,ev,(l,cls)) -> + | TacInductionDestruct (isrec,ev,(l,el,cls)) -> let sigma, l = - list_fold_map (fun sigma (lc,cbo,(ipato,ipats)) -> - let lc = List.map (interp_induction_arg ist gl) lc in - let sigma,cbo = - Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in - (sigma,(lc,cbo, + list_fold_map (fun sigma (c,(ipato,ipats)) -> + let c = interp_induction_arg ist gl c in + (sigma,(c, (Option.map (interp_intro_pattern ist gl) ipato, Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in + let sigma,el = + Option.fold_map (interp_constr_with_bindings ist env) sigma el in let cls = Option.map (interp_clause ist gl) cls in - tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,cls) + tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2839,7 +2857,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c) - | TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_glob_constr subst c,clp,b) + | TacLetTac (id,c,clp,b,eqpat) -> + TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat) (* Automation tactics *) | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l) @@ -2847,10 +2866,10 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) as x -> x - | TacInductionDestruct (isrec,ev,(l,cls)) -> - TacInductionDestruct (isrec,ev,(List.map (fun (lc,cbo,ids) -> - List.map (subst_induction_arg subst) lc, - Option.map (subst_glob_with_bindings subst) cbo, ids) l, cls)) + | TacInductionDestruct (isrec,ev,(l,el,cls)) -> + let l' = List.map (fun (c,ids) -> subst_induction_arg subst c, ids) l in + let el' = Option.map (subst_glob_with_bindings subst) el in + TacInductionDestruct (isrec,ev,(l',el',cls)) | TacDoubleInduction (h1,h2) as x -> x | TacDecomposeAnd c -> TacDecomposeAnd (subst_glob_constr subst c) | TacDecomposeOr c -> TacDecomposeOr (subst_glob_constr subst c) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index b9fd64f6..573efb19 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* goal sigma -> glob_tactic_expr -> Evd.evar_map * constr (** Interprets redexp arguments *) +val dump_glob_red_expr : raw_red_expr -> unit val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr (** Interprets tactic expressions *) diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml index 57b8c540..b846c9eb 100644 --- a/tactics/tactic_option.ml +++ b/tactics/tactic_option.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* tclIDTAC - | [a,b,c],cl -> induct_destruct isrec with_evars (a,b,c,cl) - | (a,b,c)::l,cl -> + | [],_,_ -> tclIDTAC + | [a,b],el,cl -> induct_destruct isrec with_evars ([a],el,b,cl) + | (a,b)::l,None,cl -> tclTHEN - (induct_destruct isrec with_evars (a,b,c,cl)) - (tclMAP (fun (a,b,c) -> induct_destruct false with_evars (a,b,c,cl)) l) + (induct_destruct isrec with_evars ([a],None,b,cl)) + (tclMAP (fun (a,b) -> induct_destruct false with_evars ([a],None,b,cl)) l) + | l,Some el,cl -> + let check_basic_using = function + | a,(None,None) -> a + | _ -> error "Unsupported syntax for \"using\"." + in + let l' = List.map check_basic_using l in + induct_destruct isrec with_evars (l', Some el, (None,None), cl) let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls) let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls) @@ -3406,7 +3413,7 @@ let intros_symmetry = (* Transitivity tactics *) -(* This tactic first tries to apply a constant named trans_eq, where eq +(* This tactic first tries to apply a constant named eq_trans, where eq is the name of the equality predicate. If this constant is not defined and the conclusion is a=b, it solves the goal doing Cut x1=x2; diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f8f32b79..7e24156a 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (** {6 Generic case analysis / induction tactics. } *) val induction_destruct : rec_flag -> evars_flag -> - ((evar_map * constr with_bindings) induction_arg list * - constr with_bindings option * + ((evar_map * constr with_bindings) induction_arg * (intro_pattern_expr located option * intro_pattern_expr located option)) list * + constr with_bindings option * clause option -> tactic (** {6 Eliminations giving the type instead of the proof. } *) diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index b7a58be4..4189832e 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*