Commit 7fc22352 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

simplify boolean expressions in WPs

parent ed9c52d3
......@@ -1678,6 +1678,7 @@ and f_subst_fmla_alpha f1 f2 f = if f_equal_alpha f f1 then f2 else
let f_not_simp f = match f.f_node with
| Ftrue -> f_false
| Ffalse -> f_true
| Fnot f -> f
| _ -> f_not f
let f_and_simp f1 f2 = match f1.f_node, f2.f_node with
......@@ -1726,9 +1727,9 @@ let t_if_simp f t1 t2 = match f.f_node with
let f_if_simp f1 f2 f3 = match f1.f_node, f2.f_node, f3.f_node with
| Ftrue, _, _ -> f2
| Ffalse, _, _ -> f3
| _, Ftrue, _ -> f_or_simp f1 f3
| _, Ffalse, _ -> f_and_simp (f_not f1) f3
| _, _, Ftrue -> f_or_simp (f_not f1) f2
| _, Ftrue, _ -> f_implies_simp (f_not_simp f1) f3
| _, Ffalse, _ -> f_and_simp (f_not_simp f1) f3
| _, _, Ftrue -> f_implies_simp f1 f2
| _, _, Ffalse -> f_and_simp f1 f2
| _, _, _ -> if f_equal f2 f3 then f2 else f_if f1 f2 f3
......
......@@ -54,6 +54,7 @@ type env = {
ls_False: lsymbol;
ls_andb : lsymbol;
ls_orb : lsymbol;
ls_notb : lsymbol;
ls_unit : lsymbol;
}
......@@ -139,9 +140,10 @@ let empty_env uc = {
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"];
ls_unit = find_ls uc ["Tuple0"];
ls_andb = find_ls uc ["andb"];
ls_orb = find_ls uc ["orb"];
ls_notb = find_ls uc ["notb"];
ls_unit = find_ls uc ["Tuple0"];
}
let make_arrow_type env tyl ty =
......
......@@ -54,6 +54,7 @@ type env = private {
ls_False: lsymbol;
ls_andb : lsymbol;
ls_orb : lsymbol;
ls_notb : lsymbol;
ls_unit : lsymbol;
}
......
......@@ -381,12 +381,35 @@ and wp_recfun env (_, bl, _var, t) =
let wp env e =
wp_expr env e (default_post e.expr_type e.expr_effect)
let rec t_btop env t = match t.t_node with
| Tif (f,t1,t2) -> let f = f_btop env f in
f_label t.t_label (f_if_simp f (t_btop env t1) (t_btop env t2))
| Tapp (ls, [t1;t2]) when ls_equal ls env.ls_andb ->
f_label t.t_label (f_and_simp (t_btop env t1) (t_btop env t2))
| Tapp (ls, [t1;t2]) when ls_equal ls env.ls_orb ->
f_label t.t_label (f_or_simp (t_btop env t1) (t_btop env t2))
| Tapp (ls, [t1]) when ls_equal ls env.ls_notb ->
f_label t.t_label (f_not_simp (t_btop env t1))
| Tapp (ls, []) when ls_equal ls env.ls_True ->
f_label t.t_label f_true
| Tapp (ls, []) when ls_equal ls env.ls_False ->
f_label t.t_label f_false
| _ ->
f_equ t (t_True env)
and f_btop env f = match f.f_node with
| Fapp (ls, [{t_ty = {ty_node = Tyapp (ts, [])}} as l; r])
when ls_equal ls ps_equ && ts_equal ts env.ts_bool ->
f_label_copy f (f_iff_simp (t_btop env l) (t_btop env r))
| _ -> f_map (fun t -> t) (f_btop env) f
let add_wp_decl l f env =
let s = "WP_" ^ l.ls_name.id_string in
let id = match id_from_user l.ls_name with
| None -> id_fresh s
| Some loc -> id_user s loc
in
let f = f_btop env f in
let pr = create_prsymbol id in
let d = create_prop_decl Pgoal pr f in
add_decl d env
......
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