extraction modulaire

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

4 files changed, 99 insertions, 24 deletions

diff --git a/contrib/extraction/BUGS b/contrib/extraction/BUGS
new file mode 100644
index 0000000000..3c3345da7f
--- /dev/null
+++ b/contrib/extraction/BUGS
@@ -0,0 +1,22 @@
+
+======================================================================
+
+Coq < Extraction Module Specif.
+Anomaly: Failure "nth". Please report.
+
+======================================================================
+
+Coq < Extraction Module Datatypes.
+
+donne le code suivant :
+
+type coq_Empty_set =
+
+let coq_Empty_set_ind =
+  prop
+
+let coq_Empty_set_rec = function
+
+let coq_Empty_set_rect = function
+  
+======================================================================
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index ac9fe6563c..8cf08afb18 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -135,9 +135,6 @@ end
 
 module Pp = Ocaml.Make(ToplevelParams)
 
-let pp_ast a = Pp.pp_ast (betared_ast (uncurrify_ast a))
-let pp_decl d = Pp.pp_decl (betared_decl (uncurrify_decl d))
-
 open Vernacinterp
 
 let _ = 
@@ -149,16 +146,16 @@ let _ =
 	      match kind_of_term c with
 		(* If it is a global reference, then output the declaration *)
 		| IsConst (sp,_) -> 
-		    mSGNL (pp_decl (extract_declaration (ConstRef sp)))
+		    mSGNL (Pp.pp_decl (extract_declaration (ConstRef sp)))
 		| IsMutInd (ind,_) ->
-		    mSGNL (pp_decl (extract_declaration (IndRef ind)))
+		    mSGNL (Pp.pp_decl (extract_declaration (IndRef ind)))
 		| IsMutConstruct (cs,_) ->
-		    mSGNL (pp_decl (extract_declaration (ConstructRef cs)))
+		    mSGNL (Pp.pp_decl (extract_declaration (ConstructRef cs)))
 		(* Otherwise, output the ML type or expression *)
 		| _ ->
 		    match extract_constr (Global.env()) [] c with
 		      | Emltype (t,_,_) -> mSGNL (Pp.pp_type t)
-		      | Emlterm a -> mSGNL (pp_ast a)
+		      | Emlterm a -> mSGNL (Pp.pp_ast a)
 		      | Eprop -> message "prop")
        | _ -> assert false)
 
@@ -174,13 +171,13 @@ let _ =
   vinterp_add "ExtractionRec"
     (fun vl () ->
        let rl' = decl_of_vargl vl in
-       List.iter (fun d -> mSGNL (pp_decl d)) rl')
+       List.iter (fun d -> mSGNL (Pp.pp_decl d)) rl')
 
 let _ = 
   vinterp_add "ExtractionFile"
     (function 
        | VARG_STRING f :: vl ->
-	   (fun () -> Ocaml.extract_to_file f (decl_of_vargl vl))
+	   (fun () -> Ocaml.extract_to_file f false (decl_of_vargl vl))
        | _ -> assert false)
 
 (*s Extraction of a module. *)
@@ -204,6 +201,7 @@ let _ =
        | [VARG_IDENTIFIER m] ->
 	   (fun () -> 
 	      let m = Names.string_of_id m in
+	      Ocaml.current_module := m;
 	      let f = (String.uncapitalize m) ^ ".ml" in
-	      Ocaml.extract_to_file f (extract_module m))
+	      Ocaml.extract_to_file f true (extract_module m))
        | _ -> assert false)
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1448918499..f788d4809e 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -202,9 +202,9 @@ let rec pp_expr par env args =
 	[< open_par par; 'sTR "failwith"; 'sPC; 
 	   'qS (string_of_id id); close_par par >]
     | MLprop ->
-	string "Prop"
+	string "prop"
     | MLarity ->
-	string "Arity"
+	string "arity"
     | MLcast (a,t) ->
 	[< open_par true; pp_expr false env args a; 'sPC; 'sTR ":"; 'sPC; 
 	   pp_type t; close_par true >]
@@ -329,11 +329,14 @@ let pp_decl = function
       hOV 0 [< 'sTR "let "; 
 	       pp_function (empty_env ()) (P.pp_global r) a; 'fNL >]
 
+let pp_ast a = pp_ast (betared_ast (uncurrify_ast a))
+let pp_decl d = pp_decl (betared_decl (uncurrify_decl d))
+
 end
 
-(*s Renaming issues. *)
+(*s Renaming issues for a monolithic extraction. *)
 
-module OcamlParams = struct
+module MonoParams = struct
 
 let renamings = Hashtbl.create 97
 
@@ -361,18 +364,67 @@ let pp_global r = pr_id (rename_global r)
 
 end
 
-(*s The ocaml pretty-printing module. *)
+module MonoPp = Make(MonoParams)
+
+(*s Renaming issues in a modular extraction. *)
+
+let current_module = ref ""
+
+module ModularParams = struct
+
+  let avoid = 
+    Idset.add (id_of_string "prop")
+      (Idset.add (id_of_string "arity") ocaml_keywords)
+
+  let rename_lower id = 
+    if Idset.mem id avoid || id <> lowercase_id id then 
+      "coq_" ^ string_of_id id 
+    else 
+      string_of_id id
+
+  let rename_upper id = 
+    if Idset.mem id avoid || id <> uppercase_id id then 
+      "Coq_" ^ string_of_id id 
+    else 
+      string_of_id id
+
+  let id_of_global r s =
+    let sp = match r with
+      | ConstRef sp -> sp
+      | IndRef (sp,_) -> sp
+      | ConstructRef ((sp,_),_) -> sp
+      | _ -> assert false
+    in
+    let m = list_last (dirpath sp) in
+    id_of_string 
+      (if m = !current_module then s else (String.capitalize m) ^ "." ^ s)
+
+  let rename_type_global r = 
+    let id = Environ.id_of_global (Global.env()) r in 
+    id_of_global r (rename_lower id)
+
+  let rename_global r = 
+    let id = Environ.id_of_global (Global.env()) r in 
+    match r with
+      | ConstructRef _ -> id_of_global r (rename_upper id)
+      | _ -> id_of_global r (rename_lower id)
+
+  let pp_type_global r = pr_id (rename_type_global r)
+  let pp_global r = pr_id (rename_global r)
+end
 
-module Pp = Make(OcamlParams)
+module ModularPp = Make(ModularParams)
 
-let pp_ast a = Pp.pp_ast (betared_ast (uncurrify_ast a))
-let pp_decl d = Pp.pp_decl (betared_decl (uncurrify_decl d))
+(*s Extraction to a file. *)
 
 let ocaml_preamble () =
-  [< 'sTR "type prop = Prop"; 'fNL; 'fNL;
-     'sTR "type arity = Arity"; 'fNL; 'fNL >]
+  [< 'sTR "type prop = unit"; 'fNL;
+     'sTR "let prop = ()"; 'fNL; 'fNL;
+     'sTR "type arity = unit"; 'fNL;
+     'sTR "let arity = ()"; 'fNL; 'fNL >]
 
-let extract_to_file f decls =
+let extract_to_file f modular decls =
+  let pp_decl = if modular then ModularPp.pp_decl else MonoPp.pp_decl in
   let cout = open_out f in
   let ft = Pp_control.with_output_to cout in
   pP_with ft (hV 0 (ocaml_preamble ()));
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 2760585d18..1a0cfec0c7 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -9,13 +9,16 @@
 (*i $Id$ i*)
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
-    extraction in the Coq toplevel and a module [Pp] to be used for
-    production of Ocaml files. *)
+    extraction in the Coq toplevel and a function to extract some 
+    declarations to a file. *)
 
 open Miniml
 
 module Make : functor(P : Mlpp_param) -> Mlpp
 
-val extract_to_file : string -> ml_decl list -> unit
+(* The boolean indicates if the extraction is modular. *)
+
+val current_module : string ref
+val extract_to_file : string -> bool -> ml_decl list -> unit