Code extraction (wip)

New command line nearly done

drivers/ocaml64.drv

@@ -65,7 +65,7 @@ end
 *)
 
 module mach.int.Int63
-  syntax val of_int "Z.to_int %1"
+  syntax val of_int "%1"
   syntax converter of_int "%1"
 
   syntax function to_int "Z.of_int %1"

src/mlw/compile.ml

@@ -180,7 +180,14 @@ module ML = struct
     mod_known : known_map;
   }
 
-  let add_known_decl id decl k_map =
+  let get_decl_name = function
+    | Dtype itdefl -> List.map (fun {its_name = id} -> id) itdefl
+    | Dlet (Lvar (pv, _)) -> [pv.pv_vs.vs_name]
+    | Dlet (Lsym (rs, _, _, _)) -> [rs.rs_name]
+    | Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
+    | Dexn (xs, _) -> [xs.xs_name]
+
+  let add_known_decl decl k_map id =
     Mid.add id decl k_map
 
   let rec iter_deps_ty f = function
@@ -191,7 +198,7 @@ module ML = struct
   let iter_deps_typedef f = function
     | Ddata constrl ->
       List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
-    | Drecord _pjl -> assert false (*TODO*)
+    | Drecord pjl -> List.iter (fun (_, _, ty) -> iter_deps_ty f ty) pjl
     | Dalias ty -> iter_deps_ty f ty
 
   let iter_deps_its_defn f its_d =
@@ -274,7 +281,9 @@ module ML = struct
         (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
            f rs.rs_name; iter_deps_args f args;
            iter_deps_expr f e; iter_deps_ty f res) rdef
-    | _ -> assert false (*TODO*)
+    | Dlet (Lvar (_, e)) -> iter_deps_expr f e
+    | Dexn (_, None) -> ()
+    | Dexn (_, Some ty) -> iter_deps_ty f ty
 
   let mk_expr e_node e_ity e_effect =
     { e_node = e_node; e_ity = e_ity; e_effect = e_effect }
@@ -298,7 +307,8 @@ module ML = struct
   let mk_var_unit () = id_register (id_fresh "_"), tunit, true
 
   let mk_its_defn id args private_ def =
-    { its_name = id; its_args = args; its_private = private_; its_def = def; }
+    { its_name    = id      ; its_args = args;
+      its_private = private_; its_def  = def; }
 
   let eseq e1 e2 =
     match e1.e_node, e2.e_node with
@@ -696,9 +706,8 @@ module Translate = struct
     | 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
-      let decl = ML.Dlet (ML.Lsym (rs, res, args, expr info e)) in
-      let add_known = Mid.singleton rs.rs_name decl in
-      [decl, add_known]
+      [ML.Dlet (ML.Lsym (rs, res, args, expr info e))]
+      (* let add_known = Mid.singleton rs.rs_name decl in *)
     | PDlet (LDrec rl) ->
       let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
         let e    = match e.c_node with Cfun e -> e | _ -> assert false in
@@ -708,24 +717,21 @@ module Translate = struct
           ML.rec_args = args; ML.rec_exp  = expr info e;
           ML.rec_res  = res } in
       let rec_def = filter_ghost_rdef def rl in
-      let decl    = ML.Dlet (ML.Lrec rec_def) in
-      let mk_add_km m {ML.rec_sym = rs} =
-        ML.add_known_decl rs.rs_name decl m in
-      let add_known = List.fold_left mk_add_km Mid.empty rec_def in
-      [decl, add_known]
-    | PDlet (LDsym _) | PDpure | PDlet (LDvar (_, _)) ->
+      [ML.Dlet (ML.Lrec rec_def)]
+      (* let mk_add_km m {ML.rec_sym = rs} = *)
+      (*   ML.add_known_decl decl m rs.rs_name in *)
+      (* let add_known = List.fold_left mk_add_km Mid.empty rec_def in *)
+    | PDlet (LDsym _) | PDpure | PDlet (LDvar _) ->
       []
     | PDtype itl ->
       let itsd = List.map tdef itl in
-      let decl = ML.Dtype itsd in
-      let mk_add_mk m {ML.its_name = id} = ML.add_known_decl id decl m in
-      let add_known = List.fold_left mk_add_mk Mid.empty itsd in
-      [decl, add_known]
+      [ML.Dtype itsd]
+      (* let mk_add_mk m {ML.its_name = id} = ML.add_known_decl decl m id in *)
+      (* let add_known = List.fold_left mk_add_mk Mid.empty itsd in *)
     | PDexn xs ->
-      let decl = if ity_equal xs.xs_ity ity_unit then ML.Dexn (xs, None)
-        else ML.Dexn (xs, Some (ity xs.xs_ity)) in
-      let add_known = Mid.singleton xs.xs_name decl in
-      [decl, add_known]
+      if ity_equal xs.xs_ity ity_unit then [ML.Dexn (xs, None)]
+      else [ML.Dexn (xs, Some (ity xs.xs_ity))]
+      (* let add_known = Mid.singleton xs.xs_name decl in *)
 
   let pdecl_m m pd =
     let info = {
@@ -744,14 +750,12 @@ module Translate = struct
     let info = {
       info_current_mo   = Some m;
       info_mo_known_map = m.mod_known; } in
-    let known_m = ref Mid.empty in
-    let mk_decl_and_km (decl, known_m_new) =
-      known_m := Mid.set_union !known_m known_m_new;
-      decl in
-    let comp munit =
-      let m = mdecl info munit in List.map mk_decl_and_km m in
-    let decl = List.map comp m.mod_units in
-    { ML.mod_decl = List.concat decl; ML.mod_known = !known_m }, info
+    let mod_decl = List.concat (List.map (mdecl info) m.mod_units) in
+    let add known_map decl =
+      let idl = ML.get_decl_name decl in
+      List.fold_left (ML.add_known_decl decl) known_map idl in
+    let mod_known = List.fold_left add Mid.empty mod_decl in
+    { ML.mod_decl = mod_decl; ML.mod_known = mod_known }, info
 
   let () = Exn_printer.register (fun fmt e -> match e with
     | ExtractionAny ->
@@ -838,8 +842,46 @@ 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 =
-    { m with mod_decl = List.map (pdecl info) m.mod_decl }
+    let mod_decl = List.map (pdecl info) m.mod_decl in
+    let add known_map decl =
+      let idl = get_decl_name decl in
+      List.fold_left (ML.add_known_decl decl) known_map idl in
+    let mod_known = List.fold_left add Mid.empty mod_decl in
+    { mod_decl = mod_decl; mod_known = mod_known }
 
 end
 

src/mlw/ocaml_printer.ml

@@ -87,7 +87,7 @@ module Print = struct
     fprintf fmt "%s" s
 
   let print_qident ~sanitizer info fmt id =
-    try if info.flat then raise Not_found;
+    try (* if info.flat then raise Not_found; *)
       let lp, t, q =
         try Pmodule.restore_path id
         with Not_found -> Theory.restore_path id in
@@ -99,10 +99,11 @@ module Print = struct
          Opt.fold (fun _ m -> Sid.mem id m.Pmodule.mod_local)
            false info.info_current_mo
       then fprintf fmt "%s" s
-      else
+      else begin
+        if info.flat then raise Not_found;
         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
+        fprintf fmt "%s.%s" m s end
     with Not_found ->
       let s = id_unique ~sanitizer iprinter id in
       fprintf fmt "%s" s
@@ -125,8 +126,8 @@ module Print = struct
       print_list2 sep sep_m print1 print2 fmt (r1, r2)
     | _ -> ()
 
-  let print_rs fmt rs =
-    fprintf fmt "%a" print_ident rs.rs_name
+  let print_rs info fmt rs =
+    fprintf fmt "%a" (print_lident info) rs.rs_name
 
   (** Types *)
 
@@ -194,9 +195,9 @@ module Print = struct
     | Pwild ->
        fprintf fmt "_"
     | Pident id ->
-       (print_lident info) fmt id
+       print_ident fmt id
     | Pas (p, id) ->
-       fprintf fmt "%a as %a" (print_pat info) p (print_lident info) id
+       fprintf fmt "%a as %a" (print_pat info) p print_ident id
     | Por (p1, p2) ->
        fprintf fmt "%a | %a" (print_pat info) p1 (print_pat info) p2
     | Ptuple pl ->
@@ -211,7 +212,7 @@ module Print = struct
         | []  -> print_papp info ls fmt pl
         | pjl ->
           fprintf fmt "@[<hov 2>{ %a}@]"
-            (print_list2 semi equal print_rs (print_pat info)) (pjl, pl)
+            (print_list2 semi equal (print_rs info) (print_pat info)) (pjl, pl)
 
   and print_papp info ls fmt = function
     | []  -> fprintf fmt "%a"      (print_uident info) ls.ls_name
@@ -261,18 +262,18 @@ module Print = struct
       fprintf fmt "@[(%a)@]"
         (print_list comma (print_expr info)) tl
     | _,  _, [t1] when isfield ->
-      fprintf fmt "%a.%a" (print_expr info) t1 (print_lident info) rs.rs_name
+      fprintf fmt "%a.%a" (print_expr info) t1 print_ident rs.rs_name
     | _, _, tl when isconstructor () ->
       let pjl = get_record info rs in
       begin match pjl, tl with
-        | [], [] ->
-          (print_uident info) fmt rs.rs_name
-        | [], 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 (print_expr info)) (pjl, tl)
+      | [], [] ->
+        (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
+      | pjl, tl ->
+        fprintf fmt "@[<hov 2>{ %a}@]"
+          (print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl)
       end
     | _, _, [] ->
       (print_lident info) fmt rs.rs_name
@@ -337,8 +338,8 @@ module Print = struct
     | Eassign al ->
       let assign fmt (rho, rs, pv) =
         fprintf fmt "%a.%a <-@ %a"
-          (print_lident info) (pv_name rho) (print_lident info) rs.rs_name
-          (print_lident info) (pv_name pv) in
+          print_ident (pv_name rho) print_ident rs.rs_name
+          print_ident (pv_name pv) in
       begin match al with
       | [] -> assert false | [a] -> assign fmt a
       | al -> fprintf fmt "@[begin %a end@]" (print_list semi assign) al end
@@ -431,7 +432,7 @@ module Print = struct
                (print_list star (print_ty ~paren:false info)) l in
     let print_field fmt (is_mutable, id, ty) =
       fprintf fmt "%s%a: %a;" (if is_mutable then "mutable " else "")
-        (print_lident info) id (print_ty ~paren:false info) ty in
+        print_ident id (print_ty ~paren:false info) ty in
     let print_def fmt = function
       | None ->
         ()
@@ -457,10 +458,18 @@ module Print = struct
       print_list_next newline (print_type_decl info) fmt dl;
       fprintf fmt "@\n"
     | Dexn (xs, None) ->
-       fprintf fmt "exception %a@\n" (print_uident info) xs.xs_name
-    | Dexn (xs, Some t) ->
+       fprintf fmt "exception %a@\n" print_ident xs.xs_name
+    | Dexn (xs, Some t)->
       fprintf fmt "@[<hov 2>exception %a of %a@]@\n"
-        (print_uident info) xs.xs_name (print_ty ~paren:true info) t
+        print_ident xs.xs_name (print_ty ~paren:true info) t
+
+  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
+    List.iter decide_print decl_name
+
 end
 
 let print_decl pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d =

src/tools/why3extract.ml

@@ -16,7 +16,8 @@ open Pmodule
 open Compile
 
 let usage_msg = sprintf
-  "Usage: %s [options] -D <driver> -o <dir> [[file|-] [-T <theory>]...]..."
+  "Usage: %s [options] -D <driver> [-o <dir|file>] \
+             [<file>.<Module>*.<symbol>?|-]"
   (Filename.basename Sys.argv.(0))
 
 type extract_target =
@@ -68,7 +69,9 @@ let option_list = [
   "--driver", Arg.String (fun s -> opt_driver := s::!opt_driver),
       " same as -D";
   "--recursive", Arg.Unit (fun () -> opt_rec_single := Recursive),
-      " perform a recursive extraction";
+      " recursively extract all dependencies";
+  "--flat", Arg.Unit (fun x -> x),
+      " perform a flat extraction (default option)";
   "--modular", Arg.Unit (fun () -> opt_modu_flat := Modular),
       " perform a modular extraction";
   "-o", Arg.String (fun s -> opt_output := Some s),
@@ -79,17 +82,6 @@ let option_list = [
 let config, _, env =
   Whyconf.Args.initialize option_list add_opt_file usage_msg
 
-let find_module_path mm path m = match path with
-  | [] ->
-    Mstr.find m mm
-  | path ->
-    let mm = Env.read_library Pmodule.mlw_language env path in
-    Mstr.find m mm
-
-let find_module_id mm id =
-  let (path, m, _) = Pmodule.restore_path id in
-  find_module_path mm path m
-
 let () =
   if Queue.is_empty opt_queue then begin
     Whyconf.Args.exit_with_usage option_list usage_msg
@@ -98,7 +90,6 @@ let () =
 let opt_rec_single = !opt_rec_single
 let opt_modu_flat  = !opt_modu_flat
 
-(* FIXME: accept --mono without -o and use to standard output *)
 let opt_output = match opt_modu_flat, !opt_output with
   | Modular, None ->
     eprintf "Output directory (-o) is required for modular extraction.@.";
@@ -109,8 +100,8 @@ let opt_output = match opt_modu_flat, !opt_output with
   | Modular, Some s when not (Sys.is_directory s) ->
     eprintf "Option '-o' should be given a directory as argument.@.";
     exit 1
-  | Flat, Some s when Sys.is_directory s ->
-    eprintf "Option '-o' should not be given a directory as argument.@.";
+  | Flat, Some s when Sys.file_exists s && Sys.is_directory s ->
+    eprintf "Option '-o' should be given a file as argument.@.";
     exit 1
   | Modular, Some _ | Flat, None | Flat, Some _ -> !opt_output
 
@@ -152,6 +143,17 @@ let print_mdecls ?fname m mdecls =
   List.iter (pr pargs ?old ?fname ~flat m fmt) mdecls;
   if cout <> stdout then close_out cout
 
+let find_module_path mm path m = match path with
+  | [] ->
+    Mstr.find m mm
+  | path ->
+    let mm = Env.read_library Pmodule.mlw_language env path in
+    Mstr.find m mm
+
+let find_module_id mm id =
+  let (path, m, _) = Pmodule.restore_path id in
+  find_module_path mm path m
+
 let translate_module =
   let memo = Ident.Hid.create 16 in
   fun m ->
@@ -170,7 +172,7 @@ let extract_to =
       Ident.Hid.add memo name ();
       let mdecls = match decl with
         | None   -> (translate_module m).ML.mod_decl
-        | Some d -> List.map fst (Translate.pdecl_m m d) in
+        | Some d -> Translate.pdecl_m m d in
       print_mdecls ?fname m mdecls
     end
 
@@ -316,7 +318,6 @@ let () =
         pr pargs ~flat:true pm fmt d in
       List.iter extract (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;
     exit 1