diff options
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 809 |
1 files changed, 321 insertions, 488 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index ab8b60be..9aeaf110 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -1,305 +1,252 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: mod_subst.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* Created by Claudio Sacerdoti from contents of term.ml, names.ml and + new support for constant inlining in functor application, Nov 2004 *) +(* Optimizations and bug fixes by Élie Soubiran, from Feb 2008 *) + +(* This file provides types and functions for managing name + substitution in module constructions *) open Pp open Util open Names open Term +(* For Inline, the int is an inlining level, and the constr (if present) + is the term into which we should inline *) type delta_hint = - Inline of 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 +(* 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 find_mp mp map = MPmap.find mp (fst map) + let find_kn kn map = KNmap.find kn (snd 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 map i = KNmap.fold f (snd map) 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 -module Deltamap = Map.Make(struct - type t = delta_key - let compare = Pervasives.compare - end) +let empty_delta_resolver = Deltamap.empty -type delta_resolver = delta_hint Deltamap.t +module MBImap = Map.Make + (struct + type t = mod_bound_id + let compare = Pervasives.compare + end) + +module Umap = struct + type 'a t = 'a MPmap.t * 'a MBImap.t + let empty = MPmap.empty, MBImap.empty + let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2 + let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2) + let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2) + let find_mp mp map = MPmap.find mp (fst map) + let find_mbi mbi map = MBImap.find mbi (snd map) + let mem_mp mp map = MPmap.mem mp (fst map) + let mem_mbi mbi map = MBImap.mem mbi (snd map) + let iter_mbi f map = MBImap.iter f (snd map) + let fold fmp fmbi (m1,m2) i = + MPmap.fold fmp m1 (MBImap.fold fmbi m2 i) + let join map1 map2 = fold add_mp add_mbi map1 map2 +end -let empty_delta_resolver = Deltamap.empty +type substitution = (module_path * delta_resolver) Umap.t -type substitution_domain = - | MBI of mod_bound_id - | MPI of module_path +let empty_subst = Umap.empty -let string_of_subst_domain = function - | MBI mbid -> debug_string_of_mbid mbid - | MPI mp -> string_of_mp mp +let is_empty_subst = Umap.is_empty -module Umap = Map.Make(struct - type t = substitution_domain - let compare = Pervasives.compare - end) +(* <debug> *) -type substitution = (module_path * delta_resolver) Umap.t - -let empty_subst = Umap.empty +let string_of_hint = function + | Inline (_,Some _) -> "inline(Some _)" + | Inline _ -> "inline()" + | Equiv kn -> string_of_kn kn + +let debug_string_of_delta resolve = + let kn_to_string kn hint l = + (string_of_kn kn ^ "=>" ^ string_of_hint hint) :: l + in + let mp_to_string mp mp' l = + (string_of_mp mp ^ "=>" ^ string_of_mp mp') :: l + in + let l = Deltamap.fold mp_to_string kn_to_string resolve [] in + String.concat ", " (List.rev l) + +let list_contents sub = + let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in + let mp_one_pair mp0 p l = (string_of_mp mp0, one_pair p)::l in + let mbi_one_pair mbi p l = (debug_string_of_mbid mbi, one_pair p)::l in + Umap.fold mp_one_pair mbi_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 = + 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 "]") + in + str "{" ++ hov 2 (prlist_with_sep pr_comma f l) ++ str "}" +(* </debug> *) -let string_of_subst_domain = function - | MBI mbid -> debug_string_of_mbid mbid - | MPI mp -> string_of_mp mp - -let add_mbid mbid mp resolve = - Umap.add (MBI mbid) (mp,resolve) -let add_mp mp1 mp2 resolve = - Umap.add (MPI mp1) (mp2,resolve) +(** Extending a [delta_resolver] *) +let add_inline_delta_resolver kn (lev,oc) = Deltamap.add_kn kn (Inline (lev,oc)) + +let add_kn_delta_resolver kn kn' = Deltamap.add_kn kn (Equiv kn') + +let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2 + +(** Extending a [substitution *) + +let add_mbid mbid mp resolve s = Umap.add_mbi mbid (mp,resolve) s +let add_mp mp1 mp2 resolve s = Umap.add_mp mp1 (mp2,resolve) s 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 = - Deltamap.add (KN(user_con con)) (Inline None) - -let add_inline_constr_delta_resolver con cstr = - Deltamap.add (KN(user_con con)) (Inline (Some cstr)) - -let add_constant_delta_resolver 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 - -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 - -let delta_of_kn resolve kn = - try - match Deltamap.find (KN kn) resolve with - | Equiv kn1 -> kn1 - | Inline _ -> kn - | _ -> anomaly - "mod_subst: bad association in delta_resolver" - with - Not_found -> kn +let mp_in_delta mp = Deltamap.mem_mp mp -let remove_mp_delta_resolver resolver mp = - Deltamap.remove (MP mp) resolver +let kn_in_delta kn resolver = + try + match Deltamap.find_kn kn resolver with + | Equiv _ -> true + | Inline _ -> false + with Not_found -> false -exception Inline_kn +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 rec find_prefix resolve mp = +let mp_of_delta resolve mp = + try Deltamap.find_mp mp resolve with Not_found -> 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 constr +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 (Some c) -> - raise (Change_equiv_to_inline 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 kn_of_delta resolve kn = + try solve_delta_kn resolve kn + with e when Errors.noncritical e -> kn + +let constant_of_delta_kn resolve kn = + constant_of_kn_equiv kn (kn_of_delta resolve kn) + +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 e when Errors.noncritical e -> 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_kn resolve kn = + mind_of_kn_equiv kn (kn_of_delta resolve 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 inline_of_delta resolver = - let extract key hint l = - match key,hint with - |KN kn, Inline _ -> kn::l - | _,_ -> l - in - Deltamap.fold extract resolver [] + 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 kn hint l = + match hint with + | Inline (lev,_) -> if lev <= inl_lev then (lev,kn)::l else l + | _ -> l + in + 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 None -> None - | Inline (Some const) -> Some const - | _ -> raise Not_inline - with - Not_found | Not_inline -> - try match Deltamap.find (KN kn1) resolve with - | Inline None -> None - | Inline (Some const) -> Some const - | _ -> 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 -> + if kn1 == kn2 then None + else + 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 - -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 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 = - 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 "]") - 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_mp mp 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_mp mp sub end | MPdot (mp1,l) as mp2 -> begin - try - let mp',resolve = Umap.find (MPI mp2) sub in - mp',resolve + try Umap.find_mp 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 @@ -327,107 +274,49 @@ type sideconstantsubst = | User | Canonical -let subst_ind sub mind = - let kn1,kn2 = user_mind mind,canonical_mind mind in - let mp1,dir,l = repr_kn kn1 in - let mp2,_,_ = repr_kn kn2 in - try - let side,mind',resolve = - match subst_mp0 sub mp1,subst_mp0 sub mp2 with - None,None ->raise No_subst - | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve - | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve - | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, - (make_mind_equiv mp1' mp2' dir l), resolve2 - in - match side with - |User -> - let mind = mind_of_delta resolve mind' in - mind - |Canonical -> - let mind = mind_of_delta2 resolve mind' in - mind - with - No_subst -> mind - -let subst_mind0 sub mind = - let kn1,kn2 = user_mind mind,canonical_mind mind in - let mp1,dir,l = repr_kn kn1 in - let mp2,_,_ = repr_kn kn2 in - try - let side,mind',resolve = - match subst_mp0 sub mp1,subst_mp0 sub mp2 with - None,None ->raise No_subst - | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve - | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve - | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, - (make_mind_equiv mp1' mp2' dir l), resolve2 - in - match side with - |User -> - let mind = mind_of_delta resolve mind' in - Some mind - |Canonical -> - let mind = mind_of_delta2 resolve mind' in - Some mind - with - No_subst -> Some mind +let gen_subst_mp f sub mp1 mp2 = + let o1 = subst_mp0 sub mp1 in + let o2 = if mp1 == mp2 then o1 else subst_mp0 sub mp2 in + match o1, o2 with + | None, None -> raise No_subst + | Some (mp',resolve), None -> User, (f mp' mp2), resolve + | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve + | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2 -let subst_con sub con = - let kn1,kn2 = user_con con,canonical_con con in +let subst_ind sub mind = + let kn1,kn2 = user_mind mind, canonical_mind mind in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in - try - let side,con',resolve = - match subst_mp0 sub mp1,subst_mp0 sub mp2 with - None,None ->raise No_subst - | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve - | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve - | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, - (make_con_equiv mp1' mp2' dir l), resolve2 - in - match constant_of_delta_with_inline resolve con' with - None -> begin - match side with - |User -> - let con = constant_of_delta resolve con' in - con,mkConst con - |Canonical -> - let con = constant_of_delta2 resolve con' in - con,mkConst con - end - | Some t -> - (* In case of inlining, discard the canonical part (cf #2608) *) - constant_of_kn (user_con con'), t - with No_subst -> con , mkConst con - + let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in + try + let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in + match side with + | User -> mind_of_delta resolve mind' + | Canonical -> mind_of_delta2 resolve mind' + with No_subst -> mind let subst_con0 sub con = let kn1,kn2 = user_con con,canonical_con con in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in - try - let side,con',resolve = - match subst_mp0 sub mp1,subst_mp0 sub mp2 with - None,None ->raise No_subst - | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve - | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve - | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, - (make_con_equiv mp1' mp2' dir l), resolve2 + let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in + let dup con = con, mkConst con in + let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in + match constant_of_delta_with_inline resolve con' with + | Some t -> + (* In case of inlining, discard the canonical part (cf #2608) *) + constant_of_kn (user_con con'), t + | None -> + let con'' = match side with + | User -> constant_of_delta resolve con' + | Canonical -> constant_of_delta2 resolve con' in - match constant_of_delta_with_inline resolve con' with - None ->begin - match side with - |User -> - let con = constant_of_delta resolve con' in - Some (mkConst con) - |Canonical -> - let con = constant_of_delta2 resolve con' in - Some (mkConst con) - end - | t -> t - with No_subst -> Some (mkConst con) - + if con'' == con then raise No_subst else dup con'' + +let subst_con sub con = + try subst_con0 sub con + with No_subst -> con, mkConst con + (* Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" @@ -437,29 +326,22 @@ 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 - | Const kn -> - (match f' kn with - None -> c - | Some const ->const) + | Const kn -> (try snd (f' kn) with No_subst -> c) | Ind (kn,i) -> - (match f kn with - None -> c - | Some kn' -> - mkInd (kn',i)) + let kn' = f kn in + if kn'==kn then c else mkInd (kn',i) | Construct ((kn,i),j) -> - (match f kn with - None -> c - | Some kn' -> - mkConstruct ((kn',i),j)) + let kn' = f kn in + if kn'==kn then c else mkConstruct ((kn',i),j) | Case (ci,p,ct,l) -> let ci_ind = let (kn,i) = ci.ci_ind in - (match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in + let kn' = f kn in + if kn'==kn then ci.ci_ind else kn',i + in let p' = func p in let ct' = func ct in let l' = array_smartmap func l in @@ -510,8 +392,9 @@ let rec map_kn f f' c = else mkCoFix (ln,(lna,tl',bl')) | _ -> c -let subst_mps sub = - map_kn (subst_mind0 sub) (subst_con0 sub) +let subst_mps sub c = + if is_empty_subst sub then c + else map_kn (subst_ind sub) (subst_con0 sub) c let rec replace_mp_in_mp mpfrom mpto mp = match mp with @@ -533,117 +416,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 + 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 prefixmp resolver empty_delta_resolver + 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 c -> - Deltamap.add key (Inline (Some c)) resolver) - | Inline None -> - Deltamap.add key hint resolver - | Inline (Some t) -> - Deltamap.add key (Inline (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 c -> - Deltamap.add key (Inline (Some c)) resolver) - | (KN kn),Inline None -> - let key = KN (subst_kn subst kn) in - Deltamap.add key hint resolver - | (KN kn),Inline (Some t) -> - let key = KN (subst_kn subst kn) in - Deltamap.add key (Inline (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 c -> - Deltamap.add key (Inline (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 @@ -651,63 +493,54 @@ 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 = - match key with - | MPI mpk -> - if mp_in_mp mp mpk && mp <> mpk then - let new_key = replace_mp_in_mp mp k mpk in - Umap.add (MPI new_key) (mp_to,reso) sub - else - sub - | _ -> sub + let mp_prefixmp kmp (mp_to,reso) sub = + if mp_in_mp mp kmp && mp <> kmp then + let new_key = replace_mp_in_mp mp k kmp in + Umap.add_mp new_key (mp_to,reso) sub + else sub + in + let mbi_prefixmp mbi _ sub = sub in - Umap.fold prefixmp subst empty_subst + Umap.fold mp_prefixmp mbi_prefixmp subst empty_subst -let join (subst1 : substitution) (subst2 : substitution) = - let apply_subst key (mp,resolve) res = +let join subst1 subst2 = + let apply_subst mpk add (mp,resolve) res = let mp',resolve' = match subst_mp0 subst2 mp with - None -> mp, None - | Some (mp',resolve') -> mp' - ,Some resolve' in - let resolve'' : delta_resolver = + | None -> mp, None + | Some (mp',resolve') -> mp', Some resolve' in + let resolve'' = match resolve' with - Some res -> - add_delta_resolver + | Some res -> + add_delta_resolver (subst_dom_codom_delta_resolver subst2 resolve) res - | None -> + | None -> subst_codom_delta_resolver subst2 resolve in - let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in - let prefixed_subst = substition_prefixed_by k mp subst2 in - Umap.fold Umap.add prefixed_subst - (Umap.add key (mp',resolve'') res) in - let subst = Umap.fold apply_subst subst1 empty_subst in - (Umap.fold Umap.add subst2 subst) - - - -let rec occur_in_path uid path = - match uid,path with - | MBI bid,MPbound bid' -> bid = bid' - | _,MPdot (mp1,_) -> occur_in_path uid mp1 + let prefixed_subst = substition_prefixed_by mpk mp' subst2 in + Umap.join prefixed_subst (add (mp',resolve'') res) + in + let mp_apply_subst mp = apply_subst mp (Umap.add_mp mp) in + let mbi_apply_subst mbi = apply_subst (MPbound mbi) (Umap.add_mbi mbi) in + let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in + Umap.join subst2 subst + +let rec occur_in_path mbi = function + | MPbound bid' -> mbi = bid' + | MPdot (mp1,_) -> occur_in_path mbi mp1 | _ -> false -let occur_uid uid sub = - let check_one uid' (mp,_) = - if uid = uid' || occur_in_path uid mp then raise Exit +let occur_mbid mbi sub = + let check_one mbi' (mp,_) = + if mbi = mbi' || occur_in_path mbi mp then raise Exit in - try - Umap.iter check_one sub; - false - with Exit -> true - - -let occur_mbid uid = occur_uid (MBI uid) + try + Umap.iter_mbi check_one sub; + false + with Exit -> true type 'a lazy_subst = | LSval of 'a |