Extraction: re-introduce some eta-expansions in rare situations leading to '_a types

 If there's no lambdas at the top of a constant body
  and its type is functional
  and this type contains type variable
  and we're extracting to Ocaml
  then we perform one eta-expansion to please the ML type-checker

 This might slow down things, if some computations are shared
 thanks to the partial application. But it seems quite unlikely to
 encounter both situations (clever partial application and
 non-generalizable variable) at the same time. Compcert is ok,
 for instance.

 As a consequence, no need for manual eta-expansion in AVL code
 (and by the way MSetAVL.element wasn't a problem, it is monomorphic)

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

3 files changed, 25 insertions, 2 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index eb039ba59a..ba7fc272a6 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -815,6 +815,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 =
@@ -844,6 +856,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_chop 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_chop n l in
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 684291d7ce..f9dda51255 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -270,7 +270,7 @@ Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) :=
 
 (** then [elements] is an instanciation with an empty [acc] *)
 
-Definition elements m := elements_aux nil m.
+Definition elements := elements_aux nil.
 
 (** * Fold *)
 
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index fee3f5bcfc..349cdedf7b 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -328,7 +328,7 @@ Fixpoint elements_aux (acc : list X.t) (s : t) : list X.t :=
 
 (** then [elements] is an instanciation with an empty [acc] *)
 
-Definition elements s := elements_aux nil s.
+Definition elements := elements_aux nil.
 
 (** ** Filter *)