Commit 64b1fda4 authored by Sylvain Dailler's avatar Sylvain Dailler

Keeping keep_on_simp labels during wp generation.

We changed t_map_simp, track_values and the eval_match transformation
in order to prevent them from removing terms whose head has label
 keep_on_simp. Note that simplification inside those terms is
still possible.

* src/core/term.ml
(t_map_simp): Adding the case when f has label keep_on_simp.

* src/transform/eval_match.ml
(eval_match): Adding keep_on_simp as a stop label.

* src/whyml/mlw_wp.ml
(track_values): Stopping on keep_on_simp label.
parent 11dc2598
......@@ -1598,22 +1598,41 @@ let t_exists_close_merge vs f = match f.t_node with
t_exists_close (vs@vs') trs f
| _ -> t_exists_close vs [] f
let t_map_simp fn f = t_label_copy f (match f.t_node with
| Tapp (p, [t1;t2]) when ls_equal p ps_equ ->
t_equ_simp (fn t1) (fn t2)
| Tif (f1, f2, f3) ->
t_if_simp (fn f1) (fn f2) (fn f3)
| Tlet (t, b) ->
let u,t2,close = t_open_bound_cb b in
t_let_simp (fn t) (close u (fn t2))
| Tquant (q, b) ->
let vl,tl,f1,close = t_open_quant_cb b in
t_quant_simp q (close vl (tr_map fn tl) (fn f1))
| Tbinop (op, f1, f2) ->
t_binary_simp op (fn f1) (fn f2)
| Tnot f1 ->
t_not_simp (fn f1)
| _ -> t_map fn f)
let t_map_simp fn f =
if can_simp f then
t_label_copy f (match f.t_node with
| Tapp (p, [t1;t2]) when ls_equal p ps_equ ->
t_equ_simp (fn t1) (fn t2)
| Tif (f1, f2, f3) ->
t_if_simp (fn f1) (fn f2) (fn f3)
| Tlet (t, b) ->
let u,t2,close = t_open_bound_cb b in
t_let_simp (fn t) (close u (fn t2))
| Tquant (q, b) ->
let vl,tl,f1,close = t_open_quant_cb b in
t_quant_simp q (close vl (tr_map fn tl) (fn f1))
| Tbinop (op, f1, f2) ->
t_binary_simp op (fn f1) (fn f2)
| Tnot f1 ->
t_not_simp (fn f1)
| _ -> t_map fn f)
else
t_label_copy f (match f.t_node with
| Tapp (p, [t1;t2]) when ls_equal p ps_equ ->
t_equ (fn t1) (fn t2)
| Tif (f1, f2, f3) ->
t_if (fn f1) (fn f2) (fn f3)
| Tlet (t, b) ->
let u,t2,close = t_open_bound_cb b in
t_let (fn t) (close u (fn t2))
| Tquant (q, b) ->
let vl,tl,f1,close = t_open_quant_cb b in
t_quant q (close vl (tr_map fn tl) (fn f1))
| Tbinop (op, f1, f2) ->
t_binary op (fn f1) (fn f2)
| Tnot f1 ->
t_not (fn f1)
| _ -> t_map fn f)
let t_map_simp fn = t_map_simp (fun t ->
let res = fn t in t_ty_check res t.t_ty; res)
......@@ -1639,4 +1658,3 @@ module TermTF = struct
let tr_fold fnT fnF = tr_fold (t_selecti fnT fnF)
let tr_map_fold fnT fnF = tr_map_fold (t_selecti fnT fnF)
end
......@@ -138,7 +138,8 @@ and apply_cs_equ kn cs1 tl1 env t = match t.t_node with
let eval_match ~inline kn t =
let rec eval stop env t =
let stop = stop || Slab.mem Split_goal.stop_split t.t_label in
let stop = stop || Slab.mem Split_goal.stop_split t.t_label ||
Slab.mem keep_on_simp_label t.t_label in
let eval = eval stop in
let t_eval_matched = (match t.t_node with
| Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
......
......@@ -610,6 +610,8 @@ let rec track_values state names lesson cond f = match f.t_node with
let condl = List.filter good condl in
let l = Mint.add p1 (cond::condl) lesson in
l, t_label_copy f (get_invariant state.st_km t1)
| _ when (Slab.mem keep_on_simp_label f.t_label) ->
lesson, f
| Tbinop (Timplies, f1, f2) ->
let l, f1 = track_values state names lesson cond f1 in
let _, f2 = track_values state names l cond f2 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