[wp] TacClear in conjunctions

src/plugins/wp/TacClear.ml

@@ -21,6 +21,7 @@
 (**************************************************************************)
 
 open Tactical
+open Conditions
 
 class clear =
   object(_)
@@ -34,8 +35,38 @@ class clear =
       | Clause(Step step) ->
           let removed = [ "Cleared hypothesis", Conditions.Have Lang.F.p_true] in
           Applicable (Tactical.replace ~at:step.id removed)
-      | _ ->
-          Not_applicable
+      | Inside(Step step, remove) ->
+          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
+          let rec collect p =
+            match Lang.F.p_expr p with
+            | And ps -> collect_list ps
+            | _ -> [ p ]
+          and collect_list = function
+            | [] -> []
+            | p :: l -> List.rev_append (List.rev @@ collect p) (collect_list l)
+          in
+          begin match step.condition with
+            | Type p | Have p | When p | Core p | Init p ->
+                let ps = Lang.F.e_props @@ collect p in
+                if List.mem remove ps then
+                  let ps = List.filter (fun x -> x <> remove) ps in
+                  let cond = cond @@ Lang.F.p_bool @@ Lang.F.e_and ps in
+                  let filtered = [ "Filtered", cond ] in
+                  Applicable (Tactical.replace ~at:step.id filtered)
+                else
+                  Not_applicable
+
+            | _ -> Not_applicable
+          end
+      | _ -> Not_applicable
   end
 
 let tactical = Tactical.export (new clear)

src/plugins/wp/tests/wp_tip/clear.i

 /* run.config
-   OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_DIR@/oracle/@PTEST_NAME@.session
+   OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.session
 */
 /* run.config_qualif
    DONTRUN:
@@ -26,3 +26,8 @@ void clear(void) {
     b--;
   }
 }
+
+void clear_in_step(void){
+  //@ admit P && Q && R ;
+  //@ check S(42) ;
+}

src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle

@@ -2,7 +2,147 @@
 [kernel] Parsing clear.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 1 goal scheduled
-[wp] [Failed] Goal typed_clear_ensures
-[wp] Proved goals:    0 / 1
+[wp] 2 goals scheduled
+[wp:script:allgoals] 
+  Goal Post-condition (file clear.i, line 21) in 'clear':
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+        is_sint32(b_1) /\ is_sint32(b_2).
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+    (* Pre-condition *)
+    Have: P_R.
+    If a_2 < b_2
+    Then { Have: (a_2 = a_1) /\ (b_2 = b). Have: (1 + a_1) = a. }
+    Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+  }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Check (file clear.i, line 32):
+  Assume { (* Admit *) Have: P_P /\ P_Q /\ P_R. }
+  Prove: P_S(42).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-0 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+        is_sint32(b_1) /\ is_sint32(b_2).
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+    (* Pre-condition *)
+    Have: P_R.
+    If a_2 < b_2
+    Then { Have: (a_2 = a_1) /\ (b_2 = b). }
+    Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+  }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_in_step_check subgoal:
+  
+  Goal Wp.Tactical.typed_clear_in_step_check-0 (generated):
+  Assume { (* Filtered *) Have: P_Q /\ P_R. }
+  Prove: P_S(42).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-1 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+        is_sint32(b_1) /\ is_sint32(b_2).
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+    If a_2 < b_2
+    Then { Have: (a_2 = a_1) /\ (b_2 = b). }
+    Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+  }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_in_step_check subgoal:
+  
+  Goal Wp.Tactical.typed_clear_in_step_check-1 (generated):
+  Assume { (* Filtered *) Have: P_R. }
+  Prove: P_S(42).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-2 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+        is_sint32(b_1).
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+    If a_2 < b_1
+    Then { Have: (a_2 = a_1) /\ (b_1 = b). }
+  }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_in_step_check subgoal:
+  
+  Goal Wp.Tactical.typed_clear_in_step_check-2 (generated):
+  Prove: P_S(42).
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_clear_in_step_check : Unsuccess
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-3 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+  }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-4 (generated):
+  Assume { Type: is_sint32(a) /\ is_sint32(b). (* Pre-condition *) Have: P_P. }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-5 (generated):
+  Assume { (* Pre-condition *) Have: P_P. }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-6 (generated):
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_clear_ensures : Unsuccess
+[wp] Proved goals:    0 / 2
 [wp] No updated script.

src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_in_step_check.json

+[ { "header": "Clear", "tactic": "Wp.clear", "params": {},
+    "select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
+                "target": "P_P", "pattern": "P_P" },
+    "children": { "Filtered": [ { "header": "Clear", "tactic": "Wp.clear",
+                                  "params": {},
+                                  "select": { "select": "inside-step",
+                                              "at": 2, "kind": "have",
+                                              "occur": 0, "target": "P_Q",
+                                              "pattern": "P_Q" },
+                                  "children": { "Filtered": [ { "header": "Clear",
+                                                                "tactic": "Wp.clear",
+                                                                "params": {},
+                                                                "select": 
+                                                                  { "select": "clause-step",
+                                                                    "at": 2,
+                                                                    "kind": "have",
+                                                                    "target": "P_R",
+                                                                    "pattern": "P_R" },
+                                                                "children": 
+                                                                  { "Cleared hypothesis": [] } } ] } } ] } } ]