From da76331882f9b5d7c72d993d0ef6050bd13d38b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1rio=20Pereira?= Date: Thu, 2 Mar 2017 14:36:02 +0100 Subject: [PATCH] Code extraction (wip) Empty extracted modules (all definitions are defined in the driver) are printed no more, independently of the extraction mode --- examples/leftist_heap.mlw | 2 +- src/mlw/compile.ml | 33 --------------------------------- src/mlw/ocaml_printer.ml | 12 ++++++------ src/tools/why3extract.ml | 24 +++++++++++++++--------- 4 files changed, 22 insertions(+), 49 deletions(-) diff --git a/examples/leftist_heap.mlw b/examples/leftist_heap.mlw index d1309c8d8..0437aef59 100644 --- a/examples/leftist_heap.mlw +++ b/examples/leftist_heap.mlw @@ -114,7 +114,7 @@ module LeftistHeap type t = tree elt (* [e] is no greater than the root of [h], if any *) - let predicate le_root (e: elt) (h: t) = match h with + predicate le_root (e: elt) (h: t) = match h with | E -> true | N _ _ x _ -> le e x end diff --git a/src/mlw/compile.ml b/src/mlw/compile.ml index 491aa0e90..4ed513eac 100644 --- a/src/mlw/compile.ml +++ b/src/mlw/compile.ml @@ -842,39 +842,6 @@ 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 = let mod_decl = List.map (pdecl info) m.mod_decl in let add known_map decl = diff --git a/src/mlw/ocaml_printer.ml b/src/mlw/ocaml_printer.ml index 995aa2a43..194482474 100644 --- a/src/mlw/ocaml_printer.ml +++ b/src/mlw/ocaml_printer.ml @@ -269,8 +269,8 @@ module Print = struct | [], [] -> (print_uident info) fmt rs.rs_name | [], tl -> - fprintf fmt "@[%a (%a)@]" - print_ident rs.rs_name (print_list comma (print_expr info)) tl + fprintf fmt "@[%a (%a)@]" (print_uident info) rs.rs_name + (print_list comma (print_expr info)) tl | pjl, tl -> fprintf fmt "@[{ %a}@]" (print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl) @@ -466,8 +466,9 @@ module Print = struct 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 + if query_syntax info.info_syn id = None then begin + print_decl info fmt decl; + fprintf fmt "@." end in List.iter decide_print decl_name end @@ -484,8 +485,7 @@ let print_decl pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d = info_fname = Opt.map Compile.clean_name fname; flat = flat; } in - Print.print_decl info fmt d; - fprintf fmt "@." + Print.print_decl info fmt d let fg ?fname m = let mod_name = m.mod_theory.th_name.id_string in diff --git a/src/tools/why3extract.ml b/src/tools/why3extract.ml index b54d17e18..e28147d6e 100644 --- a/src/tools/why3extract.ml +++ b/src/tools/why3extract.ml @@ -137,11 +137,17 @@ let get_cout_old ?fname fg m = match opt_output with let print_mdecls ?fname m mdecls = let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in - let cout, old = get_cout_old fg m ?fname in - let fmt = formatter_of_out_channel cout in - let flat = opt_modu_flat = Flat in - List.iter (pr pargs ?old ?fname ~flat m fmt) mdecls; - if cout <> stdout then close_out cout + let test_decl_not_driver decl = + let decl_name = ML.get_decl_name decl in + let test_id_not_driver id = + Printer.query_syntax pargs.Pdriver.syntax id = None in + List.exists test_id_not_driver decl_name in + 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 + let flat = opt_modu_flat = Flat in + List.iter (pr pargs ?old ?fname ~flat m fmt) mdecls; + if cout <> stdout then close_out cout end let find_module_path mm path m = match path with | [] -> @@ -308,15 +314,15 @@ let () = let (_fg, pargs, pr) = Pdriver.lookup_printer opt_driver in let mm = Mstr.empty in let cout = match opt_output with - | None -> stdout - | Some file -> open_out file in + | None -> stdout + | Some file -> open_out file in let fmt = formatter_of_out_channel cout in - let extract id = + let extract fmt id = let pm = find_module_id mm id in let m = translate_module pm in let d = Ident.Mid.find id m.ML.mod_known in pr pargs ~flat:true pm fmt d in - List.iter extract (List.rev !toextract); + List.iter (extract fmt) (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; -- GitLab