seisme suite. correction bugs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2138 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 28 insertions, 14 deletions

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index d0f0e1224c..7149d27787 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -54,13 +54,16 @@ let rec occurs k = function
   | MLrel i -> i = k
   | MLapp(t,argl) -> (occurs k t) || (occurs_list k argl)
   | MLlam(_,t) -> occurs (k + 1) t
+  | MLletin(_,t,t')-> (occurs k t) || (occurs (k+1) t')
   | MLcons(_,argl) -> occurs_list k argl
   | MLcase(t,pv) -> 
       (occurs k t) ||
       (array_exists
 	 (fun (_,l,t') -> let k' = List.length l in occurs (k + k') t') pv)
   | MLfix(_,l,cl) -> let k' = Array.length l in occurs_vect (k + k') cl
-  | _ -> false
+  | MLcast(t,_) -> occurs k t			
+  | MLmagic t -> occurs k t
+  | MLglob _ | MLexn _ | MLprop | MLarity -> false
 
 and occurs_list k l = List.exists (occurs k) l
 
@@ -73,6 +76,7 @@ let rec occurs_itvl k k' = function
   | MLrel i -> (k <= i) && (i <= k')
   | MLapp(t,argl) -> (occurs_itvl k k' t) || (occurs_itvl_list k k' argl)
   | MLlam(_,t) -> occurs_itvl (k + 1) (k' + 1) t
+  | MLletin(_,t,t') -> (occurs_itvl k k' t) || (occurs_itvl (k+1) (k'+1) t')
   | MLcons(_,argl) -> occurs_itvl_list k k' argl
   | MLcase(t,pv) -> 
       (occurs_itvl k k' t) ||
@@ -81,7 +85,9 @@ let rec occurs_itvl k k' = function
 	    let n = List.length l in occurs_itvl (k + n) (k' + n) t') pv)
   | MLfix(_,l,cl) -> 
       let n = Array.length l in occurs_itvl_vect (k + n) (k' + n) cl
-  | _ -> false
+  | MLcast(t,_) -> occurs_itvl k k' t
+  | MLmagic t -> occurs_itvl k k' t
+  | MLglob _ | MLexn _ | MLprop | MLarity  -> false
 
 and occurs_itvl_list k k' l = List.exists (occurs_itvl k k') l
 
@@ -221,17 +227,17 @@ let check_identity_case br =
 
 
 let check_constant_case br = 
-  let (r,l,t) = br.(0) in
+  let (_,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 (_,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
-
+ 
 
 let all_constr br = 
   try 
@@ -291,7 +297,8 @@ let rec betaiota = function
 		    | (n, i, MLcons (r,a))-> 
 			let (_,ids,c) = br.(constructor_index r) in
 			let c = ml_lift (List.length i) c in 
-			let c' = List.fold_right (fun id t -> MLlam (id,t)) ids c in
+			let c' = List.fold_right 
+				   (fun id t -> MLlam (id,t)) ids c in
 			(n,i,betaiota (MLapp (c',a)))
 		    | _ -> assert false) br'
 	     in MLcase(e', new_br)
@@ -407,8 +414,9 @@ let rec non_stricts add cand = function
   | _ -> 
       cand
 
-(* The real test: we are looking for internal non-strict variables, so we start with 
-   no candidates, and the only positive answer is via the [Toplevel] exception. *)
+(* The real test: we are looking for internal non-strict variables, so we start
+   with no candidates, and the only positive answer is via the [Toplevel] 
+   exception. *)
 
 let is_not_strict t = 
   try 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index b798d13e43..3ad6246d37 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -29,9 +29,13 @@ module Refmap =
 
 (*s Auxiliary functions *) 
 
-let check_constant r = match r with 
-  | ConstRef sp -> r 
-  | _ -> errorlabstrm "extract_constant"
+let is_constant r = match r with 
+  | ConstRef _ -> true
+  | _ -> false
+
+let check_constant r = 
+  if (is_constant r) then r 
+  else errorlabstrm "extract_constant"
 	[< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >] 
 
 let string_of_varg = function
@@ -129,7 +133,8 @@ let sorted_ml_extractions () = let (_,_,l) = !extractions in l
 
 let add_ml_extraction r s = 
   let (map,set,list) = !extractions in
-  extractions := (Refmap.add r s map, Refset.add r set, (r,s)::list)
+  let list' = if (is_constant r) then (r,s)::list else list in 
+  extractions := (Refmap.add r s map, Refset.add r set, list')
 
 let is_ml_extraction r = 
   let (_,set,_) = !extractions in Refset.mem r set
@@ -186,8 +191,9 @@ let extract_inductive r (id2,l2) = match r with
       add_anonymous_leaf (in_ml_extraction (r,id2));
       list_iter_i
 	(fun j s -> 
-	   add_anonymous_leaf 
-	     (in_ml_extraction (ConstructRef (ip,succ j),s))) l2
+	   let r = ConstructRef (ip,succ j) in 
+	   add_anonymous_leaf (inline_extraction (true,[r]));
+	   add_anonymous_leaf (in_ml_extraction (r,s))) l2
   | _ -> 
       errorlabstrm "extract_inductive"
 	[< Printer.pr_global r; 'sPC; 'sTR "is not an inductive type" >]