From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- kernel/mod_subst.ml | 306 +++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 242 insertions(+), 64 deletions(-) (limited to 'kernel/mod_subst.ml') diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 2942e101..ab4b8e47 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: mod_subst.ml 9874 2007-06-04 13:46:11Z soubiran $ *) +(* $Id: mod_subst.ml 10849 2008-04-25 15:55:16Z soubiran $ *) open Pp open Util @@ -27,11 +27,15 @@ let apply_opt_resolver resolve kn = | Some resolve -> try List.assoc kn resolve with Not_found -> None -type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id +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 type t = substitution_domain @@ -46,9 +50,13 @@ let add_msid msid mp = Umap.add (MSI msid) (mp,None) let add_mbid mbid mp resolve = Umap.add (MBI mbid) (mp,resolve) +let add_mp mp1 mp2 = + Umap.add (MPI mp1) (mp2,None) + 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 list_contents sub = let one_pair uid (mp,_) l = @@ -66,6 +74,7 @@ let debug_pr_subst sub = 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 @@ -74,13 +83,21 @@ let subst_mp0 sub mp = (* 's like subst *) mp',resolve | MPbound bid -> let mp',resolve = Umap.find (MBI bid) sub in - mp',resolve - | MPdot (mp1,l) -> - let mp1',resolve = aux mp1 in - MPdot (mp1',l),resolve + mp',resolve + | MPdot (mp1,l) as mp2 -> + begin + try + let mp',resolve = Umap.find (MPI mp2) sub in + mp',resolve + with Not_found -> + let mp1',resolve = aux mp1 in + MPdot (mp1',l),resolve + end | _ -> raise Not_found 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 @@ -130,6 +147,7 @@ let subst_evaluable_reference subst = function | 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 @@ -201,7 +219,6 @@ let rec map_kn f f' c = else mkCoFix (ln,(lna,tl',bl')) | _ -> c - let subst_mps sub = map_kn (subst_kn0 sub) (subst_con0 sub) @@ -223,60 +240,220 @@ let replace_mp_in_con mpfrom mpto kn = exception BothSubstitutionsAreIdentitySubstitutions exception ChangeDomain of resolver -let join (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') - | 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 in - let kn' = replace_mp_in_con mp key' kn in - if kn==kn' then - (*the key does not appear in mp, 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 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 - + (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 + 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 + 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)::l + | MPself msid -> ((MSI msid),newmp)::l + | _ -> ((MPI mp),newmp)::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') = + 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)::l + in + begin + match List.fold_left compute_set_newkey [] subst_mbi with + | [] -> None + | l -> Some (l) + end + | _ -> None + in + match newsetkey with + | None -> sub + | Some l -> + List.fold_left (fun s k -> Umap.add k (mp,resolve) s) + sub l + in + Umap.fold alias_subst subst1 empty_subst + +let join_alias (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 + Umap.mapi (apply_subst subst2) subst1 + +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 @@ -315,7 +492,8 @@ let force fsubst r = let subst_substituted s r = match !r with - | LSval a -> ref (LSlazy(s,a)) - | LSlazy(s',a) -> - let s'' = join s' s in - ref (LSlazy(s'',a)) + | LSval a -> ref (LSlazy(s,a)) + | LSlazy(s',a) -> + let s'' = join s' s in + ref (LSlazy(s'',a)) + -- cgit v1.2.3