From 017f33343eee887e253933c7997626418c478030 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Wed, 19 Sep 2018 14:27:38 +0200
Subject: [PATCH] Vc: another attempt at (slightly) improving termination
checking
---
src/mlw/vc.ml | 16 +++++++---------
1 file changed, 7 insertions(+), 9 deletions(-)
diff --git a/src/mlw/vc.ml b/src/mlw/vc.ml
index 225920ecb..1391e53ca 100644
--- a/src/mlw/vc.ml
+++ b/src/mlw/vc.ml
@@ -279,16 +279,14 @@ 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, Some old_r)::olds, (t, Some r)::news
- when oty_equal old_t.t_ty t.t_ty && ls_equal old_r r ->
+ | (old_t, Some old_r)::olds, (t, Some r)::news when ls_equal old_r r ->
+ if t_equal old_t t then decr olds news else
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_simp old_t t) (decr olds news))
- | (old_t, None)::olds, (t, None)::news
- when oty_equal old_t.t_ty t.t_ty ->
- 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))
+ t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds news))
+ | (old_t, None)::olds, (t, None)::news when oty_equal old_t.t_ty t.t_ty ->
+ 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
--
GitLab