Mod_subst: some simplifications, some more significant names to functions, etc

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

1 files changed, 59 insertions, 56 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 668f2d412..314cc0ee0 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -75,29 +75,63 @@ let empty_subst = Umap.empty
 
 let is_empty_subst = Umap.is_empty
 
-let add_mbid mbid mp resolve = Umap.add_mbi mbid (mp,resolve)
-let add_mp mp1 mp2 resolve = Umap.add_mp mp1 (mp2,resolve)
+(* <debug> *)
 
-let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst
-let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst
+let string_of_hint = function
+  | Inline (_,Some _) -> "inline(Some _)"
+  | Inline _ -> "inline()"
+  | Equiv kn -> string_of_kn kn
+
+let debug_string_of_delta resolve =
+  let kn_to_string kn hint s =
+    s^", "^(string_of_kn kn)^"=>"^(string_of_hint hint)
+  in
+  let mp_to_string mp mp' s =
+    s^", "^(string_of_mp mp)^"=>"^(string_of_mp mp')
+  in
+  Deltamap.fold mp_to_string kn_to_string resolve ""
+
+let list_contents sub =
+  let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in
+  let mp_one_pair mp0 p l = (string_of_mp mp0, one_pair p)::l in
+  let mbi_one_pair mbi p l = (debug_string_of_mbid mbi, one_pair p)::l in
+  Umap.fold mp_one_pair mbi_one_pair sub []
+
+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 l = list_contents sub in
+  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_comma f l) ++ str "}"
 
-let add_inline_delta_resolver con lev =
-  Deltamap.add_kn (user_con con) (Inline (lev,None))
+(* </debug> *)
 
-let add_inline_constr_delta_resolver con lev cstr =
-  Deltamap.add_kn (user_con con) (Inline (lev, Some cstr))
+(** Extending a [delta_resolver] *)
 
-let add_constant_delta_resolver con =
-  Deltamap.add_kn (user_con con) (Equiv (canonical_con con))
+let add_inline_delta_resolver kn (lev,oc) = Deltamap.add_kn kn (Inline (lev,oc))
 
-let add_mind_delta_resolver mind =
-  Deltamap.add_kn (user_mind mind) (Equiv (canonical_mind mind))
+let add_kn_delta_resolver kn kn' = Deltamap.add_kn kn (Equiv kn')
 
-let add_mp_delta_resolver mp1 mp2 =
-  Deltamap.add_mp mp1 mp2
+let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2
+
+(** Extending a [substitution *)
+
+let add_mbid mbid mp resolve s = Umap.add_mbi mbid (mp,resolve) s
+let add_mp mp1 mp2 resolve s = Umap.add_mp mp1 (mp2,resolve) s
+
+let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst
+let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst
 
-let mp_in_delta mp =
-  Deltamap.mem_mp mp
+let mp_in_delta mp = Deltamap.mem_mp mp
 
 let kn_in_delta kn resolver =
   try
@@ -109,7 +143,7 @@ let kn_in_delta kn resolver =
 let con_in_delta con resolver = kn_in_delta (user_con con) resolver
 let mind_in_delta mind resolver = kn_in_delta (user_mind mind) resolver
 
-let delta_of_mp resolve mp =
+let mp_of_delta resolve mp =
  try Deltamap.find_mp mp resolve with Not_found -> mp
 
 let rec find_prefix resolve mp =
@@ -137,15 +171,19 @@ let solve_delta_kn resolve kn =
     else
       make_kn new_mp dir l
 
+let kn_of_delta resolve kn =
+  try solve_delta_kn resolve kn
+  with _ -> kn
+
+let constant_of_delta_kn resolve kn =
+  constant_of_kn_equiv kn (kn_of_delta resolve kn)
+
 let gen_of_delta resolve x kn fix_can =
   try
     let new_kn = solve_delta_kn resolve kn in
     if kn == new_kn then x else fix_can new_kn
   with _ -> x
 
-let constant_of_delta_kn resolve kn =
-  gen_of_delta resolve (constant_of_kn kn) kn (constant_of_kn_equiv kn)
-
 let constant_of_delta resolve con =
   let kn = user_con con in
   gen_of_delta resolve con kn (constant_of_kn_equiv kn)
@@ -155,7 +193,7 @@ let constant_of_delta2 resolve con =
   gen_of_delta resolve con kn (constant_of_kn_equiv kn')
 
 let mind_of_delta_kn resolve kn =
-  gen_of_delta resolve (mind_of_kn kn) kn (mind_of_kn_equiv kn)
+  mind_of_kn_equiv kn (kn_of_delta resolve kn)
 
 let mind_of_delta resolve mind =
   let kn = user_mind mind in
@@ -188,41 +226,6 @@ let constant_of_delta_with_inline resolve con =
     try find_inline_of_delta kn1 resolve
     with Not_found -> None
 
-let string_of_hint = function
-  | Inline _ -> "inline"
-  | Equiv kn -> string_of_kn kn
-
-let debug_string_of_delta resolve =
-  let kn_to_string kn hint s =
-    s^", "^(string_of_kn kn)^"=>"^(string_of_hint hint)
-  in
-  let mp_to_string mp mp' s =
-    s^", "^(string_of_mp mp)^"=>"^(string_of_mp mp')
-  in
-  Deltamap.fold mp_to_string kn_to_string resolve ""
-
-let list_contents sub =
-  let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in
-  let mp_one_pair mp0 p l = (string_of_mp mp0, one_pair p)::l in
-  let mbi_one_pair mbi p l = (debug_string_of_mbid mbi, one_pair p)::l in
-  Umap.fold mp_one_pair mbi_one_pair sub []
-
-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 l = list_contents sub in
-  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_comma f l) ++ str "}"
-
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
   match mp with