From 682f1410efc376b9ecccd6e2f002be5e0da6a089 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mpereira@lri.fr> Date: Fri, 3 Mar 2017 14:03:04 +0100 Subject: [PATCH] Code extraction Preparing for the GT demo --- drivers/ocaml64.drv | 2 +- src/mlw/ocaml_printer.ml | 18 +++++++++--------- src/tools/why3extract.ml | 8 +++++--- 3 files changed, 15 insertions(+), 13 deletions(-) diff --git a/drivers/ocaml64.drv b/drivers/ocaml64.drv index 6a4d5acd6c..bf475ee09c 100644 --- a/drivers/ocaml64.drv +++ b/drivers/ocaml64.drv @@ -65,7 +65,7 @@ end *) module mach.int.Int63 - syntax val of_int "%1" + syntax val of_int "Z.to_int %1" syntax converter of_int "%1" syntax function to_int "Z.of_int %1" diff --git a/src/mlw/ocaml_printer.ml b/src/mlw/ocaml_printer.ml index 194482474d..1036bf05db 100644 --- a/src/mlw/ocaml_printer.ml +++ b/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 let lp, t, q = try Pmodule.restore_path id with Not_found -> Theory.restore_path id in @@ -111,8 +111,8 @@ module Print = struct let print_lident = print_qident ~sanitizer:Strings.uncapitalize let print_uident = print_qident ~sanitizer:Strings.capitalize - let print_tv fmt tv = - fprintf fmt "'%s" (id_unique aprinter tv.tv_name) + let print_tv info fmt tv = + fprintf fmt "'%a" (print_lident info) tv.tv_name let protect_on b s = if b then "(" ^^ s ^^ ")" else s @@ -133,7 +133,7 @@ module Print = struct let rec print_ty ?(paren=false) info fmt = function | Tvar tv -> - print_tv fmt tv + print_tv info fmt tv | Ttuple [] -> fprintf fmt "unit" | Ttuple tl -> @@ -161,11 +161,11 @@ module Print = struct let print_vsty info fmt (v, ty, _) = fprintf fmt "%a:@ %a" print_ident v (print_ty ~paren:false info) ty - let print_tv_arg = print_tv - let print_tv_args fmt = function + let print_tv_arg info = print_tv info + let print_tv_args info fmt = function | [] -> () - | [tv] -> fprintf fmt "%a@ " print_tv_arg tv - | tvl -> fprintf fmt "(%a)@ " (print_list comma print_tv_arg) tvl + | [tv] -> fprintf fmt "%a@ " (print_tv_arg info) tv + | tvl -> fprintf fmt "(%a)@ " (print_list comma (print_tv_arg info)) tvl let print_vs_arg info fmt vs = fprintf fmt "@[(%a)@]" (print_vsty info) vs @@ -446,7 +446,7 @@ module Print = struct fprintf fmt " =@ %a" (print_ty ~paren:false info) ty in fprintf fmt "@[<hov 2>%s %a%a%a@]" - (if fst then "type" else "and") print_tv_args its.its_args + (if fst then "type" else "and") (print_tv_args info) its.its_args (print_lident info) its.its_name print_def its.its_def let print_decl info fmt = function diff --git a/src/tools/why3extract.ml b/src/tools/why3extract.ml index e28147d6e8..246a436bc3 100644 --- a/src/tools/why3extract.ml +++ b/src/tools/why3extract.ml @@ -290,9 +290,11 @@ let visit mm id = else toextract := id :: !toextract let flat_extraction target = match Opt.get target with - | File _ -> () - (* let format = !opt_parser in - read_mlw_file ?format env fname *) + | File fname -> + let format = !opt_parser in + let mm = read_mlw_file ?format env fname in + let do_m _ m = do_extract_module ~fname m in + Mstr.iter do_m mm | Module (path, m) -> let mm = Mstr.empty in let m = find_module_path mm path m in -- GitLab