aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/unification.ml64
-rw-r--r--pretyping/unification.mli3
-rw-r--r--tactics/autorewrite.ml28
-rw-r--r--tactics/autorewrite.mli14
-rw-r--r--tactics/equality.ml118
-rw-r--r--tactics/equality.mli36
-rw-r--r--tactics/extratactics.ml433
-rw-r--r--tactics/tacinterp.ml2
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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 17:27:22 +0000