Code extraction

Why3 files from standard library are not extracted

src/mlw/compile.ml

@@ -440,33 +440,30 @@ module Translate = struct
       List.exists is_constructor its
     | _ -> false
 
-  (* let get_record info rs = *)
-  (*   match Mid.find_opt rs.rs_name info.info_mo_known_map with *)
-  (*   | Some {pd_node = PDtype itdl} -> *)
-  (*     let f itd = List.exists (rs_equal rs) itd.itd_fields in *)
-  (*     let itd = List.find f itdl in *)
-  (*     let is_private = itd.itd_its.its_private in *)
+  let is_private_record itd = itd.itd_its.its_private
+
+  let is_singleton_imutable itd =
+    let not_g e = not (rs_ghost e) in
+    let pjl = itd.itd_fields in
+    let mfields = itd.itd_its.its_mfields in
+    let pv_equal_field rs = pv_equal (Opt.get rs.rs_field) in
+    let get_mutable rs = List.exists (pv_equal_field rs) mfields in
+    match filter_ghost_params not_g get_mutable pjl with
+    | [is_mutable] -> not is_mutable
+    | _ -> false
 
-  (*   | _ -> true, [] *)
-
-  let is_private_record info rs =
-    match Mid.find_opt rs.rs_name info.info_mo_known_map with
-    | Some {pd_node = PDtype itdl} ->
-      let f itd = List.exists (rs_equal rs) itd.itd_fields in
-      let itd = List.find f itdl in
-      itd.itd_its.its_private
-    | _ -> assert false (* rs is a field *)
+  let is_optimizable_record itd =
+    not (is_private_record itd) && is_singleton_imutable itd
 
   let get_record info rs =
     match Mid.find_opt rs.rs_name info.info_mo_known_map with
     | Some {pd_node = PDtype itdl} ->
       let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
-      let itd =
-        try List.find (fun itd -> f itd.itd_constructors) itdl
-        with Not_found -> List.find (fun itd -> f itd.itd_fields) itdl in
-      let no_g e = not (rs_ghost e) in
-      List.filter no_g itd.itd_fields, Some itd.itd_its.its_private
-    | _ -> [], None
+      let itd = begin match rs.rs_field with
+        | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
+        | None -> List.find (fun itd -> f itd.itd_constructors) itdl end in
+      is_optimizable_record itd
+    | _ -> false
 
   let mk_eta_expansion rsc pvl cty_app =
     (* FIXME : effects and types of the expression in this situation *)
@@ -631,9 +628,8 @@ module Translate = struct
       mk_eta_expansion rs pvl cty
     | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
       let pvl = app pvl rs.rs_cty.cty_args in
-      let (pjl, is_private) = get_record info rs in
-      begin match pvl, pjl, is_private with
-      | [pv_expr], [_], Some false ->
+      begin match pvl with
+      | [pv_expr] when get_record info rs ->
         (* singleton public record type obtained by ghost fields erasure *)
         pv_expr
       | _ -> ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff end

src/mlw/ocaml_printer.ml

@@ -268,6 +268,9 @@ module Print = struct
       begin match pjl, tl with
       | [], [] ->
         (print_uident info) fmt rs.rs_name
+      | [], [t] ->
+        fprintf fmt "@[<hov 2>%a %a@]" (print_uident info) rs.rs_name
+          (print_expr info) t
       | [], tl ->
         fprintf fmt "@[<hov 2>%a (%a)@]" (print_uident info) rs.rs_name
           (print_list comma (print_expr info)) tl
@@ -334,7 +337,7 @@ module Print = struct
         (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")
+      "begin match @[%a@] with@\n@[%a@] end")
         (print_expr info) e (print_list newline (print_branch info)) pl
     | Eassign al ->
       let assign fmt (rho, rs, pv) =

src/tools/why3extract.ml

@@ -173,14 +173,16 @@ let translate_module =
 let extract_to =
   let memo = Ident.Hid.create 16 in
   fun ?fname ?decl m ->
-    let name = m.mod_theory.Theory.th_name in
-    if not (Ident.Hid.mem memo name) then begin
-      Ident.Hid.add memo name ();
-      let mdecls = match decl with
-        | None   -> (translate_module m).ML.mod_decl
-        | Some d -> Translate.pdecl_m m d in
-      print_mdecls ?fname m mdecls
-    end
+    match m.mod_theory.Theory.th_path with
+    | ("why3" | "map")::_ -> ()
+    | _ -> let name = m.mod_theory.Theory.th_name in
+        if not (Ident.Hid.mem memo name) then begin
+          Ident.Hid.add memo name ();
+          let mdecls = match decl with
+            | None   -> (translate_module m).ML.mod_decl
+            | Some d -> Translate.pdecl_m m d in
+          print_mdecls ?fname m mdecls
+        end
 
 let rec use_iter f l =
   List.iter
@@ -189,8 +191,7 @@ let rec use_iter f l =
 let rec do_extract_module ?fname m =
   let extract_use m' =
     let fname =
-      if m'.mod_theory.Theory.th_path = [] then fname else None
-    in
+      if m'.mod_theory.Theory.th_path = [] then fname else None in
     do_extract_module ?fname m'
   in
   begin match opt_rec_single with
@@ -278,9 +279,8 @@ let rec visit mm id =
   if not (Ident.Hid.mem visited id) then begin
     try
       let d = find_decl mm id in
-      (* Can I change these the two lines (* *) ? *)
-      Ident.Hid.add visited id (); (* *)
-      ML.iter_deps (visit mm) d;   (* *)
+      Ident.Hid.add visited id ();
+      ML.iter_deps (visit mm) d;
       toextract := id :: !toextract
     with Not_found -> ()
   end