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

16 files changed, 107 insertions, 99 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index d01398841..87474b863 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -137,4 +137,4 @@ let cook_constant env r =
 	let j = make_judge (force (Option.get body)) typ in
 	Typeops.make_polymorphic_if_constant_for_ind env j
   in
-  (body, typ, cb.const_constraints, cb.const_opaque, false)
+  (body, typ, cb.const_constraints, cb.const_opaque, None)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 09b42d0b1..4b8b4537c 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -23,7 +23,7 @@ type recipe = {
 
 val cook_constant :
   env -> recipe ->
-    constr_substituted option * constant_type * constraints * bool * bool
+    constr_substituted option * constant_type * constraints * bool * inline
 
 
 (** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 4308f9c1a..282dad0da 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -49,6 +49,8 @@ let force = force subst_mps
 
 let subst_constr_subst = subst_substituted
 
+type inline = int option (* inlining level, None for no inlining *)
+
 type constant_body = {
     const_hyps : section_context; (* New: younger hyp at top *)
     const_body : constr_substituted option;
@@ -57,7 +59,7 @@ type constant_body = {
    (* const_type_code : Cemitcodes.to_patch; *)
     const_constraints : constraints;
     const_opaque : bool;
-    const_inline : bool}
+    const_inline : inline }
 
 (*s Inductive types (internal representation with redundant
     information). *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index a92cb2cb4..d4c86fb35 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -35,6 +35,8 @@ type constr_substituted
 val from_val : constr -> constr_substituted
 val force : constr_substituted -> constr
 
+type inline = int option (* inlining level, None for no inlining *)
+
 type constant_body = {
     const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constr_substituted option;
@@ -43,7 +45,7 @@ type constant_body = {
    (* const_type_code : to_patch;*)
     const_constraints : constraints;
     const_opaque : bool;
-    const_inline : bool}
+    const_inline : inline }
 
 val subst_const_body : substitution -> constant_body -> constant_body
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index dbf802bb1..28f11c9af 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -59,8 +59,9 @@ type definition_entry = {
   const_entry_type   : types option;
   const_entry_opaque : bool }
 
-(* type and the inlining flag *)
-type parameter_entry = types * bool
+type inline = int option (* inlining level, None for no inlining *)
+
+type parameter_entry = types * inline
 
 type constant_entry =
   | DefinitionEntry of definition_entry
diff --git a/kernel/entries.mli b/kernel/entries.mli
index d45e2bbdb..08740afae 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -55,7 +55,9 @@ type definition_entry = {
   const_entry_type   : types option;
   const_entry_opaque : bool }
 
-type parameter_entry = types * bool  (*inline flag*)
+type inline = int option (* inlining level, None for no inlining *)
+
+type parameter_entry = types * inline
 
 type constant_entry =
   | DefinitionEntry of definition_entry
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
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 7164d1162..91139985b 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -19,10 +19,11 @@ type substitution
 
 val empty_delta_resolver : delta_resolver
 
-val add_inline_delta_resolver : constant -> delta_resolver -> delta_resolver
+val add_inline_delta_resolver :
+  constant -> int -> delta_resolver -> delta_resolver
 
-val add_inline_constr_delta_resolver :  constant -> constr -> delta_resolver 
-  -> delta_resolver
+val add_inline_constr_delta_resolver :
+  constant -> int -> constr -> delta_resolver -> delta_resolver
 
 val add_constant_delta_resolver : constant -> delta_resolver -> delta_resolver
 
@@ -50,7 +51,7 @@ val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
 val delta_of_mp : delta_resolver -> module_path -> module_path
 
 (** Extract the set of inlined constant in the resolver *)
-val inline_of_delta : delta_resolver -> kernel_name list
+val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list
 
 (** remove_mp is used for the computation of a resolver induced by Include P *)
 val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver
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.")
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index f14d63be9..81974edfa 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -13,20 +13,20 @@ open Mod_subst
 open Names
 
 
-val translate_module : env -> module_path -> bool -> module_entry
+val translate_module : env -> module_path -> inline -> module_entry
   -> module_body
 
-val translate_module_type : env -> module_path -> bool -> module_struct_entry ->
+val translate_module_type : env -> module_path -> inline -> module_struct_entry ->
   module_type_body
 
-val translate_struct_module_entry : env -> module_path -> bool -> module_struct_entry ->
+val translate_struct_module_entry : env -> module_path -> inline -> module_struct_entry ->
   struct_expr_body * struct_expr_body * delta_resolver * Univ.constraints
 
-val translate_struct_type_entry : env -> bool -> module_struct_entry ->
+val translate_struct_type_entry : env -> inline -> module_struct_entry ->
   struct_expr_body * struct_expr_body option * delta_resolver * module_path * Univ.constraints
 
-val translate_struct_include_module_entry : env -> module_path 
-  -> bool -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
+val translate_struct_include_module_entry : env -> module_path -> inline ->
+  module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
 
 val add_modtype_constraints : env -> module_type_body -> env
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index ce968b40e..2bcfada96 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 =
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 9c00b8194..f34fa88c4 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -39,8 +39,8 @@ val check_modpath_equiv : env -> module_path -> module_path -> unit
 
 val strengthen : env -> module_type_body -> module_path -> module_type_body
 
-val complete_inline_delta_resolver :
-  env -> module_path -> mod_bound_id -> module_type_body ->
+val inline_delta_resolver :
+  env -> inline -> module_path -> mod_bound_id -> module_type_body ->
   delta_resolver -> delta_resolver
 
 val strengthen_and_subst_mb : module_body -> module_path -> env -> bool 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2bed2bb48..41ec0c6a6 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -262,11 +262,9 @@ let add_constant dir l decl senv =
   in
   let senv' = add_constraints cb.const_constraints senv in
   let env'' = Environ.add_constant kn cb senv'.env in
-  let resolver = 
-    if cb.const_inline then
-      add_inline_delta_resolver kn senv'.modinfo.resolver
-    else
-      senv'.modinfo.resolver
+  let resolver = match cb.const_inline with
+    | None -> senv'.modinfo.resolver
+    | Some lev -> add_inline_delta_resolver kn lev senv'.modinfo.resolver
   in
     kn, { old = senv'.old;
 	  env = env'';
@@ -492,8 +490,9 @@ let end_module l restype senv =
      | SEBfunctor(mbid,mtb,str) ->
 	 let cst_sub = check_subtypes senv.env mb mtb in
 	 let senv = add_constraints cst_sub senv in
-	 let mpsup_delta = if not inl then mb.typ_delta else
-	   complete_inline_delta_resolver senv.env mp_sup mbid mtb mb.typ_delta in
+	 let mpsup_delta =
+	   inline_delta_resolver senv.env inl mp_sup mbid mtb mb.typ_delta
+	 in
 	 let subst = map_mbid mbid mp_sup mpsup_delta in
 	 let resolver = subst_codom_delta_resolver subst resolver in
 	   (compute_sign 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 406727664..0ab70b69e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -53,12 +53,12 @@ val add_mind :
 
 (** Adding a module *)
 val add_module :
-  label -> module_entry -> bool -> safe_environment
+  label -> module_entry -> inline -> safe_environment
     -> module_path * delta_resolver * safe_environment
 
 (** Adding a module type *)
 val add_modtype :
-  label -> module_struct_entry -> bool -> safe_environment
+  label -> module_struct_entry -> inline -> safe_environment
     -> module_path * safe_environment
 
 (** Adding universe constraints *)
@@ -75,11 +75,11 @@ val start_module :
   label -> safe_environment -> module_path * safe_environment
 
 val end_module :
-  label -> (module_struct_entry * bool) option
+  label -> (module_struct_entry * inline) option
       -> safe_environment -> module_path * delta_resolver * safe_environment 
 
 val add_module_parameter :
-  mod_bound_id -> module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment
+  mod_bound_id -> module_struct_entry -> inline -> safe_environment -> delta_resolver * safe_environment
 
 val start_modtype :
   label -> safe_environment -> module_path * safe_environment
@@ -88,7 +88,7 @@ val end_modtype :
   label -> safe_environment -> module_path * safe_environment
 
 val add_include :
-  module_struct_entry -> bool -> bool -> safe_environment ->
+  module_struct_entry -> bool -> inline -> safe_environment ->
    delta_resolver * safe_environment
 
 val pack_module : safe_environment -> module_body
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 432460d7d..801bd6c80 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -94,7 +94,7 @@ let infer_declaration env dcl =
       let (j,cst) = infer env c.const_entry_body in
       let (typ,cst) = constrain_type env j cst c.const_entry_type in
       Some (Declarations.from_val j.uj_val), typ, cst,
-        c.const_entry_opaque, false
+        c.const_entry_opaque, None
   | ParameterEntry (t,nl) ->
       let (j,cst) = infer env t in
       None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 500858a59..8b48fc3cf 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,10 +22,10 @@ val translate_local_assum : env -> types ->
   types * Univ.constraints
 
 val infer_declaration : env -> constant_entry ->
-   constr_substituted option * constant_type * constraints * bool * bool
+   constr_substituted option * constant_type * constraints * bool * inline
 
 val build_constant_declaration : env -> 'a ->
-    constr_substituted option * constant_type * constraints * bool * bool ->
+    constr_substituted option * constant_type * constraints * bool * inline ->
       constant_body
 
 val translate_constant : env -> constant -> constant_entry -> constant_body