travail sur le Extract Constant

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

1 files changed, 32 insertions, 29 deletions

diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 98ea283c7..057767f5e 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -103,12 +103,8 @@ let pr_binding = function
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_reference f r = 
-  try let s = find_ml_extraction r in [< 'sTR s >]
-  with Not_found -> f r
- 
-let pp_type_global = pp_reference P.pp_type_global
-let pp_global = pp_reference P.pp_global
+let pp_type_global = P.pp_type_global
+let pp_global = P.pp_global
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
@@ -338,8 +334,6 @@ let rename_type_global r =
        let id = Environ.id_of_global (Global.env()) r in
        rename_upper_global id)
 
-let pp_type_global r = pr_id (rename_type_global r)
-
 let rename_global r = 
   cache r
     (fun r -> 
@@ -348,7 +342,11 @@ let rename_global r =
 	 | ConstructRef _ -> rename_upper_global id
 	 | _ -> rename_lower_global id)
 
-let pp_global r = pr_id (rename_global r)
+let pp_type_global r = 
+  string (check_ml r (string_of_id (rename_type_global r)))
+
+let pp_global r = 
+  string (check_ml r (string_of_id (rename_global r)))
 
 let cofix_warning = true
 
@@ -376,30 +374,23 @@ module ModularParams = struct
     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 Some m = !current_module then s
-      else (String.capitalize (string_of_id m)) ^ "." ^ s)
-
-  let rename_type_global r = 
+ let rename_type_global r = 
     let id = Environ.id_of_global (Global.env()) r in 
-    id_of_global r (rename_upper id)
+    rename_lower id
 
-  let rename_global r = 
+  let rename_global_aux 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)
+      | ConstructRef _ -> rename_upper id
+      | _ -> rename_lower id
+
+  let rename_global r = id_of_string (rename_global_aux r)
 
-  let pp_type_global r = pr_id (rename_type_global r)
-  let pp_global r = pr_id (rename_global r)
+  let pp_type_global r = 
+    string ((module_option r)^(check_ml r (rename_type_global r)))
+
+  let pp_global r = 
+    string ((module_option r)^(check_ml r (rename_global_aux r)))
 
   let cofix_warning = true
 end
@@ -416,11 +407,23 @@ let haskell_preamble prm =
      'sTR "type Arity = ()"; 'fNL;
      'sTR "arity = ()"; 'fNL; 'fNL >]
 
-let extract_to_file f prm decls =
+let haskell_header ft b ml_decls =
+  let l,l' = ml_cst_extractions () in
+  List.iter2 
+    (fun r s -> 
+       if (not b) or (Some (module_of_r r) = !current_module)  then 
+       pP_with ft (hV 0  
+	 [< 'sTR (string_of_r r); 'sTR " ="; 'sPC; 'sTR s; 'fNL ; 'fNL >]))
+    ((List.rev l) @ ml_decls)
+    ((List.rev l') @ (List.map find_ml_extraction ml_decls))
+
+
+let extract_to_file f prm decls ml_decls=
   let pp_decl = if prm.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 (haskell_preamble prm));
+  haskell_header ft prm.modular ml_decls;
   begin 
     try
       List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls