Commit 4d4a23fd authored by Andrei Paskevich's avatar Andrei Paskevich

translate 'if' of WhyML to 'if' of Why when the both branches are pure

this reduces the unnecessary branching in WPs, especially
for C-inspired expressions like (if <cond> then 1 else 0).
parent a147d17e
...@@ -443,14 +443,14 @@ and wp_desc env rm e q = match e.expr_desc with ...@@ -443,14 +443,14 @@ and wp_desc env rm e q = match e.expr_desc with
| Elogic t -> | Elogic t ->
let (v, q), _ = q in let (v, q), _ = q in
t_subst_single v t q t_subst_single v t q
| Elocal v -> | Elocal pv ->
let (res, q), _ = q in let (v, q), _ = q in
t_subst (subst1 res (t_var v.pv_pure)) q t_subst_single v (t_var pv.pv_pure) q
| Eglobal { ps_kind = PSfun _ } ->
let (_, q), _ = q in q
| Eglobal { ps_kind = PSvar pv } -> | Eglobal { ps_kind = PSvar pv } ->
let (v, q), _ = q in let (v, q), _ = q in
t_subst_single v (t_var pv.pv_pure) q t_subst_single v (t_var pv.pv_pure) q
| Eglobal { ps_kind = PSfun _ } ->
let (_, q), _ = q in q
| Eglobal { ps_kind = PSlogic } -> | Eglobal { ps_kind = PSlogic } ->
assert false assert false
| Efun (bl, t) -> | Efun (bl, t) ->
...@@ -472,14 +472,29 @@ and wp_desc env rm e q = match e.expr_desc with ...@@ -472,14 +472,29 @@ and wp_desc env rm e q = match e.expr_desc with
let wl = List.map (wp_recfun env rm) dl in let wl = List.map (wp_recfun env rm) dl in
wp_ands ~sym:true (w1 :: wl) wp_ands ~sym:true (w1 :: wl)
| Eif (e1, e2, e3) -> | Eif (e1, e2, e3) ->
let w2 = wp_expr env rm e2 (filter_post e2.expr_effect q) in let res = v_result e1.expr_type in
let w3 = wp_expr env rm e3 (filter_post e3.expr_effect q) in let test = t_equ (t_var res) (t_True env) in
let q1 = (* if result=True then w2 else w3 *) (* if the both branches are pure, do not split *)
let res = v_result e1.expr_type in let q1 =
let test = t_equ (t_var res) (t_True env) in try
let q1 = t_if test w2 w3 in let r2 = match e2.expr_desc with
saturate_post e1.expr_effect (res, q1) q | Elogic t -> t
| Elocal pv -> t_var pv.pv_pure
| Eglobal { ps_kind = PSvar pv } -> t_var pv.pv_pure
| _ -> raise Exit in
let r3 = match e3.expr_desc with
| Elogic t -> t
| Elocal pv -> t_var pv.pv_pure
| Eglobal { ps_kind = PSvar pv } -> t_var pv.pv_pure
| _ -> raise Exit in
let (v, q), _ = q in
t_subst_single v (t_if test r2 r3) q
with Exit ->
let w2 = wp_expr env rm e2 (filter_post e2.expr_effect q) in
let w3 = wp_expr env rm e3 (filter_post e3.expr_effect q) in
t_if test w2 w3
in in
let q1 = saturate_post e1.expr_effect (res, q1) q in
wp_expr env rm e1 q1 wp_expr env rm e1 q1
| Eloop ({ loop_invariant = inv; loop_variant = var }, e1) -> | Eloop ({ loop_invariant = inv; loop_variant = var }, e1) ->
let wfr = well_founded_rel var in let wfr = well_founded_rel var in
......
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