Code extraction (wip)

Support for recursive extraction and qualified names

src/mlw/compile.ml

@@ -73,6 +73,20 @@ open Ty
 open Term
 open Printer
 
+let clean_name fname =
+  (* TODO: replace with Filename.remove_extension
+   * after migration to OCaml 4.04+ *)
+  let remove_extension s =
+    try Filename.chop_extension s with Invalid_argument _ -> s in
+  let f = Filename.basename fname in (remove_extension f)
+
+let module_name ?fname path t =
+  let fname    = match fname, path with
+    | None, "why3"::_ -> "why3"
+    | None, _   -> String.concat "__" path
+    | Some f, _ -> clean_name f in
+  fname ^ "__" ^ t
+
 module ML = struct
 
   open Expr
@@ -476,8 +490,7 @@ module Translate = struct
     | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
       let args = params cty.cty_args in
       ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
-    | Eexec ({c_node = Cany}, _) ->
-      raise ExtractionAny
+    | Eexec ({c_node = Cany}, _) -> raise ExtractionAny
       (* ML.mk_unit *)
     | Eabsurd ->
       ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
@@ -570,8 +583,9 @@ module Translate = struct
     match pd.pd_node with
     | PDlet (LDsym (rs, _)) when rs_ghost rs ->
       []
-    | PDlet (LDsym (rs, {c_node = Cany})) ->
-      raise (ExtractionVal rs)
+    | PDlet (LDsym (_rs, {c_node = Cany})) ->
+      []
+      (* raise (ExtractionVal _rs) *)
     | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
       let args = params cty.cty_args in
       let res = ity cty.cty_result in

src/mlw/cprinter.ml

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

src/mlw/ocaml_printer.ml

@@ -77,7 +77,7 @@ module Print = struct
 
   let print_qident ~sanitizer info fmt id =
     try
-      let _, _, q =
+      let lp, t, q =
         try Pmodule.restore_path id
         with Not_found -> Theory.restore_path id in
       let s = String.concat "__" q in
@@ -89,8 +89,8 @@ module Print = struct
            false info.info_current_mo
       then fprintf fmt "%s" s
       else
-        (* let fname = if lp = [] then info.info_fname else None in *)
-        let m = Strings.capitalize "m" in
+        let fname = if lp = [] then info.info_fname else None in
+        let m = Strings.capitalize (module_name ?fname lp t) in
         fprintf fmt "%s.%s" m s
     with Not_found ->
       let s = id_unique ~sanitizer iprinter id in
@@ -302,16 +302,19 @@ module Print = struct
       forget_let_defn let_def
     | Eabsurd ->
       fprintf fmt (protect_on paren "assert false (* absurd *)")
-    | Eapp (s, []) when rs_equal s rs_true ->
+    | Eapp (rs, []) when rs_equal rs rs_true ->
       fprintf fmt "true"
-    | Eapp (s, []) when rs_equal s rs_false ->
+    | Eapp (rs, []) when rs_equal rs rs_false ->
       fprintf fmt "false"
-    | Eapp (s, [e1; e2]) when rs_equal s rs_func_app ->
+    | Eapp (rs, [e1; e2]) when rs_equal rs rs_func_app ->
       fprintf fmt "@[<hov 1>%a %a@]"
         (print_expr info) e1 (print_expr info) e2
-    | Eapp (s, pvl) ->
+    | Eapp (rs, [])  ->
+      (* avoids parenthesis around values *)
+      fprintf fmt "%a" (print_apply info (Hrs.find_def ht_rs rs rs)) []
+    | Eapp (rs, pvl) ->
       fprintf fmt (protect_on paren "%a")
-        (print_apply info (Hrs.find_def ht_rs s s)) pvl
+        (print_apply info (Hrs.find_def ht_rs rs rs)) pvl
     | Ematch (e, pl) ->
       fprintf fmt (protect_on paren
       "begin match @[%a@] with@\n@[<hov>%a@]@\nend")
@@ -445,7 +448,7 @@ module Print = struct
         print_ident xs.xs_name (print_ty ~paren:true info) t
 end
 
-let extract_module pargs ?old fmt ({mod_theory = th} as m) =
+let extract_module pargs ?old ?fname fmt ({mod_theory = th} as m) =
   ignore (pargs);
   ignore (old);
   ignore (m);
@@ -456,7 +459,7 @@ let extract_module pargs ?old fmt ({mod_theory = th} as m) =
     info_current_mo   = Some m;
     info_th_known_map = th.th_known;
     info_mo_known_map = m.mod_known;
-    info_fname        = None; (* TODO *)
+    info_fname        = Opt.map Compile.clean_name fname
   } in
   fprintf fmt
     "(* This file has been generated from Why3 module %a *)@\n@\n"
@@ -467,18 +470,9 @@ let extract_module pargs ?old fmt ({mod_theory = th} as m) =
   fprintf fmt "@."
 
 let fg ?fname m =
-  let mod_name = m.Pmodule.mod_theory.Theory.th_name.id_string in
-  match fname with
-  | None   -> mod_name ^ ".ml"
-  | Some f ->
-    (* TODO: replace with Filename.remove_extension
-     * after migration to OCaml 4.04+ *)
-    let remove_extension s =
-      try Filename.chop_extension s
-      with Invalid_argument _ -> s
-    in
-    let f = Filename.basename f in
-    (remove_extension f) ^ "__" ^ mod_name ^ ".ml"
+  let mod_name = m.mod_theory.th_name.id_string in
+  let path     = m.mod_theory.th_path in
+  (module_name ?fname path mod_name) ^ ".ml"
 
 let () = Pdriver.register_printer "ocaml"
   ~desc:"printer for OCaml code" fg extract_module

src/mlw/pdriver.ml

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

src/mlw/pdriver.mli

@@ -37,7 +37,8 @@ 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 -> Pmodule.pmodule Pp.pp
+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 filename_generator = ?fname:string -> Pmodule.pmodule -> string
 

src/tools/why3extract.ml

@@ -50,6 +50,7 @@ let add_opt_theory x =
 let opt_parser = ref None
 let opt_output = ref None
 let opt_driver = ref []
+let opt_recurs = ref false
 
 let option_list = [
   "-", Arg.Unit (fun () -> add_opt_file "-"),
@@ -66,6 +67,8 @@ 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 ";
   "-o", Arg.String (fun s -> opt_output := Some s),
       "<dir> print the selected goals to separate files in <dir>";
   "--output", Arg.String (fun s -> opt_output := Some s),
@@ -100,6 +103,8 @@ let opt_driver =
     eprintf "%a@." Exn_printer.exn_printer e;
     exit 1
 
+let opt_recurs = !opt_recurs
+
 let extract_to ?fname m =
   let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in
   let file = Filename.concat opt_output (fg ?fname m) in
@@ -113,7 +118,7 @@ let extract_to ?fname m =
   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 pargs fmt m;
+  pr ?old ?fname pargs fmt m;
   close_out cout
 
 let extract_to =
@@ -129,14 +134,13 @@ let rec use_iter f 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' =
+  let extract_use m' =
     let fname =
       if m'.mod_theory.Theory.th_path = [] then fname else None
     in
     do_extract_module ?fname m'
   in
-  (* for now, do not do a recursive extraction *)
-  (* use_iter extract_use m.mod_units; *)
+  if opt_recurs then use_iter extract_use m.mod_units;
   extract_to ?fname m
 
 let do_global_extract (_,p,t) =
@@ -144,7 +148,6 @@ let do_global_extract (_,p,t) =
   let m = read_module env p t in
   do_extract_module m
 
-
 let do_extract_module_from fname mm (tname,_,t) =
   try
     let m = Mstr.find t mm in do_extract_module ~fname m

theories/int.why

@@ -10,8 +10,8 @@ theories for classical functions.
 
 theory Int
 
-  constant zero : int = 0
-  constant one  : int = 1
+  let constant zero : int = 0
+  let constant one  : int = 1
 
   val (=) (x y : int) : bool ensures { result <-> x = y }