legeres modifs pretty-print de l'extractions

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

6 files changed, 35 insertions, 42 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index be68910870..63a74b3d07 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -51,18 +51,20 @@ let cache r f =
 (*s Renaming issues at toplevel *)
 
 module ToplevelParams = struct
+  let cofix_warning = false
   let globals () = Idset.empty
   let rename_global r = Names.id_of_string (Global.string_of_global r)
   let pp_type_global = Printer.pr_global
   let pp_global = Printer.pr_global
-  let cofix_warning = false
 end
 
 (*s Renaming issues for a monolithic extraction. *)
 
 module MonoParams = struct
-  
-  let globals () = ! global_ids
+
+  let cofix_warning = true
+
+  let globals () = !global_ids
 		     
   let rename_global_id id = 
     let id' = rename_id id !global_ids in
@@ -89,8 +91,6 @@ module MonoParams = struct
   let pp_global r = 
     string (check_ml r (string_of_id (rename_global r)))
       
-  let cofix_warning = true
-
 end
 
 
@@ -98,6 +98,8 @@ end
 
 module ModularParams = struct
 
+  let cofix_warning = true
+
   let globals () = !global_ids 
 
   let clash r id = 
@@ -135,7 +137,6 @@ module ModularParams = struct
     string 
       (check_ml r ((module_option r)^(string_of_id (rename_global r))))
 
-  let cofix_warning = true
 end
 
 
@@ -148,36 +149,25 @@ module HaskellMonoPp = Haskell.Make(MonoParams)
 module HaskellModularPp = Haskell.Make(ModularParams)
 
 
-
 (*s Extraction to a file. *)
 
 let init_global_ids lang = 
+  Hashtbl.clear renamings;
   keywords := 
-  Idset.add (id_of_string "prop") 
-    (Idset.add (id_of_string "arity") 
-       (match lang with 
-	  | "ocaml" -> Ocaml.keywords
-	  | "haskell" -> Haskell.keywords
-	  | _ -> assert false));
+  (match lang with 
+     | "ocaml" -> Ocaml.keywords
+     | "haskell" -> Haskell.keywords
+     | _ -> assert false);
   global_ids := !keywords
 
 let extract_to_file f prm decls =
-  Hashtbl.clear renamings;
-  init_global_ids prm.lang; 
-  current_module := 
-    if prm.modular then 
-      Some prm.module_name 
-    else None;
-  let preamble = match prm.lang with 
-    | "ocaml" -> Ocaml.preamble
-    | "haskell" -> Haskell.preamble
-    | _ -> assert false
-  in
-  let pp_decl = match prm.lang,prm.modular with 
-    | "ocaml", true -> OcamlModularPp.pp_decl
-    | "ocaml", false -> OcamlMonoPp.pp_decl
-    | "haskell",true -> HaskellModularPp.pp_decl
-    | "haskell",false -> HaskellMonoPp.pp_decl 
+  current_module := prm.mod_name;
+  init_global_ids prm.lang;
+  let preamble,pp_decl = match prm.lang,prm.mod_name with 
+    | "ocaml", None -> Ocaml.preamble, OcamlMonoPp.pp_decl
+    | "ocaml", _ -> Ocaml.preamble, OcamlModularPp.pp_decl
+    | "haskell", None -> Haskell.preamble, HaskellMonoPp.pp_decl
+    | "haskell", _ -> Haskell.preamble, HaskellModularPp.pp_decl
     | _ -> assert false
   in
   let cout = open_out f in
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 7e8a0c0734..007fcf1d8c 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -112,8 +112,8 @@ let decl_of_refs refs =
 
 let local_optimize refs = 
   let prm = 
-    { lang = "ocaml" ; modular = false ; 
-      module_name = "" ; to_appear = refs} in
+    { lang = "ocaml" ; toplevel = true; 
+      mod_name = None; to_appear = refs} in
   optimize prm (decl_of_refs refs)
 
 let print_user_extract r = 
@@ -168,8 +168,8 @@ let _ =
 	   (fun () -> 
 	      let refs = refs_of_vargl vl in
 	      let prm = {lang=lang;
-			 modular=false;
-			 module_name="";
+			 toplevel=false;
+			 mod_name = None;
 			 to_appear= refs} in 
 	      let decls = decl_of_refs refs in 
 	      let decls = add_ml_decls prm decls in 
@@ -215,8 +215,8 @@ let _ =
 	      let ms = Names.string_of_id m in
 	      let f = (String.uncapitalize ms) ^ (file_suffix lang) in
 	      let prm = {lang=lang;
-			 modular=true;
-			 module_name= ms;
+			 toplevel=false;
+			 mod_name= Some ms;
 			 to_appear= []} in 
 	      let rl = extract_module m in 
 	      let decls = optimize prm (decl_of_refs rl) in
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 3282880a71..28c0612c96 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -26,11 +26,14 @@ let keywords =
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; 
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_";
-    "as"; "qualified"; "hiding" ]
+    "as"; "qualified"; "hiding" ; "prop" ; "arity" ]
   Idset.empty
 
 let preamble prm =
-  let m = if prm.modular then String.capitalize prm.module_name else "Main" in
+  let m = match prm.mod_name with 
+    | None -> "Main" 
+    | Some m -> String.capitalize m 
+  in 
   [< 'sTR "module "; 'sTR m; 'sTR " where"; 'fNL; 'fNL;
      'sTR "type Prop = ()"; 'fNL;
      'sTR "prop = ()"; 'fNL; 'fNL;
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 1cbfe3a55f..7dd1316c93 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -61,8 +61,8 @@ type ml_decl =
 
 type extraction_params =  
   { lang : string; 
-    modular : bool; 
-    module_name : string; 
+    toplevel : bool; 
+    mod_name : string option; 
     to_appear : global_reference list }
 
 module type Mlpp_param = sig
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index bb139597b6..07e7f25ff9 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -505,11 +505,11 @@ let rec optimize prm = function
       let b = expand (strict_language prm.lang) r t in
       let l = if b then 
 	begin
-	  if_verbose warning_expansion r;
+	  if prm.toplevel then if_verbose warning_expansion r;
 	  List.map (subst_glob_decl r t) l
 	end
       else l in 
-      if prm.modular || List.mem r prm.to_appear || not b then 
+      if (prm.mod_name <> None) || List.mem r prm.to_appear || not b then 
 	Dglob (r,t) :: (optimize prm l)
       else
 	optimize prm l
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 862821be77..a2d79fa664 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -112,7 +112,7 @@ let keywords =
     "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
     "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
     "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
-    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ] 
+    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "prop" ; "arity" ] 
   Idset.empty
 
 let preamble _ =