Various simplifications about constant_of_delta and mind_of_delta

 Most of the time, a constant name is built from:
  - a kernel_name for its user part
  - a delta_resolver applied to this kernel_name for its canonical part
 With this patch we avoid building unnecessary constants for immediately
 amending them (cf in particular the awkward code removed in safe_typing).

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

5 files changed, 38 insertions, 41 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index bf08841c83..275c6e6775 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -147,6 +147,9 @@ let gen_of_delta resolve x kn fix_can =
     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,6 +158,9 @@ let constant_of_delta2 resolve con =
   let kn, kn' = canonical_con con, user_con con in
   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)
+
 let mind_of_delta resolve mind =
   let kn = user_mind mind in
   gen_of_delta resolve mind kn (mind_of_kn_equiv kn)
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index dd240d7f31..e06cc816da 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -44,8 +44,10 @@ val subst_dom_codom_delta_resolver :
   substitution -> delta_resolver -> delta_resolver
 
 (** *_of_delta return the associated name of arg2 in arg1   *)
+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
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 84d8ca67ab..967523234e 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -264,18 +264,13 @@ let add_retroknowledge mp =
 let rec add_signature mp sign resolver env = 
   let add_one env (l,elem) =
     let kn = make_kn mp empty_dirpath l in
-    let con = constant_of_kn kn in
-    let mind = mind_of_kn kn in
-      match elem with
-	| SFBconst cb -> 
-	    let con =  constant_of_delta resolver con in
-	      Environ.add_constant con cb env
-	| SFBmind mib -> 
-	    let mind =  mind_of_delta resolver mind in
-	    Environ.add_mind mind mib env
-	| SFBmodule mb -> add_module mb env
-	      (* adds components as well *)
-	| SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
+    match elem with
+      | SFBconst cb ->
+	Environ.add_constant (constant_of_delta_kn resolver kn) cb env
+      | SFBmind mib ->
+	Environ.add_mind (mind_of_delta_kn resolver kn) mib env
+      | SFBmodule mb -> add_module mb env (* adds components as well *)
+      | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
   in
     List.fold_left add_one env sign
 
@@ -293,8 +288,8 @@ let strengthen_const mp_from l cb resolver =
   match cb.const_body with
     | Def _ -> cb
     | _ ->
-      let con = make_con mp_from empty_dirpath l in
-      let con = constant_of_delta resolver con in
+      let kn = make_kn mp_from empty_dirpath l in
+      let con = constant_of_delta_kn resolver kn in
       { cb with
 	const_body = Def (Declarations.from_val (mkConst con));
 	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con)
@@ -379,10 +374,9 @@ let inline_delta_resolver env inl mp mbid mtb delta =
     | [] -> delta
     | (lev,kn)::r ->
 	let kn = replace_mp_in_kn (MPbound mbid) mp kn in
-	let con = constant_of_kn kn in
-	let con' = constant_of_delta delta con in
+	let con = constant_of_delta_kn delta kn in
 	try
-	  let constant = lookup_constant con' env in
+	  let constant = lookup_constant con env in
 	  let l = make_inline delta r in
 	  match constant.const_body with
 	    | Undef _ | OpaqueDef _ -> l
@@ -432,17 +426,18 @@ and strengthen_and_subst_struct
 	  l,SFBconst (strengthen_const mp_from l
 			(subst_const_body subst cb) resolver)
 	in
-	let con = make_con mp_from empty_dirpath l in
 	let resolve_out,rest' =
 	  strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
-	  if incl then
+	if incl then
 	    (* If we are performing an inclusion we need to add
 	       the fact that the constant mp_to.l is \Delta-equivalent
 	       to resolver(mp_from.l) *)
-	    let old_name = constant_of_delta resolver con in
-	    (add_constant_delta_resolver
-	      (constant_of_kn_equiv (make_kn mp_to empty_dirpath l) (canonical_con old_name)) 
+	  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
@@ -453,17 +448,19 @@ and strengthen_and_subst_struct
     | (l,SFBmind mib) :: rest ->
 	(*Same as constant*)
 	let item' = l,SFBmind (subst_mind subst mib) in
-	let mind = make_mind mp_from empty_dirpath l in
 	let resolve_out,rest' =
 	  strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
-	  if incl then
-	    let old_name =  mind_of_delta resolver mind in 
-	    (add_mind_delta_resolver
-	      (mind_of_kn_equiv (make_kn mp_to empty_dirpath l) (canonical_mind old_name)) resolve_out),
-	item'::rest'
-	  else
-	    resolve_out,item'::rest'
+	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),
+	  item'::rest'
+	else
+	  resolve_out,item'::rest'
     | (l,SFBmodule mb) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
 	let mp_to' = MPdot(mp_to,l) in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e5b8412ec0..3c4c50a4ae 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -475,18 +475,10 @@ let end_module l restype senv =
      let new_name = match elem with
        | SFBconst _ ->
 	   let kn = make_kn mp_sup empty_dirpath l in
-	   let con = constant_of_kn_equiv kn
-	     (canonical_con
-		(constant_of_delta resolver (constant_of_kn kn)))
-	   in
-	   C con
+	   C (constant_of_delta_kn resolver kn)
        | SFBmind _ ->
 	   let kn = make_kn mp_sup empty_dirpath l in
-	   let mind = mind_of_kn_equiv kn
-	     (canonical_mind
-		(mind_of_delta resolver (mind_of_kn kn)))
-	   in
-	   I mind
+	   I (mind_of_delta_kn resolver kn)
        | SFBmodule _ -> M
        | SFBmodtype _ -> MT (MPdot(senv.modinfo.modpath, l))
      in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 00af99d980..c141a02aa3 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -163,7 +163,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   (* the inductive types and constructors types have to be convertible *)
   check (fun mib -> mib.mind_nparams) (fun x -> InductiveParamsNumberField x);
 
-  begin  
+  begin
   match mind_of_delta reso2 kn2  with
       | kn2' when kn2=kn2' -> ()
       | kn2' ->