From b87ff23b3e3207466e3de63fcafac6a44102bf72 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 31 Oct 2001 16:52:06 +0000
Subject: correction du debut d'optimisation du Fix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2148 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/mlutil.ml | 30 ++++++++++++++++--------------
 1 file changed, 16 insertions(+), 14 deletions(-)

(limited to 'contrib')

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 187df32a49..e9dd128336 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -330,25 +330,27 @@ let collect_lambda =
   in 
   collect []
 
-
-
-let test_eta l =
+let test_eta n l =
   let rec test n = function 
     | [] -> true
-    | a :: q -> a = (MLrel n) || (test (succ n) q)
-  in test 1 l 
+    | a :: q -> a = (MLrel n) && (test (succ n) q)
+  in (List.length l = n) && (test 1 l) 
 
 let optimize_fix a = 
-  if not (optim()) then a else
+  if not (optim()) then a 
+  else
     let lams,b = collect_lambda a in 
-    (match a with 
-      | MLfix(_,[|_|],[|c|]) -> a (* TODO *)
-      | MLapp(b,ids) -> 
-	  (match b with 
-	     | MLfix(_,[|_|],[|_|]) when (test_eta ids)-> b
-	     | MLfix(_,[|_|],[|_|]) -> a (* TODO *)
-	     | _ -> a)
-      | _ -> a)
+    let nlams = List.length lams in 
+    if nlams = 0 then a 
+    else  
+      (match b with 
+	 | MLfix(_,[|_|],[|c|]) -> a (* TODO *)
+	 | MLapp(b,ids) -> 
+	     (match b with 
+		| MLfix(_,[|_|],[|_|]) when (test_eta nlams ids)-> b
+		| MLfix(_,[|_|],[|_|]) -> a (* TODO *)
+		| _ -> a)
+	 | _ -> a)
 
 let normalize_decl = function
  | Dglob (id, a) -> Dglob (id, normalize a)
-- 
cgit v1.2.3