From f2a46998e4f791309d74445cf43981aedec28fd1 Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 17 Apr 2009 17:39:40 +0000 Subject: - Fix handling of clauses in setoid_rewrite to rewrite under binders correctly. - Fix the new autorewrite to implement the (unstated) invariant that the last declared rules are applied first, which makes a difference for non-confluent rewrite rules. Some scripts in CoLoR rely on that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12092 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/term_dnet.ml | 3 +++ pretyping/term_dnet.mli | 2 ++ tactics/autorewrite.ml | 62 ++++++++++++++++++++++++++----------------------- tactics/rewrite.ml4 | 15 +++++++----- 4 files changed, 47 insertions(+), 35 deletions(-) diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 656a90c70..4c6c5e631 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -367,6 +367,8 @@ struct possibly_under app_pat (search_pat pat (pat_of_constr pat)) dn init let find_all dn = Idset.elements (TDnet.find_all dn) + + let map f dn = TDnet.map f (fun x -> x) dn end module type S = @@ -385,4 +387,5 @@ sig val search_head_concl : t -> constr -> result list val search_eq_concl : t -> constr -> constr -> result list val find_all : t -> ident list + val map : (ident -> ident) -> t -> t end diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli index ccf962481..f6c1b5b61 100644 --- a/pretyping/term_dnet.mli +++ b/pretyping/term_dnet.mli @@ -102,6 +102,8 @@ sig (* [find_all dn] returns all idents contained in dn *) val find_all : t -> ident list + + val map : (ident -> ident) -> t -> t end module Make : diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index d1dc8d2e8..2472c1274 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -43,14 +43,15 @@ let subst_hint subst hint = module HintIdent = struct - type t = rew_rule + type t = int * rew_rule - let compare t t' = - Pervasives.compare t.rew_lemma t'.rew_lemma + let compare (i,t) (i',t') = + Pervasives.compare i i' +(* Pervasives.compare t.rew_lemma t'.rew_lemma *) - let subst = subst_hint + let subst s (i,t) = (i,subst_hint s t) - let constr_of t = t.rew_pat + let constr_of (i,t) = t.rew_pat end module HintOpt = @@ -84,29 +85,28 @@ let find_base bas = (str ("Rewriting base "^(bas)^" does not exist.")) let find_rewrites bas = - HintDN.find_all (find_base bas) + List.rev_map snd (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 + 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 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()) h.rew_tac) - (HintDN.find_all hints)) - + ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++ + prlist_with_sep Pp.cut + (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()) h.rew_tac) + (find_rewrites bas)) + 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 = HintDN.find_all (find_base bas) in + let lrul = find_rewrites 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 @@ -208,10 +208,12 @@ let auto_multi_rewrite_with 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.") - (* Functions necessary to the library object declaration *) let cache_hintrewrite (_,(rbase,lrl)) = - rewtab:=Stringmap.add rbase lrl !rewtab + let base = try find_base rbase with _ -> HintDN.empty in + let max = try fst (Util.list_last (HintDN.find_all base)) with _ -> 0 in + let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in + rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab let export_hintrewrite x = Some x @@ -295,14 +297,16 @@ let find_applied_relation metas loc env sigma c left2right = (* To add rewriting rules to a base *) let add_rew_rules base lrul = + let counter = ref 0 in let 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 + 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 incr counter; + HintDN.add pat (!counter, rul) dn) HintDN.empty lrul in Lib.add_anonymous_leaf (inHintRewrite (base,lrul)) + diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 8efb0176e..df4851443 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -287,14 +287,14 @@ let convertible env evd x y = let allowK = true let refresh_hypinfo env sigma hypinfo = - if !hypinfo.abs = None then - let {l2r=l2r; c = c;cl=cl} = !hypinfo in + if hypinfo.abs = None then + let {l2r=l2r; c=c;cl=cl} = hypinfo in match c with | Some c -> (* Refresh the clausenv to not get the same meta twice in the goal. *) - hypinfo := decompose_applied_relation env ( cl.evd) c l2r; - | _ -> () - else () + decompose_applied_relation env cl.evd c l2r; + | _ -> hypinfo + else hypinfo let unify_eqn env sigma hypinfo t = if isEvar t then None @@ -329,7 +329,7 @@ let unify_eqn env sigma hypinfo t = and ty2 = Typing.mtype_of env'.env env'.evd c2 in if convertible env env'.evd ty1 ty2 then ( - if occur_meta prf then refresh_hypinfo env sigma hypinfo; + if occur_meta prf then hypinfo := refresh_hypinfo env sigma !hypinfo; env', prf, c1, c2, car, rel) else raise Reduction.NotConvertible in @@ -463,12 +463,15 @@ let apply_constraint env sigma car rel cstr res = | None -> res | Some r -> resolve_subrelation env sigma car rel r res +let eq_env x y = x == y + let apply_rule hypinfo loccs : strategy = let (nowhere_except_in,occs) = loccs in let is_occ occ = if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in let occ = ref 0 in fun env sigma t ty cstr evars -> + if not (eq_env !hypinfo.cl.env env) then hypinfo := refresh_hypinfo env sigma !hypinfo; let unif = unify_eqn env sigma hypinfo t in if unif <> None then incr occ; match unif with -- cgit v1.2.3