suite chgt liés aux modules

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

4 files changed, 26 insertions, 46 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index c7f0a97d9a..bd08e8d3c3 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -27,27 +27,13 @@ let current_module = ref (id_of_string "")
 
 let is_construct = function ConstructRef _ -> true | _ -> false 
 
-let qualid_of_dirpath d = 
-  let dir,id = split_dirpath d in 
-  make_qualid dir id 
-
-(* From a valid module dirpath [d], we check if [r] belongs to this module. *)
-      
-let is_long_module d r = 
-  let dir = repr_dirpath d 
-  and dir' = repr_dirpath (fst (decode_kn (kn_of_r r))) in 
-  let l = List.length dir 
-  and l' = List.length dir' in 
-  if l' < l then false 
-  else dir = snd (list_chop (l'-l) dir')
-
-(* NB: [library_part r] computes the dirpath of the module of the global 
-   reference [r]. The difficulty comes from the possible section names 
-   at the beginning of the dirpath (due to Remark). *)
-
-let short_module r = 
-  snd (split_dirpath (library_part r))
+let long_module r = 
+  match modpath (kn_of_r r) with 
+    | MPfile d -> d
+    | _ -> anomaly "TODO: extraction not ready for true modules"
 
+let short_module r = List.hd (repr_dirpath (long_module r))
+			    
 let check_ml r d = 
   if to_inline r then 
     try 
@@ -143,11 +129,8 @@ module ModularParams = struct
   let globals () = !global_ids 
 
   let clash r id = 
-    try 
-      let _ = locate (make_qualid (fst (decode_kn (kn_of_r r))) id)
-      in true
-    with _ -> false
-
+    exists_cci (make_path (dirpath (sp_of_global None r)) id)
+      
   let rename_global_id r id id' prefix =
     let id' = 
       if (Idset.mem id' !keywords) || (id <> id' && clash r id') then 
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 9ebb110697..d831f00b78 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -14,9 +14,7 @@ open Mlutil
 open Names
 open Libnames
 
-val is_long_module : dir_path -> global_reference -> bool
-
-val short_module : global_reference -> identifier
+val long_module : global_reference -> dir_path
 
 val set_globals : unit -> unit
 
@@ -28,5 +26,3 @@ val pp_decl : bool -> ml_decl -> std_ppcmds
 
 val extract_to_file : 
   string option -> extraction_params -> ml_decl list -> unit
-
-
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index d04a65fde6..e6fa6e822c 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -46,10 +46,11 @@ let clash_error sn n1 n2 =
      fnl () ++ str "This is not allowed in ML. Please do some renaming first.")
     
 let check_r m sm r = 
-  let rm = String.capitalize (string_of_id (short_module r)) in 
-  if rm = sm && not (is_long_module m r) 
-  then clash_error sm m (library_part r)
-
+  let rlm = long_module r in 
+  let rsm = List.hd (repr_dirpath rlm) in 
+  if (String.capitalize (string_of_id rsm)) = sm && m <> rlm
+  then clash_error sm m rlm
+    
 let check_decl m sm = function 
   | Dterm (r,_) -> check_r m sm r 
   | Dtype (r,_,_) -> check_r m sm r
@@ -274,14 +275,14 @@ let extraction_file f vl =
   \verb!Extraction Module! [M]. *) 
 
 let decl_in_m m = function 
-  | Dterm (r,_) -> is_long_module m r
-  | Dtype (r,_,_) -> is_long_module m r
-  | Dind ((_,r,_)::_, _) -> is_long_module m r 
+  | Dterm (r,_) -> m = long_module r
+  | Dtype (r,_,_) -> m = long_module r
+  | Dind ((_,r,_)::_, _) -> m = long_module r 
   | Dind ([],_) -> false
-  | DdummyType r -> is_long_module m r
-  | DcustomTerm (r,_) ->  is_long_module m r
-  | DcustomType (r,_) ->  is_long_module m r
-  | Dfix (rv,_) -> is_long_module m rv.(0)
+  | DdummyType r -> m = long_module r
+  | DcustomTerm (r,_) ->  m = long_module r
+  | DcustomType (r,_) ->  m = long_module r
+  | Dfix (rv,_) -> m = long_module rv.(0)
 
 let module_file_name m = match lang () with 
   | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml"
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 5abd599ed0..073d574bb9 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -752,10 +752,10 @@ let inline_test t =
   not (is_fix t) && (is_constr t || (ml_size t < 12 && is_not_strict t))
 
 let manual_inline_list = 
-  let dir =  dirpath_of_string "Coq.Init.Wf" 
-  in List.map (fun s -> encode_kn dir (id_of_string s))
-       [ "Acc_rec" ; "Acc_rect" ; 
-	 "well_founded_induction" ; "well_founded_induction_type" ]
+  let dir = dirpath_of_string "Coq.Init.Wf" in 
+  List.map (fun s -> (encode_kn dir (id_of_string s)))
+    [ "well_founded_induction"; 
+      "well_founded_induction_type" ]
 
 let manual_inline = function 
   | ConstRef c -> List.mem c manual_inline_list
@@ -839,7 +839,7 @@ and optimize_Dfix prm r t b l =
 	  else optimize prm l
 	else 
 	  let v = try 
-	    let d,_ = decode_kn (kn_of_r r) in 
+	    let d = dirpath (sp_of_global None r) in 
 	    Array.map (fun id -> locate (make_qualid d id)) f 
 	  with Not_found -> raise Impossible 
 	  in