diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-30 18:46:00 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-06-30 18:46:00 +0000 |
commit | fa7e44d2b1a71fd8662ee720efdde2295679975b (patch) | |
tree | 2df28cd5b608f0a6cfc1cc3689dbaa885d5673bb | |
parent | f8e2c78e8bfd8679a77e3cf676bde58c4efffd45 (diff) |
Add new variants of [rewrite] and [autorewrite] which differ in the
selection of occurrences.
We use a new function [unify_to_subterm_all] to return all occurrences
of a lemma and produce the rewrite depending on a new [conditions] option
that controls if we must rewrite one or all occurrences and if the side
conditions should be solved or not for a single rewrite to be successful.
[rewrite*] will rewrite the first occurrence whose side-conditions are
solved while [autorewrite*] will rewrite all occurrences whose
side-conditions are solved.
Not supported by [setoid_rewrite] yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12218 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | pretyping/unification.ml | 64 | ||||
-rw-r--r-- | pretyping/unification.mli | 3 | ||||
-rw-r--r-- | tactics/autorewrite.ml | 28 | ||||
-rw-r--r-- | tactics/autorewrite.mli | 14 | ||||
-rw-r--r-- | tactics/equality.ml | 118 | ||||
-rw-r--r-- | tactics/equality.mli | 36 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 33 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 2 |
8 files changed, 221 insertions, 77 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c1bca3f9f..ba8c37fb6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -783,6 +783,70 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd = with ex when precatchable_exception ex -> raise (PretypeError (env,NoOccurrenceFound (op, None))) +(* Tries to find all instances of term [cl] in term [op]. + Unifies [cl] to every subterm of [op] and return all the matches. + Fails if no match is found *) +let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd = + let return a b = + let (evd,c as a) = a () in + if List.exists (fun (evd',c') -> eq_constr c c') b then b else a :: b + in + let fail str _ = error str in + let bind f g a = + let a1 = try f a + with ex + when precatchable_exception ex -> a + in try g a1 + with ex + when precatchable_exception ex -> a1 + in + let bind_iter f a = + let n = Array.length a in + let rec ffail i = + if i = n then fun a -> a + else bind (f a.(i)) (ffail (i+1)) + in ffail 0 + in + let rec matchrec cl = + let cl = strip_outer_cast cl in + (bind + (if closed0 cl + then return (fun () -> w_typed_unify env topconv flags op cl evd,cl) + else fail "Bound 1") + (match kind_of_term cl with + | App (f,args) -> + let n = Array.length args in + assert (n>0); + let c1 = mkApp (f,Array.sub args 0 (n-1)) in + let c2 = args.(n-1) in + bind (matchrec c1) (matchrec c2) + + | Case(_,_,c,lf) -> (* does not search in the predicate *) + bind (matchrec c) (bind_iter matchrec lf) + + | LetIn(_,c1,_,c2) -> + bind (matchrec c1) (matchrec c2) + + | Fix(_,(_,types,terms)) -> + bind (bind_iter matchrec types) (bind_iter matchrec terms) + + | CoFix(_,(_,types,terms)) -> + bind (bind_iter matchrec types) (bind_iter matchrec terms) + + | Prod (_,t,c) -> + bind (matchrec t) (matchrec c) + + | Lambda (_,t,c) -> + bind (matchrec t) (matchrec c) + + | _ -> fail "Match_subterm")) + in + let res = matchrec cl [] in + if res = [] then + raise (PretypeError (env,NoOccurrenceFound (op, None))) + else + res + let w_unify_to_subterm_list env flags allow_K oplist t evd = List.fold_right (fun op (evd,l) -> diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0e85f8243..8d71ec4bd 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -34,6 +34,9 @@ val w_unify : val w_unify_to_subterm : env -> ?flags:unify_flags -> constr * constr -> evar_defs -> evar_defs * constr +val w_unify_to_subterm_all : + env -> ?flags:unify_flags -> constr * constr -> evar_defs -> (evar_defs * constr) list + val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs (* [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 2472c1274..04c4ed161 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -111,33 +111,35 @@ let one_base general_rewrite_maybe_in tac_main bas = tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) -> tclTHEN tac (tclREPEAT_MAIN - (tclTHENSFIRSTn (general_rewrite_maybe_in dir csr) [|tac_main|] tc))) + (tclTHENFIRST (general_rewrite_maybe_in dir csr tc) tac_main))) tclIDTAC lrul)) (* The AutoRewrite tactic *) -let autorewrite tac_main lbas = +let autorewrite ?(conds=Naive) tac_main lbas = tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac bas -> tclTHEN tac - (one_base (fun dir -> general_rewrite dir all_occurrences) + (one_base (fun dir c tac -> + let tac = tac, conds in + general_rewrite dir all_occurrences ~tac c) tac_main bas)) tclIDTAC lbas)) -let autorewrite_multi_in idl tac_main lbas : tactic = +let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic = fun gl -> (* let's check at once if id exists (to raise the appropriate error) *) let _ = List.map (Tacmach.pf_get_hyp gl) idl in let general_rewrite_in id = let id = ref id in let to_be_cleared = ref false in - fun dir cstr gl -> + fun dir cstr tac gl -> let last_hyp_id = match (Environ.named_context_of_val gl.Evd.it.Evd.evar_hyps) with (last_hyp_id,_,_)::_ -> last_hyp_id | _ -> (* even the hypothesis id is missing *) error ("No such hypothesis: " ^ (string_of_id !id) ^".") in - let gl' = general_rewrite_in dir all_occurrences !id cstr false gl in + let gl' = general_rewrite_in dir all_occurrences ~tac:(tac, conds) !id cstr false gl in let gls = (fst gl').Evd.it in match gls with g::_ -> @@ -167,11 +169,11 @@ let autorewrite_multi_in idl tac_main lbas : tactic = tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) tclIDTAC lbas))) idl gl -let autorewrite_in id = autorewrite_multi_in [id] +let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id] -let gen_auto_multi_rewrite tac_main lbas cl = +let gen_auto_multi_rewrite conds tac_main lbas cl = let try_do_hyps treat_id l = - autorewrite_multi_in (List.map treat_id l) tac_main lbas + autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas in if cl.concl_occs <> all_occurrences_expr & cl.concl_occs <> no_occurrences_expr @@ -184,7 +186,7 @@ let gen_auto_multi_rewrite tac_main lbas cl = | _ -> tclTHENFIRST t1 t2 in compose_tac - (if cl.concl_occs <> no_occurrences_expr then autorewrite tac_main lbas else tclIDTAC) + (if cl.concl_occs <> no_occurrences_expr then autorewrite ~conds tac_main lbas else tclIDTAC) (match cl.onhyps with | Some l -> try_do_hyps (fun ((_,id),_) -> id) l | None -> @@ -194,16 +196,16 @@ let gen_auto_multi_rewrite tac_main lbas cl = let ids = Tacmach.pf_ids_of_hyps gl in try_do_hyps (fun id -> id) ids gl) -let auto_multi_rewrite = gen_auto_multi_rewrite Refiner.tclIDTAC +let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds Refiner.tclIDTAC -let auto_multi_rewrite_with tac_main lbas cl gl = +let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl = let onconcl = cl.Tacexpr.concl_occs <> no_occurrences_expr in match onconcl,cl.Tacexpr.onhyps with | false,Some [_] | true,Some [] | false,Some [] -> (* autorewrite with .... in clause using tac n'est sur que si clause represente soit le but soit UNE hypothese *) - gen_auto_multi_rewrite tac_main lbas cl gl + gen_auto_multi_rewrite conds tac_main lbas cl gl | _ -> Util.errorlabstrm "autorewrite" (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index c8b3410dc..17777084d 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -12,6 +12,7 @@ open Term open Tacexpr open Tacmach +open Equality (*i*) (* Rewriting rules before tactic interpretation *) @@ -20,9 +21,12 @@ type raw_rew_rule = Util.loc * Term.constr * bool * Tacexpr.raw_tactic_expr (* To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit -(* The AutoRewrite tactic *) -val autorewrite : tactic -> string list -> tactic -val autorewrite_in : Names.identifier -> tactic -> string list -> tactic +(* The AutoRewrite tactic. + The optional conditions tell rewrite how to handle matching and side-condition solving. + Default is Naive: first match in the clause, don't look at the side-conditions to + tell if the rewrite succeeded. *) +val autorewrite : ?conds:conditions -> tactic -> string list -> tactic +val autorewrite_in : ?conds:conditions -> Names.identifier -> tactic -> string list -> tactic (* Rewriting rules *) type rew_rule = { rew_lemma: constr; @@ -35,9 +39,9 @@ val find_rewrites : string -> rew_rule list val find_matches : string -> constr -> rew_rule list -val auto_multi_rewrite : string list -> Tacticals.clause -> tactic +val auto_multi_rewrite : ?conds:conditions -> string list -> Tacticals.clause -> tactic -val auto_multi_rewrite_with : tactic -> string list -> Tacticals.clause -> tactic +val auto_multi_rewrite_with : ?conds:conditions -> tactic -> string list -> Tacticals.clause -> tactic val print_rewrite_hintdb : string -> unit diff --git a/tactics/equality.ml b/tactics/equality.ml index 0b3bf54bf..96cadbb02 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -46,6 +46,13 @@ open Evd (* Rewriting tactics *) +type orientation = bool + +type conditions = + | Naive (* Only try the first occurence of the lemma (default) *) + | FirstSolved (* Use the first match whose side-conditions are solved *) + | AllMatches (* Rewrite all matches whose side-conditions are solved *) + (* Warning : rewriting from left to right only works if there exists in the context a theorem named <eqname>_<suffsort>_r with type (A:<sort>)(x:A)(P:A->Prop)(P x)->(y:A)(eqname A y x)->(P y). @@ -61,7 +68,12 @@ let rewrite_unif_flags = { Unification.resolve_evars = true; } -let instantiate_lemma env sigma gl c ty l l2r concl = +let side_tac tac sidetac = + match sidetac with + | None -> tac + | Some sidetac -> tclTHENSFIRSTn tac [|tclIDTAC|] sidetac + +let instantiate_lemma_all env sigma gl c ty l l2r concl = let eqclause = Clenv.make_clenv_binding { gl with sigma = sigma } (c,ty) l in let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in let rec split_last_two = function @@ -70,22 +82,22 @@ let instantiate_lemma env sigma gl c ty l l2r concl = let l,res = split_last_two (y::z) in x::l, res | _ -> error "The term provided is not an applied relation." in let others,(c1,c2) = split_last_two args in - let evd', c' = - Unification.w_unify_to_subterm ~flags:rewrite_unif_flags env - ((if l2r then c1 else c2),concl) eqclause.evd - in - let cl' = {eqclause with evd = evd'} in - let cl' = + let try_occ (evd', c') = + let cl' = {eqclause with evd = evd'} in let mvs = clenv_dependent false cl' in clenv_pose_metas_as_evars cl' mvs - in cl' + in + let occs = + Unification.w_unify_to_subterm_all ~flags:rewrite_unif_flags env + ((if l2r then c1 else c2),concl) eqclause.evd + in List.map try_occ occs let instantiate_lemma env sigma gl c ty l l2r concl = let gl = { gl with sigma = sigma } in let ct = pf_type_of gl c in let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in let eqclause = Clenv.make_clenv_binding gl (c,t) l in - eqclause + [eqclause] let rewrite_elim with_evars c e ?(allow_K=true) = general_elim_clause_gen (elimination_clause_scheme with_evars allow_K) c e @@ -108,11 +120,25 @@ let general_elim_clause with_evars cls rew elim = raise (Pretype_errors.PretypeError (env, (Pretype_errors.NoOccurrenceFound (c', cls)))) -let general_elim_clause with_evars cls sigma c t l l2r elim gl = - let c = instantiate_lemma (pf_env gl) sigma gl c t l l2r - (match cls with None -> pf_concl gl | Some id -> pf_get_hyp_typ gl id) - in - tclTHEN (Refiner.tclEVARS c.evd) (general_elim_clause with_evars cls c elim) gl +let general_elim_clause with_evars tac cls sigma c t l l2r elim gl = + let all, firstonly, tac = + match tac with + | None -> false, false, None + | Some (tac, Naive) -> false, false, Some tac + | Some (tac, FirstSolved) -> true, true, Some (tclCOMPLETE tac) + | Some (tac, AllMatches) -> true, false, Some (tclCOMPLETE tac) + in + let cs = + (if not all then instantiate_lemma else instantiate_lemma_all) + (pf_env gl) sigma gl c t l l2r + (match cls with None -> pf_concl gl | Some id -> pf_get_hyp_typ gl id) + in + let try_clause c = + side_tac (tclTHEN (Refiner.tclEVARS c.evd) (general_elim_clause with_evars cls c elim)) tac + in + if firstonly then + tclFIRST (List.map try_clause cs) gl + else tclMAP try_clause cs gl (* The next function decides in particular whether to try a regular rewrite or a setoid rewrite. @@ -137,9 +163,9 @@ let find_elim hdcncl lft2rgt cls gl = try pf_global gl (id_of_string rwr_thm) with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".") -let leibniz_rewrite_ebindings_clause cls lft2rgt sigma c t l with_evars gl hdcncl = +let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars gl hdcncl = let elim = find_elim hdcncl lft2rgt cls gl in - general_elim_clause with_evars cls sigma c t l lft2rgt (elim,NoBindings) gl + general_elim_clause with_evars tac cls sigma c t l lft2rgt (elim,NoBindings) gl let adjust_rewriting_direction args lft2rgt = if List.length args = 1 then @@ -150,9 +176,12 @@ let adjust_rewriting_direction args lft2rgt = (* other equality *) lft2rgt -let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_bindings) with_evars gl = +let setoid_side_tac tac sidetac = side_tac tac (Option.map fst sidetac) + +let general_rewrite_ebindings_clause cls lft2rgt occs ?tac + ((c,l) : open_constr with_bindings) with_evars gl = if occs <> all_occurrences then ( - !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl) + setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl) else let env = pf_env gl in let sigma, c' = c in @@ -162,7 +191,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_ match match_with_equality_type t with | Some (hdcncl,args) -> (* Fast path: direct leibniz rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in - leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' (it_mkProd_or_LetIn t rels) + leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' (it_mkProd_or_LetIn t rels) l with_evars gl hdcncl | None -> let env' = push_rel_context rels env in @@ -171,34 +200,37 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_ | Some (hdcncl,args) -> (* Maybe a setoid relation with eq inside *) let lft2rgt = adjust_rewriting_direction args lft2rgt in if l = NoBindings && !is_applied_setoid_relation t then - !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl + setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl else - (try leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' + (try leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars gl hdcncl with e -> - try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl + try setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl with _ -> raise e) | None -> (* Can't be leibniz, try setoid *) if l = NoBindings - then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl + then setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl else error "The term provided does not end with an equation." let general_rewrite_ebindings = general_rewrite_ebindings_clause None -let general_rewrite_bindings l2r occs (c,bl) = - general_rewrite_ebindings_clause None l2r occs (inj_open c,inj_ebindings bl) -let general_rewrite l2r occs c = - general_rewrite_bindings l2r occs (c,NoBindings) false +let general_rewrite_bindings l2r occs ?tac (c,bl) = + general_rewrite_ebindings_clause None l2r occs ?tac (inj_open c,inj_ebindings bl) + +let general_rewrite l2r occs ?tac c = + general_rewrite_bindings l2r occs ?tac (c,NoBindings) false -let general_rewrite_ebindings_in l2r occs id = - general_rewrite_ebindings_clause (Some id) l2r occs -let general_rewrite_bindings_in l2r occs id (c,bl) = - general_rewrite_ebindings_clause (Some id) l2r occs (inj_open c,inj_ebindings bl) -let general_rewrite_in l2r occs id c = - general_rewrite_ebindings_clause (Some id) l2r occs (inj_open c,NoBindings) +let general_rewrite_ebindings_in l2r occs ?tac id = + general_rewrite_ebindings_clause (Some id) l2r occs ?tac -let general_multi_rewrite l2r with_evars c cl = +let general_rewrite_bindings_in l2r occs ?tac id (c,bl) = + general_rewrite_ebindings_clause (Some id) l2r occs ?tac (inj_open c,inj_ebindings bl) + +let general_rewrite_in l2r occs ?tac id c = + general_rewrite_ebindings_clause (Some id) l2r occs ?tac (inj_open c,NoBindings) + +let general_multi_rewrite l2r with_evars ?tac c cl = let occs_of = on_snd (List.fold_left (fun acc -> function ArgArg x -> x :: acc | ArgVar _ -> acc) @@ -212,12 +244,12 @@ let general_multi_rewrite l2r with_evars c cl = | [] -> tclIDTAC | ((occs,id),_) :: l -> tclTHENFIRST - (general_rewrite_ebindings_in l2r (occs_of occs) id c with_evars) + (general_rewrite_ebindings_in l2r (occs_of occs) ?tac id c with_evars) (do_hyps l) in if cl.concl_occs = no_occurrences_expr then do_hyps l else tclTHENFIRST - (general_rewrite_ebindings l2r (occs_of cl.concl_occs) c with_evars) + (general_rewrite_ebindings l2r (occs_of cl.concl_occs) ?tac c with_evars) (do_hyps l) | None -> (* Otherwise, if we are told to rewrite in all hypothesis via the @@ -226,7 +258,7 @@ let general_multi_rewrite l2r with_evars c cl = | [] -> (fun gl -> error "Nothing to rewrite.") | id :: l -> tclIFTHENTRYELSEMUST - (general_rewrite_ebindings_in l2r all_occurrences id c with_evars) + (general_rewrite_ebindings_in l2r all_occurrences ?tac id c with_evars) (do_hyps_atleastonce l) in let do_hyps gl = @@ -238,16 +270,11 @@ let general_multi_rewrite l2r with_evars c cl = in if cl.concl_occs = no_occurrences_expr then do_hyps else tclIFTHENTRYELSEMUST - (general_rewrite_ebindings l2r (occs_of cl.concl_occs) c with_evars) + (general_rewrite_ebindings l2r (occs_of cl.concl_occs) ?tac c with_evars) do_hyps let general_multi_multi_rewrite with_evars l cl tac = - let do1 l2r c = - match tac with - None -> general_multi_rewrite l2r with_evars c cl - | Some tac -> tclTHENSFIRSTn (general_multi_rewrite l2r with_evars c cl) - [|tclIDTAC|] (tclCOMPLETE tac) - in + let do1 l2r c = general_multi_rewrite l2r with_evars ?tac c cl in let rec doN l2r c = function | Precisely n when n <= 0 -> tclIDTAC | Precisely 1 -> do1 l2r c @@ -1300,4 +1327,5 @@ let replace_multi_term dir_opt c = in rewrite_multi_assumption_cond cond_eq_fun -let _ = Tactics.register_general_multi_rewrite general_multi_rewrite +let _ = Tactics.register_general_multi_rewrite + (fun b evars t cls -> general_multi_rewrite b evars t cls) diff --git a/tactics/equality.mli b/tactics/equality.mli index bcbe3e222..deb68aac8 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -27,36 +27,46 @@ open Rawterm open Genarg (*i*) +type orientation = bool + +type conditions = + | Naive (* Only try the first occurence of the lemma (default) *) + | FirstSolved (* Use the first match whose side-conditions are solved *) + | AllMatches (* Rewrite all matches whose side-conditions are solved *) + val general_rewrite_bindings : - bool -> occurrences -> constr with_bindings -> evars_flag -> tactic + orientation -> occurrences -> ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic val general_rewrite : - bool -> occurrences -> constr -> tactic + orientation -> occurrences -> ?tac:(tactic * conditions) -> constr -> tactic (* Equivalent to [general_rewrite l2r] *) -val rewriteLR : constr -> tactic -val rewriteRL : constr -> tactic +val rewriteLR : ?tac:(tactic * conditions) -> constr -> tactic +val rewriteRL : ?tac:(tactic * conditions) -> constr -> tactic (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *) val register_general_setoid_rewrite_clause : - (identifier option -> bool -> + (identifier option -> orientation -> occurrences -> open_constr -> new_goals:constr list -> tactic) -> unit val register_is_applied_setoid_relation : (constr -> bool) -> unit -val general_rewrite_bindings_in : - bool -> occurrences -> identifier -> constr with_bindings -> evars_flag -> tactic +val general_rewrite_ebindings_clause : identifier option -> + orientation -> occurrences -> ?tac:(tactic * conditions) -> open_constr with_bindings -> evars_flag -> tactic + +val general_rewrite_bindings_in : + orientation -> occurrences -> ?tac:(tactic * conditions) -> identifier -> constr with_bindings -> evars_flag -> tactic val general_rewrite_in : - bool -> occurrences -> identifier -> constr -> evars_flag -> tactic + orientation -> occurrences -> ?tac:(tactic * conditions) -> identifier -> constr -> evars_flag -> tactic -val general_multi_rewrite : - bool -> evars_flag -> open_constr with_bindings -> clause -> tactic +val general_multi_rewrite : + orientation -> evars_flag -> ?tac:(tactic * conditions) -> open_constr with_bindings -> clause -> tactic val general_multi_multi_rewrite : evars_flag -> (bool * multi * open_constr with_bindings) list -> clause -> - tactic option -> tactic + (tactic * conditions) option -> tactic -val conditional_rewrite : bool -> tactic -> open_constr with_bindings -> tactic +val conditional_rewrite : orientation -> tactic -> open_constr with_bindings -> tactic val conditional_rewrite_in : - bool -> identifier -> tactic -> open_constr with_bindings -> tactic + orientation -> identifier -> tactic -> open_constr with_bindings -> tactic val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic val replace : constr -> constr -> tactic diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f9de72757..6676b90ac 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -19,6 +19,8 @@ open Names open Tacexpr open Rawterm open Tactics +open Util +open Termops (* Equality *) open Equality @@ -190,8 +192,39 @@ TACTIC EXTEND autorewrite ] END +TACTIC EXTEND autorewrite_star +| [ "autorewrite" "*" "with" ne_preident_list(l) in_arg_hyp(cl) ] -> + [ auto_multi_rewrite ~conds:AllMatches l (glob_in_arg_hyp_to_clause cl) ] +| [ "autorewrite" "*" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] -> + [ let cl = glob_in_arg_hyp_to_clause cl in + auto_multi_rewrite_with ~conds:AllMatches (snd t) l cl ] +END +open Extraargs +let rewrite_star clause orient occs c (tac : glob_tactic_expr option) = + let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in + general_rewrite_ebindings_clause clause orient occs ?tac:tac' (c,NoBindings) true + +let occurrences_of = function + | n::_ as nl when n < 0 -> (false,List.map abs nl) + | nl -> + if List.exists (fun n -> n < 0) nl then + error "Illegal negative occurrence number."; + (true,nl) + +TACTIC EXTEND rewrite_star +| [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> + [ rewrite_star (Some id) o (occurrences_of occ) c tac ] +| [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] -> + [ rewrite_star (Some id) o (occurrences_of occ) c tac ] +| [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) by_arg_tac(tac) ] -> + [ rewrite_star (Some id) o all_occurrences c tac ] +| [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) by_arg_tac(tac) ] -> + [ rewrite_star None o (occurrences_of occ) c tac ] +| [ "rewrite" "*" orient(o) open_constr(c) by_arg_tac(tac) ] -> + [ rewrite_star None o all_occurrences c tac ] + END let add_rewrite_hint name ort t lcsr = let env = Global.env() and sigma = Evd.empty in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0942fde83..667f5b84f 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2345,7 +2345,7 @@ and interp_atomic ist gl = function Equality.general_multi_multi_rewrite ev (List.map (fun (b,m,c) -> (b,m,interp_open_constr_with_bindings ist gl c)) l) (interp_clause ist gl cl) - (Option.map (interp_tactic ist) by) + (Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) | TacInversion (DepInversion (k,c,ids),hyp) -> Inv.dinv k (Option.map (pf_interp_constr ist gl) c) (Option.map (interp_intro_pattern ist gl) ids) |