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

4 files changed, 17 insertions, 13 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 906d9aa3c..10dc35b95 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -103,13 +103,13 @@ type constant_declaration = constant_entry * logical_kind
 let load_constant i ((sp,kn),(_,_,kind)) =
   if Nametab.exists_cci sp then
     alreadydeclared (pr_id (basename sp) ++ str " already exists");
-  let con = Global.constant_of_delta (constant_of_kn kn) in
+  let con = Global.constant_of_delta_kn kn in
   Nametab.push (Nametab.Until i) sp (ConstRef con);
   add_constant_kind con kind
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
-  let con = Global.constant_of_delta (constant_of_kn kn) in
+  let con = Global.constant_of_delta_kn kn in
     Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
 let exists_name id =
@@ -162,7 +162,7 @@ let inConstant =
 
 let declare_constant_common id dhyps (cd,kind) =
   let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in
-  let c = Global.constant_of_delta (constant_of_kn kn) in
+  let c = Global.constant_of_delta_kn kn in
   declare_constant_implicits c;
   Heads.declare_head (EvalConstRef c);
   Notation.declare_ref_arguments_scope (ConstRef c);
@@ -184,7 +184,7 @@ let declare_inductive_argument_scopes kn mie =
 
 let inductive_names sp kn mie =
   let (dp,_) = repr_path sp in
-  let kn = Global.mind_of_delta (mind_of_kn kn) in
+  let kn = Global.mind_of_delta_kn kn in
   let names, _ =
     List.fold_left
       (fun (names, n) ind ->
@@ -225,7 +225,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
 
 
 let discharge_inductive ((sp,kn),(dhyps,mie)) =
-  let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+  let mind = Global.mind_of_delta_kn kn in
   let mie = Global.lookup_mind mind in
   let repl = replacement_context () in
   let sechyps = section_segment_of_mutual_inductive mind in
@@ -261,7 +261,7 @@ let declare_mind isrecord mie =
     | ind::_ -> ind.mind_entry_typename
     | [] -> anomaly "cannot declare an empty list of inductives" in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
-  let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+  let mind = Global.mind_of_delta_kn kn in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
   !xml_declare_inductive (isrecord,oname);
diff --git a/library/declaremods.ml b/library/declaremods.ml
index d4712762a..95d2310ce 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -845,7 +845,7 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   (* Undo the simulated interactive building of the module *)
   (* and declare the module as a whole *)
   Summary.unfreeze_summaries fs;
-  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+  let mp = mp_of_kn (Lib.make_kn id) in
   let inl = if inl_expr = None then None else inl_res in (*PLTODO *)
   let mp_env,resolver = Global.add_module id entry inl in
 
diff --git a/library/global.ml b/library/global.ml
index 6548e6537..ab70bb7c3 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -119,15 +119,19 @@ let lookup_mind kn = lookup_mind kn (env())
 let lookup_module mp = lookup_module mp (env())
 let lookup_modtype kn = lookup_modtype kn (env())
 
-let constant_of_delta con = 
+let constant_of_delta_kn kn =
   let resolver,resolver_param = (delta_of_senv !global_env) in
+  (* TODO : are resolver and resolver_param orthogonal ?
+     the effect of resolver is lost if resolver_param isn't
+     trivial at that spot. *)
     Mod_subst.constant_of_delta resolver_param
-      (Mod_subst.constant_of_delta resolver con)
+      (Mod_subst.constant_of_delta_kn resolver kn)
 
-let mind_of_delta mind = 
+let mind_of_delta_kn kn =
   let resolver,resolver_param = (delta_of_senv !global_env) in
+  (* TODO idem *)
     Mod_subst.mind_of_delta resolver_param
-      (Mod_subst.mind_of_delta resolver mind)
+      (Mod_subst.mind_of_delta_kn resolver kn)
 
 let exists_label id = exists_label id !global_env
 
diff --git a/library/global.mli b/library/global.mli
index 7859c51ef..1a0fabdc8 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -85,8 +85,8 @@ val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
 val lookup_mind      : mutual_inductive -> mutual_inductive_body
 val lookup_module    : module_path -> module_body
 val lookup_modtype   : module_path -> module_type_body
-val constant_of_delta : constant -> constant
-val mind_of_delta : mutual_inductive -> mutual_inductive
+val constant_of_delta_kn : kernel_name -> constant
+val mind_of_delta_kn : kernel_name -> mutual_inductive
 val exists_label     : label -> bool
 
 (** Compiled modules *)