aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/autorewrite.ml184
-rw-r--r--tactics/autorewrite.mli32
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/rewrite.ml430
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v6
5 files changed, 174 insertions, 80 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 130f7e7fc5..d1dc8d2e8b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -25,15 +25,45 @@ open Tacexpr
open Mod_subst
(* Rewriting rules *)
-(* the type is the statement of the lemma constr. Used to elim duplicates. *)
-type rew_rule = constr * types * bool * glob_tactic_expr
+type rew_rule = { rew_lemma: constr;
+ rew_type: types;
+ rew_pat: constr;
+ rew_l2r: bool;
+ rew_tac: glob_tactic_expr }
+let subst_hint subst hint =
+ let cst' = subst_mps subst hint.rew_lemma in
+ let typ' = subst_mps subst hint.rew_type in
+ let pat' = subst_mps subst hint.rew_pat in
+ let t' = Tacinterp.subst_tactic subst hint.rew_tac in
+ if hint.rew_lemma == cst' && hint.rew_tac == t' then hint else
+ { hint with
+ rew_lemma = cst'; rew_type = typ';
+ rew_pat = pat'; rew_tac = t' }
+module HintIdent =
+struct
+ type t = rew_rule
+
+ let compare t t' =
+ Pervasives.compare t.rew_lemma t'.rew_lemma
+ let subst = subst_hint
+
+ let constr_of t = t.rew_pat
+end
+
+module HintOpt =
+struct
+ let reduce c = c
+ let direction = true
+end
+
+module HintDN = Term_dnet.Make(HintIdent)(HintOpt)
(* Summary and Object declaration *)
let rewtab =
- ref (Stringmap.empty : rew_rule list Stringmap.t)
+ ref (Stringmap.empty : HintDN.t Stringmap.t)
let _ =
let init () = rewtab := Stringmap.empty in
@@ -53,36 +83,37 @@ let find_base bas =
errorlabstrm "AutoRewrite"
(str ("Rewriting base "^(bas)^" does not exist."))
+let find_rewrites bas =
+ HintDN.find_all (find_base bas)
+
+let find_matches bas pat =
+ let base = find_base bas in
+ let res = HintDN.search_pattern base pat in
+ List.map (fun (rew, esubst, subst) -> rew) res
+
let print_rewrite_hintdb bas =
let hints = find_base bas in
ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++
prlist_with_sep Pp.cut
- (fun (c,typ,d,t) ->
- str (if d then "rewrite -> " else "rewrite <- ") ++
- Printer.pr_lconstr c ++ str " of type " ++ Printer.pr_lconstr typ ++
+ (fun h ->
+ str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
+ Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
str " then use tactic " ++
- Pptactic.pr_glob_tactic (Global.env()) t) hints)
+ Pptactic.pr_glob_tactic (Global.env()) h.rew_tac)
+ (HintDN.find_all hints))
-type raw_rew_rule = constr * bool * raw_tactic_expr
+type raw_rew_rule = loc * constr * bool * raw_tactic_expr
(* Applies all the rules of one base *)
let one_base general_rewrite_maybe_in tac_main bas =
- let lrul =
- try
- Stringmap.find bas !rewtab
- with Not_found ->
- errorlabstrm "AutoRewrite"
- (str ("Rewriting base "^(bas)^" does not exist."))
- in
- let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in
+ let lrul = HintDN.find_all (find_base bas) in
+ let lrul = List.map (fun h -> (h.rew_lemma,h.rew_l2r,Tacinterp.eval_tactic h.rew_tac)) lrul in
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)))
tclIDTAC lrul))
-
-
(* The AutoRewrite tactic *)
let autorewrite tac_main lbas =
tclREPEAT_MAIN (tclPROGRESS
@@ -180,38 +211,12 @@ let auto_multi_rewrite_with tac_main lbas cl gl =
(* Functions necessary to the library object declaration *)
let cache_hintrewrite (_,(rbase,lrl)) =
- let l =
- try
- let oldl = Stringmap.find rbase !rewtab in
- let lrl =
- List.map
- (fun (c,dummy,b,t) ->
- (* here we substitute the dummy value with the right one *)
- c,Typing.type_of (Global.env ()) Evd.empty c,b,t) lrl in
- (List.filter
- (fun (_,typ,_,_) ->
- not (List.exists (fun (_,typ',_,_) -> Term.eq_constr typ typ') oldl)
- ) lrl) @ oldl
- with
- | Not_found -> lrl
- in
- rewtab:=Stringmap.add rbase l !rewtab
+ rewtab:=Stringmap.add rbase lrl !rewtab
let export_hintrewrite x = Some x
let subst_hintrewrite (_,subst,(rbase,list as node)) =
- let subst_first (cst,typ,b,t as pair) =
- let cst' = subst_mps subst cst in
- let typ' =
- (* here we do not have the environment and Global.env () is not the
- one where cst' lives in. Thus we can just put a dummy value and
- override it in cache_hintrewrite *)
- typ (* dummy value, it will be recomputed by cache_hintrewrite *) in
- let t' = Tacinterp.subst_tactic subst t in
- if cst == cst' && t == t' then pair else
- (cst',typ',b,t')
- in
- let list' = list_smartmap subst_first list in
+ let list' = HintDN.subst subst list in
if list' == list then node else
(rbase,list')
@@ -221,18 +226,83 @@ let classify_hintrewrite (_,x) = Libobject.Substitute x
(* Declaration of the Hint Rewrite library object *)
let (inHintRewrite,_)=
Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
- Libobject.cache_function = cache_hintrewrite;
- Libobject.load_function = (fun _ -> cache_hintrewrite);
- Libobject.subst_function = subst_hintrewrite;
- Libobject.classify_function = classify_hintrewrite;
- Libobject.export_function = export_hintrewrite }
+ Libobject.cache_function = cache_hintrewrite;
+ Libobject.load_function = (fun _ -> cache_hintrewrite);
+ Libobject.subst_function = subst_hintrewrite;
+ Libobject.classify_function = classify_hintrewrite;
+ Libobject.export_function = export_hintrewrite }
+
+
+open Clenv
+type hypinfo = {
+ hyp_cl : clausenv;
+ hyp_prf : constr;
+ hyp_ty : types;
+ hyp_car : constr;
+ hyp_rel : constr;
+ hyp_l2r : bool;
+ hyp_left : constr;
+ hyp_right : constr;
+}
+
+let evd_convertible env evd x y =
+ try ignore(Evarconv.the_conv_x env x y evd); true
+ with _ -> false
+
+let decompose_applied_relation metas env sigma c ctype left2right =
+ let find_rel ty =
+ let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
+ let eqclause =
+ if metas then eqclause
+ else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
+ in
+ let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+ let rec split_last_two = function
+ | [c1;c2] -> [],(c1, c2)
+ | x::y::z ->
+ let l,res = split_last_two (y::z) in x::l, res
+ | _ -> raise Not_found
+ in
+ try
+ let others,(c1,c2) = split_last_two args in
+ let ty1, ty2 =
+ Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2
+ in
+ if not (evd_convertible env eqclause.evd ty1 ty2) then None
+ else
+ Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty;
+ hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
+ hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
+ with Not_found -> None
+ in
+ match find_rel ctype with
+ | Some c -> Some c
+ | None ->
+ let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
+ match find_rel (it_mkProd_or_LetIn t' ctx) with
+ | Some c -> Some c
+ | None -> None
+
+let find_applied_relation metas loc env sigma c left2right =
+ let ctype = Typing.type_of env sigma c in
+ match decompose_applied_relation metas env sigma c ctype left2right with
+ | Some c -> c
+ | None ->
+ user_err_loc (loc, "decompose_applied_relation",
+ str"The type" ++ spc () ++ Printer.pr_constr_env env ctype ++
+ spc () ++ str"of this term does not end with an applied relation.")
+
(* To add rewriting rules to a base *)
let add_rew_rules base lrul =
let lrul =
- List.rev_map
- (fun (c,b,t) ->
- (c,mkProp (* dummy value *), b,Tacinterp.glob_tactic t)
- ) lrul
- in
- Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
+ List.fold_left
+ (fun dn (loc,c,b,t) ->
+ let info = find_applied_relation false loc (Global.env ()) Evd.empty c b in
+ let pat = if b then info.hyp_left else info.hyp_right in
+ let rul = { rew_lemma = c; rew_type = info.hyp_ty;
+ rew_pat = pat; rew_l2r = b;
+ rew_tac = Tacinterp.glob_tactic t}
+ in HintDN.add pat rul dn)
+ (try find_base base with _ -> HintDN.empty) lrul
+ in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 632a281709..c8b3410dcb 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -15,7 +15,7 @@ open Tacmach
(*i*)
(* Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Term.constr * bool * Tacexpr.raw_tactic_expr
+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
@@ -25,13 +25,37 @@ val autorewrite : tactic -> string list -> tactic
val autorewrite_in : Names.identifier -> tactic -> string list -> tactic
(* Rewriting rules *)
-(* the type is the statement of the lemma constr. Used to elim duplicates. *)
-type rew_rule = constr * types * bool * glob_tactic_expr
+type rew_rule = { rew_lemma: constr;
+ rew_type: types;
+ rew_pat: constr;
+ rew_l2r: bool;
+ rew_tac: glob_tactic_expr }
-val find_base : string -> rew_rule list
+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_with : tactic -> string list -> Tacticals.clause -> tactic
val print_rewrite_hintdb : string -> unit
+
+open Clenv
+
+
+type hypinfo = {
+ hyp_cl : clausenv;
+ hyp_prf : constr;
+ hyp_ty : types;
+ hyp_car : constr;
+ hyp_rel : constr;
+ hyp_l2r : bool;
+ hyp_left : constr;
+ hyp_right : constr;
+}
+
+val find_applied_relation : bool ->
+ Util.loc ->
+ Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo
+
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index d3aba06899..28e3888453 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -195,7 +195,7 @@ END
let add_rewrite_hint name ort t lcsr =
let env = Global.env() and sigma = Evd.empty in
- let f c = Constrintern.interp_constr sigma env c, ort, t in
+ let f c = Topconstr.constr_loc c, Constrintern.interp_constr sigma env c, ort, t in
add_rew_rules name (List.map f lcsr)
VERNAC COMMAND EXTEND HintRewrite
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 1bbb2324f3..147e5384e2 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -242,7 +242,7 @@ let evd_convertible env evd x y =
try ignore(Evarconv.the_conv_x env x y evd); true
with _ -> false
-let decompose_setoid_eqhyp env sigma c left2right =
+let decompose_applied_relation env sigma c left2right =
let ctype = Typing.type_of env sigma c in
let find_rel ty =
let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
@@ -295,7 +295,7 @@ let refresh_hypinfo env sigma hypinfo =
match c with
| Some c ->
(* Refresh the clausenv to not get the same meta twice in the goal. *)
- hypinfo := decompose_setoid_eqhyp env ( cl.evd) c l2r;
+ hypinfo := decompose_applied_relation env ( cl.evd) c l2r;
| _ -> ()
else ()
@@ -489,7 +489,7 @@ let apply_rule hypinfo loccs : strategy =
let apply_lemma (evm,c) left2right loccs : strategy =
fun env sigma ->
let evars = Evd.merge sigma evm in
- let hypinfo = ref (decompose_setoid_eqhyp env evars c left2right) in
+ let hypinfo = ref (decompose_applied_relation env evars c left2right) in
apply_rule hypinfo loccs env sigma
let subterm all flags (s : strategy) : strategy =
@@ -588,11 +588,6 @@ let subterm all flags (s : strategy) : strategy =
let all_subterms = subterm true default_flags
let one_subterm = subterm false default_flags
-let morphism_proof env evars carrier relation x =
- let goal =
- mkApp (Lazy.force morphism_proxy_type, [| carrier ; relation; x |])
- in Evarutil.e_new_evar evars env goal
-
(** Requires transitivity of the rewrite step, not tail-recursive. *)
let transitivity env sigma (res : rewrite_result_info) (next : strategy) : rewrite_result option =
@@ -660,10 +655,10 @@ module Strategies =
seq s (any s)
let bu (s : strategy) : strategy =
- fix (fun s' -> choice (seq (all_subterms s') (try_ s')) s)
+ fix (fun s' -> seq (choice (all_subterms s') s) (try_ s'))
let td (s : strategy) : strategy =
- fix (fun s' -> choice s (seq (all_subterms s') (try_ s')))
+ fix (fun s' -> seq (choice s (all_subterms s')) (try_ s'))
let innermost (s : strategy) : strategy =
fix (fun ins -> choice (one_subterm ins) s)
@@ -676,9 +671,15 @@ module Strategies =
choice tac (apply_lemma l l2r (false,[])))
fail cs
+ let old_hints (db : string) : strategy =
+ let rules = Autorewrite.find_rewrites db in
+ lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules)
+
let hints (db : string) : strategy =
- let rules = Autorewrite.find_base db in
- lemmas (List.map (fun (b,_,l2r,_) -> (inj_open b, l2r)) rules)
+ fun env sigma t ty cstr evars ->
+ let rules = Autorewrite.find_matches db t in
+ lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules)
+ env sigma t ty cstr evars
end
@@ -693,7 +694,7 @@ let rewrite_strat flags occs hyp =
let rewrite_with (evm,c) left2right loccs : strategy =
fun env sigma ->
let evars = Evd.merge sigma evm in
- let hypinfo = ref (decompose_setoid_eqhyp env evars c left2right) in
+ let hypinfo = ref (decompose_applied_relation env evars c left2right) in
rewrite_strat default_flags loccs hypinfo env sigma
let apply_strategy (s : strategy) env sigma concl cstr evars =
@@ -854,6 +855,7 @@ ARGUMENT EXTEND rewstrategy TYPED AS strategy
| [ rewstrategy(h) ";" rewstrategy(h') ] -> [ Strategies.seq 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 sigma -> Strategies.lemmas (interp_constr_list env sigma h) env sigma ]
END
@@ -1263,7 +1265,7 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
{cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
let get_hyp gl evars (evm,c) clause l2r =
- let hi = decompose_setoid_eqhyp (pf_env gl) evars c l2r in
+ let hi = decompose_applied_relation (pf_env gl) evars c l2r in
let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index 00c7aeec65..c72abed619 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -269,10 +269,8 @@ Section DoubleSqrt.
Let spec_ww_Bm1 : [[wwBm1]] = wwB - 1.
Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed.
-
- Hint Rewrite spec_w_0 spec_w_1 w_Bm1 spec_w_WW spec_w_sub
- spec_w_div21 spec_w_add_mul_div spec_ww_Bm1
- spec_w_add_c spec_w_sqrt2: w_rewrite.
+ Hint Rewrite spec_w_0 spec_w_1 spec_w_WW spec_w_sub
+ spec_w_add_mul_div spec_ww_Bm1 spec_w_add_c : w_rewrite.
Lemma spec_ww_is_even : forall x,
if ww_is_even x then [[x]] mod 2 = 0 else [[x]] mod 2 = 1.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 06:28:30 +0000