Commit 06ec684d authored by MARCHE Claude's avatar MARCHE Claude

use_api: example of application of a WhyML function

parent 4063e434
......@@ -242,6 +242,7 @@ let () =
(* build a whyml program *)
(* start a module named "Program" *)
let m = Mlw_module.create_module env (Ident.id_fresh "Program")
let mul_int : Term.lsymbol =
......@@ -249,6 +250,13 @@ let mul_int : Term.lsymbol =
let unit_type = Ty.ty_tuple []
(* declaration of
let f (_dummy:unit) : unit
requires { true }
ensures { true }
=
assert { 6*7 = 42 }
*)
let d =
let args =
[Mlw_ty.create_pvsymbol
......@@ -257,7 +265,7 @@ let d =
let result = Term.create_vsymbol (Ident.id_fresh "result") unit_type in
let spec = {
Mlw_ty.c_pre = Term.t_true;
c_post = Term.t_eps (Term.t_close_bound result Term.t_true);
c_post = Mlw_ty.create_post result Term.t_true;
c_xpost = Mlw_ty.Mexn.empty;
c_effect = Mlw_ty.eff_empty;
c_variant = [];
......@@ -282,6 +290,80 @@ let d =
let def = Mlw_expr.create_fun_defn (Ident.id_fresh "f") lambda in
Mlw_decl.create_rec_decl [def]
(*
declaration of
let f (_dummy:unit) : unit
requires { true }
ensures { result = 0 }
=
let x = ref 0 in
!x
*)
(* import the ref.Ref module *)
let ref_modules, ref_theories =
Env.read_lib_file (Mlw_main.library_of_env env) ["ref"]
let ref_module : Mlw_module.modul = Stdlib.Mstr.find "Ref" ref_modules
let ref_type : Mlw_ty.T.itysymbol =
match
Mlw_module.ns_find_ts ref_module.Mlw_module.mod_export ["ref"]
with
| Mlw_module.PT itys -> itys
| Mlw_module.TS _ -> assert false
(* the "ref" function *)
let ref_fun : Mlw_expr.psymbol =
match
Mlw_module.ns_find_ps ref_module.Mlw_module.mod_export ["ref"]
with
| Mlw_module.PS p -> p
| _ -> assert false
let d2 =
let args =
[Mlw_ty.create_pvsymbol
(Ident.id_fresh "_dummy") (Mlw_ty.vty_value Mlw_ty.ity_unit)]
in
let result = Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int in
let spec = {
Mlw_ty.c_pre = Term.t_true;
c_post = Mlw_ty.create_post result Term.t_true;
c_xpost = Mlw_ty.Mexn.empty;
c_effect = Mlw_ty.eff_empty;
c_variant = [];
c_letrec = 0;
}
in
let body =
let pv = Mlw_ty.create_pvsymbol (Ident.id_fresh "a") (Mlw_ty.vty_value Mlw_ty.ity_int) in
let ity = Mlw_ty.ity_app_fresh ref_type [Mlw_ty.ity_int] in
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue (Mlw_ty.vty_value ity)) in
let e1 = Mlw_expr.e_arrow ref_fun vta in
let c0 = Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0")) in
let e = Mlw_expr.e_app e1 [c0] in
let letdef = Mlw_expr.create_let_defn (Ident.id_fresh "x") e in
Mlw_expr.e_let letdef c0
in
let lambda = {
Mlw_expr.l_args = args;
l_expr = body;
l_spec = spec;
}
in
let def = Mlw_expr.create_fun_defn (Ident.id_fresh "f") lambda in
Mlw_decl.create_rec_decl [def]
(* TODO: continue *)
......
......@@ -56,11 +56,11 @@ let oct_escape = '\\' rO rO? rO?
(* integer literals, both decimal, hexadecimal and octal *)
rule integer_literal = parse
(* hexadecimal *)
| '0'['x''X'] (rH+ as d) rIS eof { Term.int_const_hexa d }
| '0'['x''X'] (rH+ as d) rIS eof { Number.int_const_hex d }
(* octal *)
| '0' (rO+ as d) rIS eof { Term.int_const_octal d }
| '0' (rO+ as d) rIS eof { Number.int_const_oct d }
(* decimal *)
| (rD+ as d) rIS eof { Term.int_const_decimal d }
| (rD+ as d) rIS eof { Number.int_const_dec d }
(* TODO: character literals
| ('L'? "'" as prelude) (([^ '\\' '\'' '\n']|("\\"[^ '\n']))+ as content) "'"
{
......
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