From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- kernel/mod_subst.ml | 865 +++++++++++++++++++++++++++++++++------------------- 1 file changed, 549 insertions(+), 316 deletions(-) (limited to 'kernel/mod_subst.ml') diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 9a76922b..f85cfaaf 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -6,97 +6,299 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: mod_subst.ml 11924 2009-02-13 13:51:54Z soubiran $ *) +(* $Id$ *) open Pp 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 +type delta_hint = + Inline of constr option + | Equiv of kernel_name + | Prefix_equiv of module_path -let apply_opt_resolver resolve kn = - match resolve with - None -> None - | Some resolve -> - try List.assoc kn resolve with Not_found -> None +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 = - MSI of mod_self_id | 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 -module Umap = Map.Make(struct +module Umap = Map.Make(struct type t = substitution_domain 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 + +exception Change_equiv_to_inline of 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 + + +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 + +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 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 + +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 [] + +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,_) l = - (string_of_subst_domain uid, string_of_mp mp)::l + 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 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 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 "}" - - + 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 - | 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 + try let mp',resolve = Umap.find (MPI mp2) sub in mp',resolve - with Not_found -> + with Not_found -> let mp1',resolve = aux mp1 in MPdot (mp1',l),resolve end - | _ -> raise Not_found in try - Some (aux mp) + Some (aux mp) with Not_found -> None let subst_mp sub mp = @@ -104,39 +306,126 @@ let subst_mp sub mp = None -> mp | Some (mp',_) -> mp' +let subst_kn_delta sub kn = + let mp,dir,l = repr_kn kn in + match subst_mp0 sub mp with + Some (mp',resolve) -> + solve_delta_kn resolve (make_kn mp' dir l) + | None -> kn + -let subst_kn0 sub kn = +let subst_kn 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 + (make_kn mp' dir l) + | None -> kn -let subst_kn sub kn = - match subst_kn0 sub kn with - None -> kn - | Some kn' -> 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" @@ -148,352 +437,296 @@ let subst_evaluable_reference subst = function -let rec map_kn f f' c = +let rec map_kn f f' c = let func = map_kn f f' in match kind_of_term c with - | Const kn -> + | Const kn -> (match f' kn with None -> c | Some const ->const) - | Ind (kn,i) -> + | Ind (kn,i) -> (match f kn with None -> c | Some kn' -> mkInd (kn',i)) - | Construct ((kn,i),j) -> + | Construct ((kn,i),j) -> (match f kn with None -> c | Some kn' -> mkConstruct ((kn',i),j)) - | Case (ci,p,ct,l) -> + | 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 p' = func p in let ct' = func ct in let l' = array_smartmap func l in - if (ci.ci_ind==ci_ind && p'==p + if (ci.ci_ind==ci_ind && p'==p && l'==l && ct'==ct)then c - else + else mkCase ({ci with ci_ind = ci_ind}, - p',ct', l') - | Cast (ct,k,t) -> + p',ct', l') + | Cast (ct,k,t) -> let ct' = func ct in let t'= func t in - if (t'==t && ct'==ct) then c + if (t'==t && ct'==ct) then c else mkCast (ct', k, t') - | Prod (na,t,ct) -> + | Prod (na,t,ct) -> let ct' = func ct in let t'= func t in - if (t'==t && ct'==ct) then c + if (t'==t && ct'==ct) then c else mkProd (na, t', ct') - | Lambda (na,t,ct) -> + | Lambda (na,t,ct) -> let ct' = func ct in let t'= func t in - if (t'==t && ct'==ct) then c + if (t'==t && ct'==ct) then c else mkLambda (na, t', ct') - | LetIn (na,b,t,ct) -> + | LetIn (na,b,t,ct) -> let ct' = func ct in let t'= func t in let b'= func b in - if (t'==t && ct'==ct && b==b') then c + if (t'==t && ct'==ct && b==b') then c else mkLetIn (na, b', t', ct') - | App (ct,l) -> + | App (ct,l) -> let ct' = func ct in let l' = array_smartmap func l in if (ct'== ct && l'==l) then c else mkApp (ct',l') - | Evar (e,l) -> + | Evar (e,l) -> let l' = array_smartmap func l in if (l'==l) then c else mkEvar (e,l') | Fix (ln,(lna,tl,bl)) -> let tl' = array_smartmap func tl in let bl' = array_smartmap func bl in - if (bl == bl'&& tl == tl') then c + if (bl == bl'&& tl == tl') then c else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> let tl' = array_smartmap func tl in let bl' = array_smartmap func bl in - if (bl == bl'&& tl == tl') then c + if (bl == bl'&& tl == tl') then c else mkCoFix (ln,(lna,tl',bl')) | _ -> c -let subst_mps sub = - map_kn (subst_kn0 sub) (subst_con0 sub) +let subst_mps sub = + map_kn (subst_mind0 sub) (subst_con0 sub) let rec replace_mp_in_mp mpfrom mpto mp = match mp with | _ when mp = mpfrom -> mpto - | MPdot (mp1,l) -> + | MPdot (mp1,l) -> let mp1' = replace_mp_in_mp mpfrom mpto mp1 in if mp1==mp1' then 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 + else make_kn mp'' dir l -exception BothSubstitutionsAreIdentitySubstitutions -exception ChangeDomain of resolver +let rec mp_in_mp mp mp1 = + match mp1 with + | _ 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 + in + Deltamap.fold prefixmp resolver empty_delta_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 - |None -> begin - match resolve' with - None -> raise BothSubstitutionsAreIdentitySubstitutions - | Some res -> raise (ChangeDomain res) end - | Some res -> 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 +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 - 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 - 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) -> + (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 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 - 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 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" + in + Deltamap.fold apply_subst resolver empty_delta_resolver + +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 - match newsetkey with - | None -> sub - | Some l -> - List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s) - sub l + 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 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 in - Umap.fold alias_subst subst1 empty_subst + Umap.fold prefixmp subst empty_subst -let join_alias (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) key (mp,resolve) = +let join (subst1 : substitution) (subst2 : substitution) = + let apply_subst key (mp,resolve) res = let mp',resolve' = - match subst_mp0 sub mp with + match subst_mp0 subst2 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 subst2 resolve) res + | None -> + subst_codom_delta_resolver subst2 resolve in - mp',resolve'' in - Umap.mapi (apply_subst subst2) subst1 + 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 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 - -let occur_uid uid sub = + +let occur_uid uid sub = let check_one uid' (mp,_) = if uid = uid' || occur_in_path uid mp then raise Exit in - try + try Umap.iter check_one 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 = | LSval of 'a - | LSlazy of substitution * 'a - + | LSlazy of substitution list * 'a + type 'a substituted = 'a lazy_subst ref - + let from_val a = ref (LSval a) - -let force fsubst r = + +let force fsubst r = match !r with | LSval a -> a - | LSlazy(s,a) -> - let a' = fsubst s a in + | LSlazy(s,a) -> + let subst = List.fold_left join empty_subst (List.rev s) in + let a' = fsubst subst a in r := LSval a'; - a' + a' let subst_substituted s r = match !r with - | LSval a -> ref (LSlazy(s,a)) + | LSval a -> ref (LSlazy([s],a)) | LSlazy(s',a) -> - let s'' = join s' s in - ref (LSlazy(s'',a)) - + ref (LSlazy(s::s',a)) + -- cgit v1.2.3