Code extraction (wip)

Empty extracted modules (all definitions are defined in the driver)
are printed no more, independently of the extraction mode

examples/leftist_heap.mlw

@@ -114,7 +114,7 @@ module LeftistHeap
   type t = tree elt
 
   (* [e] is no greater than the root of [h], if any *)
-  let predicate le_root (e: elt) (h: t) = match h with
+  predicate le_root (e: elt) (h: t) = match h with
     | E -> true
     | N _ _ x _ -> le e x
     end

src/mlw/compile.ml

@@ -842,39 +842,6 @@ module Transform = struct
     | Dtype _ | Dexn _ as d -> d
     | Dlet def -> Dlet (let_def info Mpv.empty def)
 
-  (* let pdecl, module_ = *)
-  (*   let mod_known = ref Mid.empty in *)
-  (*   let pdecl info = function *)
-  (*     | (Dtype itdefl) as decl -> *)
-  (*       let add {its_name = id} = mod_known := Mid.add id decl !mod_known in *)
-  (*       List.iter add itdefl; *)
-  (*       decl *)
-  (*     | Dexn (xs, _) as decl -> *)
-  (*       mod_known := Mid.add xs.xs_name decl !mod_known; *)
-  (*       decl *)
-  (*     | Dlet (Lvar (pv, e)) -> *)
-  (*       let let_var = Lvar (pv, expr info Mpv.empty e) in *)
-  (*       let decl = Dlet let_var in *)
-  (*       mod_known := Mid.add pv.pv_vs.vs_name decl !mod_known; *)
-  (*       decl *)
-  (*     | Dlet (Lsym (rs, res, args, e)) -> *)
-  (*       let let_sym = Lsym (rs, res, args, expr info Mpv.empty e) in *)
-  (*       let decl = Dlet let_sym in *)
-  (*       mod_known := Mid.add rs.Expr.rs_name decl !mod_known; *)
-  (*       decl *)
-  (*     | Dlet (Lrec rl) -> *)
-  (*       let let_rec = Lrec (List.map (rdef info Mpv.empty) rl) in *)
-  (*       let decl = Dlet let_rec in *)
-  (*       List.iter (fun {rec_sym = rs} -> *)
-  (*           mod_known := Mid.add rs.Expr.rs_name decl !mod_known) rl; *)
-  (*       decl in *)
-  (*   let module_ info m = *)
-  (*     let mod_decl = List.map (pdecl info) m.mod_decl in *)
-  (*     let r = { mod_decl = mod_decl; mod_known = !mod_known } in *)
-  (*     mod_known := Mid.empty; *)
-  (*     r in *)
-  (*   pdecl, module_ *)
-
   let module_ info m =
     let mod_decl = List.map (pdecl info) m.mod_decl in
     let add known_map decl =

src/mlw/ocaml_printer.ml

@@ -269,8 +269,8 @@ module Print = struct
       | [], [] ->
         (print_uident info) fmt rs.rs_name
       | [], tl ->
-        fprintf fmt "@[<hov 2>%a (%a)@]"
-          print_ident rs.rs_name (print_list comma (print_expr info)) tl
+        fprintf fmt "@[<hov 2>%a (%a)@]" (print_uident info) rs.rs_name
+          (print_list comma (print_expr info)) tl
       | pjl, tl ->
         fprintf fmt "@[<hov 2>{ %a}@]"
           (print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl)
@@ -466,8 +466,9 @@ module Print = struct
   let print_decl info fmt decl =
     let decl_name = get_decl_name decl in
     let decide_print id =
-      if query_syntax info.info_syn id = None then
-        print_decl info fmt decl in
+      if query_syntax info.info_syn id = None then begin
+        print_decl info fmt decl;
+        fprintf fmt "@." end in
     List.iter decide_print decl_name
 
 end
@@ -484,8 +485,7 @@ let print_decl pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d =
     info_fname        = Opt.map Compile.clean_name fname;
     flat              = flat;
   } in
-  Print.print_decl info fmt d;
-  fprintf fmt "@."
+  Print.print_decl info fmt d
 
 let fg ?fname m =
   let mod_name = m.mod_theory.th_name.id_string in

src/tools/why3extract.ml

@@ -137,11 +137,17 @@ let get_cout_old ?fname fg m = match opt_output with
 
 let print_mdecls ?fname m mdecls =
   let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in
-  let cout, old = get_cout_old fg m ?fname in
-  let fmt = formatter_of_out_channel cout in
-  let flat = opt_modu_flat = Flat in
-  List.iter (pr pargs ?old ?fname ~flat m fmt) mdecls;
-  if cout <> stdout then close_out cout
+  let test_decl_not_driver decl =
+    let decl_name = ML.get_decl_name decl in
+    let test_id_not_driver id =
+      Printer.query_syntax pargs.Pdriver.syntax id = None in
+    List.exists test_id_not_driver decl_name in
+  if List.exists test_decl_not_driver mdecls then begin
+    let cout, old = get_cout_old fg m ?fname in
+    let fmt = formatter_of_out_channel cout in
+    let flat = opt_modu_flat = Flat in
+    List.iter (pr pargs ?old ?fname ~flat m fmt) mdecls;
+    if cout <> stdout then close_out cout end
 
 let find_module_path mm path m = match path with
   | [] ->
@@ -308,15 +314,15 @@ let () =
       let (_fg, pargs, pr) = Pdriver.lookup_printer opt_driver in
       let mm = Mstr.empty in
       let cout = match opt_output with
-          | None -> stdout
-          | Some file -> open_out file in
+        | None -> stdout
+        | Some file -> open_out file in
       let fmt = formatter_of_out_channel cout in
-      let extract id =
+      let extract fmt id =
         let pm = find_module_id mm id in
         let m = translate_module pm in
         let d = Ident.Mid.find id m.ML.mod_known in
         pr pargs ~flat:true pm fmt d in
-      List.iter extract (List.rev !toextract);
+      List.iter (extract fmt) (List.rev !toextract);
       if cout <> stdout then close_out cout
   with e when not (Debug.test_flag Debug.stack_trace) ->
     eprintf "%a@." Exn_printer.exn_printer e;