diff options
| -rw-r--r-- | doc/refman/Extraction.tex | 56 | ||||
| -rw-r--r-- | plugins/extraction/mlutil.ml | 4 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 13 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 4 |
4 files changed, 54 insertions, 23 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 1ec25f9f1..53ef490ff 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -95,23 +95,25 @@ of the extraction options. Default is Ocaml. \asubsection{Inlining and optimizations} -Since Objective Caml is a strict language, the extracted -code has to be optimized in order to be efficient (for instance, when -using induction principles we do not want to compute all the recursive -calls but only the needed ones). So the extraction mechanism provides -an automatic optimization routine that will be -called each time the user want to generate Ocaml programs. Essentially, -it performs constants inlining and reductions. Therefore some -constants may not appear in resulting monolithic Ocaml program. -In the case of modular extraction, even if some inlining is done, the -inlined constant are nevertheless printed, to ensure -session-independent programs. - -Concerning Haskell, such optimizations are less useful because of -lazyness. We still make some optimizations, for example in order to -produce more readable code. - -All these optimizations are controled by the following \Coq\ options: +Since Objective Caml is a strict language, the extracted code has to +be optimized in order to be efficient (for instance, when using +induction principles we do not want to compute all the recursive calls +but only the needed ones). So the extraction mechanism provides an +automatic optimization routine that will be called each time the user +want to generate Ocaml programs. The optimizations can be split in two +groups: the type preserving ones -- essentially constant inlining and +reductions -- and the non type perserving ones -- some function +abstractions of dummy types are removed when it's deemed safe in order +to have more elegant types. Therefore some constants may not appear in +resulting monolithic Ocaml program. In the case of modular extraction, +even if some inlining is done, the inlined constant are nevertheless +printed, to ensure session-independent programs. + +Concerning Haskell, type preserving optimizations are less useful +because of lazyness. We still make some optimizations, for example in +order to produce more readable code. + +The type preserving optimizations are controled by the following \Coq\ options: \begin{description} @@ -121,10 +123,22 @@ All these optimizations are controled by the following \Coq\ options: \item \comindex{Unset Extraction Optimize} {\tt Unset Extraction Optimize.} -Default is Set. This control all optimizations made on the ML terms -(mostly reduction of dummy beta/iota redexes, but also simplifications on -Cases, etc). Put this option to Unset if you want a ML term as close as -possible to the Coq term. +Default is Set. This control all type preserving optimizations made on +the ML terms (mostly reduction of dummy beta/iota redexes, but also +simplifications on Cases, etc). Put this option to Unset if you want a +ML term as close as possible to the Coq term. + +\item \comindex{Set Extraction Conservative Types} +{\tt Set Extraction Conservative Types.} + +\item \comindex{Unset Extraction Conservative Types} +{\tt Unset Extraction Conservative Types.} + +Default is Unset. This control the non type preserving optimizations +made on ML terms (which try to avoid function abstraction of dummy +types). If you turn this option to Set to make sure that {\tt e:t} +implies that {\tt e':t'} where {\tt e'} and {\tt t'} are the extracted +code of {\tt e} and {\tt t} respectively. \item \comindex{Set Extraction KeepSingleton} {\tt Set Extraction KeepSingleton.} diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 2b6122cd3..321af2946 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -285,13 +285,13 @@ let type_simpl = type_expand (fun _ -> None) (*s Generating a signature from a ML type. *) let type_to_sign env t = match type_expand env t with - | Tdummy d -> Kill d + | Tdummy d when not (conservative_types ()) -> Kill d | _ -> Keep let type_to_signature env t = let rec f = function | Tmeta {contents = Some t} -> f t - | Tarr (Tdummy d, b) -> Kill d :: f b + | Tarr (Tdummy d, b) when not (conservative_types ()) -> Kill d :: f b | Tarr (_, b) -> Keep :: f b | _ -> [] in f (type_expand env t) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index d785fdde9..3fb183995 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -533,6 +533,19 @@ let _ = declare_int_option | None -> chg_flag 0 | Some i -> chg_flag (max i 0))} +(* This option controls whether "dummy lambda" are removed when a + toplevel constant is defined. *) +let conservative_types_ref = ref false +let conservative_types () = !conservative_types_ref + +let _ = declare_bool_option + {optsync = true; + optdepr = false; + optname = "Extraction Conservative Types"; + optkey = ["Extraction"; "Conservative"; "Types"]; + optread = (fun () -> !conservative_types_ref); + optwrite = (fun b -> conservative_types_ref := b) } + (*s Extraction Lang *) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 060abf804..b17f83715 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -132,6 +132,10 @@ type opt_flag = val optims : unit -> opt_flag +(*s Controls whether dummy lambda are removed *) + +val conservative_types : unit -> bool + (*s Target language. *) type lang = Ocaml | Haskell | Scheme |