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

3 files changed, 19 insertions, 2 deletions

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