Verification supplementaire avant optimisation singleton

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

4 files changed, 21 insertions, 7 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index c34ac21c0a..6f89c384a8 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -754,7 +754,7 @@ and is_singleton_inductive (sp,_) =
   let mis = build_mis ((sp,0),[||]) mib in
   (mis_nconstr mis = 1) && 
   match extract_constructor ((sp,0),1) with 
-    | Cml ([_],_,_)-> true
+    | Cml ([mlt],_,_)-> (try parse_ml_type sp mlt; true with Found_sp -> false)
     | _ -> false
 	  
 and is_singleton_constructor ((sp,i),_) = 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 63a8e11f9d..e4ae07a12e 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -35,6 +35,20 @@ let rec update_args sp vl = function
       Tarr (update_args sp vl a, update_args sp vl b)
   | a -> a
 
+exception Found_sp
+
+let sp_of_r r = match r with 
+    | ConstRef sp -> sp
+    | IndRef (sp,_) -> sp
+    | ConstructRef ((sp,_),_) -> sp
+    | _ -> assert false
+
+let rec parse_ml_type sp = function 
+  | Tglob r -> if (sp_of_r r)=sp then raise Found_sp
+  | Tapp l -> List.iter (parse_ml_type sp) l
+  | Tarr (a,b) -> (parse_ml_type sp a; parse_ml_type sp b)
+  | _ -> ()
+      
 (*s [occurs k t] returns true if [(Rel k)] occurs in [t]. *)
 
 let rec occurs k = function
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 1e85212832..6f7168ed07 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -23,6 +23,12 @@ val prop_name : identifier
 
 val update_args : section_path -> ml_type list -> ml_type -> ml_type
 
+exception Found_sp
+
+val sp_of_r : global_reference -> section_path
+
+val parse_ml_type : section_path -> ml_type -> unit
+
 (*s Utility functions over ML terms. [occurs n t] checks whether [Rel
     n] occurs (freely) in [t]. [ml_lift] is de Bruijn
     lifting. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. *)
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 2d983fab55..71c32d215b 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -82,12 +82,6 @@ let rename_upper_global id = rename_global (uppercase_id id)
 
 (*s Modules considerations *)
 
-let sp_of_r r = match r with 
-    | ConstRef sp -> sp
-    | IndRef (sp,_) -> sp
-    | ConstructRef ((sp,_),_) -> sp
-    | _ -> assert false
-
 let module_of_r r = list_last (dirpath (sp_of_r r))
 
 let string_of_r r = string_of_id (basename (sp_of_r r))