[wp] refine GUI proof status for smoke tests

src/plugins/wp/GuiGoal.ml

@@ -421,6 +421,25 @@ class pane (gprovers : GuiConfig.provers) =
             save_script#set_enabled save ;
           end
 
+    method private update_pending kind proof n =
+      match ProofEngine.current proof with
+      | `Main | `Internal _ ->
+          next#set_enabled false ;
+          prev#set_enabled false ;
+          if n = 1 then
+            Pretty_utils.ksfprintf status#set_text "One %s Goal" kind
+          else
+            Pretty_utils.ksfprintf status#set_text "%d %s Goals" n kind
+      | `Leaf(k,_) ->
+          prev#set_enabled (0 < k) ;
+          next#set_enabled (k+1 < n) ;
+          if k = 0 && n = 1 then
+            Pretty_utils.ksfprintf status#set_text
+              "Last %s Goal" kind
+          else
+            Pretty_utils.ksfprintf status#set_text
+              "%s Goal #%d /%d" kind (succ k) n
+
     method private update_statusbar =
       match state with
       | Empty ->
@@ -442,20 +461,27 @@ class pane (gprovers : GuiConfig.provers) =
             help#set_enabled
               (match state with Proof _ -> not helpmode | _ -> false) ;
             match ProofEngine.status proof with
-            | `Main ->
+            | `Unproved ->
                 icon#set_icon GuiProver.ko_status ;
                 next#set_enabled false ;
                 prev#set_enabled false ;
                 cancel#set_enabled false ;
                 forward#set_enabled false ;
                 status#set_text "Non Proved Property" ;
-            | `Invalid ->
+            | `Invalid | `StillResist 0 ->
                 icon#set_icon GuiProver.wg_status ;
                 next#set_enabled false ;
                 prev#set_enabled false ;
                 cancel#set_enabled false ;
                 forward#set_enabled false ;
                 status#set_text "Invalid Smoke-test" ;
+            | `Passed ->
+                icon#set_icon GuiProver.smoke_status ;
+                next#set_enabled false ;
+                prev#set_enabled false ;
+                cancel#set_enabled false ;
+                forward#set_enabled false ;
+                status#set_text "Passed Smoke Test" ;
             | `Proved ->
                 icon#set_icon GuiProver.ok_status ;
                 next#set_enabled false ;
@@ -474,23 +500,12 @@ class pane (gprovers : GuiConfig.provers) =
                 icon#set_icon GuiProver.ko_status ;
                 forward#set_enabled nofork ;
                 cancel#set_enabled nofork ;
-                match ProofEngine.current proof with
-                | `Main | `Internal _ ->
-                    next#set_enabled false ;
-                    prev#set_enabled false ;
-                    if n = 1 then
-                      Pretty_utils.ksfprintf status#set_text "One Pending Goal"
-                    else
-                      Pretty_utils.ksfprintf status#set_text "%d Pending Goals" n
-                | `Leaf(k,_) ->
-                    prev#set_enabled (0 < k) ;
-                    next#set_enabled (k+1 < n) ;
-                    if k = 0 && n = 1 then
-                      Pretty_utils.ksfprintf status#set_text
-                        "Last Pending Goal"
-                    else
-                      Pretty_utils.ksfprintf status#set_text
-                        "%d/%d Pending Goals" (succ k) n
+                self#update_pending "Pending" proof n ;
+            | `StillResist n ->
+                icon#set_icon GuiProver.smoke_status ;
+                forward#set_enabled nofork ;
+                cancel#set_enabled nofork ;
+                self#update_pending "Smoking" proof n ;
           end
 
     method private update_tacticbar =

src/plugins/wp/GuiProver.ml

@@ -24,6 +24,7 @@ let no_status = `Share "theme/default/never_tried.png"
 let ok_status = `Share "theme/default/surely_valid.png"
 let ko_status = `Share "theme/default/unknown.png"
 let wg_status = `Share "theme/default/surely_invalid.png"
+let smoke_status = `Share "theme/default/valid_under_hyp.png"
 
 let filter = function
   | VCS.Qed | VCS.Tactical | VCS.NativeCoq -> false

src/plugins/wp/GuiProver.mli

@@ -26,6 +26,7 @@ val no_status : icon
 val ok_status : icon
 val ko_status : icon
 val wg_status : icon
+val smoke_status : icon
 
 val filter : VCS.prover -> bool
 

src/plugins/wp/ProofEngine.ml

@@ -205,18 +205,28 @@ let children n =
 (* --- State & Status                                                     --- *)
 (* -------------------------------------------------------------------------- *)
 
-type status = [ `Main | `Proved | `Invalid | `Pending of int ]
+type status = [
+  | `Unproved (* proof obligation not proved *)
+  | `Proved   (* proof obligation is proved *)
+  | `Pending of int (* proof is pending *)
+  | `Passed   (* smoke test is passed (PO is not proved) *)
+  | `Invalid  (* smoke test has failed (PO is proved) *)
+  | `StillResist of int (* proof is pending *)
+]
 
 let status t : status =
   match t.root with
   | None ->
       if Wpo.is_proved t.main
       then if Wpo.is_smoke_test t.main then `Invalid else `Proved
-      else `Main
+      else if Wpo.is_smoke_test t.main then `Passed else `Unproved
   | Some root ->
       match root.script with
-      | Opened | Script _ -> `Main
-      | Tactic _ -> `Pending (pending root)
+      | Opened | Script _ ->
+          if Wpo.is_smoke_test t.main then `Passed else `Unproved
+      | Tactic _ ->
+          let n = pending root in
+          if Wpo.is_smoke_test t.main then `StillResist n else `Pending n
 
 (* -------------------------------------------------------------------------- *)
 (* --- Navigation                                                         --- *)

src/plugins/wp/ProofEngine.mli

@@ -35,7 +35,15 @@ val validate : ?incomplete:bool -> tree -> unit
 
 (** Leaves are numbered from 0 to n-1 *)
 
-type status = [ `Main | `Invalid | `Proved | `Pending of int ]
+
+type status = [
+  | `Unproved (** proof obligation not proved *)
+  | `Proved   (** proof obligation is proved *)
+  | `Pending of int (** proof is pending *)
+  | `Passed   (** smoke test is passed (PO is not proved) *)
+  | `Invalid  (** smoke test has failed (PO is proved) *)
+  | `StillResist of int (** proof is pending *)
+]
 type current = [ `Main | `Internal of node | `Leaf of int * node ]
 type position = [ `Main | `Node of node | `Leaf of int ]
 

src/plugins/wp/ProverScript.ml

@@ -165,9 +165,10 @@ struct
     Prover.prove wpo ?config ~mode:VCS.BatchMode
       ~progress:env.progress prover
 
-  let pending env =
+  let backtracking env =
     match ProofEngine.status env.tree with
-    | `Main | `Invalid | `Proved -> 0 | `Pending n -> n
+    | `Unproved | `Invalid | `Proved | `Passed -> 0
+    | `Pending n | `StillResist n -> n
 
   let setup_backtrack env node depth =
     if env.backtrack > 0 then
@@ -181,11 +182,11 @@ struct
               bk_node = node ;
               bk_best = (-1) ;
               bk_depth = depth ;
-              bk_pending = pending env ;
+              bk_pending = backtracking env ;
             }
 
   let search env node ~depth =
-    if env.auto <> [] && depth < env.depth && pending env < env.width
+    if env.auto <> [] && depth < env.depth && backtracking env < env.width
     then
       match ProverSearch.search env.tree ~anchor:node env.auto with
       | None -> None
@@ -197,7 +198,7 @@ struct
       match env.backtracking with
       | None -> None
       | Some point ->
-          let n = pending env in
+          let n = backtracking env in
           let anchor = point.bk_node in
           if n < point.bk_pending then
             begin
@@ -300,7 +301,7 @@ and autosearch env ~depth node : bool Task.task =
 
 and autofork env ~depth fork =
   let _,children = ProofEngine.commit fork in
-  let pending = Env.pending env in
+  let pending = Env.backtracking env in
   if pending > 0 then
     begin
       Env.progress env (Printf.sprintf "Auto %d" pending) ;

src/plugins/wp/wpAnnot.ml

@@ -162,13 +162,6 @@ let is_proved pf =
 let is_invalid pf =
   pf.invalid && not (is_proved pf)
 
-let status pf =
-  try
-    Array.iter (function Complete -> raise Exit | _ -> ()) pf.proved ;
-    `Proved
-  with Exit ->
-    if pf.invalid then `Invalid else `Partial
-
 (* -------------------------------------------------------------------------- *)
 (* --- PID for Functions                                                  --- *)
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/wpAnnot.mli

@@ -49,8 +49,6 @@ val is_proved : proof -> bool
 val is_invalid : proof -> bool
 (** whether an invalid proof result has been registered or not *)
 
-val status : proof -> [ `Proved | `Invalid | `Partial ]
-
 val target : proof -> Property.t
 val dependencies : proof -> Property.t list