From 8193b6affb0fb3a3ad14ffbd7d68ea57f234b5be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1rio=20Pereira?= Date: Thu, 23 Feb 2017 19:14:41 +0100 Subject: [PATCH] Code extraction (wip) Better treatment of partial applied constructors --- drivers/ocaml64.drv | 4 ++-- src/mlw/compile.ml | 34 +++++++++++++++++++--------------- src/mlw/ocaml_printer.ml | 16 ++++++++++++---- src/mlw/pdriver.ml | 2 +- src/mlw/pdriver.mli | 2 +- src/tools/why3extract.ml | 19 +++++++++---------- 6 files changed, 44 insertions(+), 33 deletions(-) diff --git a/drivers/ocaml64.drv b/drivers/ocaml64.drv index 027f2a5f1..bf475ee09 100644 --- a/drivers/ocaml64.drv +++ b/drivers/ocaml64.drv @@ -71,8 +71,8 @@ module mach.int.Int63 syntax function to_int "Z.of_int %1" syntax type int63 "int" - syntax constant min_int63 "min_int" - syntax constant max_int63 "max_int" + syntax constant min_int63 "Z.of_int min_int" + syntax constant max_int63 "Z.of_int max_int" syntax val ( + ) "%1 + %2" syntax val ( - ) "%1 - %2" syntax val (-_) "- %1" diff --git a/src/mlw/compile.ml b/src/mlw/compile.ml index 2ae6a5a38..472ab5504 100644 --- a/src/mlw/compile.ml +++ b/src/mlw/compile.ml @@ -211,18 +211,6 @@ module ML = struct end -type decl = ML.decl - -type info = { - info_syn : syntax_map; - info_convert : syntax_map; - info_current_th : Theory.theory; - info_current_mo : Pmodule.pmodule option; - info_th_known_map : Decl.known_map; - info_mo_known_map : Pdecl.known_map; - info_fname : string option; -} - (** Translation from Mlw to ML *) module Translate = struct @@ -231,6 +219,16 @@ module Translate = struct open Pmodule open Pdecl + type info = { + (* info_syn : syntax_map; *) + (* info_convert : syntax_map; *) + (* info_current_th : Theory.theory; *) + info_current_mo : Pmodule.pmodule option; + (* info_th_known_map : Decl.known_map; *) + info_mo_known_map : Pdecl.known_map; + (* info_fname : string option; *) + } + (* useful predicates and transformations *) let pv_not_ghost e = not e.pv_ghost @@ -337,7 +335,7 @@ module Translate = struct List.exists is_constructor its | _ -> false - let make_eta_expansion rsc pvl cty_app = + let mk_eta_expansion rsc pvl cty_app = (* FIXME : effects and types of the expression in this situation *) let args_f = let def pv = pv_name pv, ity pv.pv_ity, pv.pv_ghost in @@ -452,9 +450,12 @@ module Translate = struct ML.mk_expr ml_letrec (ML.I e.e_ity) eff | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) when isconstructor info rs_app -> - let eta_app = make_eta_expansion rs_app pvl cty in + (* partial application of constructor *) + let eta_app = mk_eta_expansion rs_app pvl cty in let ein = expr info ein in - let res = ity cty.cty_result in + let mk_func pv f = ity_func pv.pv_ity f in + let func = List.fold_right mk_func cty.cty_args cty.cty_result in + let res = ity func in let ml_letrec = ML.Elet (ML.Lsym (rsf, res, [], eta_app), ein) in ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) -> @@ -486,6 +487,9 @@ module Translate = struct ML.mk_unit | 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 -> + mk_eta_expansion rs pvl cty | Eexec ({c_node = Capp (rs, pvl); _}, _) -> let pvl = app pvl in ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff diff --git a/src/mlw/ocaml_printer.ml b/src/mlw/ocaml_printer.ml index b69699090..06c72c423 100644 --- a/src/mlw/ocaml_printer.ml +++ b/src/mlw/ocaml_printer.ml @@ -25,6 +25,16 @@ open Stdlib open Pdecl open Printer +type info = { + info_syn : syntax_map; + info_convert : syntax_map; + info_current_th : Theory.theory; + info_current_mo : Pmodule.pmodule option; + info_th_known_map : Decl.known_map; + info_mo_known_map : Pdecl.known_map; + info_fname : string option; +} + module Print = struct open ML @@ -448,10 +458,8 @@ module Print = struct print_ident xs.xs_name (print_ty ~paren:true info) t end -let extract_module pargs ?old ?fname ({mod_theory = th} as m) fmt d = - ignore (pargs); +let print_decl pargs ?old ?fname ({mod_theory = th} as m) fmt d = ignore (old); - ignore (m); let info = { info_syn = pargs.Pdriver.syntax; info_convert = pargs.Pdriver.converter; @@ -470,7 +478,7 @@ let fg ?fname m = (module_name ?fname path mod_name) ^ ".ml" let () = Pdriver.register_printer "ocaml" - ~desc:"printer for OCaml code" fg extract_module + ~desc:"printer for OCaml code" fg print_decl (* * Local Variables: diff --git a/src/mlw/pdriver.ml b/src/mlw/pdriver.ml index 6763b2dbf..67d548a41 100644 --- a/src/mlw/pdriver.ml +++ b/src/mlw/pdriver.ml @@ -222,7 +222,7 @@ type filename_generator = ?fname:string -> Pmodule.pmodule -> string type printer = printer_args -> ?old:in_channel -> ?fname:string -> Pmodule.pmodule -> - Compile.decl Pp.pp + Compile.ML.decl Pp.pp type reg_printer = Pp.formatted * filename_generator * printer diff --git a/src/mlw/pdriver.mli b/src/mlw/pdriver.mli index 8fbf0feb2..d8accfbfd 100644 --- a/src/mlw/pdriver.mli +++ b/src/mlw/pdriver.mli @@ -39,7 +39,7 @@ val load_driver : Env.env -> string -> string list -> driver type printer = printer_args -> ?old:in_channel -> ?fname:string -> Pmodule.pmodule -> - Compile.decl Pp.pp + Compile.ML.decl Pp.pp type filename_generator = ?fname:string -> Pmodule.pmodule -> string diff --git a/src/tools/why3extract.ml b/src/tools/why3extract.ml index b254b1aec..140294560 100644 --- a/src/tools/why3extract.ml +++ b/src/tools/why3extract.ml @@ -119,16 +119,16 @@ let opt_driver = eprintf "%a@." Exn_printer.exn_printer e; exit 1 -let extract_to ?fname ({mod_theory = th} as m) = +let extract_to ?fname m = let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in let info = { - info_syn = pargs.Pdriver.syntax; - info_convert = pargs.Pdriver.converter; - info_current_th = th; - info_current_mo = Some m; - info_th_known_map = th.Theory.th_known; - info_mo_known_map = m.mod_known; - info_fname = Opt.map Compile.clean_name fname + (* info_syn = pargs.Pdriver.syntax; *) + (* info_convert = pargs.Pdriver.converter; *) + (* info_current_th = th; *) + Translate.info_current_mo = Some m; + (* info_th_known_map = th.Theory.th_known; *) + Translate.info_mo_known_map = m.mod_known; + (* info_fname = Opt.map Compile.clean_name fname *) } in let mdecls = Translate.module_ info m in let mdecls = Transform.module_ info mdecls in @@ -147,8 +147,7 @@ let extract_to ?fname ({mod_theory = th} as m) = Debug.dprintf Pdriver.debug "extract module %s to file %s@." tname file; List.iter (pr ?old ?fname pargs m fmt) mdecls; close_out cout - | Monolithic -> - () + | Monolithic -> () let extract_to = let visited = Ident.Hid.create 17 in -- GitLab