Commit 0fb980c6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Improve the lexicographic order for variants.

1. better handle the equality case, which is the reason for using a
   lexicographic order in the first place;
2. implement a proper lexicographic order, i.e., make (a,b) smaller
   than (a,b,c).

As a consequence of these two changes, in the following example, the VC
for f goes from (0 <= x /\ x < x) to true:

let rec f (x y : int) : int variant { x, () } = g x y
with g (x y : int) : int variant { x } = f (x-1) y
parent 250deb85
......@@ -267,13 +267,16 @@ let decrease env loc attrs expl 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
| _ -> t_false in
vc_expl loc attrs expl (decr olds news)
......
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