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

5 files changed, 20 insertions, 8 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index f11bdb4a8e..9b6c74398a 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -179,7 +179,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	in
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
-	  (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
+	  (Entries.ParameterEntry (termtype,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in instance_hook k None false imps ?hook (ConstRef cst); id
       end
     else
@@ -286,7 +286,7 @@ let context ?(hook=fun _ -> ()) l =
   let fn (id, _, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
       let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
-	(ParameterEntry (t,false), IsAssumption Logical)
+	(ParameterEntry (t,None), IsAssumption Logical)
       in
 	match class_of_constr t with
 	| Some tc ->
@@ -299,7 +299,7 @@ let context ?(hook=fun _ -> ()) l =
 	   match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
       in
 	Command.declare_assumption false (Local (* global *), Definitional) t
-	  [] impl (* implicit *) false (* inline *) (dummy_loc, id);
+	  [] impl (* implicit *) None (* inline *) (dummy_loc, id);
 	match class_of_constr t with
 	| None -> ()
 	| Some tc -> hook (VarRef id))
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 163f68fd05..b12479b457 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -44,11 +44,11 @@ val interp_assumption :
 
 val declare_assumption : coercion_flag -> assumption_kind -> types ->
   manual_implicits ->
-  bool (** implicit *) -> bool (* inline *) -> variable located -> unit
+  bool (** implicit *) -> inline -> variable located -> unit
 
 val declare_assumptions : variable located list ->
   coercion_flag -> assumption_kind -> types -> manual_implicits ->
-  bool -> bool -> unit
+  bool -> inline -> unit
 
 (** {6 Inductive and coinductive types} *)
 
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 847278b07a..c0ce16ceae 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -199,7 +199,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
           (Local,VarRef id,imps)
       | Global ->
           let k = IsAssumption Conjectural in
-          let kn = declare_constant id (ParameterEntry (t_i,false), k) in
+          let kn = declare_constant id (ParameterEntry (t_i,None), k) in
           (Global,ConstRef kn,imps))
   | Some body ->
       let k = logical_kind_of_goal_kind kind in
@@ -330,7 +330,7 @@ let start_proof_com kind thms hook =
 let admit () =
   let (id,k,typ,hook) = Pfedit.current_proof_statement () in
   let kn =
-    declare_constant id (ParameterEntry (typ,false),IsAssumption Conjectural) in
+    declare_constant id (ParameterEntry (typ,None),IsAssumption Conjectural) in
   Pfedit.delete_current_proof ();
   assumption_message id;
   hook Global (ConstRef kn)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a18340e904..f4fc8714be 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -941,6 +941,16 @@ let _ =
       optwrite = (fun b -> Vconv.set_use_vm b) }
 
 let _ =
+  declare_int_option
+    { optsync  = true;
+      optname  = "level of inling duging functor application";
+      optkey   = ["Inline";"Level"];
+      optread  = (fun () -> Some (Flags.get_inline_level ()));
+      optwrite = (fun o ->
+	           let lev = Option.default Flags.default_inline_level o in
+	           Flags.set_inline_level lev) }
+
+let _ =
   declare_bool_option
     { optsync  = true;
       optname  = "use of boxed values";
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 80191b8fda..3091f10c53 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -196,6 +196,8 @@ type scheme =
   | CaseScheme of bool * reference or_by_notation * sort_expr
   | EqualityScheme of reference or_by_notation
 
+type inline = int option (* inlining level, none for no inlining *)
+
 type vernac_expr =
   (* Control *)
   | VernacList of located_vernac_expr list
@@ -226,7 +228,7 @@ type vernac_expr =
         bool * declaration_hook
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
-  | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list
+  | VernacAssumption of assumption_kind * inline * simple_binder with_coercion list
   | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list