correction de bugs concernant la gestion des modules. debranchement du test d'extraction sur les Reals en attendant

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

7 files changed, 145 insertions, 50 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 637a30bd7..9b111bbf4 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -16,6 +16,7 @@ open Table
 open Mlutil
 open Ocaml
 open Nametab
+open Util
 
 (*s Modules considerations *)
 
@@ -27,11 +28,43 @@ let sp_of_r r = match r with
     | ConstructRef ((sp,_),_) -> sp
     | _ -> assert false
 
-let module_of_r r = 
-  snd (split_dirpath (dirpath (sp_of_r r)))
+let qualid_of_dirpath d = 
+  let dir,id = split_dirpath d in 
+  make_qualid dir id 
+
+(* [long_module 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 long_module r = 
+  let rec check_module d = 
+    try 
+      locate_loaded_library (qualid_of_dirpath d)
+    with Not_found -> 
+      let d' = 
+	try 
+	  dirpath_prefix d 
+	with _ -> errorlabstrm "long_module_message"
+	[< 'sTR "Can't find the module of"; 'sPC; 
+	   Printer.pr_global r >]
+      in check_module d' 
+  in check_module (dirpath (sp_of_r r))
+
+(* 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 (dirpath (sp_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')
+
+let short_module r = 
+  snd (split_dirpath (long_module r))
 
 let module_option r = 
-  let m = module_of_r r in
+  let m = short_module r in
   if Some m = !current_module then ""
   else (String.capitalize (string_of_id m)) ^ "."
 
@@ -42,7 +75,7 @@ let check_ml r d =
     with Not_found -> d
   else d
 
-(*s tables of global renamings *)
+(*s Tables of global renamings *)
 
 let keywords = ref Idset.empty
 let global_ids = ref Idset.empty
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index c9b41a4ef..e196fd852 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -17,7 +17,11 @@ module ToplevelPp : Mlpp
 
 val sp_of_r : global_reference -> section_path
 
-val module_of_r : global_reference -> identifier
+val long_module : global_reference -> dir_path
+
+val is_long_module : dir_path -> global_reference -> bool
+
+val short_module : global_reference -> identifier
 
 val extract_to_file : 
   string -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 77e20c785..8ce82a45b 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -22,18 +22,62 @@ open Nametab
 open Vernacinterp
 open Common
 
+(*s Auxiliary functions dealing with modules. *)
+
+module Dirset =
+  Set.Make(struct type t = dir_path let compare = compare end)
+
+let module_of_id m = 
+  try 
+    locate_loaded_library (make_short_qualid m) 
+  with Not_found ->  
+    errorlabstrm "module_message"
+      [< 'sTR "Module"; 'sPC;pr_id m; 'sPC; 'sTR "not found." >] 
+
+(*s Module name clash verification. *)
+
+let clash_error sn n1 n2 = 
+  errorlabstrm "clash_module_message"
+    [< 'sTR ("There are two Coq modules with ML name " ^ sn ^" :"); 
+       'fNL ; 'sTR ("  "^(string_of_dirpath n1)) ; 
+       'fNL ; 'sTR ("  "^(string_of_dirpath 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 (long_module r)
+
+let check_decl m sm = function 
+  | Dglob (r,_) -> check_r m sm r 
+  | Dabbrev (r,_,_) -> check_r m sm r
+  | Dtype ((_,r,_)::_, _) -> check_r m sm r 
+  | Dtype ([],_) -> ()
+  | Dcustom (r,_) ->  check_r m sm r
+
+(* [check_one_module m l] checks that no module names in [l] clashes with [m]. *)
+
+let check_one_module m l = 
+  let sm = String.capitalize (string_of_id (snd (split_dirpath m))) in 
+  List.iter (check_decl m sm) l
+
+(* [check_modules m] checks if there are conflicts within the set [m] of modules dirpath. *) 
+
+let check_modules m = 
+  let map = ref Idmap.empty in 
+  Dirset.iter 
+    (fun m -> 
+       let sm = String.capitalize (string_of_id (snd (split_dirpath m))) in 
+       let idm = id_of_string sm in 
+       try 
+	 let m' = Idmap.find idm !map in clash_error sm m m'
+       with Not_found -> map := Idmap.add idm m !map) m
+    
 (*s [extract_module m] returns all the global reference declared 
-  in a module. This is done by traversing the segment of module [M]. 
+  in a module. This is done by traversing the segment of module [m]. 
   We just keep constants and inductives. *)
 
 let extract_module m =
-  let m = 
-    try 
-      Nametab.locate_loaded_library (Nametab.make_short_qualid m) 
-    with Not_found ->  
-      errorlabstrm "module_message"
-	[< 'sTR "Module"; 'sPC;pr_id m; 'sPC; 'sTR "not found." >] 
-    in
   let seg = Library.module_segment (Some m) in
   let get_reference = function
     | sp, Leaf o ->
@@ -59,11 +103,13 @@ let extract_module m =
 type extracted_env = {
   mutable visited : Refset.t;
   mutable to_extract : global_reference list;
-  mutable modules : Idset.t
+  mutable modules : Dirset.t
 }
 
 let empty () = 
-  { visited = ml_extractions (); to_extract = []; modules = Idset.empty }
+  { visited = ml_extractions (); 
+    to_extract = []; 
+    modules = Dirset.empty }
 
 let rec visit_reference m eenv r =
   let r' = match r with
@@ -76,12 +122,10 @@ let rec visit_reference m eenv r =
        and in module extraction *)
     eenv.visited <- Refset.add r' eenv.visited;
     if m then begin 
-      let m_name = module_of_r r' in 
-      if not (Idset.mem m_name eenv.modules) then begin
-	eenv.modules <- Idset.add m_name eenv.modules;
- 	try (* HACK temporaire pour eviter les m_name qui sont des sections *)
-	  List.iter (visit_reference m eenv) (extract_module m_name)
-	with _ -> ()
+      let m_name = long_module r' in 
+      if not (Dirset.mem m_name eenv.modules) then begin
+	eenv.modules <- Dirset.add m_name eenv.modules;
+	List.iter (visit_reference m eenv) (extract_module m_name)
       end
     end;
     visit_decl m eenv (extract_declaration r);
@@ -141,7 +185,7 @@ let extract_env rl =
 
 let modules_extract_env m =
   let eenv = empty () in
-  eenv.modules <- Idset.singleton m;
+  eenv.modules <- Dirset.singleton m;
   List.iter (visit_reference true eenv) (extract_module m);
   eenv.modules, List.rev eenv.to_extract
 
@@ -158,7 +202,6 @@ let local_optimize refs =
   let prm = 
     { lang = "ocaml" ; toplevel = true; 
       mod_name = None; to_appear = refs} in
-  clear_singletons ();
   optimize prm (decl_of_refs refs)
 
 let print_user_extract r = 
@@ -223,7 +266,6 @@ let _ =
     (function 
        | VARG_STRING lang :: VARG_STRING f :: vl ->
 	   (fun () -> 
-	      clear_singletons ();
 	      let refs = refs_of_vargl vl in
 	      let prm = {lang=lang;
 			 toplevel=false;
@@ -239,11 +281,11 @@ let _ =
   \verb!Extraction Module! [M]. *) 
 
 let decl_in_m m = function 
-  | Dglob (r,_) -> m = module_of_r r
-  | Dabbrev (r,_,_) -> m = module_of_r r
-  | Dtype ((_,r,_)::_, _) -> m = module_of_r r 
+  | Dglob (r,_) -> is_long_module m r
+  | Dabbrev (r,_,_) -> is_long_module m r
+  | Dtype ((_,r,_)::_, _) -> is_long_module m r 
   | Dtype ([],_) -> false
-  | Dcustom (r,_) ->  m = module_of_r r
+  | Dcustom (r,_) ->  is_long_module m r
 
 let file_suffix = function
   | "ocaml" -> ".ml"
@@ -255,21 +297,22 @@ let _ =
     (function 
        | [VARG_STRING lang; VARG_IDENTIFIER m] ->
 	   (fun () -> 
-	      clear_singletons ();
+	      let dir_m = module_of_id m in 
 	      let f = (String.uncapitalize (string_of_id m))
 		       ^ (file_suffix lang) in
 	      let prm = {lang=lang;
 			 toplevel=false;
 			 mod_name= Some m;
 			 to_appear= []} in 
-	      let rl = extract_module m in 
+	      let rl = extract_module dir_m in 
 	      let decls = optimize prm (decl_of_refs rl) in
 	      let decls = add_ml_decls prm decls in 
-	      let decls = List.filter (decl_in_m m) decls in
+	      check_one_module dir_m decls; 
+	      let decls = List.filter (decl_in_m dir_m) decls in
 	      extract_to_file f prm decls)
        | _ -> assert false)
 
-(*s Recusrive Extraction of all the modules [M] depends on. 
+(*s Recursive Extraction of all the modules [M] depends on. 
   The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
 
 let _ = 
@@ -277,23 +320,26 @@ let _ =
         (function 
        | [VARG_STRING lang; VARG_IDENTIFIER m] ->
 	   (fun () -> 
-	      clear_singletons ();
-	      let modules,refs = modules_extract_env m in 
+	      let dir_m = module_of_id m in 
+	      let modules,refs = 
+		modules_extract_env dir_m in
+	      check_modules modules; 
 	      let dummy_prm = {lang=lang;
 			      toplevel=false;
 			      mod_name= Some m;
 			      to_appear= []} in
 	      let decls = optimize dummy_prm (decl_of_refs refs) in
 	      let decls = add_ml_decls dummy_prm decls in
-	      Idset.iter 
+	      Dirset.iter 
 		(fun m ->
-		   let f = (String.uncapitalize (string_of_id m))
+		   let short_m = snd (split_dirpath m) in
+		   let f = (String.uncapitalize (string_of_id short_m))
 			   ^ (file_suffix lang) in
 		   let prm = {lang=lang;
 			      toplevel=false;
-			      mod_name= Some m;
+			      mod_name= Some short_m;
 			      to_appear= []} in 
 		   let decls = List.filter (decl_in_m m) decls in
-		   extract_to_file f prm decls)
+		   if decls <> [] then extract_to_file f prm decls)
 		modules)
        | _ -> assert false)
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 0ae088384..32ad5053b 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -616,7 +616,7 @@ let is_exn = function
   | MLexn _ -> true
   | _ -> false
 
-let rec optimize prm = function
+let rec optim prm = function
   | [] -> 
       []
   | ( Dabbrev (r,_,Tarity) |
@@ -624,8 +624,8 @@ let rec optimize prm = function
 	  Dglob(r,MLarity) | 
 	    Dglob(r,MLprop) ) as d :: l ->
       if List.mem r prm.to_appear then
-	d :: (optimize prm l) 
-      else optimize prm l
+	d :: (optim prm l) 
+      else optim prm l
   | Dglob (r,t) :: l ->
       let t = normalize t in
       let b = expand (strict_language prm.lang) r t
@@ -644,19 +644,20 @@ let rec optimize prm = function
       if not b' && 
 	(not b || prm.mod_name <> None || List.mem r prm.to_appear) then 
 	let t = optimize_fix t in
-	Dglob (r,t) :: (optimize prm l)
+	Dglob (r,t) :: (optim prm l)
       else 
-	optimize prm l
+	optim prm l
   | (Dtype ([],_) | Dabbrev _ | Dcustom _) as d :: l -> 
-      d :: (optimize prm l)
+      d :: (optim prm l)
   | Dtype ([ids,r,[r0,[t0]]],false) :: l when not (type_mem r t0) ->
       (* Detection of informative singleton. *)
       add_singleton r0; 
-      Dabbrev (r, ids, t0) :: (optimize prm l)
+      Dabbrev (r, ids, t0) :: (optim prm l)
   | Dtype(il,b) :: l -> 
       (* Detection of empty inductives. *)
       let l1,l2 = empty_ind il in 
-      if l2 = [] then l1 @ (optimize prm l) 
-      else l1 @ (Dtype(l2,b) :: (optimize prm l))
+      if l2 = [] then l1 @ (optim prm l) 
+      else l1 @ (Dtype(l2,b) :: (optim prm l))
 
 
+let optimize prm l = clear_singletons(); optim prm l
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 391bf7350..778683646 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -35,6 +35,12 @@ let open_par = function true -> string "(" | false -> [< >]
 
 let close_par = function true -> string ")" | false -> [< >]
 
+let pp_tvar id = 
+  let s = string_of_id id in 
+  if String.length s < 2 || s.[1]<>'\'' 
+  then string ("'"^s)
+  else string ("' "^s)
+
 let pp_tuple f = function
   | [] -> [< >]
   | [x] -> f x
@@ -129,7 +135,7 @@ let empty_env () = [], P.globals()
 let rec pp_type par t =
   let rec pp_rec par = function
     | Tvar id -> 
-	string ("'" ^ string_of_id id)
+	pp_tvar id
     | Tapp l ->
 	(match collapse_type_app l with
 	   | [] -> assert false
@@ -295,7 +301,7 @@ let pp_ast a = hOV 0 (pp_expr false (empty_env ()) [] a)
 (*s Pretty-printing of inductive types declaration. *)
 
 let pp_parameters l = 
-  [< pp_tuple (fun id -> string ("'" ^ string_of_id id)) l; space_if (l<>[]) >]
+  [< pp_tuple pp_tvar l; space_if (l<>[]) >]
 
 let pp_one_inductive (pl,name,cl) =
   let pp_constructor (id,l) =
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 1db621f18..90598daa4 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -9,6 +9,7 @@ TOPDIR=../../..
 AXIOMSVO:= \
 theories/Arith/Arith.vo \
 theories/Lists/List.vo \
+theories/Reals/% \
 theories/Reals/Rsyntax.vo \
 theories/Num/% \
 theories/ZArith/Zsyntax.vo
diff --git a/contrib/extraction/test/custom/Reals.v b/contrib/extraction/test/custom/Reals.v
index d42fe0a53..b817c3600 100644
--- a/contrib/extraction/test/custom/Reals.v
+++ b/contrib/extraction/test/custom/Reals.v
@@ -9,4 +9,8 @@ Extract Inlined Constant Rinv => "(fun x -> 1.0 /. x)".
 Extract Inlined Constant Rlt => "(<)".
 Extract Inlined Constant up => "AddReals.my_ceil".
 Extract Inlined Constant total_order_T => "AddReals.total_order_T".
-
+Extract Inlined Constant sqrt => "sqrt".
+Extract Inlined Constant sigma => "(fun l h -> sigma_aux l h (Minus.minus h l))".
+Extract Inlined Constant PI => "3.141593".
+Extract Inlined Constant cos => cos.
+Extract Inlined Constant sin => sin.