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, 15 insertions, 17 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 58b0d6a46..b6b3a766f 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -78,7 +78,7 @@ let modtab_objects =
 let openmod_info =
   ref ((MPfile(initial_dir),[],None,[])
 	 : module_path *  mod_bound_id list *
-           (module_struct_entry * bool) option * module_type_body list)
+           (module_struct_entry * inline) option * module_type_body list)
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
@@ -425,24 +425,20 @@ let rec get_objs_modtype_application env = function
     Modops.error_application_to_not_path mexpr
 | _ -> error "Application of a non-functor."
 
-let rec compute_subst env mbids sign mp_l inline =
+let rec compute_subst env mbids sign mp_l inl =
   match mbids,mp_l with
     | _,[] -> mbids,empty_subst
     | [],r -> error "Application of a functor with too few arguments."
     | mbid::mbids,mp::mp_l ->
 	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
 	let mb = Environ.lookup_module mp env in
-	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inline in
-	match discr_resolver mb with
-	  | None ->
-	      mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst
+	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in
+	let resolver = match discr_resolver mb with
+	  | None -> empty_delta_resolver
 	  | Some mp_delta ->
-	      let mp_delta =
-		if not inline then mp_delta else
-		  Modops.complete_inline_delta_resolver env mp
-		    farg_id farg_b mp_delta
-	      in
-	      mbid_left,join (map_mbid mbid mp mp_delta) subst
+	      Modops.inline_delta_resolver env inl mp farg_id farg_b mp_delta
+	in
+	mbid_left,join (map_mbid mbid mp resolver) subst
 
 let rec get_modtype_substobjs env mp_from inline = function
     MSEident ln -> 
@@ -748,15 +744,16 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
 
   let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
   let env = Global.env() in
+  let default_inl = Some (Flags.get_inline_level ()) in (* PLTODO *)
   let mty_entry_o, subs, inl_res = match res with
     | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl
     | Topconstr.Check mtys ->
-	None, build_subtypes interp_modtype mmp arg_entries mtys, true
+	None, build_subtypes interp_modtype mmp arg_entries mtys, default_inl
   in
  
   (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
   let mexpr_entry_o, inl_expr = match mexpr_o with
-    | None -> None, true
+    | None -> None, default_inl
     | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl
   in
   let entry =
@@ -775,7 +772,8 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   (* 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_env,resolver = Global.add_module id entry (inl_expr&&inl_res) 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
 
   if mp_env <> mp then anomaly "Kernel and Library names do not match";
 
@@ -853,8 +851,8 @@ let rec include_subst env mb mbids sign inline =
     | mbid::mbids ->
 	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
 	let subst = include_subst env mb mbids fbody_b inline in
-	let mp_delta = if not inline then mb.mod_delta else
-	  Modops.complete_inline_delta_resolver env mb.mod_mp
+	let mp_delta =
+	  Modops.inline_delta_resolver env inline mb.mod_mp
 	    farg_id farg_b mb.mod_delta
 	in
 	join (map_mbid mbid mb.mod_mp mp_delta) subst