From 7821800c1a76ebf6a704eb0dec3abbddc682ef15 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 19 Dec 2022 08:46:03 +0100
Subject: [PATCH] [wp] more determinism during split tactic
---
src/libraries/qed/pool.ml | 3 ++-
src/libraries/qed/pool.mli | 1 +
src/libraries/qed/term.ml | 1 +
src/plugins/wp/TacSplit.ml | 12 ++++++++----
src/plugins/wp/tests/wp_tip/oracle/split.res.oracle | 8 ++++----
5 files changed, 16 insertions(+), 9 deletions(-)
diff --git a/src/libraries/qed/pool.ml b/src/libraries/qed/pool.ml
index b431def8e77..b817c26909c 100644
--- a/src/libraries/qed/pool.ml
+++ b/src/libraries/qed/pool.ml
@@ -29,6 +29,7 @@ sig
type t
val dummy : t
val equal : t -> t -> bool
+ val compare : t -> t -> int
end
module Make(T : Type) =
@@ -79,7 +80,7 @@ struct
if cmp <> 0 then cmp else
let cmp = Stdlib.compare x.vrank y.vrank in
if cmp <> 0 then cmp else
- Stdlib.compare x.vid y.vid
+ T.compare x.vtau y.vtau
(* POOL *)
diff --git a/src/libraries/qed/pool.mli b/src/libraries/qed/pool.mli
index e6b236fc74c..ea3845fb60e 100644
--- a/src/libraries/qed/pool.mli
+++ b/src/libraries/qed/pool.mli
@@ -29,6 +29,7 @@ sig
type t
val dummy : t
val equal : t -> t -> bool
+ val compare : t -> t -> int
end
module Make(T : Type) :
diff --git a/src/libraries/qed/term.ml b/src/libraries/qed/term.ml
index be5a1a97ea5..bd6a98bf5ee 100644
--- a/src/libraries/qed/term.ml
+++ b/src/libraries/qed/term.ml
@@ -45,6 +45,7 @@ struct
type t = tau
let dummy = Prop
let equal = Kind.eq_tau Field.equal ADT.equal
+ let compare = Kind.compare_tau Field.compare ADT.compare
end)
open POOL
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 023633e34a2..ebd670aac56 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -29,7 +29,7 @@ module PartitionsQQ : sig
Lang.F.Vars.t * Lang.F.QED.term
val get : vars:Lang.F.Vars.t -> Lang.F.term list ->
- int * Lang.F.Tset.t list
+ int * Lang.F.term list list
end
= struct
let dkey = Wp_parameters.register_category "tac_split_quantifiers" (* debugging key *)
@@ -147,7 +147,11 @@ end
r
let get ~vars es =
- extract (partitions ~vars es)
+ let nbparts, parts = extract (partitions ~vars es) in
+ let sorted_ts e = List.sort Lang.F.compare @@ Lang.F.Tset.elements e in
+ let sort_es = List.sort (Extlib.list_compare Lang.F.compare) in
+ let parts = sort_es @@ List.map sorted_ts parts in
+ nbparts, parts
end
open Lang.F
@@ -260,7 +264,7 @@ class split =
feedback#set_descr
"Decompose the quantifier into %d parts." nb_parts ;
let bind es =
- bind Exists ~vars (F.e_and (F.Tset.elements es)) in
+ bind Exists ~vars (F.e_and es) in
let goal i n es =
Printf.sprintf "Goal %d/%d" i n , F.p_bool (bind es) in
Applicable (Tactical.split (Tactical.mapi goal parts))
@@ -352,7 +356,7 @@ class split =
else begin
feedback#set_title "Split (forall or)" ;
feedback#set_descr "Decompose the quantifier between %d parts of the disjunction." nb_parts ;
- let bind es = bind Forall ~vars (F.e_or (F.Tset.elements es)) in
+ let bind es = bind Forall ~vars (F.e_or es) in
let goal i n es = Printf.sprintf "Goal %d/%d" i n , When (F.p_bool (bind es)) in
let cases = Tactical.mapi goal parts in
Applicable (Tactical.replace ~at:step.id cases)
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
index 17b2f4d692c..4a51426aad2 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
@@ -475,7 +475,7 @@
typed_test_step_fa_or_ensures subgoal:
Goal Wp.Tactical.typed_test_step_fa_or_ensures-0 (generated):
- Assume { (* Goal 1/2 *) When: forall i : Z. P_Pi(i) \/ P_Qi(i). }
+ Assume { (* Goal 1/2 *) When: P_P \/ P_Q \/ P_R. }
Prove: P_S.
------------------------------------------------------------
@@ -483,7 +483,7 @@
typed_test_step_fa_or_ensures subgoal:
Goal Wp.Tactical.typed_test_step_fa_or_ensures-1 (generated):
- Assume { (* Goal 2/2 *) When: P_P \/ P_Q \/ P_R. }
+ Assume { (* Goal 2/2 *) When: forall i : Z. P_Pi(i) \/ P_Qi(i). }
Prove: P_S.
------------------------------------------------------------
@@ -691,7 +691,7 @@
Goal Wp.Tactical.typed_test_goal_ex_and_ensures-0 (generated):
Assume { (* Pre-condition *) Have: P_S. }
- Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
+ Prove: P_P /\ P_Q.
------------------------------------------------------------
[wp:script:allgoals]
@@ -699,7 +699,7 @@
Goal Wp.Tactical.typed_test_goal_ex_and_ensures-1 (generated):
Assume { (* Pre-condition *) Have: P_S. }
- Prove: P_P /\ P_Q.
+ Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
------------------------------------------------------------
[wp] [Unsuccess] typed_test_goal_ex_and_ensures (Tactic) (Qed)
--
GitLab