[wp] extend split to conjunctions in hypotheses

src/plugins/wp/Conditions.ml

@@ -1737,14 +1737,15 @@ let step_at seq k =
 (* --- Insertion                                                          --- *)
 (* -------------------------------------------------------------------------- *)
 
-let in_sequence ~replace =
+let in_sequence_add_list ~replace =
   let rec in_list k h w =
     if k = 0 then
-      h :: (if replace
-            then match w with
-              | [] -> assert false
-              | _::w -> w
-            else w)
+      List.rev_append h
+        (if replace
+         then match w with
+           | [] -> assert false
+           | _::w -> w
+         else w)
     else
       match w with
       | [] -> assert false
@@ -1760,9 +1761,9 @@ let in_sequence ~replace =
     | Branch(p,a,b) ->
         let n = a.seq_size in
         if k < n then
-          Branch(p,in_sequence k h a,b)
+          Branch(p,in_sequence_add_list k h a,b)
         else
-          Branch(p,a,in_sequence (k-n) h b)
+          Branch(p,a,in_sequence_add_list (k-n) h b)
     | Either cs -> Either (in_case k h cs)
 
   and in_case k h = function
@@ -1770,11 +1771,13 @@ let in_sequence ~replace =
     | c::cs ->
         let n = c.seq_size in
         if k < n
-        then in_sequence k h c :: cs
+        then in_sequence_add_list k h c :: cs
         else c :: in_case (k-n) h cs
 
-  and in_sequence k h s = sequence (in_list k h s.seq_list)
-  in in_sequence
+  and in_sequence_add_list k h s = sequence (in_list k h s.seq_list)
+  in in_sequence_add_list
+
+let in_sequence ~replace id h = in_sequence_add_list ~replace id [h]
 
 let size seq = seq.seq_size
 
@@ -1791,6 +1794,12 @@ let replace ~at step sequent =
   then in_sequence ~replace:true at step seq , goal
   else raise Not_found
 
+let replace_by_step_list ~at step_list sequent =
+  let seq,goal = sequent in
+  if 0 <= at && at <= seq.seq_size
+  then in_sequence_add_list ~replace:true at step_list seq , goal
+  else raise Not_found
+
 (* -------------------------------------------------------------------------- *)
 (* --- Replace                                                            --- *)
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/Conditions.mli

@@ -153,6 +153,10 @@ val replace : at:int -> step -> sequent -> sequent
 (** replace a step in the sequent, the one [at] the specified position.
     @raise Invalid_argument if the index is out of bounds. *)
 
+val replace_by_step_list : at:int -> step list -> sequent -> sequent
+(** replace a step in the sequent, the one [at] the specified position.
+    @raise Invalid_argument if the index is out of bounds. *)
+
 val subst : (term -> term) -> sequent -> sequent
 (** Apply the atomic substitution recursively using [Lang.F.p_subst f].
     Function [f] should only transform the head of the predicate, and can assume

src/plugins/wp/TacSplit.ml

@@ -402,6 +402,20 @@ class split =
                       let q = F.p_bool (F.e_and [e_not c;q]) in
                       let cases = [ "Then" , When p ; "Else" , When q ] in
                       Applicable (Tactical.replace ~at:step.id cases)
+                  | And ps ->
+                      let cond p = (* keep original kind of step *)
+                        match step.condition with
+                        | Type _ -> Type p
+                        | Have _ -> Have p
+                        | When _ -> When p
+                        | Core _ -> Core p
+                        | Init _ -> Init p
+                        | _ -> assert false (* see above pattern matching *)
+                      in
+                      feedback#set_title "Split (conjunction)" ;
+                      feedback#set_descr "Split conjunction into steps" ;
+                      let ps = List.map (fun p -> cond @@ p_bool p) ps in
+                      Applicable (Tactical.replace_step ~at:step.id ps)
                   | _ ->
                       Not_applicable
                 end

src/plugins/wp/Tactical.ml

@@ -357,6 +357,15 @@ let replace ~at cases sequent =
        descr , Conditions.replace ~at step sequent)
     cases
 
+let replace_step ~at conditions sequent =
+  let step =
+    let s = Conditions.step_at (fst sequent) at in
+    (* keep original infos *)
+    Conditions.step ?descr:s.descr ?stmt:s.stmt ~deps:s.deps ~warn:s.warn
+  in
+  let conditions = List.map step conditions in
+  [ "Split conj", Conditions.replace_by_step_list ~at conditions sequent ]
+
 let split cases sequent =
   let hyps = fst sequent in
   List.map (fun (descr,p) -> descr,(hyps,p)) cases

src/plugins/wp/Tactical.mli

@@ -179,6 +179,7 @@ val at : selection -> int option
 val mapi : (int -> int -> 'a -> 'b) -> 'a list -> 'b list
 val insert : ?at:int -> (string * pred) list -> process
 val replace : at:int -> (string * condition) list -> process
+val replace_step : at:int -> condition list -> process
 val split : (string * pred) list -> process
 val rewrite : ?at:int -> (string * pred * term * term) list -> process
 (** For each pattern [(descr,guard,src,tgt)] replace [src] with [tgt]