From eb698d2b16206a057a29779204e3817f2f4da093 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 3 Nov 2001 16:00:52 +0000
Subject: retablissement de l'optim case constant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2154 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/mlutil.ml     | 17 ++++++++++++++++-
 contrib/extraction/test/Makefile |  6 ++++++
 2 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 27c971c65c..2f3a67b6e6 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -239,6 +239,19 @@ let check_case br =
     if check_and_generalize br.(i) <> f then raise Impossible 
   done; f
 
+let check_constant_case br = 
+  if br = [||] then raise Impossible; 
+  let (r,l,t) = br.(0) in
+  let n = List.length l in 
+  if occurs_itvl 1 n t then raise Impossible; 
+  let cst = ml_lift (-n) t in 
+  for i = 1 to Array.length br - 1 do 
+    let (r,l,t) = br.(i) in
+    let n = List.length l in
+    if (occurs_itvl 1 n t) || (cst <> (ml_lift (-n) t)) 
+    then raise Impossible
+  done; cst
+
 (*s Some Beta-iota reductions + simplifications*)
 
 let constructor_index = function
@@ -320,7 +333,9 @@ let normalize a =
 		 try 
 		   let f = check_case br' in 
 		   simplify (MLapp (MLlam (anonymous,f),[e']))
-		 with Impossible -> MLcase (e', br')
+		 with Impossible -> 
+	           try check_constant_case br' 
+                   with Impossible -> MLcase (e', br')
 	       else MLcase (e', br'))
     | MLletin(_,c,e) when (is_atomic c) || (nb_occur e <= 1) -> 
 	(* expansion of a letin in special cases *)
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 787abb32ac..01875a6d26 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -75,6 +75,12 @@ $(REALSML): realsml
 #	Utilities
 #
 
+open: 
+	find theories -name "*".ml -exec qualify2open \{\} \;
+
+undo_open: 
+	find theories -name "*".ml -exec mv \{\}.orig \{\} \;
+
 ml2v: ml2v.ml
 	ocamlc -o $@ $<
 
-- 
cgit v1.2.3