programs: lazy operators

parent 260ddcbd
parameter incr : x:int ref -> { } unit writes x { !x = old !x + 1 }
parameter x : int ref
parameter id_not_0 : x:int -> { x <> 0 } int { result = x }
parameter id : x:int -> { } int { result = x }
let test_and_1 () =
{ }
if (incr x; !x > 0) && id !x = 1 then !x else 0+1
{ result = 1 }
let test_and_2 () =
{ !x <> 0 }
if id_not_0 !x >= 1 && !x <= 1 then !x else 0+1
{ result = 1 }
let test_or_1 () =
{ }
if (incr x; !x > 0) || !x < 0 then 1 else 2
{ result = 1 -> !x <> 0 }
let test_or_2 () =
{ }
if !x = 0 || !x = 1 then !x else 1
{ 0 <= result <= 1 }
let test_not_1 () =
{ }
if not (!x = 0) then x := 0
{ !x = 0 }
let test_not_2 () =
{ !x <= 0 }
while not (!x = 0) do invariant { !x <= 0 } incr x done
{ !x = 0 }
let test_all_1 () =
{ }
(!x >= 0 && not (!x = 0) || !x >= 1)
{ result=True <-> !x>=1 }
(* from Cesar Munoz's CD3D *)
{
logic d : int
}
parameter vx : int ref
parameter vy : int ref
parameter sq : x:int -> {} int { result = x*x }
let test_cd3d () =
{ true }
if !vx=0 && !vy=0 && sq !vx + sq !vy < sq d then 1 else 2
{ result=1 -> !vx=0 and !vy=0 }
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/booleans"
End:
*)
../programs/good/booleans.mlw
\ No newline at end of file
......@@ -101,6 +101,9 @@ let equal t1 t2 =
Sref.equal t1.writes t2.writes &&
Sls.equal t1.raises t2.raises
let no_side_effect t =
Sref.is_empty t.writes && Sls.is_empty t.raises
let subst vs r t =
let add1 r' s = match r' with
| Rlocal vs' when vs_equal vs' vs -> Sref.add r s
......
......@@ -52,6 +52,8 @@ val union : t -> t -> t
val equal : t -> t -> bool
val no_side_effect : t -> bool
val subst : vsymbol -> reference -> t -> t
val print_reference : Format.formatter -> reference -> unit
......
......@@ -52,6 +52,9 @@ type env = {
ls_bang : lsymbol;
ls_old : lsymbol;
ls_True : lsymbol;
ls_False: lsymbol;
ls_andb : lsymbol;
ls_orb : lsymbol;
}
......@@ -135,6 +138,9 @@ let empty_env uc = {
ls_bang = find_ls uc ["prefix !"];
ls_old = find_ls uc ["old"];
ls_True = find_ls uc ["True"];
ls_False = find_ls uc ["False"];
ls_andb = find_ls uc ["andb"];
ls_orb = find_ls uc ["orb"];
}
let make_arrow_type env tyl ty =
......
......@@ -48,6 +48,9 @@ type env = private {
ls_bang : lsymbol;
ls_old : lsymbol;
ls_True : lsymbol;
ls_False: lsymbol;
ls_andb : lsymbol;
ls_orb : lsymbol;
}
val empty_env : theory_uc -> env
......
......@@ -819,6 +819,35 @@ let without_exn_check f x =
end else
f x
(*s Pure expressions. Used in [Slazy_and] and [Slazy_or] to decide
whether to use [strict_bool_and_] and [strict_bool_or_] or not. *)
let rec is_pure_expr e =
E.no_side_effect e.expr_effect &&
match e.expr_desc with
| Elocal _ | Elogic _ | Eskip -> true
| Eif (e1, e2, e3) -> is_pure_expr e1 && is_pure_expr e2 && is_pure_expr e3
| Elet (_, e1, e2) -> is_pure_expr e1 && is_pure_expr e2
| Elabel (_, e1) -> is_pure_expr e1
| Eany c -> E.no_side_effect c.c_effect
| Eghost _ | Eassert _ | Etry _ | Eraise _ | Ematch _
| Elazy _ | Eloop _ | Esequence _ | Eletrec _ | Efun _
| Eglobal _ | Eabsurd -> false (* TODO: improve *)
let mk_expr loc ty ef d =
{ expr_desc = d; expr_type = ty; expr_type_v = Tpure ty;
expr_effect = ef; expr_loc = loc }
let mk_simple_expr loc ty d = mk_expr loc ty E.empty d
let mk_bool_constant loc gl ls =
let ty = ty_app gl.ts_bool [] in
{ expr_desc = Elogic (t_app ls [] ty); expr_type = ty; expr_type_v = Tpure ty;
expr_effect = E.empty; expr_loc = loc }
let mk_false loc gl = mk_bool_constant loc gl gl.ls_False
let mk_true loc gl = mk_bool_constant loc gl gl.ls_True
(* [expr] translates iexpr into expr
[env : type_v Mvs.t] maps local variables to their types *)
......@@ -890,8 +919,29 @@ and expr_desc gl env loc ty = function
| None -> ef
in
Eloop (a, e1), type_v_unit gl, ef
| IElazy _ ->
assert false (*TODO*)
| IElazy (op, e1, e2) ->
let e1 = expr gl env e1 in
let e2 = expr gl env e2 in
let ef = E.union e1.expr_effect e2.expr_effect in
let d =
if is_pure_expr e2 then
let ls = match op with
| Pgm_ptree.LazyAnd -> gl.ls_andb
| Pgm_ptree.LazyOr -> gl.ls_orb
in
let v1 = create_vsymbol (id_fresh "lazy") ty in
let v2 = create_vsymbol (id_fresh "lazy") ty in
let t = t_app ls [t_var v1; t_var v2] ty in
Elet (v1, e1,
mk_expr loc ty ef
(Elet (v2, e2, mk_simple_expr loc ty (Elogic t))))
else match op with
| Pgm_ptree.LazyAnd ->
Eif (e1, e2, mk_false loc gl)
| Pgm_ptree.LazyOr ->
Eif (e1, mk_true loc gl, e2)
in
d, Tpure ty, ef
| IEmatch _ ->
assert false (*TODO*)
| IEskip ->
......
let rec f (x:int) =
{ x>=0 }
if x = 0 then 0 else g (x-1)
{ result=0 }
and g (x:int) =
{}
f 3
{ result=0}
let foo (x:int ref) =
{ }
if !x = 0 && !x = 1 then 2 else 3
{ result = 3 }
(*
Local Variables:
......
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