Commit 614d8b16 authored by Mário Pereira's avatar Mário Pereira

Code extraction : extracting now into file; registered printer for ocaml

parent d39596d4
......@@ -1669,6 +1669,16 @@ test-ocaml-extraction: bin/why3.opt bin/why3extract.opt lib/why3/why3extract.cmx
ref__Refint.ml test_extraction__TestExtraction.ml main.ml
@tests/test-extraction/a.out
#######################################
# this should be removed in the future
######################################
test-extraction: bin/why3.opt bin/why3extract.opt lib/why3/why3extract.cmxa
@mkdir -p tests/test-extraction-mario
@cd tests ; ../bin/why3extract.opt -D ../drivers/ocaml64.drv \
test_extraction_mario.mlw -o test-extraction-mario
@cd tests/test-extraction-mario/ ; \
$(OCAMLOPT) test_extraction_mario__M.ml
################
# documentation
################
......
......@@ -135,7 +135,7 @@ module matrix.Matrix
prelude "open Why3extract"
syntax type matrix "(%1 Why3__Matrix.t)"
syntax function get "(Why3__Matrix.get %1 %2)"
(* FIXME syntax function get "(Why3__Matrix.get %1 %2)" *)
syntax exception OutOfBounds "Why3__Matrix.OutOfBounds"
......
(** Arithmetic-independent OCaml driver *)
(* FIXME
theory HighOrd
syntax type func "(%1 -> %2)"
syntax type pred "(%1 -> bool)"
syntax function (@) "(%1 %2)"
end
*)
theory option.Option
syntax type option "(%1 option)"
......@@ -80,4 +82,3 @@ module null.Null
syntax val get "(fun x -> x)"
end
......@@ -197,7 +197,7 @@ module mach.array.Array32
end
module mach.array.Array63
syntax type array63 "(%1 array)"
(* FIXME syntax type array63 "(%1 array)" *)
syntax val make "Array.make"
syntax val ([]) "Array.get"
......@@ -211,7 +211,7 @@ module mach.array.Array63
syntax val self_blit "Array.blit"
end
module mach.array.Array63
syntax type array63 "(%1 array)"
(* FIXME syntax type array63 "(%1 array)" *)
syntax val make "Array.make"
syntax val ([]) "Array.get"
......
......@@ -52,6 +52,10 @@
- comme l'AST [expr] est déjà en forme normale-A, est-ce que ça
fait du sense pour vous d'utiliser des applications de la forme
[Eapp of ident * ident list] ?
- faire un module Erasure, pour y concentrer tout ce qui
appartient à l'éffacement du code fantôme ?
*)
(*
......@@ -65,6 +69,7 @@ open Ident
open Ity
open Ty
open Term
open Printer
module ML = struct
......@@ -155,6 +160,16 @@ module ML = struct
end
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
......@@ -252,6 +267,9 @@ module Translate = struct
let e2 = expr e2 in
let e3 = expr e3 in
ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
(* | Eassign [(_, {rs_field = None; rs_name = id}, pv)] -> *)
(* let pv_id = pv_name pv in *)
(* ML.mk_expr ( *)
| _ -> (* TODO *) assert false
and ebranch ({pp_pat = p}, e) =
......@@ -271,7 +289,7 @@ module Translate = struct
rs.rs_name, List.map (fun {pv_vs = pv} -> type_ pv.vs_ty) rsc.cty_args)
(* type declarations/definitions *)
let tdef itd =
let tdef info itd =
let s = itd.itd_its in
let id = itd_name itd in
let args = its_args s in
......@@ -287,12 +305,12 @@ module Translate = struct
end
(* program declarations *)
let pdecl pd =
let pdecl info pd =
match pd.pd_node with
| PDlet (LDvar (_, _)) ->
[]
| PDlet (LDsym ({rs_name = rsn; rs_cty = cty}, {c_node = Cfun e})) ->
Format.printf "exec:%b@." (Exec.is_exec_pdecl () pd);
(* Format.printf "exec:%b@." (Exec.is_exec_pdecl () pd); *)
[ML.Dlet (false, [rsn, args cty.cty_args, expr e])]
| PDlet (LDsym ({rs_name = rsn}, {c_node = Capp _})) ->
Format.printf "LDsym Capp--> %s@." rsn.id_string;
......@@ -312,7 +330,7 @@ module Translate = struct
| PDpure ->
[]
| PDtype itl ->
List.map tdef itl
List.map (tdef info) itl
| PDexn ({xs_name = xsn} as xs) ->
if ity_equal xs.xs_ity ity_unit then
[ML.Dexn (xsn, None)]
......@@ -320,19 +338,19 @@ module Translate = struct
[ML.Dexn (xsn, Some (ity xs.xs_ity))]
(* unit module declarations *)
let mdecl = function
let mdecl info = function
| Udecl pd ->
pdecl pd
pdecl info pd
| _ -> (* TODO *) []
(* modules *)
let module_ m =
List.concat (List.map mdecl m.mod_units)
let module_ info m =
List.concat (List.map (mdecl info) m.mod_units)
end
(*
* Local Variables:
* compile-command: "make -C ../.. -j3"
* compile-command: "make -C ../.. -j3 bin/why3extract.opt"
* End:
*)
......@@ -139,6 +139,8 @@ module Print = struct
| Some o, [t1; t2] ->
fprintf fmt "@[<hov 1>%a %s %a@]"
print_ident t1 o print_ident t2
| _, [] ->
print_ident fmt s
| _, tl ->
fprintf fmt "@[<hov 2>%a %a@]"
print_ident s (print_list space print_ident) tl
......@@ -221,16 +223,36 @@ module Print = struct
end
let extract_module fmt m =
let extract_module pargs ?old fmt ({mod_theory = th} as m) =
ignore (pargs);
ignore (old);
ignore (m);
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.th_known;
info_mo_known_map = m.mod_known;
info_fname = None; (* TODO *)
} in
fprintf fmt
"(* This file has been generated from Why3 module %a *)@\n@\n"
Print.print_module_name m;
let mdecls = Translate.module_ m in
let mdecls = Translate.module_ info m in
print_list nothing Print.print_decl fmt mdecls;
fprintf fmt "@."
let fg ?fname m =
let mod_name = m.Pmodule.mod_theory.Theory.th_name.id_string in
match fname with
| None -> mod_name ^ ".ml"
| Some f -> (Filename.remove_extension f) ^ "__" ^ mod_name ^ ".ml"
let () = Pdriver.register_printer "ocaml" ~desc:"printer for OCaml code" fg extract_module
(*
* Local Variables:
* compile-command: "make -C ../.. -j3"
* compile-command: "make -C ../.. -j3 bin/why3extract.opt"
* End:
*)
......@@ -14,7 +14,7 @@ open Why3
open Stdlib
open Pmodule
(* open Compile (\* intermediate ML AST *\) *)
open Ocaml_printer
(* open Ocaml_printer *)
let usage_msg = sprintf
"Usage: %s [options] -D <driver> -o <dir> [[file|-] [-T <theory>]...]..."
......@@ -130,14 +130,23 @@ let extract_to =
let rec use_iter f l =
List.iter (function Uuse t -> f t | Uscope (_,_,l) -> use_iter f l | _ -> ()) l
let test_extract fmt m =
print_module fmt m;
fprintf fmt "@\n@\n";
(* Translate.module_ m *)
extract_module fmt m
(* let test_extract ?fname m = *)
(* Format.printf "antes@\n"; *)
(* let (fg, _, _) = Pdriver.lookup_printer opt_driver in *)
(* Format.printf "aqui@\n"; *)
(* let file = Filename.concat opt_output (fg ?fname m) in *)
(* let cout = open_out file in *)
(* let fmt = formatter_of_out_channel cout in *)
(* fprintf fmt "(\*@\n"; *)
(* print_module fmt m; *)
(* fprintf fmt "(\*@\n"; *)
(* fprintf fmt "@\n@\n"; *)
(* (\* Translate.module_ m *\) *)
(* extract_module opt_driver fmt m; *)
(* close_out cout *)
let rec do_extract_module ?fname m =
test_extract (Format.formatter_of_out_channel stdout) m;
(* test_extract ?fname m; *)
let _extract_use m' =
let fname =
if m'.mod_theory.Theory.th_path = [] then fname else None
......@@ -188,3 +197,9 @@ let () =
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3extract.opt"
End:
*)
......@@ -31,8 +31,10 @@ module M
ghost mutable v : seq 'a;
}
let update (c: cursor int) : unit
= let t = ghost c.v <- empty in t; ()
use import ref.Ref
(* let update (c: cursor int) : int *)
(* = c.index *)
exception Empty (list int, int)
exception Out_of_bounds int
......@@ -51,10 +53,16 @@ module M
let a () : unit
= assert { true }
let singleton (x: int) (l: list int) : list int =
let x = Nil in x
let test (x: int) : int =
let y = x in y + 1
end
(*
* Local Variables:
* compile-command: "make -C .. -j3; ../bin/why3extract -D ../drivers/c.drv -o extract test_extraction_mario.mlw"
* compile-command: "make -C .. test-extraction"
* End:
*)
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment