Names.substitution (and related functions) and Term.subst_mps moved to

the new module kernel/mod_subst.ml.

MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now
possible to define substitutions that also delta-expand constants
(by associating the delta-expanded form to the constant name).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7

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)