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, 36 insertions, 33 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 452c2e69a..9e8ce3fe5 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -18,9 +18,11 @@ open Util
 open Names
 open Term
 
+(* For Inline, the int is an inlining level, and the constr (if present)
+   is the term into which we should inline *)
 
 type delta_hint =
-    Inline of constr option
+    Inline of int * constr option
   | Equiv of kernel_name
   | Prefix_equiv of module_path
 
@@ -63,11 +65,11 @@ let add_mp mp1 mp2 resolve =
 let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst
 let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst
 
-let add_inline_delta_resolver con =
-  Deltamap.add (KN(user_con con)) (Inline None)
-    
-let add_inline_constr_delta_resolver con cstr =
-  Deltamap.add (KN(user_con con)) (Inline (Some cstr))
+let add_inline_delta_resolver con lev =
+  Deltamap.add (KN(user_con con)) (Inline (lev,None))
+
+let add_inline_constr_delta_resolver con lev cstr =
+  Deltamap.add (KN(user_con con)) (Inline (lev, Some cstr))
 
 let add_constant_delta_resolver con =
   Deltamap.add (KN(user_con con)) (Equiv (canonical_con con))
@@ -131,15 +133,15 @@ let rec find_prefix resolve mp =
     with
 	Not_found -> mp
 
-exception Change_equiv_to_inline of constr
+exception Change_equiv_to_inline of (int * constr)
 
 let solve_delta_kn resolve kn =
   try 
       match Deltamap.find (KN kn) resolve with
 	| Equiv kn1 -> kn1
-	| Inline (Some c) -> 
-	    raise (Change_equiv_to_inline c)
-	| Inline None -> raise Inline_kn
+	| Inline (lev, Some c) ->
+	    raise (Change_equiv_to_inline (lev,c))
+	| Inline (_, None) -> raise Inline_kn
 	| _ -> anomaly 
 	    "mod_subst: bad association in delta_resolver"
   with
@@ -199,13 +201,16 @@ let mind_of_delta2 resolve mind =
 	_ -> mind
 	  
 
-let inline_of_delta resolver = 
-  let extract key hint l =
-    match key,hint with 
-      |KN kn, Inline _ -> kn::l
-      | _,_ -> l
-  in
-    Deltamap.fold extract resolver []
+let inline_of_delta inline resolver =
+  match inline with
+    | None -> []
+    | Some inl_lev ->
+      let extract key hint l =
+	match key,hint with
+	  |KN kn, Inline (lev,_) -> if lev <= inl_lev then (lev,kn)::l else l
+	  | _,_ -> l
+      in
+      Deltamap.fold extract resolver []
 
 exception Not_inline
   
@@ -213,14 +218,12 @@ let constant_of_delta_with_inline resolve con =
   let kn1,kn2 = canonical_con con,user_con con in
     try
       match Deltamap.find (KN kn2) resolve with 
-	| Inline None -> None
-	| Inline (Some const) -> Some const
+	| Inline (_,o) -> o
 	| _ -> raise Not_inline
     with
 	Not_found | Not_inline -> 
 	  try match Deltamap.find (KN kn1) resolve with 
-	    | Inline None -> None
-	    | Inline (Some const) -> Some const
+	    | Inline (_,o) -> o
 	    | _ -> raise Not_inline
 	  with
 	      Not_found | Not_inline -> None
@@ -575,12 +578,12 @@ let subst_codom_delta_resolver subst resolver =
 	  (try
 	     Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
 	   with
-	       Change_equiv_to_inline c ->
-		 Deltamap.add key (Inline (Some c)) resolver)
-      | Inline None ->
+	       Change_equiv_to_inline (lev,c) ->
+		 Deltamap.add key (Inline (lev,Some c)) resolver)
+      | Inline (_,None) ->
 	  Deltamap.add key hint resolver
-      | Inline (Some t) ->
-	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
+      | Inline (lev,Some t) ->
+	  Deltamap.add key (Inline (lev,Some (subst_mps subst t))) resolver
   in
     Deltamap.fold apply_subst resolver empty_delta_resolver
 
@@ -597,14 +600,14 @@ let subst_dom_codom_delta_resolver subst resolver =
 	    (try
 	       Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
 	     with
-		 Change_equiv_to_inline c ->
-		   Deltamap.add key (Inline (Some c)) resolver)
-      | (KN kn),Inline None ->
+		 Change_equiv_to_inline (lev,c) ->
+		   Deltamap.add key (Inline (lev,Some c)) resolver)
+      | (KN kn),Inline (_,None) ->
 	  let key = KN (subst_kn subst kn) in
 	    Deltamap.add key hint resolver
-      | (KN kn),Inline (Some t) ->
+      | (KN kn),Inline (lev,Some t) ->
 	  let key = KN (subst_kn subst kn) in
-	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
+	  Deltamap.add key (Inline (lev,Some (subst_mps subst t))) resolver
       | _,_ -> anomaly "Mod_subst: Bad association in resolver" 
   in
     Deltamap.fold apply_subst resolver empty_delta_resolver
@@ -625,8 +628,8 @@ let update_delta_resolver resolver1 resolver2 =
 		   Equiv (solve_delta_kn resolver2 kn)
 		 in Deltamap.add key new_hint res
 	       with
-		   Change_equiv_to_inline c ->
-		     Deltamap.add key (Inline (Some c)) res)
+		   Change_equiv_to_inline (lev,c) ->
+		     Deltamap.add key (Inline (lev,Some c)) res)
 	  | _ -> Deltamap.add key hint res
       with Not_found ->
 	Deltamap.add key hint res