From b965cebb9c4a107c60aeb95700f0bd77b1480c55 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 9 Oct 2020 15:23:43 +0200
Subject: [PATCH] [wp] only search closed terms for tactics
---
src/plugins/wp/Footprint.ml | 8 ++++++--
src/plugins/wp/Footprint.mli | 2 ++
2 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/Footprint.ml b/src/plugins/wp/Footprint.ml
index a05d0d02ad7..0198e11baab 100644
--- a/src/plugins/wp/Footprint.ml
+++ b/src/plugins/wp/Footprint.ml
@@ -31,7 +31,8 @@ let iter f e =
Queue.add e q ;
while not (Queue.is_empty q) do
let e = Queue.pop q in
- f e ; F.lc_iter (fun e -> Queue.push e q) e
+ if F.lc_closed e then f e ;
+ F.lc_iter (fun e -> Queue.push e q) e
done
let once f e =
@@ -42,7 +43,8 @@ let once f e =
Queue.add e q ;
while not (Queue.is_empty q) do
let e = Queue.pop q in
- f e ; F.lc_iter (fun e -> if once m e then Queue.push e q) e
+ if F.lc_closed e then f e ;
+ F.lc_iter (fun e -> if once m e then Queue.push e q) e
done
(* -------------------------------------------------------------------------- *)
@@ -151,3 +153,5 @@ let lookup ~occur ~inside =
) inside ;
raise Not_found
with Found e -> e
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Footprint.mli b/src/plugins/wp/Footprint.mli
index 868824c83bf..9e2e9a739a4 100644
--- a/src/plugins/wp/Footprint.mli
+++ b/src/plugins/wp/Footprint.mli
@@ -49,3 +49,5 @@ val locate : select:term -> inside:term -> occurrence
(** Retrieve back the [k]-th occurrence of a footprint inside a term. *)
val lookup : occur:occurrence -> inside:term -> term
+
+(* -------------------------------------------------------------------------- *)
--
GitLab