summaryrefslogtreecommitdiff
path: root/plugins/extraction/extraction.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
commit3e96002677226c0cdaa8f355938a76cfb37a722a (patch)
tree3ca96e142fdb68e464d2f5f403f315282b94f922 /plugins/extraction/extraction.ml
parentf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff)
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'plugins/extraction/extraction.ml')
-rw-r--r--plugins/extraction/extraction.ml25
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