Merge branch 'feature/wp/details-tacclear' into 'master'

[wp] display more info in TacClear/Unfold

See merge request frama-c/frama-c!3708

src/plugins/wp/TacClear.ml

@@ -37,12 +37,33 @@ let tactical_step step =
     (* 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)
+module Filtered =
+struct
+  type t =
+    | Fun of Lang.Fun.t
+    | Other of Lang.F.term
+
+  let of_term t =
+    match Lang.F.repr t with
+    | Qed.Logic.Fun(f, _) -> Fun f
+    | _ -> Other t
+
+  let pretty fmt = function
+    | Fun f -> Format.fprintf fmt "%a(...)" Lang.Fun.pretty f
+    | Other t -> Lang.F.pp_term fmt t
+
+  let compare a b =
+    match a, b with
+    | Fun a, Fun b -> Lang.Fun.compare a b
+    | Other a, Other b -> Lang.F.compare a b
+    | Fun _, _ -> 1
+    | _, Fun _ -> -1
+
+  let equal a b = 0 = compare a b
+end
 
-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
+module TermLset = Qed.Listset.Make(Lang.F.QED.Term)
+module Filteredset = Qed.Listset.Make(Filtered)
 
 
 let tactical_inside step remove =
@@ -56,12 +77,17 @@ let tactical_inside step remove =
     | Type p | Have p | When p | Core p | Init p ->
       let ps = Lang.F.e_props @@ collect p in
       let kept = TermLset.diff ps remove in
+      let removed =
+        let add s e = Filteredset.add (Filtered.of_term e) s in
+        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:", " pp_filtered) remove
+          (Pretty_utils.pp_list ~sep:", " pp) removed
       in
       let cond = condition step @@ Lang.F.p_bool @@ Lang.F.e_and kept in
-      Tactical.replace_single ~at:step.id (feedback, cond)
+      removed, Tactical.replace_single ~at:step.id (feedback, cond)
 
     | _ -> raise Not_found
   end
@@ -83,8 +109,18 @@ let collect_remove m = function
 
 let fold_selection s seq =
   let m = List.fold_left collect_remove Smap.empty s in
-  "Filtered mutiple selection",
-  Smap.fold (fun s l seq -> snd @@ tactical_inside s l seq) m seq
+  let tactical s l (acc_rm, seq) =
+    let rm, op = tactical_inside s l in
+    Filteredset.union rm acc_rm, snd @@ op 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:", " pp) removed
+  in
+  feedback, seq
+
 
 let process (f: sequent -> string * sequent) s = [ f s ]
 
@@ -101,7 +137,7 @@ class clear =
         Applicable(process @@ tactical_step step)
       | Inside(Step step, remove) ->
         begin
-          try Applicable(process @@ tactical_inside step [remove])
+          try Applicable(process @@ snd @@ tactical_inside step [remove])
           with Not_found -> Not_applicable
         end
       | Multi es ->

src/plugins/wp/TacUnfold.ml

@@ -113,27 +113,29 @@ let unfolds_from_list phis es =
 let unfolds_from_smap phis m =
   Smap.map (fun _s es -> unfolds_from_list phis es) m
 
+module Unfoldedset = Qed.Listset.Make(Lang.Fun)
+
 let tactical_inside step unfolds sequent =
   if Lang.F.Tmap.is_empty unfolds
   then raise Not_found
   else match step.condition with
     | Type p | Have p | When p | Core p | Init p ->
-      let unfolded = ref [] in
+      let unfolded = ref Unfoldedset.empty 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
+          | Qed.Logic.Fun(f,_) -> unfolded := Unfoldedset.add f !unfolded
           | _ -> ()
         end ;
         result
       in
       let p = condition step @@ Lang.p_subst subst p in
-      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
+        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
-      snd @@ Tactical.replace_single ~at:step.id (feedback, p) sequent
+      !unfolded, snd @@ Tactical.replace_single ~at:step.id (feedback, p) sequent
     | _ -> raise Not_found
 
 let tactical_goal unfolds (seq, g) =
@@ -144,12 +146,21 @@ let tactical_goal unfolds (seq, g) =
     seq, Lang.p_subst subst g
 
 let fold_selection goal_unfolds step_unfolds sequent =
-  "Unfolded multiple selection",
+  let tactical s l (acc_unfolded, seq) =
+    let unfolded, seq = tactical_inside s l seq in
+    Unfoldedset.union unfolded acc_unfolded, seq
+  in
+  let unfolded, seq = Smap.fold tactical step_unfolds ([], sequent) in
+  let feedback =
+    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
   let add_goal = match goal_unfolds with
     | None -> Extlib.id
     | Some goal_unfolds -> tactical_goal goal_unfolds
   in
-  add_goal @@ Smap.fold tactical_inside step_unfolds sequent
+  feedback, add_goal seq
 
 let process (f: sequent -> string * sequent) s = [ f s ]
 

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).
   
   ------------------------------------------------------------