From f16fd5a0fe7277d87c45574d634c3c0c03f02889 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 2 May 2022 14:17:57 +0200
Subject: [PATCH] [wp] Coherence between messages in Clear and Unfold
---
src/plugins/wp/TacClear.ml | 6 ++++--
src/plugins/wp/TacUnfold.ml | 5 +++--
src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle | 4 ++--
3 files changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
index b804eb95c97..bf1f7aeaeee 100644
--- a/src/plugins/wp/TacClear.ml
+++ b/src/plugins/wp/TacClear.ml
@@ -82,8 +82,9 @@ let tactical_inside step remove =
List.fold_left add Filteredset.empty remove
in
let feedback =
+ let pp fmt f = Format.fprintf fmt "'%a'" Filtered.pretty f in
Format.asprintf "Filtered: %a"
- (Pretty_utils.pp_list ~sep:", " Filtered.pretty) removed
+ (Pretty_utils.pp_list ~sep:", " pp) removed
in
let cond = condition step @@ Lang.F.p_bool @@ Lang.F.e_and kept in
removed, Tactical.replace_single ~at:step.id (feedback, cond)
@@ -114,8 +115,9 @@ let fold_selection s seq =
in
let removed, seq = Smap.fold tactical m ([], seq) in
let feedback =
+ let pp fmt f = Format.fprintf fmt "'%a'" Filtered.pretty f in
Format.asprintf "Filtered: %a"
- (Pretty_utils.pp_list ~sep:", " Filtered.pretty) removed
+ (Pretty_utils.pp_list ~sep:", " pp) removed
in
feedback, seq
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index af0f08d7ecd..a30d3798e06 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/src/plugins/wp/TacUnfold.ml
@@ -131,8 +131,9 @@ let tactical_inside step unfolds sequent =
in
let p = condition step @@ Lang.p_subst subst p in
let feedback =
- Format.asprintf "Unfold '%a'"
- (Pretty_utils.pp_list ~sep:", " Lang.Fun.pretty) !unfolded
+ let pp fmt f = Format.fprintf fmt "'%a'" Lang.Fun.pretty f in
+ Format.asprintf "Unfold %a"
+ (Pretty_utils.pp_list ~sep:", " pp) !unfolded
in
!unfolded, snd @@ Tactical.replace_single ~at:step.id (feedback, p) sequent
| _ -> raise Not_found
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
index 7af1209d3c4..9c2a626fc58 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -51,7 +51,7 @@
typed_clear_in_step_check subgoal:
Goal Wp.Tactical.typed_clear_in_step_check-0 (generated):
- Assume { (* Filtered: P_P(...) *) Have: P_Q /\ P_R. }
+ Assume { (* Filtered: 'P_P(...)' *) Have: P_Q /\ P_R. }
Prove: P_S(42).
------------------------------------------------------------
@@ -77,7 +77,7 @@
typed_clear_in_step_check subgoal:
Goal Wp.Tactical.typed_clear_in_step_check-1 (generated):
- Assume { (* Filtered: P_Q(...) *) Have: P_R. }
+ Assume { (* Filtered: 'P_Q(...)' *) Have: P_R. }
Prove: P_S(42).
------------------------------------------------------------
--
GitLab