[wp] more determinism during split tactic

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

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

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

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)

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)