Commit b8d3a796 authored by Mário Pereira's avatar Mário Pereira

Code extraction (wip)

parent fb4b1eba
......@@ -1671,7 +1671,7 @@ test-ocaml-extraction: bin/why3.opt bin/why3extract.opt lib/why3/why3extract.cmx
#######################################
# 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
@bin/why3extract.opt -D drivers/ocaml64.drv \
......
......@@ -106,10 +106,9 @@ module queue.Queue
end
module array.Array
prelude "open Why3extract"
syntax type array "(%1 Why3__Array.t)"
syntax type array "(%1 Array.t)"
syntax function ([]) "(Why3__Array.get %1 %2)"
syntax function ([]) "(Array.get %1 %2)"
syntax exception OutOfBounds "Why3__Array.OutOfBounds"
......
......@@ -354,6 +354,8 @@ module Translate = struct
let args = filter_params args in
if args = [] then [ML.mk_var_unit ()] else args
exception ExtractionAny
(* expressions *)
let rec expr info ({e_effect = eff} as e) =
assert (not eff.eff_ghost);
......@@ -422,7 +424,7 @@ module Translate = struct
let args = params cty.cty_args in
ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
| Eexec ({c_node = Cany}, _) ->
(* Error message here *) assert false
raise ExtractionAny
| Eabsurd ->
ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
| Ecase (e1, _) when e_ghost e1 ->
......@@ -504,19 +506,15 @@ module Translate = struct
ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
end
let is_val e =
match e.e_node with
| Eexec ({c_node = Cany}, _) -> true
| _ -> false
exception ExtractionVal of rsymbol
(* program declarations *)
let pdecl info pd =
match pd.pd_node with
| PDlet (LDsym (rs, _)) when rs_ghost rs ->
[]
| PDlet (LDsym (_, {c_node = Cfun e})) when is_val e ->
(* FIXME: check that this symbol is defined in driver *)
[]
| PDlet (LDsym (rs, {c_node = Cany}))->
raise (ExtractionVal rs)
| PDlet (LDsym ({rs_cty = {cty_args = []}} as rs, {c_node = Cfun e})) ->
[ML.Dlet (ML.Lsym (rs, [], expr info e))]
| PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
......@@ -528,20 +526,15 @@ module Translate = struct
let e = match e.c_node with Cfun e -> e | _ -> assert false in
let args = params rs1.rs_cty.cty_args in
{ ML.rec_sym = rs1; ML.rec_rsym = rs2;
ML.rec_args = args; ML.rec_exp = expr info e }) rl
in
ML.rec_args = args; ML.rec_exp = expr info e }) rl in
[ML.Dlet (ML.Lrec rec_def)]
| PDlet (LDsym _)
| PDpure
| PDlet (LDvar (_, _)) ->
| PDlet (LDsym _) | PDpure | PDlet (LDvar (_, _)) ->
[]
| PDtype itl ->
[ML.Dtype (List.map tdef itl)]
| PDexn xs ->
if ity_equal xs.xs_ity ity_unit then
[ML.Dexn (xs, None)]
else
[ML.Dexn (xs, Some (ity xs.xs_ity))]
if ity_equal xs.xs_ity ity_unit then [ML.Dexn (xs, None)]
else [ML.Dexn (xs, Some (ity xs.xs_ity))]
(* unit module declarations *)
let mdecl info = function
......@@ -553,6 +546,14 @@ module Translate = struct
let module_ info m =
List.concat (List.map (mdecl info) m.mod_units)
let () = Exn_printer.register (fun fmt e -> match e with
| ExtractionAny ->
Format.fprintf fmt "Cannot extract an undefined node"
| ExtractionVal rs ->
Format.fprintf fmt "Function %a cannot be extracted"
print_rs rs
| _ -> raise e)
end
(** Some transformations *)
......@@ -575,7 +576,7 @@ module Transform = struct
| Elet (Lvar (pv, ({e_node = Eapp (rs, [])} as e1)), e2)
when Translate.isconstructor info rs ->
(* only optimize constructors with no argument *)
(* as it is a Lvar the constructor is not completely applied *)
(* because of Lvar we know the constructor is completely applied *)
add_subst pv e1 e2
| Elet (ld, e) ->
mk (Elet (let_def info subst ld, expr info subst e))
......
......@@ -315,7 +315,7 @@ module Print = struct
| Eapp (s, pvl) ->
print_apply info fmt (Hrs.find_def ht_rs s s) pvl
| Ematch (e, pl) ->
fprintf fmt "begin match @[%a@] with@\n@[<hov>%a@] end"
fprintf fmt "begin match @[%a@] with@\n@[<hov>%a@]@\nend"
(print_expr info) e (print_list newline (print_branch info)) pl
| Eassign al ->
let assign fmt (rho, rs, pv) =
......@@ -438,7 +438,6 @@ let extract_module pargs ?old fmt ({mod_theory = th} as m) =
info_mo_known_map = m.mod_known;
info_fname = None; (* TODO *)
} in
(* fprintf fmt "(\*@\n%a@\n*\)@\n" print_module m; *)
fprintf fmt
"(* This file has been generated from Why3 module %a *)@\n@\n"
Print.print_module_name m;
......@@ -447,7 +446,6 @@ let extract_module pargs ?old fmt ({mod_theory = th} as m) =
print_list nothing (Print.print_decl info) fmt mdecls;
fprintf fmt "@."
let fg ?fname m =
let mod_name = m.Pmodule.mod_theory.Theory.th_name.id_string in
match fname with
......
(* main file for ../test_extraction.mlw so that we *run* the extracted code *)
open Why3extract
open Test_extraction__TestExtraction
let (=) = Z.eq
let (=) = Why3__BigInt.eq
let b42 = Why3__BigInt.of_int 42
let b42 = Z.of_int 42
let () = assert (test_int () = b42)
let () = assert (test_int32 () = b42)
let () = assert (test_uint32 () = b42)
......
......@@ -4,6 +4,9 @@ module M
use import int.Int
use import mach.int.Int
val test_val (x: int) : int
ensures { result > x }
let function f_function (y: int) (x: int) : int
requires { x >= 0 }
ensures { result >= 0 }
......
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