summaryrefslogtreecommitdiff
path: root/plugins/extraction/mlutil.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
commit300293c119981054c95182a90c829058530a6b6f (patch)
treed7303613741c5796b58ced7db24ec7203327dbb2 /plugins/extraction/mlutil.ml
parent9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff)
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'plugins/extraction/mlutil.ml')
-rw-r--r--plugins/extraction/mlutil.ml57
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