extraction: translation and pretty-print separated

in preparation of command-line option --mono

Makefile.in

@@ -177,7 +177,7 @@ LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer dri
              parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
 
 LIB_MLW = ity expr dexpr pdecl eval_match vc pmodule \
-          pinterp pdriver cprinter compile ocaml_printer
+          pinterp compile pdriver cprinter ocaml_printer
 
 LIB_PARSER = ptree glob typing parser lexer
 

src/mlw/compile.ml

@@ -211,6 +211,8 @@ module ML = struct
 
 end
 
+type decl = ML.decl
+
 type info = {
   info_syn          : syntax_map;
   info_convert      : syntax_map;

src/mlw/cprinter.ml

@@ -79,10 +79,11 @@ let fg ?fname m =
 
 open Format
 
-let pr args ?old ?fname fmt m =
+let pr args ?old ?fname m fmt d =
   ignore(args);
   ignore(old);
   ignore(m);
+  ignore(d);
   ignore(fname);
   fprintf fmt "#include <stdio.h>\n\
 \n\

src/mlw/ocaml_printer.ml

@@ -448,7 +448,7 @@ module Print = struct
         print_ident xs.xs_name (print_ty ~paren:true info) t
 end
 
-let extract_module pargs ?old ?fname fmt ({mod_theory = th} as m) =
+let extract_module pargs ?old ?fname ({mod_theory = th} as m) fmt d =
   ignore (pargs);
   ignore (old);
   ignore (m);
@@ -461,12 +461,7 @@ let extract_module pargs ?old ?fname fmt ({mod_theory = th} as m) =
     info_mo_known_map = m.mod_known;
     info_fname        = Opt.map Compile.clean_name fname
   } in
-  fprintf fmt
-    "(* This file has been generated from Why3 module %a *)@\n@\n"
-    Print.print_module_name m;
-  let mdecls = Translate.module_ info m in
-  let mdecls = Transform.module_ info mdecls in
-  print_list nothing (Print.print_decl info) fmt mdecls;
+  Print.print_decl info fmt d;
   fprintf fmt "@."
 
 let fg ?fname m =

src/mlw/pdriver.ml

@@ -220,7 +220,9 @@ open Stdlib
 
 type filename_generator = ?fname:string -> Pmodule.pmodule -> string
 
-type printer = printer_args -> ?old:in_channel -> ?fname:string -> Pmodule.pmodule Pp.pp
+type printer =
+  printer_args -> ?old:in_channel -> ?fname:string -> Pmodule.pmodule ->
+  Compile.decl Pp.pp
 
 type reg_printer = Pp.formatted * filename_generator * printer
 

src/mlw/pdriver.mli

@@ -37,12 +37,14 @@ val load_driver : Env.env -> string -> string list -> driver
       @param string driver file name
       @param string list additional drivers containing only theories/modules *)
 
-type printer = printer_args -> ?old:in_channel -> ?fname:string -> Pmodule.pmodule Pp.pp
-(* type printer = printer_args -> ?old:in_channel -> ?mono:bool -> Compile.ML.decl Pp.pp *)
+type printer =
+  printer_args -> ?old:in_channel -> ?fname:string -> Pmodule.pmodule ->
+  Compile.decl Pp.pp
 
 type filename_generator = ?fname:string -> Pmodule.pmodule -> string
 
-val register_printer : desc:Pp.formatted -> string -> filename_generator -> printer -> unit
+val register_printer :
+  desc:Pp.formatted -> string -> filename_generator -> printer -> unit
 
 val lookup_printer : driver -> filename_generator * printer_args * printer
 

src/tools/why3extract.ml

@@ -13,6 +13,7 @@ open Format
 open Why3
 open Stdlib
 open Pmodule
+open Compile
 
 let usage_msg = sprintf
   "Usage: %s [options] -D <driver> -o <dir> [[file|-] [-T <theory>]...]..."
@@ -27,7 +28,6 @@ let add_opt_file x =
   Queue.push (Some x, tlist) opt_queue;
   opt_input := Some tlist
 
-(* TODO : rename theory into module, -T into -M *)
 let add_opt_theory x =
   let l = Strings.split '.' x in
   let p, t = match List.rev l with
@@ -36,7 +36,7 @@ let add_opt_theory x =
   in
   match !opt_input, p with
   | None, [] ->
-      eprintf "Option '-T'/'--theory' with a non-qualified \
+      eprintf "Option '-M'/'--module' with a non-qualified \
         argument requires an input file.@.";
       exit 1
   | Some tlist, [] ->
@@ -50,15 +50,21 @@ let add_opt_theory x =
 let opt_parser = ref None
 let opt_output = ref None
 let opt_driver = ref []
-let opt_recurs = ref false
+type extraction_mode = Monolithic | Recursive | SingleModule
+let opt_recurs = ref SingleModule
 
 let option_list = [
   "-", Arg.Unit (fun () -> add_opt_file "-"),
       " read the input file from stdin";
+  (* TODO: -T/--theory should disappear *)
   "-T", Arg.String add_opt_theory,
       "<theory> select <theory> in the input file or in the library";
   "--theory", Arg.String add_opt_theory,
       " same as -T";
+  "-M", Arg.String add_opt_theory,
+      "<module> select <module> in the input file or in the library";
+  "--module", Arg.String add_opt_theory,
+      " same as -M";
   "-F", Arg.String (fun s -> opt_parser := Some s),
       "<format> select input format (default: \"why\")";
   "--format", Arg.String (fun s -> opt_parser := Some s),
@@ -67,10 +73,12 @@ let option_list = [
       "<file> specify an extraction driver";
   "--driver", Arg.String (fun s -> opt_driver := s::!opt_driver),
       " same as -D";
-  "--recursive", Arg.Unit (fun () -> opt_recurs := true),
-      " perform recursive extraction ";
+  "--recursive", Arg.Unit (fun () -> opt_recurs := Recursive),
+      " perform a recursive extraction";
+  "--mono", Arg.Unit (fun () -> opt_recurs := Monolithic),
+      " perform a monolithic extraction";
   "-o", Arg.String (fun s -> opt_output := Some s),
-      "<dir> print the selected goals to separate files in <dir>";
+      "<file|dir> destination of extracted code";
   "--output", Arg.String (fun s -> opt_output := Some s),
       " same as -o" ]
 
@@ -81,12 +89,20 @@ let () =
   if Queue.is_empty opt_queue then
     Whyconf.Args.exit_with_usage option_list usage_msg
 
+let opt_recurs = !opt_recurs
+
+(* FIXME: accept --mono without -o and use to standard output *)
 let opt_output =
-  match !opt_output with
-  | None ->
-    eprintf "Output directory (-o) is required.@.";
-    exit 1
-  | Some d -> d
+  match !opt_output, opt_recurs with
+  | None, Monolithic ->
+    eprintf "Output file (-o) is required.@."; exit 1
+  | None, (Recursive | SingleModule) ->
+    eprintf "Output directory (-o) is required.@."; exit 1
+  | Some d, (Recursive | SingleModule) when not (Sys.file_exists d) ->
+    eprintf "%s: no such directory.@." d; exit 1
+  | Some d, (Recursive | SingleModule) when not (Sys.is_directory d) ->
+    eprintf "%s: not a directory.@." d; exit 1
+  | Some d, _ -> d
 
 let driver_file s =
   if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
@@ -103,23 +119,36 @@ let opt_driver =
     eprintf "%a@." Exn_printer.exn_printer e;
     exit 1
 
-let opt_recurs = !opt_recurs
-
-let extract_to ?fname m =
+let extract_to ?fname ({mod_theory = th} as m) =
   let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in
-  let file = Filename.concat opt_output (fg ?fname m) in
-  let old =
-    if Sys.file_exists file then begin
-      let backup = file ^ ".bak" in
-      Sys.rename file backup;
-      Some (open_in backup)
-    end else None in
-  let cout = open_out file in
-  let fmt = formatter_of_out_channel cout in
-  let tname = m.mod_theory.Theory.th_name.Ident.id_string in
-  Debug.dprintf Pdriver.debug "extract module %s to file %s@." tname file;
-  pr ?old ?fname pargs fmt m;
-  close_out cout
+  let info = {
+    info_syn          = pargs.Pdriver.syntax;
+    info_convert      = pargs.Pdriver.converter;
+    info_current_th   = th;
+    info_current_mo   = Some m;
+    info_th_known_map = th.Theory.th_known;
+    info_mo_known_map = m.mod_known;
+    info_fname        = Opt.map Compile.clean_name fname
+  } in
+  let mdecls = Translate.module_ info m in
+  let mdecls = Transform.module_ info mdecls in
+  match opt_recurs with
+  | Recursive | SingleModule ->
+    let file = Filename.concat opt_output (fg ?fname m) in
+    let old =
+      if Sys.file_exists file then begin
+        let backup = file ^ ".bak" in
+        Sys.rename file backup;
+        Some (open_in backup)
+      end else None in
+    let cout = open_out file in
+    let fmt = formatter_of_out_channel cout in
+    let tname = m.mod_theory.Theory.th_name.Ident.id_string in
+    Debug.dprintf Pdriver.debug "extract module %s to file %s@." tname file;
+    List.iter (pr ?old ?fname pargs m fmt) mdecls;
+    close_out cout
+  | Monolithic ->
+    ()
 
 let extract_to =
   let visited = Ident.Hid.create 17 in
@@ -131,7 +160,8 @@ let extract_to =
     end
 
 let rec use_iter f l =
-  List.iter (function Uuse t -> f t | Uscope (_,_,l) -> use_iter f l | _ -> ()) l
+  List.iter
+    (function Uuse t -> f t | Uscope (_,_,l) -> use_iter f l | _ -> ()) l
 
 let rec do_extract_module ?fname m =
   let extract_use m' =
@@ -140,7 +170,10 @@ let rec do_extract_module ?fname m =
     in
     do_extract_module ?fname m'
   in
-  if opt_recurs then use_iter extract_use m.mod_units;
+  begin match opt_recurs with
+  | Recursive | Monolithic -> use_iter extract_use m.mod_units
+  | SingleModule -> ()
+  end;
   extract_to ?fname m
 
 let do_global_extract (_,p,t) =
@@ -149,6 +182,13 @@ let do_global_extract (_,p,t) =
   do_extract_module m
 
 let do_extract_module_from fname mm (tname,_,t) =
+(*
+  fprintf fmt
+    "(* This file has been generated from Why3 module %a *)@\n@\n"
+    Print.print_module_name m;
+  let mdecls = Translate.module_ info m in
+  let mdecls = Transform.module_ info mdecls in
+*)
   try
     let m = Mstr.find t mm in do_extract_module ~fname m
   with Not_found ->
@@ -178,9 +218,25 @@ let do_input = function
     do_local_extract fname cin tlist;
     close_in cin
 
+(*
+let visited = Hid.create (1 lsl 20)
+let toextract = ref []
+
+let rec visit id =
+  if not (Hid.mem id visited) then begin
+    let d = Hid.find Compile.knownmap id in
+    ML.iter_deps visit d;
+    Hid.add visited id ();
+    toextract := id :: !toextract
+  end
+*)
+
 let () =
   try
     Queue.iter do_input opt_queue;
+    begin match opt_recurs with
+    | Monolithic -> assert false (*TODO*)
+    | Recursive | SingleModule -> () end
   with e when not (Debug.test_flag Debug.stack_trace) ->
     eprintf "%a@." Exn_printer.exn_printer e;
     exit 1