setting up the command line for program extraction

note: program extraction IS NOT yet implemented

Makefile.in

@@ -364,7 +364,7 @@ install_no_local::
 ########
 
 PGM_FILES = pgm_ttree pgm_types pgm_pretty \
-	    pgm_module pgm_wp pgm_typing pgm_ocaml pgm_main
+	    pgm_module pgm_wp pgm_typing pgm_main
 
 PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
 
@@ -392,7 +392,7 @@ clean::
 ########
 
 MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
-	    mlw_dtree mlw_dty mlw_typing mlw_main
+	    mlw_dtree mlw_dty mlw_typing mlw_ocaml mlw_main
 
 MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))
 
@@ -422,6 +422,9 @@ clean::
 src/main.cmo: src/why3.cma
 src/main.cmx: src/why3.cmxa
 
+src/main.cmo src/main.cmx: INCLUDES += -I src/whyml
+src/main.dep: DEPFLAGS += -I src/whyml
+
 byte: bin/why3.byte
 opt:  bin/why3.opt
 
@@ -441,6 +444,12 @@ install_no_local::
 
 install_local: bin/why3
 
+ifneq "$(MAKECMDGOALS)" "clean"
+include src/main.dep
+endif
+
+depend: src/main.dep
+
 clean::
 	rm -f src/main.cm[iox] src/main.annot src/main.o
 	rm -f bin/why3.byte bin/why3.opt bin/why3

src/main.ml

@@ -103,6 +103,7 @@ let opt_memlimit = ref None
 let opt_command = ref None
 let opt_task = ref None
 let opt_realize = ref false
+let opt_extract = ref false
 let opt_bisect = ref false
 
 let opt_print_libdir = ref false
@@ -178,6 +179,10 @@ let option_list = Arg.align [
       " same as -o";
   "--realize", Arg.Set opt_realize,
       " Realize selected theories from the library";
+  "-E", Arg.Set opt_extract,
+      " Generate OCaml code for selected theories/modules from the library";
+  "--extract", Arg.Set opt_extract,
+      " same as -E";
   "--bisect", Arg.Set opt_bisect,
       " Reduce the set of needed axioms which prove a goal, \
         and output the resulting task";
@@ -300,11 +305,14 @@ let () = try
     exit 1
   end;
 
+  if !opt_output <> None
+  && !opt_driver = None && !opt_prover = None && not !opt_extract then begin
+    eprintf
+      "Option '-o'/'--output' requires a prover, a driver, or option '-E'.@.";
+    exit 1
+  end;
+
   if !opt_prover = None then begin
-    if !opt_driver = None && !opt_output <> None then begin
-      eprintf "Option '-o'/'--output' requires a prover or a driver.@.";
-      exit 1
-    end;
     if !opt_timelimit <> None then begin
       eprintf "Option '-t'/'--timelimit' requires a prover.@.";
       exit 1
@@ -321,6 +329,12 @@ let () = try
       opt_print_theory := true
   end;
 
+  if !opt_extract && !opt_output = None then begin
+    eprintf
+      "Option '-E'/'--extract' require a directory to output the result.@.";
+    exit 1
+  end;
+
   if !opt_bisect && !opt_output = None then begin
     eprintf "Option '--bisect' require a directory to output the result.@.";
     exit 1
@@ -505,12 +519,81 @@ let do_local_theory env drv fname m (tname,_,t,glist) =
   in
   do_theory env drv fname tname th glist
 
+(* program extraction *)
+
+let do_extract_theory _env tname th _glist =
+  printf "do_extract_theory: tname=%s th_path=%a@." tname
+    (Pp.print_list Pp.dot Format.pp_print_string) th.th_path
+
+let do_extract_module _env tname m _glist =
+  printf "do_extract_module: tname=%s th_path=%a@." tname
+    (Pp.print_list Pp.dot Format.pp_print_string)
+    m.Mlw_module.mod_theory.th_path
+
+let do_global_extract env (tname,p,t,glist) =
+  try
+    let lib = Mlw_main.library_of_env env in
+    let mm, thm = Env.read_lib_file lib p in
+    try
+      let m = Mstr.find t mm in
+      do_extract_module env tname m glist
+    with Not_found ->
+      let th = Mstr.find t thm in
+      do_extract_theory env tname th glist
+  with Env.LibFileNotFound _ | Not_found -> try
+    let format = Util.def_option "why" !opt_parser in
+    let th = Env.read_theory ~format env p t in
+    do_extract_theory env tname th glist
+  with Env.LibFileNotFound _ | Env.TheoryNotFound _ ->
+    eprintf "Theory/module '%s' not found.@." tname;
+    exit 1
+
+let do_extract_theory_from env fname m (tname,_,t,glist) =
+  let th = try Mstr.find t m with Not_found ->
+    eprintf "Theory '%s' not found in file '%s'.@." tname fname;
+    exit 1
+  in
+  do_extract_theory env tname th glist
+
+let do_extract_module_from env fname mm thm (tname,_,t,glist) =
+  try
+    let m = Mstr.find t mm in do_extract_module env tname m glist
+  with Not_found -> try
+    let th = Mstr.find t thm in do_extract_theory env tname th glist
+  with Not_found ->
+    eprintf "Theory/module '%s' not found in file '%s'.@." tname fname;
+    exit 1
+
+let do_local_extract env fname cin tlist =
+  if !opt_parser = Some "whyml" || Filename.check_suffix fname ".mlw" then begin
+    let lib = Mlw_main.library_of_env env in
+    let mm, thm = Mlw_main.read_channel lib [] fname cin in
+    if Queue.is_empty tlist then begin
+      let glist = Queue.create () in
+      let do_m t m thm = do_extract_module env t m glist; Mstr.remove t thm in
+      let thm = Mstr.fold do_m mm thm in
+      Mstr.iter (fun t th -> do_extract_theory env t th glist) thm
+    end else
+      Queue.iter (do_extract_module_from env fname mm thm) tlist
+  end else begin
+    let m = Env.read_channel ?format:!opt_parser env fname cin in
+    if Queue.is_empty tlist then
+      let glist = Queue.create () in
+      let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
+      let do_th _ (t,th) = do_extract_theory env t th glist in
+      Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
+    else
+      Queue.iter (do_extract_theory_from env fname m) tlist
+  end
+
 let total_annot_tokens = ref 0
 let total_program_tokens = ref 0
 
 let do_input env drv = function
   | None, _ when !opt_parse_only || !opt_type_only ->
       ()
+  | None, tlist when !opt_extract ->
+      Queue.iter (do_global_extract env) tlist
   | None, tlist ->
       Queue.iter (do_global_theory env drv) tlist
   | Some f, tlist ->
@@ -518,24 +601,24 @@ let do_input env drv = function
         | "-" -> "stdin", stdin
         | f   -> f, open_in f
       in
-      if !opt_token_count then
+      if !opt_token_count then begin
         let lb = Lexing.from_channel cin in
         let a,p = Lexer.token_counter lb in
         close_in cin;
-        if a = 0 then
-          begin
-            (* hack: we assume it is a why file and not a mlw *)
-            total_annot_tokens := !total_annot_tokens + p;
-            Format.printf "File %s: %d tokens@." f p;
-          end
-        else
-          begin
-            total_program_tokens := !total_program_tokens + p;
-            total_annot_tokens := !total_annot_tokens + a;
-            Format.printf "File %s: %d tokens in annotations@." f a;
-            Format.printf "File %s: %d tokens in programs@." f p
-          end
-      else
+        if a = 0 then begin
+          (* hack: we assume it is a why file and not a mlw *)
+          total_annot_tokens := !total_annot_tokens + p;
+          Format.printf "File %s: %d tokens@." f p;
+        end else begin
+          total_program_tokens := !total_program_tokens + p;
+          total_annot_tokens := !total_annot_tokens + a;
+          Format.printf "File %s: %d tokens in annotations@." f a;
+          Format.printf "File %s: %d tokens in programs@." f p
+        end
+      end else if !opt_extract then begin
+        do_local_extract env fname cin tlist;
+        close_in cin
+      end else begin
         let m = Env.read_channel ?format:!opt_parser env fname cin in
         close_in cin;
         if !opt_type_only then
@@ -548,6 +631,7 @@ let do_input env drv = function
             Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
           else
             Queue.iter (do_local_theory env drv fname m) tlist
+      end
 
 let () =
   try

src/programs/pgm_main.ml

@@ -81,7 +81,6 @@ let add_module ?(type_only=false) env path (ltm, lmod) m =
   let uc = use_export_theory uc prelude in
   let uc = List.fold_left (Pgm_typing.decl ~wp env ltm lmod) uc m.mod_decl in
   let md = close_module uc in
-  if Debug.test_flag debug_extraction then Pgm_ocaml.extract_module path md;
   Mstr.add ("WP " ^ id.id) md.m_pure ltm, (* avoids a theory/module clash *)
   Mstr.add id.id md lmod
 

src/programs/pgm_ocaml.ml → src/whyml/mlw_ocaml.ml

@@ -27,9 +27,8 @@ open Ty
 open Term
 open Decl
 open Theory
-open Pgm_types.T
-open Pgm_ttree
-open Pgm_module
+open Mlw_expr
+open Mlw_decl
 
 (** Driver *)
 
@@ -434,9 +433,11 @@ let logic_tdecl fmt td = match td.td_node with
 let extract_theory _path _th =
   assert false (*TODO*)
 
-(** Program Expression *)
+(** Program expressions *)
 
-let rec print_expr fmt e = match e.expr_desc with
+let rec print_expr _fmt e = match e.e_node with
+  | _ -> assert false (*TODO*)
+(***
   | Elogic t ->
       print_term fmt t
   | Elocal v ->
@@ -507,10 +508,13 @@ and print_branch fmt (p, e) =
 
 and print_pattern fmt p =
   print_pat fmt p.ppat_pat
+***)
 
 (** Program Declarations *)
 
-let decl fmt = function
+let decl _fmt pd = match pd.pd_node with
+  | _ -> assert false (*TODO*)
+(***
   | Dlet (ps, e) ->
       fprintf fmt "@[<hov 2>let %a =@ %a@]"
         print_ls ps.ps_pure print_expr e
@@ -518,9 +522,11 @@ let decl fmt = function
       fprintf fmt "(* pgm let rec *)" (* TODO *)
   | Dparam ps ->
       print_param_decl fmt ps.ps_pure
+***)
 
 (** Modules *)
 
+(***
 let extract_module_to m fmt =
   (* extract all logic decls first *)
   print_list newline2 logic_tdecl fmt m.m_pure.th_decls;
@@ -540,6 +546,11 @@ let extract_module path m =
     eprintf "  to file %s@." file;
     print_in_file (extract_module_to m) file
   end
+***)
+
+let extract_module _env _pr _thpr ?old _fmt _m =
+  ignore (old);
+  assert false (*TODO*)
 
 (*
 Local Variables:

src/programs/pgm_ocaml.mli → src/whyml/mlw_ocaml.mli

@@ -20,5 +20,9 @@
 
 (* OCaml program extraction *)
 
-val extract_module: string list -> Pgm_module.t -> unit
+open Why3
+
+val extract_module:
+  Env.env -> Printer.prelude -> Printer.prelude_map ->
+  ?old:Pervasives.in_channel -> Format.formatter -> Mlw_module.modul -> unit