Imported Upstream version 8.3upstream/8.3

1 files changed, 24 insertions, 1 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 057057d1..b615955f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extraction.ml 13427 2010-09-17 17:37:52Z letouzey $ i*)
 
 (*i*)
 open Util
@@ -817,6 +817,18 @@ let rec decomp_lams_eta_n n m env c t =
   let eta_args = List.rev_map mkRel (interval 1 d) in
   rels, applist (lift d c,eta_args)
 
+(* Let's try to identify some situation where extracted code
+   will allow generalisation of type variables *)
+
+let rec gentypvar_ok c = match kind_of_term c with
+  | Lambda _ | Const _ -> true
+  | App (c,v) ->
+      (* if all arguments are variables, these variables will
+	 disappear after extraction (see [empty_s] below) *)
+      array_for_all isRel v && gentypvar_ok c
+  | Cast (c,_,_) -> gentypvar_ok c
+  | _ -> false
+
 (*s From a constant to a ML declaration. *)
 
 let extract_std_constant env kn body typ =
@@ -846,6 +858,17 @@ let extract_std_constant env kn body typ =
       then decompose_lam_n m body
       else decomp_lams_eta_n n m env body typ
   in
+  (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
+  let rels, c =
+    let n = List.length rels in
+    let s,s' = list_split_at n s in
+    let k = sign_kind s in
+    let empty_s = (k = EmptySig || k = SafeLogicalSig) in
+    if lang () = Ocaml && empty_s && not (gentypvar_ok c)
+      && s' <> [] && type_maxvar t <> 0
+    then decomp_lams_eta_n (n+1) n env body typ
+    else rels,c
+  in
   let n = List.length rels in
   let s = list_firstn n s in
   let l,l' = list_split_at n l in