From fc1d0588f38bbe5793d90e4571dd55a5f6e591f8 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Fri, 21 Sep 2018 11:24:20 +0200
Subject: [PATCH] Vc: avoid generating trivial VCs
---
src/mlw/vc.ml | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/mlw/vc.ml b/src/mlw/vc.ml
index 1391e53ca..9d8bb0cef 100644
--- a/src/mlw/vc.ml
+++ b/src/mlw/vc.ml
@@ -1503,15 +1503,19 @@ let mk_vc_decl kn id f =
Eval_match.eval_match kn f in
create_pure_decl (create_prop_decl Pgoal pr f)
+let add_vc_decl kn id f vcl =
+ if can_simp f then vcl else mk_vc_decl kn id f :: vcl
+
let vc env kn tuc d = match d.pd_node with
| PDlet (LDsym (s, {c_node = Cfun e; c_cty = cty})) ->
let env = mk_env env kn tuc in
let f = vc_fun env (Debug.test_noflag debug_sp) cty e in
- [mk_vc_decl kn s.rs_name f]
+ add_vc_decl kn s.rs_name f []
| PDlet (LDrec rdl) ->
let env = mk_env env kn tuc in
let fl = vc_rec env (Debug.test_noflag debug_sp) rdl in
- List.map2 (fun rd f -> mk_vc_decl kn rd.rec_sym.rs_name f) rdl fl
+ let add rd f vcl = add_vc_decl kn rd.rec_sym.rs_name f vcl in
+ List.fold_right2 add rdl fl []
| PDtype tdl ->
let add_witness d vcl =
let add_fd (mv,ldl) fd e =
@@ -1529,14 +1533,14 @@ let vc env kn tuc d = match d.pd_node with
let c = c_fun [] [] [] Mxs.empty Mpv.empty e in
let f = vc_fun (mk_env env kn tuc)
(Debug.test_noflag debug_sp) c.c_cty e in
- mk_vc_decl kn d.itd_its.its_ts.ts_name f :: vcl in
+ add_vc_decl kn d.itd_its.its_ts.ts_name f vcl in
let add_invariant d vcl =
let vs_of_rs fd = (fd_of_rs fd).pv_vs in
let vl = List.map vs_of_rs d.itd_fields in
let expl f = vc_expl None Sattr.empty expl_type_inv f in
let f = t_and_asym_l (List.map expl d.itd_invariant) in
let f = t_exists_close_simp vl [] f in
- mk_vc_decl kn d.itd_its.its_ts.ts_name f :: vcl in
+ add_vc_decl kn d.itd_its.its_ts.ts_name f vcl in
let add_itd d vcl =
if d.itd_witness <> [] then add_witness d vcl else
if d.itd_invariant <> [] then add_invariant d vcl else
--
GitLab