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

4 files changed, 102 insertions, 100 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 668f2d412e..314cc0ee0b 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
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 90b3d8c692..55d2ff15a0 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -11,64 +11,55 @@
 open Names
 open Term
 
-(** A delta_resolver maps name (constant, inductive, module_path) 
+(** {6 Delta resolver} *)
+
+(** A delta_resolver maps name (constant, inductive, module_path)
    to canonical name  *)
 type delta_resolver
 
-type substitution
-
 val empty_delta_resolver : delta_resolver
 
-val add_inline_delta_resolver :
-  constant -> int -> delta_resolver -> delta_resolver
-
-val add_inline_constr_delta_resolver :
-  constant -> int -> constr -> delta_resolver -> delta_resolver
-
-val add_constant_delta_resolver : constant -> delta_resolver -> delta_resolver
+val add_mp_delta_resolver :
+  module_path -> module_path -> delta_resolver -> delta_resolver
 
-val add_mind_delta_resolver : mutual_inductive -> delta_resolver -> delta_resolver
+val add_kn_delta_resolver :
+  kernel_name -> kernel_name -> delta_resolver -> delta_resolver
 
-val add_mp_delta_resolver : module_path -> module_path -> delta_resolver 
-  -> delta_resolver
+val add_inline_delta_resolver :
+  kernel_name -> (int * constr option) -> delta_resolver -> delta_resolver
 
 val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
 
-(** Apply the substitution on the domain of the resolver  *)
-val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver
-
-(** Apply the substitution on the codomain of the resolver  *)
-val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver
+(** Effect of a [delta_resolver] on kernel name, constant, inductive, etc *)
 
-val subst_dom_codom_delta_resolver : 
-  substitution -> delta_resolver -> delta_resolver
-
-(** *_of_delta return the associated name of arg2 in arg1   *)
+val kn_of_delta : delta_resolver -> kernel_name -> kernel_name
 val constant_of_delta_kn : delta_resolver -> kernel_name -> constant
 val constant_of_delta : delta_resolver -> constant -> constant
 
 val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive
 val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
 
-val delta_of_mp : delta_resolver -> module_path -> module_path
+val mp_of_delta : delta_resolver -> module_path -> module_path
 
 (** Extract the set of inlined constant in the resolver *)
 val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list
 
-(** mem tests *)
-val mp_in_delta : module_path -> delta_resolver -> bool
+(** Does a [delta_resolver] contains a [mp], a constant, an inductive ? *)
 
+val mp_in_delta : module_path -> delta_resolver -> bool
 val con_in_delta : constant -> delta_resolver -> bool
-
 val mind_in_delta : mutual_inductive -> delta_resolver -> bool
 
-(*substitution*)
+
+(** {6 Substitution} *)
+
+type substitution
 
 val empty_subst : substitution
 
 val is_empty_subst : substitution -> bool
 
-(** add_* add [arg2/arg1]\{arg3\} to the substitution with no 
+(** add_* add [arg2/arg1]\{arg3\} to the substitution with no
    sequential composition  *)
 val add_mbid :
   mod_bound_id -> module_path -> delta_resolver  -> substitution -> substitution
@@ -86,6 +77,18 @@ val map_mp :
 *)
 val join : substitution -> substitution -> substitution
 
+
+(** Apply the substitution on the domain of the resolver  *)
+val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver
+
+(** Apply the substitution on the codomain of the resolver  *)
+val subst_codom_delta_resolver :
+  substitution -> delta_resolver -> delta_resolver
+
+val subst_dom_codom_delta_resolver :
+  substitution -> delta_resolver -> delta_resolver
+
+
 type 'a substituted
 val from_val : 'a -> 'a substituted
 val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a
@@ -109,7 +112,7 @@ val subst_mp :
 val subst_ind :
   substitution -> mutual_inductive -> mutual_inductive
 
-val subst_kn : 
+val subst_kn :
   substitution -> kernel_name -> kernel_name
 
 val subst_con :
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 967523234e..0c2c6bd71a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -145,7 +145,7 @@ let check_modpath_equiv env mp1 mp2 =
   if mp1=mp2 then () else
     let mb1=lookup_module  mp1 env in
     let mb2=lookup_module mp2 env in
-      if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2)
+      if (mp_of_delta mb1.mod_delta mp1)=(mp_of_delta mb2.mod_delta mp2)
       then ()
       else error_not_equal_modpaths mp1 mp2
 	
@@ -382,7 +382,7 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	    | Undef _ | OpaqueDef _ -> l
 	    | Def body ->
 	      let constr = Declarations.force body in
-	      add_inline_constr_delta_resolver con lev constr l
+	      add_inline_delta_resolver kn (lev, Some constr) l
 	with Not_found ->
 	  error_no_such_label_sub (con_label con)
 	    (string_of_mp (con_modpath con))
@@ -435,16 +435,14 @@ and strengthen_and_subst_struct
 	       to resolver(mp_from.l) *)
 	  let kn_from = make_kn mp_from empty_dirpath l in
 	  let kn_to = make_kn mp_to empty_dirpath l in
-	  let old_name = constant_of_delta_kn resolver kn_from in
-	  (add_constant_delta_resolver
-	      (constant_of_kn_equiv kn_to (canonical_con old_name))
-	      resolve_out),
-	item'::rest'
-	  else
+	  let old_name = kn_of_delta resolver kn_from in
+	  (add_kn_delta_resolver kn_to old_name resolve_out),
+	  item'::rest'
+	else
 	    (*In this case the fact that the constant mp_to.l is 
 	      \Delta-equivalent to resolver(mp_from.l) is already known
 	       because resolve_out contains mp_to maps to resolver(mp_from)*)
-	    resolve_out,item'::rest'
+	  resolve_out,item'::rest'
     | (l,SFBmind mib) :: rest ->
 	(*Same as constant*)
 	let item' = l,SFBmind (subst_mind subst mib) in
@@ -454,10 +452,8 @@ and strengthen_and_subst_struct
 	if incl then
 	  let kn_from = make_kn mp_from empty_dirpath l in
 	  let kn_to = make_kn mp_to empty_dirpath l in
-	  let old_name = mind_of_delta_kn resolver kn_from in
-	  (add_mind_delta_resolver
-	     (mind_of_kn_equiv kn_to (canonical_mind old_name))
-	     resolve_out),
+	  let old_name = kn_of_delta resolver kn_from in
+	  (add_kn_delta_resolver kn_to old_name resolve_out),
 	  item'::rest'
 	else
 	  resolve_out,item'::rest'
@@ -506,7 +502,7 @@ let strengthen_and_subst_mb mb mp include_b =
 	  let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
 	    (*if mb.mod_mp is an alias then the strengthening is useless 
 	      (i.e. it is already done)*)
-	  let mp_alias = delta_of_mp mb.mod_delta mb.mod_mp in
+	  let mp_alias = mp_of_delta mb.mod_delta mb.mod_mp in
 	  let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in
 	  let new_resolver = 
 	    add_mp_delta_resolver mp mp_alias
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c620d8dd26..c2d71ebb27 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -271,7 +271,7 @@ let add_constant dir l decl senv =
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
-      update_resolver (add_inline_delta_resolver kn lev) senv'
+      update_resolver (add_inline_delta_resolver (user_con kn) (lev,None)) senv'
     | _ -> senv'
   in
   kn, senv''