Code extraction (wip)

src/mlw/compile.ml

@@ -509,7 +509,8 @@ module Translate = struct
     | Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
       ML.mk_unit
     | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
-      when isconstructor info rs ->
+      when isconstructor info rs && cty.cty_args <> [] ->
+      (* partial application of constructors *)
       mk_eta_expansion rs pvl cty
     | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
       let pvl = app pvl in
@@ -517,8 +518,8 @@ 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
-      (* ML.mk_unit *)
+    | Eexec ({c_node = Cany}, _) -> (* raise ExtractionAny *)
+      ML.mk_unit
     | Eabsurd ->
       ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
     | Ecase (e1, _) when e_ghost e1 ->

src/mlw/ocaml_printer.ml

@@ -447,14 +447,14 @@ module Print = struct
     | Dlet ldef ->
       print_let_def info fmt ldef;
       forget_tvs ();
-      fprintf fmt "@\n@\n"
+      fprintf fmt "@\n"
     | Dtype dl ->
       print_list_next newline (print_type_decl info) fmt dl;
-      fprintf fmt "@\n@\n"
+      fprintf fmt "@\n"
     | Dexn (xs, None) ->
-       fprintf fmt "exception %a@\n@\n" print_ident xs.xs_name
+       fprintf fmt "exception %a@\n" print_ident xs.xs_name
     | Dexn (xs, Some t) ->
-      fprintf fmt "@[<hov 2>exception %a of %a@]@\n@\n"
+      fprintf fmt "@[<hov 2>exception %a of %a@]@\n"
         print_ident xs.xs_name (print_ty ~paren:true info) t
 end
 

src/tools/why3extract.ml

@@ -150,7 +150,7 @@ let extract_to ?fname m =
     let fmt = formatter_of_out_channel stdout in
     let tname = m.mod_theory.Theory.th_name.Ident.id_string in
     Debug.dprintf Pdriver.debug "extract module %s standard output@." tname;
-    List.iter (pr ?fname pargs m fmt) mdecls
+    List.iter (pr pargs m fmt) mdecls
 
 let extract_to =
   let visited = Ident.Hid.create 17 in