From 81ca1cef7082906530f96a68f209e25651264cd4 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 21 Mar 2022 11:19:03 +0100
Subject: [PATCH] [wp] Make multi select clear/unfold more verbose

---
 src/plugins/wp/TacClear.ml                    | 23 +++++++++++++++----
 src/plugins/wp/TacUnfold.ml                   | 17 ++++++++++++--
 .../wp/tests/wp_tip/oracle/clear.res.oracle   |  4 ++--
 3 files changed, 35 insertions(+), 9 deletions(-)

diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
index 48a835f0071..3808c290909 100644
--- a/src/plugins/wp/TacClear.ml
+++ b/src/plugins/wp/TacClear.ml
@@ -33,10 +33,18 @@ let condition original p = (* keep original kind of simple condition *)
   | _ -> assert false
 
 let tactical_step step =
-  Tactical.replace_single ~at:step.id ("Removed", Conditions.Have Lang.F.p_true)
+  Tactical.replace_single ~at:step.id
+    (* Note: the provided name is used in the GUi for the subgoal title *)
+    ("Removed Step", Conditions.Have Lang.F.p_true)
 
 module TermLset = Qed.Listset.Make(Lang.F.QED.Term)
 
+let pp_filtered fmt t =
+  match Lang.F.repr t with
+  | Qed.Logic.Fun(f,_) -> Format.fprintf fmt "%a(...)" Lang.Fun.pretty f
+  | _ -> Lang.F.pp_term fmt t
+
+
 let tactical_inside step remove =
   let remove = List.sort_uniq Lang.F.compare remove in
   let collect p =
@@ -47,9 +55,13 @@ let tactical_inside step remove =
   begin match step.condition with
     | Type p | Have p | When p | Core p | Init p ->
       let ps = Lang.F.e_props @@ collect p in
-      let ps = TermLset.diff ps remove in
-      let cond = condition step @@ Lang.F.p_bool @@ Lang.F.e_and ps in
-      Tactical.replace_single ~at:step.id ("Filtered", cond)
+      let kept = TermLset.diff ps remove in
+      let feedback =
+        Format.asprintf "Filtered: %a"
+          (Pretty_utils.pp_list ~sep:", " pp_filtered) remove
+      in
+      let cond = condition step @@ Lang.F.p_bool @@ Lang.F.e_and kept in
+      Tactical.replace_single ~at:step.id (feedback, cond)
 
     | _ -> raise Not_found
   end
@@ -71,7 +83,8 @@ let collect_remove m = function
 
 let fold_selection s seq =
   let m = List.fold_left collect_remove Smap.empty s in
-  "Filtered", Smap.fold (fun s l seq -> snd @@ tactical_inside s l seq) m seq
+  "Filtered mutiple selection",
+  Smap.fold (fun s l seq -> snd @@ tactical_inside s l seq) m seq
 
 let process (f: sequent -> string * sequent) s = [ f s ]
 
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index cb40a592325..f72efde27b4 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/src/plugins/wp/TacUnfold.ml
@@ -118,9 +118,22 @@ let tactical_inside step unfolds sequent =
   then raise Not_found
   else match step.condition with
     | Type p | Have p | When p | Core p | Init p ->
-      let subst t = Lang.F.Tmap.find t unfolds in
+      let unfolded = ref [] in
+      let subst t =
+        let result = Lang.F.Tmap.find t unfolds in
+        begin match F.repr t with
+          | Qed.Logic.Fun(f,_) -> unfolded := f :: !unfolded
+          | _ -> ()
+        end ;
+        result
+      in
       let p = condition step @@ Lang.p_subst subst p in
-      snd @@ Tactical.replace_single ~at:step.id ("Unfolded", p) sequent
+      let unfolded = List.sort_uniq Lang.Fun.compare !unfolded in
+      let feedback =
+        Format.asprintf "Unfolded: %a"
+          (Pretty_utils.pp_list ~sep:", " Lang.Fun.pretty) unfolded
+      in
+      snd @@ Tactical.replace_single ~at:step.id (feedback, p) sequent
     | _ -> raise Not_found
 
 let tactical_goal unfolds (seq, g) =
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 ebcdcd1cd22..7af1209d3c4 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 *) 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 *) Have: P_R. }
+  Assume { (* Filtered: P_Q(...) *) Have: P_R. }
   Prove: P_S(42).
   
   ------------------------------------------------------------
-- 
GitLab