diff options
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 732 |
1 files changed, 459 insertions, 273 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 238aa3544..a9d4a246d 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -13,27 +13,30 @@ open Util open Names open Term -(* WARNING: not every constant in the associative list domain used to exist - in the environment. This allows a simple implementation of the join - operation. However, iterating over the associative list becomes a non-sense -*) -type resolver = (constant * constr option) list - -let make_resolver resolve = resolve - -let apply_opt_resolver resolve kn = - match resolve with - None -> None - | Some resolve -> - try List.assoc kn resolve with Not_found -> None - -type substitution_domain = - MSI of mod_self_id + +type delta_hint = + Inline of 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 + +let empty_delta_resolver = Deltamap.empty + +type substitution_domain = | MBI of mod_bound_id | MPI of module_path let string_of_subst_domain = function - MSI msid -> debug_string_of_msid msid | MBI mbid -> debug_string_of_mbid mbid | MPI mp -> string_of_mp mp @@ -42,48 +45,233 @@ module Umap = Map.Make(struct let compare = Pervasives.compare end) -type substitution = (module_path * resolver option) Umap.t - +type substitution = (module_path * delta_resolver) Umap.t + let empty_subst = Umap.empty -let add_msid msid mp = - Umap.add (MSI msid) (mp,None) + +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 = - Umap.add (MPI mp1) (mp2,None) +let add_mp mp1 mp2 resolve = + Umap.add (MPI mp1) (mp2,resolve) -let map_msid msid mp = add_msid msid mp empty_subst let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst -let map_mp mp1 mp2 = add_mp mp1 mp2 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 remove_mp_delta_resolver resolver mp = + Deltamap.remove (MP mp) resolver + +exception Inline_kn + +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" + in + try + sub_mp mp + with + Not_found -> mp + +let solve_delta_kn resolve kn = + try + match Deltamap.find (KN kn) resolve with + | Equiv kn1 -> kn1 + | Inline _ -> 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 + + +let constant_of_delta resolve con = + let kn = user_con con in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + con + else + constant_of_kn_equiv kn new_kn + +let constant_of_delta2 resolve con = + let kn = canonical_con con in + let kn1 = user_con con in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + con + else + constant_of_kn_equiv kn1 new_kn + +let mind_of_delta resolve mind = + let kn = user_mind mind in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + mind + else + mind_of_kn_equiv kn new_kn + +let mind_of_delta2 resolve mind = + let kn = canonical_mind mind in + let kn1 = user_mind mind in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + mind + else + mind_of_kn_equiv kn1 new_kn + + + +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 list_contents sub = - let one_pair uid (mp,_) l = - (string_of_subst_domain uid, string_of_mp mp)::l +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 + +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) -> s1^"|->"^s2) (list_contents sub) in + 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) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2) + 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_coma f l) ++ str "}" - - + + let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = match mp with - | MPself sid -> - let mp',resolve = Umap.find (MSI sid) sub in + | MPfile sid -> + let mp',resolve = Umap.find (MPI (MPfile sid)) sub in mp',resolve | MPbound bid -> - let mp',resolve = Umap.find (MBI bid) sub in - mp',resolve + 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 + end | MPdot (mp1,l) as mp2 -> begin try @@ -93,7 +281,6 @@ let subst_mp0 sub mp = (* 's like subst *) let mp1',resolve = aux mp1 in MPdot (mp1',l),resolve end - | _ -> raise Not_found in try Some (aux mp) @@ -104,39 +291,126 @@ let subst_mp sub mp = None -> mp | Some (mp',_) -> mp' - -let subst_kn0 sub kn = +let subst_kn_delta sub kn = let mp,dir,l = repr_kn kn in match subst_mp0 sub mp with - Some (mp',_) -> - Some (make_kn mp' dir l) - | None -> None + Some (mp',resolve) -> + solve_delta_kn resolve (make_kn mp' dir l) + | None -> kn + let subst_kn sub kn = - match subst_kn0 sub kn with - None -> kn - | Some kn' -> kn' + let mp,dir,l = repr_kn kn in + match subst_mp0 sub mp with + Some (mp',_) -> + (make_kn mp' dir l) + | None -> kn + +exception No_subst + +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 subst_con sub con = - let mp,dir,l = repr_con con in - match subst_mp0 sub mp with - None -> con,mkConst con - | Some (mp',resolve) -> - let con' = make_con mp' dir l in - match apply_opt_resolver resolve con with - None -> con',mkConst con' - | Some t -> con',t + 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 + 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 -> con',t + with No_subst -> con , mkConst con + let subst_con0 sub con = - let mp,dir,l = repr_con con in - match subst_mp0 sub mp with - None -> None - | Some (mp',resolve) -> - let con' = make_con mp' dir l in - match apply_opt_resolver resolve con with - None -> Some (mkConst con') - | Some t -> Some t - + 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 + 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) + (* 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" @@ -220,7 +494,7 @@ let rec map_kn f f' c = | _ -> c let subst_mps sub = - map_kn (subst_kn0 sub) (subst_con0 sub) + map_kn (subst_mind0 sub) (subst_con0 sub) let rec replace_mp_in_mp mpfrom mpto mp = match mp with @@ -231,233 +505,145 @@ let rec replace_mp_in_mp mpfrom mpto mp = else MPdot (mp1',l) | _ -> mp -let replace_mp_in_con mpfrom mpto kn = - let mp,dir,l = repr_con kn in +let replace_mp_in_kn mpfrom mpto kn = + let mp,dir,l = repr_kn kn in let mp'' = replace_mp_in_mp mpfrom mpto mp in if mp==mp'' then kn - else make_con mp'' dir l - -exception BothSubstitutionsAreIdentitySubstitutions -exception ChangeDomain of resolver - -let join (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) key (mp,resolve) = - let mp',resolve' = - match subst_mp0 sub mp with - None -> mp, None - | Some (mp',resolve') -> mp',resolve' in - let resolve'' : resolver option = - try - let res = - match resolve with - Some res -> res - | None -> - match resolve' with - None -> raise BothSubstitutionsAreIdentitySubstitutions - | Some res -> raise (ChangeDomain res) - in - Some - (List.map - (fun (kn,topt) -> - kn, - match topt with - None -> - (match key with - MSI msid -> - let kn' = replace_mp_in_con (MPself msid) mp kn in - apply_opt_resolver resolve' kn' - | MBI mbid -> - let kn' = replace_mp_in_con (MPbound mbid) mp kn in - apply_opt_resolver resolve' kn' - | MPI mp1 -> - let kn' = replace_mp_in_con mp1 mp kn in - apply_opt_resolver resolve' kn') - | Some t -> Some (subst_mps sub t)) res) - with - BothSubstitutionsAreIdentitySubstitutions -> None - | ChangeDomain res -> - let rec changeDom = function - | [] -> [] - | (kn,topt)::r -> - let key' = - match key with - MSI msid -> MPself msid - | MBI mbid -> MPbound mbid - | MPI mp1 -> mp1 in - let kn' = replace_mp_in_con mp key' kn in - if kn==kn' then - (*the key does not appear in kn, we remove it - from the resolver that we are building*) - changeDom r - else - (kn',topt)::(changeDom r) - in - Some (changeDom res) - in - mp',resolve'' in - let subst = Umap.mapi (apply_subst subst2) subst1 in - (Umap.fold Umap.add subst2 subst) - -let subst_key subst1 subst2 = - let replace_in_key key (mp,resolve) sub= - let newkey = - match key with - | MPI mp1 -> - begin - match subst_mp0 subst1 mp1 with - | None -> None - | Some (mp2,_) -> Some (MPI mp2) - end - | _ -> None - in - match newkey with - | None -> Umap.add key (mp,resolve) sub - | Some mpi -> Umap.add mpi (mp,resolve) sub + else make_kn mp'' dir l + +let mp_in_key mp key = + let rec mp_rec mp1 = + match mp1 with + | _ when mp1 = mp -> true + | MPdot (mp2,l) -> mp_rec mp2 + | _ -> false + in + match key with + | MP mp1 -> + mp_rec mp1 + | KN kn -> + let mp1,dir,l = repr_kn kn in + mp_rec mp1 + +let subset_prefixed_by mp resolver = + let prefixmp key hint resolv = + if mp_in_key mp key then + Deltamap.add key hint resolv + else + resolv in - Umap.fold replace_in_key subst2 empty_subst - -let update_subst_alias subst1 subst2 = - let subst_inv key (mp,resolve) sub = - let newmp = - match key with - | MBI msid -> MPbound msid - | MSI msid -> MPself msid - | MPI mp -> mp - in - match mp with - | MPbound mbid -> Umap.add (MBI mbid) (newmp,None) sub - | MPself msid -> Umap.add (MSI msid) (newmp,None) sub - | _ -> Umap.add (MPI mp) (newmp,None) sub + Deltamap.fold prefixmp 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 in - let subst_mbi = Umap.fold subst_inv subst2 empty_subst in - let alias_subst key (mp,resolve) sub= - let newkey = - match key with - | MPI mp1 -> - begin - match subst_mp0 subst_mbi mp1 with - | None -> None - | Some (mp2,_) -> Some (MPI mp2) - end - | _ -> None - in - match newkey with - | None -> Umap.add key (mp,resolve) sub - | Some mpi -> Umap.add mpi (mp,resolve) sub + Deltamap.fold apply_subst resolver empty_delta_resolver + +let subst_mp_delta sub mp key= + match subst_mp0 sub mp with + None -> empty_delta_resolver,mp + | 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) -> + Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver + | Inline None -> + Deltamap.add key hint resolver + | Inline (Some t) -> + Deltamap.add key (Inline (Some (subst_mps subst t))) resolver in - Umap.fold alias_subst subst1 empty_subst - -let update_subst subst1 subst2 = - let subst_inv key (mp,resolve) l = - let newmp = - match key with - | MBI msid -> MPbound msid - | MSI msid -> MPself msid - | MPI mp -> mp - in - match mp with - | MPbound mbid -> ((MBI mbid),newmp,resolve)::l - | MPself msid -> ((MSI msid),newmp,resolve)::l - | _ -> ((MPI mp),newmp,resolve)::l + 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 + Deltamap.add key (Equiv (subst_kn_delta subst kn)) 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" in - let subst_mbi = Umap.fold subst_inv subst2 [] in - let alias_subst key (mp,resolve) sub= - let newsetkey = - match key with - | MPI mp1 -> - let compute_set_newkey l (k,mp',resolve) = - let mp_from_key = match k with - | MBI msid -> MPbound msid - | MSI msid -> MPself msid - | MPI mp -> mp - in - let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in - if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l - in - begin - match List.fold_left compute_set_newkey [] subst_mbi with - | [] -> None - | l -> Some (l) - end - | _ -> None + Deltamap.fold apply_subst resolver empty_delta_resolver + +let update_delta_resolver resolver1 resolver2 = + let apply_res key hint res = + try + match hint with + Prefix_equiv mp -> + let new_hint = + Prefix_equiv (find_prefix resolver2 mp) + in Deltamap.add key new_hint res + | Equiv kn -> + let new_hint = + Equiv (solve_delta_kn resolver2 kn) + in Deltamap.add key new_hint res + | _ -> Deltamap.add key hint res + with not_found -> + Deltamap.add key hint res in - match newsetkey with - | None -> sub - | Some l -> - List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s) - sub l - in - Umap.fold alias_subst subst1 empty_subst + Deltamap.fold apply_res resolver1 empty_delta_resolver + +let add_delta_resolver resolver1 resolver2 = + if resolver1 == resolver2 then + resolver2 + else if resolver2 = empty_delta_resolver then + resolver1 + else + Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2) + resolver2 -let join_alias (subst1 : substitution) (subst2 : substitution) = +let join (subst1 : substitution) (subst2 : substitution) = let apply_subst (sub : substitution) key (mp,resolve) = let mp',resolve' = match subst_mp0 sub mp with None -> mp, None - | Some (mp',resolve') -> mp',resolve' in - let resolve'' : resolver option = - try - let res = - match resolve with - Some res -> res - | None -> - match resolve' with - None -> raise BothSubstitutionsAreIdentitySubstitutions - | Some res -> raise (ChangeDomain res) - in - Some - (List.map - (fun (kn,topt) -> - kn, - match topt with - None -> - (match key with - MSI msid -> - let kn' = replace_mp_in_con (MPself msid) mp kn in - apply_opt_resolver resolve' kn' - | MBI mbid -> - let kn' = replace_mp_in_con (MPbound mbid) mp kn in - apply_opt_resolver resolve' kn' - | MPI mp1 -> - let kn' = replace_mp_in_con mp1 mp kn in - apply_opt_resolver resolve' kn') - | Some t -> Some (subst_mps sub t)) res) - with - BothSubstitutionsAreIdentitySubstitutions -> None - | ChangeDomain res -> - let rec changeDom = function - | [] -> [] - | (kn,topt)::r -> - let key' = - match key with - MSI msid -> MPself msid - | MBI mbid -> MPbound mbid - | MPI mp1 -> mp1 in - let kn' = replace_mp_in_con mp key' kn in - if kn==kn' then - (*the key does not appear in kn, we remove it - from the resolver that we are building*) - changeDom r - else - (kn',topt)::(changeDom r) - in - Some (changeDom res) + | Some (mp',resolve') -> mp' + ,Some resolve' in + let resolve'' : delta_resolver = + match resolve' with + Some res -> + add_delta_resolver + (subst_dom_codom_delta_resolver sub resolve) + res + | None -> + subst_codom_delta_resolver sub resolve in mp',resolve'' in - Umap.mapi (apply_subst subst2) subst1 + let subst = Umap.mapi (apply_subst subst2) subst1 in + (Umap.fold Umap.add subst2 subst) -let remove_alias subst = - let rec remove key (mp,resolve) sub = - match key with - MPI _ -> sub - | _ -> Umap.add key (mp,resolve) sub - in - Umap.fold remove subst empty_subst let rec occur_in_path uid path = match uid,path with - | MSI sid,MPself sid' -> sid = sid' | MBI bid,MPbound bid' -> bid = bid' | _,MPdot (mp1,_) -> occur_in_path uid mp1 | _ -> false @@ -471,7 +657,7 @@ let occur_uid uid sub = false with Exit -> true -let occur_msid uid = occur_uid (MSI uid) + let occur_mbid uid = occur_uid (MBI uid) type 'a lazy_subst = |