Commit 1d1515e3 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Merge branch 'use_api_with_expr' into 'master'

Use api with expr

See merge request why3/why3!141
parents 1aca8fe6 12b304de
......@@ -185,6 +185,44 @@ let d2 =
with exn -> Format.eprintf "error: %a@." Exn_printer.exn_printer exn;
exit 1
let d2' =
let id = Ident.id_fresh "f" in
let result =
Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int
in
let post =
Term.ps_app Term.ps_equ [Term.t_var result; Term.t_nat_const 0]
in
let body =
(* building expression "ref 0" *)
let e =
let c0 = Expr.e_const (Number.int_const_of_int 0) Ity.ity_int in
let refzero_type = Ity.ity_app ref_type [Ity.ity_int] [] in
let f = Expr.e_app ref_fun [c0] [] refzero_type in
Expr.e_func_app f c0
in
(* building the first part of the let x = ref 0 *)
let id_x = Ident.id_fresh "x" in
let letdef, var_x = Expr.let_var id_x e in
(* building expression "!x" *)
let bang_x = Expr.e_app get_fun [Expr.e_var var_x] [] Ity.ity_int in
(* the complete body *)
Expr.e_let letdef bang_x
in
let arg_unit =
let unit = Ident.id_fresh "unit" in
Ity.create_pvsymbol unit Ity.ity_unit
in
let def,rs = Expr.let_sym id
(Expr.c_fun [arg_unit] [post] [] Ity.Mxs.empty Ity.Mpv.empty body) in
try
let def = Pdecl.create_let_decl def in
Format.eprintf "It works!@.";
def
with exn -> Format.eprintf "error: %a@." Exn_printer.exn_printer exn;
exit 1
(*
(* let f (a:array int)
requires { a.length >= 1 }
......
......@@ -362,6 +362,8 @@ type effect = private {
}
val eff_empty : effect
(** Effect of a non-ghost total function without any observational effect of any
kinds *)
val eff_equal : effect -> effect -> bool
val eff_pure : effect -> bool
......
Supports Markdown
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