travail sur le Extract Constant

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

8 files changed, 166 insertions, 69 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index bfe459b18d..f32b3e96db 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -36,6 +36,11 @@ Grammar vernac vernac : ast :=
      [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
   -> [ (EXTRACT_CONSTANT $x $y) ]
 
+| extract_inlined_constant 
+     [ "Extract" "Inlined" "Constant" qualidarg($x) 
+      "=>" idorstring($y) "." ]
+  -> [ (EXTRACT_INLINED_CONSTANT $x $y) ]
+
 | extract_inductive 
      [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."]
   -> [ (EXTRACT_INDUCTIVE $x $y) ]
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index ba4c4a6163..4099b5163e 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -201,12 +201,17 @@ let _ =
   vinterp_add "ExtractionFile"
     (function 
        | VARG_STRING lang :: VARG_VARGLIST o :: VARG_STRING f :: vl ->
-	   let refs = refs_of_vargl vl in
-	   let prm = interp_options lang refs false "" o in
 	   (fun () -> 
+	      let refs = refs_of_vargl vl in
+	      let prm = interp_options lang refs false "" o in
 	      let decls = decl_of_refs refs in 
 	      let decls = optimize prm decls in
-	      extract_to_file lang f prm decls)
+	      let ml_decls = 
+		list_subtract 
+		  (List.filter is_ml_extraction refs)
+		  (fst (ml_cst_extractions ()))
+	      in
+	      extract_to_file lang f prm decls ml_decls)
        | _ -> assert false)
 
 (*s Extraction of a module. The vernacular command is \verb!Extraction Module!
@@ -250,5 +255,5 @@ let _ =
 	      let rl = extract_module m in 
 	      let decls = optimize prm (decl_of_refs rl) in
 	      let decls = List.filter (decl_mem rl) decls in
-	      extract_to_file lang f prm decls)
+	      extract_to_file lang f prm decls [])
        | _ -> assert false)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 98ea283c71..057767f5e6 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
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 8e09da5c4c..77bea2b8b5 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -12,5 +12,7 @@
 
 open Miniml
 open Mlutil
+open Term
 
-val extract_to_file : string -> extraction_params -> ml_decl list -> unit
+val extract_to_file : 
+  string -> extraction_params -> ml_decl list -> global_reference list -> unit
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 2d0e96a2fc..63a8e11f9d 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -406,7 +406,6 @@ let rec optimize prm = function
       else
 	optimize prm l
 
-
 (*s Table for direct ML extractions. *)
 
 module Refmap = 
@@ -445,6 +444,29 @@ let _ = declare_summary "ML extractions"
 	    init_function = (fun () -> extractions := empty_extractions);
 	    survive_section = true }
 
+(*s List of Extract Constant directives *)
+
+let cst_extractions = ref ([],[])
+
+let ml_cst_extractions () = !cst_extractions
+
+let add_ml_cst_extraction r s = 
+  let l,l' = !cst_extractions in 
+  cst_extractions := r::l,s::l'
+
+let (in_ml_cst_extraction,_) = 
+  declare_object ("ML constants extractions",
+		  { cache_function = (fun (_,(r,s)) -> add_ml_cst_extraction r s);
+		    load_function = (fun (_,(r,s)) -> add_ml_cst_extraction r s);
+		    open_function = (fun _ -> ());
+		    export_function = (fun x -> Some x) })
+
+let _ = declare_summary "ML constants extractions"
+	  { freeze_function = (fun () -> !cst_extractions);
+	    unfreeze_function = ((:=) cst_extractions);
+	    init_function = (fun () -> cst_extractions := [],[]);
+	    survive_section = true }
+
 (*s Grammar entries. *)
 
 open Vernacinterp
@@ -466,6 +488,27 @@ let reference_of_varg = function
 (*s \verb!Extract Constant qualid => string! *)
 
 let extract_constant r s = match r with
+  | ConstRef sp -> 
+      let rs = string_of_id (basename sp) in
+      add_anonymous_leaf (in_ml_cst_extraction (r,s));
+      add_anonymous_leaf (in_ml_extraction (r,rs))
+  | _ -> 
+      errorlabstrm "extract_constant"
+	[< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >]
+
+let _ = 
+  vinterp_add "EXTRACT_CONSTANT"
+    (function 
+       | [id; s] -> 
+	   (fun () -> 
+	      extract_constant 
+		(reference_of_varg id)
+		(string_of_varg s))
+       | _ -> assert false)
+
+(*s \verb!Extract Inlined Constant qualid => string! *)
+
+let extract_inlined_constant r s = match r with
   | ConstRef _ -> 
       add_anonymous_leaf (in_ml_extraction (r,s))
   | _ -> 
@@ -473,11 +516,13 @@ let extract_constant r s = match r with
 	[< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >]
 
 let _ = 
-  vinterp_add "EXTRACT_CONSTANT"
+  vinterp_add "EXTRACT_INLINED_CONSTANT"
     (function 
        | [id; s] -> 
 	   (fun () -> 
-	      extract_constant (reference_of_varg id) (string_of_varg s))
+	      extract_inlined_constant 
+		(reference_of_varg id) 
+		(string_of_varg s))
        | _ -> assert false)
 
 (*s \verb!Extract Inductive qualid => string [ string ... string ]! *)
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 381033a016..1e85212832 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -66,3 +66,8 @@ val is_ml_extraction : global_reference -> bool
 val find_ml_extraction : global_reference -> string
 
 val ml_extractions : unit -> Refset.t
+
+(* List of Extract Constant directives *)
+
+val ml_cst_extractions : 
+  unit -> global_reference list * string list
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index e1061423f8..2d983fab55 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -18,6 +18,8 @@ open Miniml
 open Mlutil
 open Options
 
+let current_module = ref None
+
 (*s Some utility functions. *)
 
 let string s = [< 'sTR s >]
@@ -78,6 +80,27 @@ let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
 let rename_lower_global id = rename_global (lowercase_id id)
 let rename_upper_global id = rename_global (uppercase_id id)
 
+(*s Modules considerations *)
+
+let sp_of_r r = match r with 
+    | ConstRef sp -> sp
+    | IndRef (sp,_) -> sp
+    | ConstructRef ((sp,_),_) -> sp
+    | _ -> assert false
+
+let module_of_r r = list_last (dirpath (sp_of_r r))
+
+let string_of_r r = string_of_id (basename (sp_of_r r))
+
+let module_option r = 
+  let m = module_of_r r in
+  if Some m = !current_module then ""
+  else (String.capitalize (string_of_id m)) ^ "."
+
+let check_ml r d = 
+  try find_ml_extraction r
+  with Not_found -> d
+
 (*s de Bruijn environments for programs *)
 
 type env = identifier list * Idset.t
@@ -126,12 +149,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. *)
@@ -375,8 +394,6 @@ let rename_type_global r =
        let id = Environ.id_of_global (Global.env()) r in
        rename_lower_global id)
 
-let pp_type_global r = pr_id (rename_type_global r)
-
 let rename_global r = 
   cache r
     (fun r -> 
@@ -385,7 +402,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
 
@@ -395,7 +416,7 @@ module MonoPp = Make(MonoParams)
 
 (*s Renaming issues in a modular extraction. *)
 
-let current_module = ref None
+
 
 module ModularParams = struct
 
@@ -415,34 +436,23 @@ module ModularParams = struct
     else 
       string_of_id id
 
-  let qualify_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
-    if Some m = !current_module then s 
-    else (String.capitalize (string_of_id m)) ^ "." ^ s
-
-  let rename_qualified_type_global r = 
+  let rename_type_global r = 
     let id = Environ.id_of_global (Global.env()) r in 
-    qualify_global r (rename_lower id)
+    rename_lower id
 
-  let rename_global_to_string r = 
+  let rename_global_aux r = 
     let id = Environ.id_of_global (Global.env()) r in 
     match r with
       | ConstructRef _ -> rename_upper id
       | _ -> rename_lower id
 
-  let rename_global r = id_of_string (rename_global_to_string r)
+  let rename_global r = id_of_string (rename_global_aux r)
 
-  let rename_qualified_global r = 
-    qualify_global r (rename_global_to_string r)
- 
-  let pp_type_global r = string (rename_qualified_type_global r)
-  let pp_global r = string (rename_qualified_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
@@ -457,11 +467,23 @@ let ocaml_preamble () =
      'sTR "type arity = unit"; 'fNL;
      'sTR "let arity = ()"; 'fNL; 'fNL >]
 
-let extract_to_file f prm decls =
+
+let ocaml_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 "let "; '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 (ocaml_preamble ()));
+  ocaml_header ft prm.modular ml_decls;
   begin 
     try
       List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 6ab76aded6..e1325d4814 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -13,6 +13,7 @@
 open Pp
 open Miniml
 open Names
+open Term
 
 val string : string -> std_ppcmds
 val open_par : bool -> std_ppcmds
@@ -24,6 +25,14 @@ val push_vars : identifier list -> identifier list * Idset.t ->
 
 val current_module : identifier option ref
 
+val module_of_r : global_reference -> module_ident
+
+val string_of_r : global_reference -> string
+
+val check_ml : global_reference -> string -> string
+
+val module_option : global_reference -> string
+
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
     declarations to a file. *)
@@ -33,6 +42,7 @@ open Mlutil
 module Make : functor(P : Mlpp_param) -> Mlpp
 
 val current_module : Names.identifier option ref
-val extract_to_file : string -> extraction_params -> ml_decl list -> unit
+val extract_to_file : 
+  string -> extraction_params -> ml_decl list -> global_reference list -> unit