diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
index 3808c2909095b05c7af9415ce7f47e2085947f0c..bf1f7aeaeee5ee9305a2d56a58abcb875acb0ebf 100644
--- a/src/plugins/wp/TacClear.ml
+++ b/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 ->
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index f72efde27b4351668c9ad6f5d474747613b8ed08..a30d3798e06589c1e4ed673a63cda1e608de72bf 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/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 ]
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 7af1209d3c472e1e717ba1dcdf4090b5f4b641ba..9c2a626fc58df6e504db7003ad19ac459f55babc 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).
------------------------------------------------------------