Extraction: nicer printing of functors modules

drivers/ocaml64.drv

@@ -238,6 +238,17 @@ module mach.int.Random63
   syntax val random_int63  "Random.int %1"
 end
 
+module mach.int.State63
+  (* the most appropriate way to do this would be to have
+     something similar to [remove] from smt drivers:
+     remove val create *)
+  syntax val create       "SHOULD_NOT_BE_HERE"
+  syntax val init         "SHOULD_NOT_BE_HERE"
+  syntax val self_init    "SHOULD_NOT_BE_HERE"
+  syntax val random_bool  "SHOULD_NOT_BE_HERE"
+  syntax val random_int63 "SHOULD_NOT_BE_HERE"
+end
+
 module mach.peano.Peano
   syntax type t      "int"
   syntax val  to_int "Z.of_int %1"
@@ -360,4 +371,3 @@ module ocaml.Pervasives
   syntax val succ                   "succ %1"
   syntax val pred                   "pred %1"
 end
-

src/mlw/compile.ml

@@ -723,8 +723,10 @@ module Translate = struct
         let args = params cty.cty_args in
         let res = mlty_of_ity cty.cty_mask cty.cty_result in
         [Mltree.Dlet (Mltree.Lany (rs, res, args))]
-    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
-        []
+    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e}))
+      when is_val e.e_node -> (* zero argument functions *)
+        let res = mlty_of_ity cty.cty_mask cty.cty_result in
+        [Mltree.Dlet (Mltree.Lany (rs, res, []))]
     | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
         let args = params cty.cty_args in
         let res = mlty_of_ity cty.cty_mask cty.cty_result in
@@ -816,14 +818,6 @@ module Translate = struct
       Mltree.mod_known = mod_known;
     }
 
-  (* let () = Exn_printer.register (fun fmt e -> match e with *)
-  (*   | ExtractionAny -> *)
-  (*     Format.fprintf fmt "Cannot extract an undefined node" *)
-  (*   | ExtractionVal rs -> *)
-  (*     Format.fprintf fmt "Function %a cannot be extracted" *)
-  (*       print_rs rs *)
-  (*   | _ -> raise e) *)
-
 end
 
 (** Some transformations *)

src/mlw/ocaml_printer.ml

@@ -277,7 +277,7 @@ module Print = struct
     (* here [rs] refers to a [val] declaration *)
     match query_syntax info.info_convert rs.rs_name,
           query_syntax info.info_syn     rs.rs_name with
-    | None, None when info.info_flat ->
+    | None, None (* when info.info_flat *) ->
         Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
     | _ -> ()
 
@@ -318,7 +318,7 @@ module Print = struct
               else fprintf fmt "%s" s
           | _ -> assert false in
         syntax_arguments s print_constant fmt pvl
-    | _, Some s, _ ->
+    | _, Some s, _ (* when is_local_id info rs.rs_name  *)->
         syntax_arguments s (print_expr ~paren:true info) fmt pvl;
     | _, None, tl when is_rs_tuple rs ->
         fprintf fmt "@[(%a)@]"
@@ -344,7 +344,7 @@ module Print = struct
         end
     | _, None, [] ->
         (print_lident info) fmt rs.rs_name
-    | _, None, tl ->
+    | _, _, tl -> (* FIXME? when is in driver but is not a local id *)
         fprintf fmt "@[<hov 2>%a %a@]"
           (print_lident info) rs.rs_name
           (print_apply_args info) (tl, rs.rs_cty.cty_args)
@@ -395,6 +395,10 @@ module Print = struct
         List.iter (fun fd -> Hrs.replace ht_rs fd.rec_rsym fd.rec_sym) rdef;
         print_list_next newline print_one fmt rdef;
         List.iter (fun fd -> Hrs.remove ht_rs fd.rec_rsym) rdef
+    | Lany (rs, res, []) when functor_arg ->
+        fprintf fmt "@[<hov 2>val %a : %a@]"
+          (print_lident info) rs.rs_name
+          (print_ty info) res;
     | Lany (rs, res, args) when functor_arg ->
         let print_ty_arg info fmt (_, ty, _) =
           fprintf fmt "@[%a@]" (print_ty info) ty in
@@ -600,18 +604,18 @@ module Print = struct
     | Dmodule (s, dl) ->
         let args, dl = extract_functor_args info dl in
         let info = { info with info_current_ph = s :: info.info_current_ph } in
-        fprintf fmt "@[@[<hov 2>module %s%a@ =@ struct@ %a@]@ end@]" s
+        fprintf fmt "@[@[<hov 2>module %s%a@ =@]@\n@[<hov 2>struct@ %a@]@ end" s
           (print_functor_args info) args
           (print_list newline2 (print_decl info)) dl
 
   and print_functor_args info fmt args =
     let print_sig info fmt dl =
       fprintf fmt "sig@ %a@ end"
-        (print_list space (print_decl info ~functor_arg:true)) dl in
+        (print_list newline (print_decl info ~functor_arg:true)) dl in
     let print_pair fmt (s, dl) =
       let info = { info with info_current_ph = s :: info.info_current_ph } in
       fprintf fmt "(%s:@ %a)" s (print_sig info) dl in
-    fprintf fmt "@[%a@]" (print_list space print_pair) args
+    fprintf fmt "%a" (print_list space print_pair) args
 
   let print_decl info fmt decl =
     (* avoids printing the same decl for mutually recursive decls *)

src/mlw/ocaml_printer.mli

+module Print : sig
+  val optional_arg : Ident.label
+
+  val named_arg : Ident.label
+
+  val ocaml_remove : Ident.label
+end

src/tools/why3extract.ml

@@ -135,6 +135,14 @@ let get_cout_old ?fname fg m = match opt_output with
       Some (open_in backup) end else None in
     open_out file, old
 
+let print_preludes =
+  let ht = Hstr.create 8 in
+  let add l s = if Hstr.mem ht s then l else (Hstr.add ht s (); s :: l) in
+  fun id_th fmt pm ->
+    let th_pm = Ident.Mid.find_def [] id_th pm in
+    let l = List.fold_left add [] th_pm in
+    Printer.print_prelude fmt l
+
 let print_mdecls ?fname m mdecls =
   let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in
   let test_decl_not_driver decl =
@@ -145,6 +153,9 @@ let print_mdecls ?fname m mdecls =
   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
+    (* print driver prelude *)
+    let pm = pargs.Pdriver.thprelude in
+    print_preludes m.mod_theory.Theory.th_name fmt pm;
     let flat = opt_modu_flat = Flat in
     let pr_decl fmt d = fprintf fmt "%a" (pr pargs ?old ?fname ~flat m) d in
     Pp.print_list Pp.newline pr_decl fmt mdecls;