A fine-grain control of inlining at functor application via priority levels

  As said in CHANGES:

<<
  The inlining done during application of functors can now be controlled
  more precisely. In addition to the "!F G" syntax preventing any inlining,
  we can now use a priority level to select parameters to inline :
  "<30>F G" means "only inline in F the parameters whose levels are <= 30".
  The level of a parameter can be fixed by "Parameter Inline(30) foo".
  When levels aren't given, the default value is 100. One can also use
  the flag "Set Inline Level ..." to set a level.
>>

  Nota : the syntax "Parameter Inline(30) foo" is equivalent to
  "Set Inline Level 30. Parameter Inline foo.",
  and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G."

  For instance, in ZBinary, eq is @Logic.eq and should rather be inlined,
  while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined.
  We could achieve this behavior by setting a level such as 30 to the
  parameter eq, and then tweaking the current level when applying functors.

  This idea of levels might be too restrictive, we'll see, but at least
  the implementation of this change was quite simple. There might be
  situation where parameters cannot be linearly ordered according to their
  "inlinablility". For these cases, we would need to mention names to inline
  or not at a functor application, and this is a bit more tricky
  (and might be a pain to use if there are many names).

  No documentation for the moment, since this feature is experimental
  and might still evolve.

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

1 files changed, 14 insertions, 13 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 407ae73ca..13ac21437 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -294,11 +294,11 @@ and translate_struct_module_entry env mp inl mse  = match mse with
 	      (* place for nondep_supertype *) in
       let cst = check_subtypes env mtb farg_b in
       let mp_delta = discr_resolver env mtb in
-      let mp_delta = if not inl then mp_delta else
-	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta
       in
-      let subst = map_mbid farg_id mp1 mp_delta in
-	(subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst),
+      let subst = map_mbid farg_id mp1 mp_delta
+      in
+      (subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst),
       (subst_codom_delta_resolver subst resolver),
       Univ.union_constraints cst1 cst
   | MSEwith(mte, with_decl) ->
@@ -333,12 +333,13 @@ and translate_struct_type_entry env inl mse = match mse with
 	      (* place for nondep_supertype *) in
       let cst2 = check_subtypes env mtb farg_b in
       let mp_delta = discr_resolver env mtb in
-      let mp_delta = if not inl then mp_delta else
-	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta
+      in
+      let subst = map_mbid farg_id mp1 mp_delta
       in
-      let subst = map_mbid farg_id mp1 mp_delta in
-	(subst_struct_expr subst fbody_b),None,
-      (subst_codom_delta_resolver subst resolve),mp_from,Univ.union_constraints cst1 cst2
+      (subst_struct_expr subst fbody_b),None,
+      (subst_codom_delta_resolver subst resolve),mp_from,
+      Univ.union_constraints cst1 cst2
   | MSEwith(mte, with_decl) ->
       let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in
       let sign,alg,resolve,cst1 = 
@@ -375,11 +376,11 @@ let rec translate_struct_include_module_entry env mp inl mse  = match mse with
 	      (* place for nondep_supertype *) in
       let cst = check_subtypes env mtb farg_b in
       let mp_delta =  discr_resolver env mtb in
-      let mp_delta = if not inl then mp_delta else
-	complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta
+      let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta
+      in
+      let subst = map_mbid farg_id mp1 mp_delta
       in
-      let subst = map_mbid farg_id mp1 mp_delta in
-	(subst_struct_expr subst fbody_b),
+      (subst_struct_expr subst fbody_b),
       (subst_codom_delta_resolver subst resolver),
       Univ.union_constraints cst1 cst
   | _ -> error ("You cannot Include a high-order structure.")