diff options
author | 2015-04-03 07:24:42 -0400 | |
---|---|---|
committer | 2015-04-06 08:52:16 +0200 | |
commit | 5d03ea0729ff1ed01bf64e9c98355149bb4c04e9 (patch) | |
tree | e02886fa349d6c6805a603b8656a0f15079a6edd | |
parent | b667f6fec675d3a05ba0475bdb84beaeed7622ac (diff) |
refresh metas in rewrite hints loaded from .vo files (fix bug #3815)
Meta variables in rewrite rules are named by integers that are allocated
sequentially at runtime (fresh_meta in tactics/term_dnet.ml). This causes
a problem when some rewrite rules (with meta variables) are generated by
coqc, saved in a .vo file, and then imported into another coqc/coqtop
process. The new process will allocate its own meta variable numbers
starting from 0, colliding with existing imported meta variable numbers.
One manifestation of this issue was various failures of [rewrite_strat];
see bug #3815 for examples.
This change fixes the problem, by replacing all meta variable numbers
in imported rewrite rules at import time. This seems to fix the various
failures reported in bug #3815.
Thanks to Jason Gross for tracking down the commit that introduced this
bug in the first place (71a9b7f2).
-rw-r--r-- | tactics/autorewrite.ml | 1 | ||||
-rw-r--r-- | tactics/dnet.ml | 10 | ||||
-rw-r--r-- | tactics/dnet.mli | 2 | ||||
-rw-r--r-- | tactics/term_dnet.ml | 12 | ||||
-rw-r--r-- | tactics/term_dnet.mli | 2 |
5 files changed, 27 insertions, 0 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index ee8e1855d..4eb8a7925 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -211,6 +211,7 @@ let cache_hintrewrite (_,(rbase,lrl)) = let base = try raw_find_base rbase with Not_found -> HintDN.empty in let max = try fst (Util.List.last (HintDN.find_all base)) with Failure _ -> 0 in + let lrl = HintDN.refresh_metas lrl in let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in rewtab:=String.Map.add rbase (HintDN.union lrl base) !rewtab diff --git a/tactics/dnet.ml b/tactics/dnet.ml index bb71620c0..93334db73 100644 --- a/tactics/dnet.ml +++ b/tactics/dnet.ml @@ -39,6 +39,7 @@ sig val inter : t -> t -> t val union : t -> t -> t val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t + val map_metas : (meta -> meta) -> t -> t end module Make = @@ -288,4 +289,13 @@ struct | Node e -> Node (T.map (map sidset sterm) e) in Nodes (tmap_map sterm snode t, Mmap.map (idset_map sidset) m) + let rec map_metas f (Nodes (t, m)) : t = + let f_node = function + | Terminal (e, is) -> Terminal (T.map (map_metas f) e, is) + | Node e -> Node (T.map (map_metas f) e) + in + let m' = Mmap.fold (fun m s acc -> Mmap.add (f m) s acc) m Mmap.empty in + let t' = Tmap.fold (fun k n acc -> Tmap.add k (f_node n) acc) t Tmap.empty in + Nodes (t', m') + end diff --git a/tactics/dnet.mli b/tactics/dnet.mli index 4bfa7263e..52853d702 100644 --- a/tactics/dnet.mli +++ b/tactics/dnet.mli @@ -113,6 +113,8 @@ sig (** apply a function on each identifier and node of terms in a dnet *) val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t + + val map_metas : (meta -> meta) -> t -> t end module Make : diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index e637b2e36..e79fc6dc9 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -371,6 +371,17 @@ struct let find_all dn = Idset.elements (TDnet.find_all dn) let map f dn = TDnet.map f (fun x -> x) dn + + let refresh_metas dn = + let new_metas = ref Int.Map.empty in + let refresh_one_meta i = + try Int.Map.find i !new_metas + with Not_found -> + let new_meta = fresh_meta () in + let () = new_metas := Int.Map.add i new_meta !new_metas in + new_meta + in + TDnet.map_metas refresh_one_meta dn end module type S = @@ -385,4 +396,5 @@ sig val search_pattern : t -> constr -> ident list val find_all : t -> ident list val map : (ident -> ident) -> t -> t + val refresh_metas : t -> t end diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli index a5c80cc00..58f95ac6c 100644 --- a/tactics/term_dnet.mli +++ b/tactics/term_dnet.mli @@ -80,6 +80,8 @@ sig val find_all : t -> ident list val map : (ident -> ident) -> t -> t + + val refresh_metas : t -> t end module Make : |