diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 95 |
1 files changed, 0 insertions, 95 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index db1b1b6df8..e15d4ab2f7 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -138,95 +138,6 @@ end module MPset = Set.Make(MPord) module MPmap = Map.Make(MPord) - -(* this is correct under the condition that bound and struct - identifiers can never be identical (i.e. get the same stamp)! *) - -type substitution = module_path Umap.t - -let empty_subst = Umap.empty - -let add_msid = Umap.add -let add_mbid = Umap.add - -let map_msid msid mp = add_msid msid mp empty_subst -let map_mbid mbid mp = add_msid mbid mp empty_subst - -let list_contents sub = - let one_pair uid mp l = - (string_of_uid uid, string_of_mp mp)::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 - "{" ^ String.concat "; " l ^ "}" - -let debug_pr_subst sub = - let l = list_contents sub in - let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2) - in - str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" - -let rec subst_mp sub mp = (* 's like subst *) - match mp with - | MPself sid -> - (try Umap.find sid sub with Not_found -> mp) - | MPbound bid -> - (try Umap.find bid sub with Not_found -> mp) - | MPdot (mp1,l) -> - let mp1' = subst_mp sub mp1 in - if mp1==mp1' then - mp - else - MPdot (mp1',l) - | _ -> mp - -let join subst1 subst2 = - let subst = Umap.map (subst_mp subst2) subst1 in - Umap.fold Umap.add subst2 subst - -let rec occur_in_path uid = function - | MPself sid -> sid = uid - | MPbound bid -> bid = uid - | MPdot (mp1,_) -> occur_in_path uid mp1 - | _ -> false - -let occur_uid uid sub = - let check_one uid' mp = - if uid = uid' || occur_in_path uid mp then raise Exit - in - try - Umap.iter check_one sub; - false - with Exit -> true - -let occur_msid = occur_uid -let occur_mbid = occur_uid - -type 'a lazy_subst = - | LSval of 'a - | LSlazy of substitution * 'a - -type 'a substituted = 'a lazy_subst ref - -let from_val a = ref (LSval a) - -let force fsubst r = - match !r with - | LSval a -> a - | LSlazy(s,a) -> - let a' = fsubst s a in - r := LSval a'; - a' - -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)) - (* Kernel names *) type kernel_name = module_path * dir_path * label @@ -246,11 +157,6 @@ let string_of_kn (mp,dir,l) = let pr_kn kn = str (string_of_kn kn) -let subst_kn sub (mp,dir,l as kn) = - let mp' = subst_mp sub mp in - if mp==mp' then kn else (mp',dir,l) - - let kn_ord kn1 kn2 = let mp1,dir1,l1 = kn1 in let mp2,dir2,l2 = kn2 in @@ -298,7 +204,6 @@ let string_of_con = string_of_kn let con_label = label let pr_con = pr_kn let con_modpath = modpath -let subst_con = subst_kn let ith_mutual_inductive (kn,_) i = (kn,i) let ith_constructor_of_inductive ind i = (ind,i) |