Creation de Recursive Extarction Module

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

6 files changed, 104 insertions, 51 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index b8c7eeb9a..7153d652a 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -29,6 +29,13 @@ Grammar vernac vernac : ast :=
 | haskell_extr_module 
      [ "Haskell" "Extraction" "Module" identarg($m) "." ]
   -> [ (ExtractionModule "haskell" $m) ]
+| rec_extr_module 
+     [ "Recursive" "Extraction" "Module" identarg($m) "." ]
+  -> [ (RecursiveExtractionModule "ocaml" $m) ]
+| rec_haskell_extr_module 
+     [ "Haskell" "Recursive" "Extraction" "Module" identarg($m) "." ]
+  -> [ (RecursiveExtractionModule "haskell" $m) ]
+
 
 (* Custum inlining directives *)
 | inline_constant
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 5fe9264c5..fd7c3da03 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -22,12 +22,12 @@ open Nametab
 let current_module = ref None
 
 let module_of_r r = 
-  string_of_id (snd (split_dirpath (dirpath (sp_of_r r))))
+  snd (split_dirpath (dirpath (sp_of_r r)))
 
 let module_option r = 
   let m = module_of_r r in
   if Some m = !current_module then ""
-  else (String.capitalize m) ^ "."
+  else (String.capitalize (string_of_id m)) ^ "."
 
 let check_ml r d = 
   if to_inline r then 
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 00136ef93..823388f4b 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -14,6 +14,8 @@ open Names
 
 module ToplevelPp : Mlpp
 
+val module_of_r : 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 007fcf1d8..da5d0d9c1 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -20,6 +20,21 @@ open Mlutil
 open Vernacinterp
 open Common
 
+(*s [extract_module m] returns all the global reference declared in a module *)
+
+let extract_module m =
+  let m = Nametab.locate_loaded_library (Nametab.make_short_qualid m) in
+  let seg = Library.module_segment (Some m) in
+  let get_reference = function
+    | sp, Leaf o ->
+	(match Libobject.object_tag o with
+	   | "CONSTANT" | "PARAMETER" -> ConstRef sp
+	   | "INDUCTIVE" -> IndRef (sp,0)
+	   | _ -> failwith "caught")
+    | _ -> failwith "caught"
+  in
+  Util.map_succeed get_reference seg
+
 (*s Recursive computation of the global references to extract. 
     We use a set of functions visiting the extracted objects in
     a depth-first way ([visit_type], [visit_ast] and [visit_decl]).
@@ -33,73 +48,90 @@ open Common
 
 type extracted_env = {
   mutable visited : Refset.t;
-  mutable to_extract : global_reference list 
+  mutable to_extract : global_reference list;
+  mutable modules : identifier list
 }
 
-let empty () = { visited = ml_extractions (); to_extract = [] }
+let empty () = 
+  { visited = ml_extractions (); to_extract = []; modules = []}
 
-let rec visit_reference eenv r =
+let rec visit_reference m eenv r =
   let r' = match r with
     | ConstructRef ((sp,_),_) -> IndRef (sp,0)
     | IndRef (sp,i) -> if i = 0 then r else IndRef (sp,0)
     | _ -> r
   in
   if not (Refset.mem r' eenv.visited) then begin
-    (* we put [r'] in [visited] first to avoid loops in inductive defs *)
+    (* we put [r'] in [visited] first to avoid loops in inductive defs 
+       and in module extraction *)
     eenv.visited <- Refset.add r' eenv.visited;
-    visit_decl eenv (extract_declaration r);
+    if m then begin 
+      let m_name = module_of_r r' in 
+      if not (List.mem m_name eenv.modules) then begin
+	eenv.modules <- m_name :: eenv.modules;
+ 	List.iter (visit_reference m eenv) (extract_module m_name)
+      end
+    end;
+    visit_decl m eenv (extract_declaration r);
     eenv.to_extract <- r' :: eenv.to_extract
   end
-
-and visit_type eenv t =
+    
+and visit_type m eenv t =
   let rec visit = function
-    | Tglob r -> visit_reference eenv r
+    | Tglob r -> visit_reference m eenv r
     | Tapp l -> List.iter visit l
     | Tarr (t1,t2) -> visit t1; visit t2
     | Tvar _ | Tprop | Tarity -> ()
   in
   visit t
-
-and visit_ast eenv a =
+    
+and visit_ast m eenv a =
   let rec visit = function
-    | MLglob r -> visit_reference eenv r
+    | MLglob r -> visit_reference m eenv r
     | MLapp (a,l) -> visit a; List.iter visit l
     | MLlam (_,a) -> visit a
     | MLletin (_,a,b) -> visit a; visit b
-    | MLcons (r,l) -> visit_reference eenv r; List.iter visit l
+    | MLcons (r,l) -> visit_reference m eenv r; List.iter visit l
     | MLcase (a,br) -> 
-	visit a; Array.iter (fun (r,_,a) -> visit_reference eenv r; visit a) br
+	visit a; Array.iter (fun (r,_,a) -> visit_reference m eenv r; visit a) br
     | MLfix (_,_,l) -> Array.iter visit l
-    | MLcast (a,t) -> visit a; visit_type eenv t
+    | MLcast (a,t) -> visit a; visit_type m eenv t
     | MLmagic a -> visit a
     | MLrel _ | MLprop | MLarity | MLexn _ -> ()
   in
   visit a
 
-and visit_inductive eenv inds =
-  let visit_constructor (_,tl) = List.iter (visit_type eenv) tl in
+and visit_inductive m eenv inds =
+  let visit_constructor (_,tl) = List.iter (visit_type m eenv) tl in
   let visit_ind (_,_,cl) = List.iter visit_constructor cl in
   List.iter visit_ind inds
 
-and visit_decl eenv = function
+and visit_decl m eenv = function
   | Dtype (inds,_) ->
-      visit_inductive eenv inds
+      visit_inductive m eenv inds
   | Dabbrev (_,_,t) ->
-      visit_type eenv t
+      visit_type m eenv t
   | Dglob (_,a) ->
-      visit_ast eenv a
+      visit_ast m eenv a
   | Dcustom _ -> ()
-
+	
 (*s Recursive extracted environment for a list of reference: we just
     iterate [visit_reference] on the list, starting with an empty
     extracted environment, and we return the reversed list of 
-    references in the field [to_extract]. *)
+    references in the field [to_extract], and the visited_modules in 
+    case of recursive module extraction *)
 
 let extract_env rl =
   let eenv = empty () in
-  List.iter (visit_reference eenv) rl;
+  List.iter (visit_reference false eenv) rl;
   List.rev eenv.to_extract
 
+let modules_extract_env m =
+  let eenv = empty () in
+  eenv.modules <- [m];
+  List.iter (visit_reference true eenv) (extract_module m);
+  eenv.modules, List.rev eenv.to_extract
+
 (*s Extraction in the Coq toplevel. We display the extracted term in
     Ocaml syntax and we use the Coq printers for globals. The
     vernacular command is \verb!Extraction! [term]. Whenever [term] is
@@ -107,8 +139,7 @@ let extract_env rl =
 
 let refs_set_of_list l = List.fold_right Refset.add l Refset.empty 
 
-let decl_of_refs refs =
-  List.map extract_declaration (extract_env refs) 
+let decl_of_refs refs = List.map extract_declaration (extract_env refs)
 
 let local_optimize refs = 
   let prm = 
@@ -182,25 +213,12 @@ let _ =
     module [M]. We just keep constants and inductives, and we remove
     those having an ML extraction. *)
 
-let extract_module m =
-  let m = Nametab.locate_loaded_library (Nametab.make_short_qualid m) in
-  let seg = Library.module_segment (Some m) in
-  let get_reference = function
-    | sp, Leaf o ->
-	(match Libobject.object_tag o with
-	   | "CONSTANT" | "PARAMETER" -> ConstRef sp
-	   | "INDUCTIVE" -> IndRef (sp,0)
-	   | _ -> failwith "caught")
-    | _ -> failwith "caught"
-  in
-  Util.map_succeed get_reference seg
-
-let decl_mem rl = function 
-  | Dglob (r,_) -> List.mem r rl 
-  | Dabbrev (r,_,_) -> List.mem r rl 
-  | Dtype ((_,r,_)::_, _) -> List.mem r rl
+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 
   | Dtype ([],_) -> false
-  | Dcustom (r,s) ->  List.mem r rl 
+  | Dcustom (r,_) ->  m = module_of_r r
 
 let file_suffix = function
   | "ocaml" -> ".ml"
@@ -212,15 +230,41 @@ let _ =
     (function 
        | [VARG_STRING lang; VARG_IDENTIFIER m] ->
 	   (fun () -> 
-	      let ms = Names.string_of_id m in
-	      let f = (String.uncapitalize ms) ^ (file_suffix lang) in
+	      let f = (String.uncapitalize (string_of_id m))
+		       ^ (file_suffix lang) in
 	      let prm = {lang=lang;
 			 toplevel=false;
-			 mod_name= Some ms;
+			 mod_name= Some m;
 			 to_appear= []} in 
 	      let rl = extract_module m in 
 	      let decls = optimize prm (decl_of_refs rl) in
 	      let decls = add_ml_decls prm decls in 
-	      let decls = List.filter (decl_mem rl) decls in
+	      let decls = List.filter (decl_in_m m) decls in
 	      extract_to_file f prm decls)
        | _ -> assert false)
+
+
+let _ = 
+  vinterp_add "RecursiveExtractionModule"
+        (function 
+       | [VARG_STRING lang; VARG_IDENTIFIER m] ->
+	   (fun () -> 
+	      let modules,refs = modules_extract_env m in 
+	      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
+	      List.iter 
+		(fun m ->
+		   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 decls = List.filter (decl_in_m m) decls in
+		   extract_to_file f prm decls)
+		modules)
+       | _ -> assert false)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index f3d64fcee..cb1ac038d 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -32,7 +32,7 @@ let keywords =
 let preamble prm =
   let m = match prm.mod_name with 
     | None -> "Main" 
-    | Some m -> String.capitalize m 
+    | Some m -> String.capitalize (string_of_id m) 
   in 
   [< 'sTR "module "; 'sTR m; 'sTR " where"; 'fNL; 'fNL;
      'sTR "type Prop = ()"; 'fNL;
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 35cd8a592..125bf7865 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -62,7 +62,7 @@ type ml_decl =
 type extraction_params =  
   { lang : string; 
     toplevel : bool; 
-    mod_name : string option; 
+    mod_name : identifier option; 
     to_appear : global_reference list }
 
 module type Mlpp_param = sig