diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-31 16:27:54 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-31 16:27:54 +0000 |
commit | fa9175c646ac804af0f446eeb981b2143d310537 (patch) | |
tree | 6114b08fd00e47b0b7627bed0cb6fa5221e4ef77 /library/declaremods.mli | |
parent | f19a9d9d3a410fda982b2cf9154da5774f9ec84f (diff) |
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
Diffstat (limited to 'library/declaremods.mli')
-rw-r--r-- | library/declaremods.mli | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index 83c6b2bb6..b1978c282 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -37,13 +37,13 @@ val declare_module : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> identifier -> - (identifier located list * ('modast * bool)) list -> - ('modast * bool) Topconstr.module_signature -> - ('modast * bool) list -> module_path + (identifier located list * ('modast * inline)) list -> + ('modast * inline) Topconstr.module_signature -> + ('modast * inline) list -> module_path val start_module : (env -> 'modast -> module_struct_entry) -> - bool option -> identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) Topconstr.module_signature -> module_path + bool option -> identifier -> (identifier located list * ('modast * inline)) list -> + ('modast * inline) Topconstr.module_signature -> module_path val end_module : unit -> module_path @@ -53,12 +53,12 @@ val end_module : unit -> module_path val declare_modtype : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> - identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) list -> ('modast * bool) list -> module_path + identifier -> (identifier located list * ('modast * inline)) list -> + ('modast * inline) list -> ('modast * inline) list -> module_path val start_modtype : (env -> 'modast -> module_struct_entry) -> - identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) list -> module_path + identifier -> (identifier located list * ('modast * inline)) list -> + ('modast * inline) list -> module_path val end_modtype : unit -> module_path @@ -103,7 +103,7 @@ val import_module : bool -> module_path -> unit (** Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> - ('struct_expr * bool) list -> unit + ('struct_expr * inline) list -> unit (** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' @@ -120,5 +120,5 @@ val debug_print_modtab : unit -> Pp.std_ppcmds (** For translator *) val process_module_bindings : module_ident list -> - (mod_bound_id * (module_struct_entry * bool)) list -> unit + (mod_bound_id * (module_struct_entry * inline)) list -> unit |