Add option Set/Unset Extraction Conservative Types.

Extracted code need not preserve typing relations (e:t) from the source code.
This may be a problem as the extracted code may not implement the intented
interface. This option disables the optimisations which would prevent an
extracted term's type to be its extracted source term's type.

At this point the only such optimization is (I think) removing some dummy
λ-abstractions in constant definitions.

Extraction Implicit is still honored in this mode, and it's mostly necessary
to produce reasonable types. So in the conservative type mode, which
abstractions can be removed and which can'tt is entirely under the user's
control.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 85f007b7-540e-0410-9357-904b9bb8a0f7

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