Commit 2b5ecd47 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Revert "Vc: slight improvement for identical terms in termination checking"

This reverts commit ce0b3584.

Counterexample:

predicate rev (x y:int) = x <= 1 /\ x > y
let rec function
     f1 () : () variant { 0, 1, 0 }          = f2 ()
with f2 () : () variant { 0, 0, 1 }          = f3 ()
with f3 () : () variant { 0, 0 with rev, 0 } = f4 ()
with f4 () : () variant { 0, 1 with rev, 1 } = f1 ()
parent 68effd14
......@@ -279,17 +279,16 @@ let decrease_def env loc old_t t =
let decrease env loc attrs expl olds news =
if olds = [] && news = [] then t_true else
let rec decr olds news = match olds, news with
| (old_t, _)::olds, (t, _)::news
when t_equal old_t t ->
decr olds news
| (old_t, Some old_r)::olds, (t, Some r)::news
when oty_equal old_t.t_ty t.t_ty && ls_equal old_r r ->
let dt = t_and (ps_app r [t; old_t]) (acc env r old_t) in
t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds news))
t_or_simp dt (t_and_simp (t_equ_simp old_t t) (decr olds news))
| (old_t, None)::olds, (t, None)::news
when oty_equal old_t.t_ty t.t_ty ->
let dt = decrease_def env loc old_t t in
t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds news))
if t_equal old_t t then decr olds news
else
let dt = decrease_def env loc old_t t in
t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds news))
| (old_t, None)::_, (t, None)::_ ->
decrease_def env loc old_t t
| _::_, [] -> t_true
......
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