From edbfb435e9d78db2bc1b6ae9d3808f808617d5e8 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 11 Feb 2011 16:53:52 +0000 Subject: Mod_subst: split delta_resolver in two tables (mp / kn) This way, no more absurd mixing of mp/kn and Prefix_equiv/Equiv to consider, and hence no more anomaly or assert false left in Mod_subst. As we say here, "faut pas melanger les torchons et les serviettes" ... With these two specialized tables, efficiency might also be better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13835 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mod_subst.ml | 443 ++++++++++++++++++++-------------------------------- 1 file changed, 168 insertions(+), 275 deletions(-) (limited to 'kernel/mod_subst.ml') diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 9e8ce3fe5..0c97910dc 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -22,20 +22,29 @@ open Term is the term into which we should inline *) type delta_hint = - Inline of int * constr option + | Inline of int * constr option | Equiv of kernel_name - | Prefix_equiv of module_path -type delta_key = - KN of kernel_name - | MP of module_path - -module Deltamap = Map.Make(struct - type t = delta_key - let compare = Pervasives.compare - end) - -type delta_resolver = delta_hint Deltamap.t +(* NB: earlier constructor Prefix_equiv of module_path + is now stored in a separate table, see Deltamap.t below *) + +module Deltamap = struct + type t = module_path MPmap.t * delta_hint KNmap.t + let empty = MPmap.empty, KNmap.empty + let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km) + let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km) + let remove_mp mp (mm,km) = (MPmap.remove mp mm, km) + let find_kn kn map = KNmap.find kn (snd map) + let find_mp mp map = MPmap.find mp (fst map) + let mem_mp mp map = MPmap.mem mp (fst map) + let mem_kn kn map = KNmap.mem kn (snd map) + let fold_kn f (mm,km) i = KNmap.fold f km i + let fold fmp fkn (mm,km) i = + MPmap.fold fmp mm (KNmap.fold fkn km i) + let join map1 map2 = fold add_mp add_kn map1 map2 +end + +type delta_resolver = Deltamap.t let empty_delta_resolver = Deltamap.empty @@ -53,7 +62,7 @@ module Umap = Map.Make(struct end) type substitution = (module_path * delta_resolver) Umap.t - + let empty_subst = Umap.empty let add_mbid mbid mp resolve = @@ -66,233 +75,161 @@ let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst let add_inline_delta_resolver con lev = - Deltamap.add (KN(user_con con)) (Inline (lev,None)) + Deltamap.add_kn (user_con con) (Inline (lev,None)) let add_inline_constr_delta_resolver con lev cstr = - Deltamap.add (KN(user_con con)) (Inline (lev, Some cstr)) + Deltamap.add_kn (user_con con) (Inline (lev, Some cstr)) let add_constant_delta_resolver con = - Deltamap.add (KN(user_con con)) (Equiv (canonical_con con)) + Deltamap.add_kn (user_con con) (Equiv (canonical_con con)) let add_mind_delta_resolver mind = - Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind)) - -let add_mp_delta_resolver mp1 mp2 = - Deltamap.add (MP mp1) (Prefix_equiv mp2) - -let mp_in_delta mp = - Deltamap.mem (MP mp) - -let con_in_delta con resolver = -try - match Deltamap.find (KN(user_con con)) resolver with - | Inline _ | Prefix_equiv _ -> false - | Equiv _ -> true -with - Not_found -> false - -let mind_in_delta mind resolver = -try - match Deltamap.find (KN(user_mind mind)) resolver with - | Inline _ | Prefix_equiv _ -> false - | Equiv _ -> true -with - Not_found -> false + Deltamap.add_kn (user_mind mind) (Equiv (canonical_mind mind)) + +let add_mp_delta_resolver mp1 mp2 = + Deltamap.add_mp mp1 mp2 + +let mp_in_delta mp = + Deltamap.mem_mp mp + +let kn_in_delta kn resolver = + try + match Deltamap.find_kn kn resolver with + | Equiv _ -> true + | Inline _ -> false + with Not_found -> false + +let con_in_delta con resolver = kn_in_delta (user_con con) resolver +let mind_in_delta mind resolver = kn_in_delta (user_mind mind) resolver let delta_of_mp resolve mp = - try - match Deltamap.find (MP mp) resolve with - | Prefix_equiv mp1 -> mp1 - | _ -> anomaly "mod_subst: bad association in delta_resolver" - with - Not_found -> mp + try Deltamap.find_mp mp resolve with Not_found -> mp let remove_mp_delta_resolver resolver mp = - Deltamap.remove (MP mp) resolver - -exception Inline_kn + Deltamap.remove_mp mp resolver -let rec find_prefix resolve mp = +let rec find_prefix resolve mp = let rec sub_mp = function - | MPdot(mp,l) as mp_sup -> - (try - match Deltamap.find (MP mp_sup) resolve with - | Prefix_equiv mp1 -> mp1 - | _ -> anomaly - "mod_subst: bad association in delta_resolver" - with - Not_found -> MPdot(sub_mp mp,l)) - | p -> - match Deltamap.find (MP p) resolve with - | Prefix_equiv mp1 -> mp1 - | _ -> anomaly - "mod_subst: bad association in delta_resolver" + | MPdot(mp,l) as mp_sup -> + (try Deltamap.find_mp mp_sup resolve + with Not_found -> MPdot(sub_mp mp,l)) + | p -> Deltamap.find_mp p resolve in - try - sub_mp mp - with - Not_found -> mp + try sub_mp mp with Not_found -> mp exception Change_equiv_to_inline of (int * constr) let solve_delta_kn resolve kn = - try - match Deltamap.find (KN kn) resolve with - | Equiv kn1 -> kn1 - | Inline (lev, Some c) -> - raise (Change_equiv_to_inline (lev,c)) - | Inline (_, None) -> raise Inline_kn - | _ -> anomaly - "mod_subst: bad association in delta_resolver" - with - Not_found | Inline_kn -> - let mp,dir,l = repr_kn kn in - let new_mp = find_prefix resolve mp in - if mp == new_mp then - kn - else - make_kn new_mp dir l - + try + match Deltamap.find_kn kn resolve with + | Equiv kn1 -> kn1 + | Inline (lev, Some c) -> raise (Change_equiv_to_inline (lev,c)) + | Inline (_, None) -> raise Not_found + with Not_found -> + let mp,dir,l = repr_kn kn in + let new_mp = find_prefix resolve mp in + if mp == new_mp then + kn + else + make_kn new_mp dir l + +let gen_of_delta resolve x kn fix_can = + try + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then x else fix_can new_kn + with _ -> x let constant_of_delta resolve con = let kn = user_con con in - try - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - con - else - constant_of_kn_equiv kn new_kn - with - _ -> con - + gen_of_delta resolve con kn (constant_of_kn_equiv kn) + let constant_of_delta2 resolve con = - let kn = canonical_con con in - let kn1 = user_con con in - try - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - con - else - constant_of_kn_equiv kn1 new_kn - with - _ -> con + let kn, kn' = canonical_con con, user_con con in + gen_of_delta resolve con kn (constant_of_kn_equiv kn') let mind_of_delta resolve mind = let kn = user_mind mind in - try - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - mind - else - mind_of_kn_equiv kn new_kn - with - _ -> mind + gen_of_delta resolve mind kn (mind_of_kn_equiv kn) let mind_of_delta2 resolve mind = - let kn = canonical_mind mind in - let kn1 = user_mind mind in - try - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - mind - else - mind_of_kn_equiv kn1 new_kn - with - _ -> mind - + let kn, kn' = canonical_mind mind, user_mind mind in + gen_of_delta resolve mind kn (mind_of_kn_equiv kn') let inline_of_delta inline resolver = match inline with | None -> [] | Some inl_lev -> - let extract key hint l = - match key,hint with - |KN kn, Inline (lev,_) -> if lev <= inl_lev then (lev,kn)::l else l - | _,_ -> l + let extract kn hint l = + match hint with + | Inline (lev,_) -> if lev <= inl_lev then (lev,kn)::l else l + | _ -> l in - Deltamap.fold extract resolver [] + Deltamap.fold_kn extract resolver [] + +let find_inline_of_delta kn resolve = + match Deltamap.find_kn kn resolve with + | Inline (_,o) -> o + | _ -> raise Not_found -exception Not_inline - let constant_of_delta_with_inline resolve con = let kn1,kn2 = canonical_con con,user_con con in - try - match Deltamap.find (KN kn2) resolve with - | Inline (_,o) -> o - | _ -> raise Not_inline - with - Not_found | Not_inline -> - try match Deltamap.find (KN kn1) resolve with - | Inline (_,o) -> o - | _ -> raise Not_inline - with - Not_found | Not_inline -> None - -let string_of_key = function - | KN kn -> string_of_kn kn - | MP mp -> string_of_mp mp + try find_inline_of_delta kn2 resolve + with Not_found -> + try find_inline_of_delta kn1 resolve + with Not_found -> None let string_of_hint = function - | Inline _ -> "inline" - | Equiv kn -> string_of_kn kn - | Prefix_equiv mp -> string_of_mp mp + | Inline _ -> "inline" + | Equiv kn -> string_of_kn kn let debug_string_of_delta resolve = - let to_string key hint s = - s^", "^(string_of_key key)^"=>"^(string_of_hint hint) - in - Deltamap.fold to_string resolve "" - -let list_contents sub = + let kn_to_string kn hint s = + s^", "^(string_of_kn kn)^"=>"^(string_of_hint hint) + in + let mp_to_string mp mp' s = + s^", "^(string_of_mp mp)^"=>"^(string_of_mp mp') + in + Deltamap.fold mp_to_string kn_to_string resolve "" + +let list_contents sub = let one_pair uid (mp,reso) l = (string_of_subst_domain uid, string_of_mp mp,debug_string_of_delta reso)::l in Umap.fold one_pair sub [] - + let debug_string_of_subst sub = let l = List.map (fun (s1,s2,s3) -> s1^"|->"^s2^"["^s3^"]") (list_contents sub) in "{" ^ String.concat "; " l ^ "}" - -let debug_pr_delta resolve = + +let debug_pr_delta resolve = str (debug_string_of_delta resolve) let debug_pr_subst sub = let l = list_contents sub in let f (s1,s2,s3) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2 ++ - spc () ++ str "[" ++ str s3 ++ str "]") + spc () ++ str "[" ++ str s3 ++ str "]") in str "{" ++ hov 2 (prlist_with_sep pr_comma f l) ++ str "}" - - + let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = match mp with - | MPfile sid -> - let mp',resolve = Umap.find (MPI (MPfile sid)) sub in - mp',resolve + | MPfile sid -> Umap.find (MPI (MPfile sid)) sub | MPbound bid -> begin - try - let mp',resolve = Umap.find (MBI bid) sub in - mp',resolve - with Not_found -> - let mp',resolve = Umap.find (MPI mp) sub in - mp',resolve + try Umap.find (MBI bid) sub + with Not_found -> Umap.find (MPI mp) sub end | MPdot (mp1,l) as mp2 -> begin - try - let mp',resolve = Umap.find (MPI mp2) sub in - mp',resolve + try Umap.find (MPI mp2) sub with Not_found -> let mp1',resolve = aux mp1 in - MPdot (mp1',l),resolve + MPdot (mp1',l),resolve end in - try - Some (aux mp) - with Not_found -> None + try Some (aux mp) with Not_found -> None let subst_mp sub mp = match subst_mp0 sub mp with @@ -428,8 +365,6 @@ let subst_evaluable_reference subst = function | EvalVarRef id -> EvalVarRef id | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn)) - - let rec map_kn f f' c = let func = map_kn f f' in match kind_of_term c with @@ -524,117 +459,76 @@ let rec mp_in_mp mp mp1 = | _ when mp1 = mp -> true | MPdot (mp2,l) -> mp_in_mp mp mp2 | _ -> false - -let mp_in_key mp key = - match key with - | MP mp1 -> - mp_in_mp mp mp1 - | KN kn -> - let mp1,dir,l = repr_kn kn in - mp_in_mp mp mp1 - + let subset_prefixed_by mp resolver = - let prefixmp key hint resolv = - match hint with - | Inline _ -> resolv - | _ -> - if mp_in_key mp key then - Deltamap.add key hint resolv - else - resolv + let mp_prefix mkey mequ rslv = + if mp_in_mp mp mkey then Deltamap.add_mp mkey mequ rslv else rslv in - Deltamap.fold prefixmp resolver empty_delta_resolver + let kn_prefix kn hint rslv = + match hint with + | Inline _ -> rslv + | Equiv _ -> + if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv + in + Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver let subst_dom_delta_resolver subst resolver = - let apply_subst key hint resolver = - match key with - (MP mp) -> - Deltamap.add (MP (subst_mp subst mp)) hint resolver - | (KN kn) -> - Deltamap.add (KN (subst_kn subst kn)) hint resolver + let mp_apply_subst mkey mequ rslv = + Deltamap.add_mp (subst_mp subst mkey) mequ rslv + in + let kn_apply_subst kkey hint rslv = + Deltamap.add_kn (subst_kn subst kkey) hint rslv in - Deltamap.fold apply_subst resolver empty_delta_resolver + Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver -let subst_mp_delta sub mp key= +let subst_mp_delta sub mp mkey = match subst_mp0 sub mp with None -> empty_delta_resolver,mp - | Some (mp',resolve) -> + | Some (mp',resolve) -> let mp1 = find_prefix resolve mp' in let resolve1 = subset_prefixed_by mp1 resolve in - match key with - MP mpk -> - (subst_dom_delta_resolver - (map_mp mp1 mpk empty_delta_resolver) resolve1),mp1 - | _ -> anomaly "Mod_subst: Bad association in resolver" - -let subst_codom_delta_resolver subst resolver = - let apply_subst key hint resolver = - match hint with - Prefix_equiv mp -> - let derived_resolve,mpnew = subst_mp_delta subst mp key in - Deltamap.fold Deltamap.add derived_resolve - (Deltamap.add key (Prefix_equiv mpnew) resolver) - | (Equiv kn) -> - (try - Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver - with - Change_equiv_to_inline (lev,c) -> - Deltamap.add key (Inline (lev,Some c)) resolver) - | Inline (_,None) -> - Deltamap.add key hint resolver - | Inline (lev,Some t) -> - Deltamap.add key (Inline (lev,Some (subst_mps subst t))) resolver + (subst_dom_delta_resolver + (map_mp mp1 mkey empty_delta_resolver) resolve1),mp1 + +let gen_subst_delta_resolver dom subst resolver = + let mp_apply_subst mkey mequ rslv = + let mkey' = if dom then subst_mp subst mkey else mkey in + let rslv',mequ' = subst_mp_delta subst mequ mkey in + Deltamap.join rslv' (Deltamap.add_mp mkey' mequ' rslv) in - Deltamap.fold apply_subst resolver empty_delta_resolver - -let subst_dom_codom_delta_resolver subst resolver = - let apply_subst key hint resolver = - match key,hint with - (MP mp1),Prefix_equiv mp -> - let key = MP (subst_mp subst mp1) in - let derived_resolve,mpnew = subst_mp_delta subst mp key in - Deltamap.fold Deltamap.add derived_resolve - (Deltamap.add key (Prefix_equiv mpnew) resolver) - | (KN kn1),(Equiv kn) -> - let key = KN (subst_kn subst kn1) in - (try - Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver - with - Change_equiv_to_inline (lev,c) -> - Deltamap.add key (Inline (lev,Some c)) resolver) - | (KN kn),Inline (_,None) -> - let key = KN (subst_kn subst kn) in - Deltamap.add key hint resolver - | (KN kn),Inline (lev,Some t) -> - let key = KN (subst_kn subst kn) in - Deltamap.add key (Inline (lev,Some (subst_mps subst t))) resolver - | _,_ -> anomaly "Mod_subst: Bad association in resolver" + let kn_apply_subst kkey hint rslv = + let kkey' = if dom then subst_kn subst kkey else kkey in + let hint' = match hint with + | Equiv kequ -> + (try Equiv (subst_kn_delta subst kequ) + with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c)) + | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t)) + | Inline (_,None) -> hint + in + Deltamap.add_kn kkey' hint' rslv in - Deltamap.fold apply_subst resolver empty_delta_resolver + Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver + +let subst_codom_delta_resolver = gen_subst_delta_resolver false +let subst_dom_codom_delta_resolver = gen_subst_delta_resolver true let update_delta_resolver resolver1 resolver2 = - let apply_res key hint res = - try - if Deltamap.mem key resolver2 then - res else - match hint with - Prefix_equiv mp -> - let new_hint = - Prefix_equiv (find_prefix resolver2 mp) - in Deltamap.add key new_hint res - | Equiv kn -> - (try - let new_hint = - Equiv (solve_delta_kn resolver2 kn) - in Deltamap.add key new_hint res - with - Change_equiv_to_inline (lev,c) -> - Deltamap.add key (Inline (lev,Some c)) res) - | _ -> Deltamap.add key hint res - with Not_found -> - Deltamap.add key hint res - in - Deltamap.fold apply_res resolver1 empty_delta_resolver + let mp_apply_rslv mkey mequ rslv = + if Deltamap.mem_mp mkey resolver2 then rslv + else Deltamap.add_mp mkey (find_prefix resolver2 mequ) rslv + in + let kn_apply_rslv kkey hint rslv = + if Deltamap.mem_kn kkey resolver2 then rslv + else + let hint' = match hint with + | Equiv kequ -> + (try Equiv (solve_delta_kn resolver2 kequ) + with Change_equiv_to_inline (lev,c) -> Inline (lev, Some c)) + | _ -> hint + in + Deltamap.add_kn kkey hint' rslv + in + Deltamap.fold mp_apply_rslv kn_apply_rslv resolver1 empty_delta_resolver let add_delta_resolver resolver1 resolver2 = if resolver1 == resolver2 then @@ -642,8 +536,7 @@ let add_delta_resolver resolver1 resolver2 = else if resolver2 = empty_delta_resolver then resolver1 else - Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2) - resolver2 + Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2 let substition_prefixed_by k mp subst = let prefixmp key (mp_to,reso) sub = -- cgit v1.2.3