Commit b6878d8d authored by Andrei Paskevich's avatar Andrei Paskevich

optimize wp generation

parent 7732e4ce
......@@ -56,8 +56,19 @@ let is_arrow_ty env ty = match ty.ty_node with
| Tyapp (ts, _) -> ts_equal ts env.ts_arrow
| _ -> false
let wp_forall env v f =
if is_arrow_ty env v.vs_ty then f else f_forall_close_simp [v] [] f
let wp_forall env v f =
if is_arrow_ty env v.vs_ty then f else match f.f_node with
| Fbinop (Fimplies, {f_node = Fapp (s,[{t_node = Tvar u};r])},h)
when ls_equal s ps_equ && vs_equal u v && not (t_occurs_single v r) ->
f_subst_single v r h
| Fbinop (Fimplies, {f_node = Fbinop (Fand, g,
{f_node = Fapp (s,[{t_node = Tvar u};r])})},h)
when ls_equal s ps_equ && vs_equal u v && not (t_occurs_single v r) ->
f_subst_single v r (f_implies_simp g h)
| _ when f_occurs_single v f ->
f_forall_close_simp [v] [] f
| _ ->
f
(* utility functions for building WPs *)
......@@ -252,7 +263,7 @@ let rec wp_expr env e q =
and wp_desc env e q = match e.expr_desc with
| Elogic t ->
let (v, q), _ = q in
f_let_close v t q
f_subst_single v t q
| Elocal v ->
let (res, q), _ = q in
f_subst (subst1 res (t_var v)) q
......@@ -304,6 +315,8 @@ and wp_desc env e q = match e.expr_desc with
(quantify env e.expr_effect (wp_implies i we)))
in
w
| Ematch (_, [{pat_node = Pwild}, e]) ->
wp_expr env e (filter_post e.expr_effect q)
| Ematch (x, bl) ->
let branch (p, e) =
f_close_branch p (wp_expr env e (filter_post e.expr_effect q))
......
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