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, 16 insertions, 19 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index ce968b40ef..2bcfada964 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -364,31 +364,28 @@ let module_type_of_module env mp mb =
 	 typ_constraints = mb.mod_constraints;
 	 typ_delta = mb.mod_delta}
 
-let complete_inline_delta_resolver env mp mbid mtb delta =
-  let constants = inline_of_delta mtb.typ_delta in
+let inline_delta_resolver env inl mp mbid mtb delta =
+  let constants = inline_of_delta inl mtb.typ_delta in
   let rec make_inline delta = function
     | [] -> delta
-    | kn::r -> 
+    | (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
-	  try
-	    let constant = lookup_constant con' env in
-	      if (not constant.Declarations.const_opaque) then
-		let constr = Option.map Declarations.force 
-		  constant.Declarations.const_body in
-		  if constr = None then 
-		    (make_inline delta r)
-		  else
-		    add_inline_constr_delta_resolver con (Option.get constr)
-		      (make_inline delta r)
-	      else
-		(make_inline delta r)
-	  with 
-	      Not_found -> error_no_such_label_sub (con_label con) 
-		(string_of_mp (con_modpath con))
+	try
+	  let constant = lookup_constant con' env in
+	  let l = make_inline delta r in
+	  if constant.Declarations.const_opaque then l
+	  else match constant.Declarations.const_body with
+	    | None -> l
+	    | Some body ->
+	      let constr = Declarations.force body in
+	      add_inline_constr_delta_resolver con lev constr l
+	with Not_found ->
+	  error_no_such_label_sub (con_label con)
+	    (string_of_mp (con_modpath con))
   in
-    make_inline delta constants
+  make_inline delta constants
 
 let rec strengthen_and_subst_mod
     mb subst env mp_from mp_to env resolver =