Imported Upstream version 8.3.pl3upstream/8.3.pl3

1 files changed, 38 insertions, 19 deletions

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index c242e4ab..3c7ee0f2 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.ml 14003 2011-04-14 23:09:41Z letouzey $ i*)
+(*i $Id: mlutil.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
 
 (*i*)
 open Pp
@@ -119,6 +119,7 @@ let rec mgu = function
       mgu (a, a'); mgu (b, b')
   | Tglob (r,l), Tglob (r',l') when r = r' ->
        List.iter mgu (List.combine l l')
+  | (Tdummy _, _ | _, Tdummy _) when lang() = Haskell -> ()
   | Tdummy _, Tdummy _ -> ()
   | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
   | _ -> raise Impossible
@@ -129,6 +130,11 @@ let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
 
 let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
 
+let generalizable a =
+  lang () <> Ocaml ||
+    match a with
+      | MLapp _ -> false
+      | _ -> true (* TODO, this is just an approximation for the moment *)
 
 (*S ML type env. *)
 
@@ -961,10 +967,18 @@ let kill_some_lams bl (ids,c) =
 let kill_dummy_lams c =
   let ids,c = collect_lams c in
   let bl = List.map sign_of_id ids in
-  if (List.mem Keep bl) && (List.exists isKill bl) then
-    let ids',c = kill_some_lams bl (ids,c) in
-    ids, named_lams ids' c
-  else raise Impossible
+  if not (List.mem Keep bl) then raise Impossible;
+  let rec fst_kill n = function
+    | [] -> raise Impossible
+    | Kill _ :: bl -> n
+    | Keep :: bl -> fst_kill (n+1) bl
+  in
+  let skip = max 0 ((fst_kill 0 bl) - 1) in
+  let ids_skip, ids = list_chop skip ids in
+  let _, bl = list_chop skip bl in
+  let c = named_lams ids_skip c in
+  let ids',c = kill_some_lams bl (ids,c) in
+  ids, named_lams ids' c
 
 (*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c]
    and a signature [s] and builds a eta-long version. *)
@@ -1005,21 +1019,26 @@ let term_expunge s (ids,c) =
       MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
-(*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and
-  purge the args of [t0] corresponding to a [dummy_name].
+(*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and
+  purge the args of [MLrel r] corresponding to a [dummy_name].
   It makes eta-expansion if needed. *)
 
-let kill_dummy_args ids t0 t =
+let kill_dummy_args ids r t =
   let m = List.length ids in
   let bl = List.rev_map sign_of_id ids in
+  let rec found n = function
+    | MLrel r' when r' = r + n -> true
+    | MLmagic e -> found n e
+    | _ -> false
+  in
   let rec killrec n = function
-    | MLapp(e, a) when e = ast_lift n t0 ->
+    | MLapp(e, a) when found n e ->
 	let k = max 0 (m - (List.length a)) in
 	let a = List.map (killrec n) a in
 	let a = List.map (ast_lift k) a in
 	let a = select_via_bl bl (a @ (eta_args k)) in
 	named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
-    | e when e = ast_lift n t0 ->
+    | e when found n e ->
 	let a = select_via_bl bl (eta_args m) in
 	named_lams ids (MLapp (ast_lift m e, a))
     | e -> ast_map_lift killrec n e
@@ -1031,28 +1050,28 @@ let rec kill_dummy = function
   | MLfix(i,fi,c) ->
       (try
 	 let ids,c = kill_dummy_fix i c in
-	 ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1))
+	 ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids 1 (MLrel 1))
        with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
   | MLapp (MLfix (i,fi,c),a) ->
       let a = List.map kill_dummy a in
       (try
 	 let ids,c = kill_dummy_fix i c in
 	 let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in
-	 let fake' = kill_dummy_args ids (MLrel 1) fake in
+	 let fake' = kill_dummy_args ids 1 fake in
 	 ast_subst (MLfix (i,fi,c)) fake'
        with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),a))
   | MLletin(id, MLfix (i,fi,c),e) ->
       (try
 	 let ids,c = kill_dummy_fix i c in
-	 let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in
+	 let e = kill_dummy (kill_dummy_args ids 1 e) in
 	 MLletin(id, MLfix(i,fi,c),e)
       with Impossible ->
 	MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
   | MLletin(id,c,e) ->
       (try
 	 let ids,c = kill_dummy_lams (kill_dummy_hd c) in
-	 let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in
-	 let c = eta_red (kill_dummy c) in
+	 let e = kill_dummy (kill_dummy_args ids 1 e) in
+	 let c = kill_dummy c in
 	 if is_atomic c then ast_subst c e else MLletin (id, c, e)
        with Impossible -> MLletin(id,kill_dummy c,kill_dummy e))
   | a -> ast_map kill_dummy a
@@ -1064,8 +1083,8 @@ and kill_dummy_hd = function
   | MLletin(id,c,e) ->
       (try
 	 let ids,c = kill_dummy_lams (kill_dummy_hd c) in
-	 let e = kill_dummy_hd (kill_dummy_args ids (MLrel 1) e) in
-	 let c = eta_red (kill_dummy c) in
+	 let e = kill_dummy_hd (kill_dummy_args ids 1 e) in
+	 let c = kill_dummy c in
 	 if is_atomic c then ast_subst c e else MLletin (id, c, e)
        with Impossible -> MLletin(id,kill_dummy c,kill_dummy_hd e))
   | a -> a
@@ -1075,7 +1094,7 @@ and kill_dummy_fix i c =
   let ids,ci = kill_dummy_lams (kill_dummy_hd c.(i)) in
   let c = Array.copy c in c.(i) <- ci;
   for j = 0 to (n-1) do
-    c.(j) <- kill_dummy (kill_dummy_args ids (MLrel (n-i)) c.(j))
+    c.(j) <- kill_dummy (kill_dummy_args ids (n-i) c.(j))
   done;
   ids,c