[wp] fix simplification callback in prover script

src/plugins/wp/ProverScript.ml

@@ -392,16 +392,19 @@ let task
     ~depth ~width ~backtrack ~auto
     ~start ~progress ~result ~success wpo =
   begin fun () ->
-    start wpo ;
-    let json = ProofSession.load wpo in
-    let script = Priority.sort (ProofScript.decode json) in
-    let tree = ProofEngine.proof ~main:wpo in
-    let env = Env.make tree
-        ~valid ~failed ~provers
-        ~depth ~width ~backtrack ~auto
-        ~progress ~result ~success in
-    crawl env (process env) None script >>?
-    (fun _ -> ProofEngine.forward tree) ;
+    Prover.simplify ~start ~result wpo >>= fun succeed ->
+    if succeed
+    then Task.return ()
+    else
+      let json = ProofSession.load wpo in
+      let script = Priority.sort (ProofScript.decode json) in
+      let tree = ProofEngine.proof ~main:wpo in
+      let env = Env.make tree
+          ~valid ~failed ~provers
+          ~depth ~width ~backtrack ~auto
+          ~progress ~result ~success in
+      crawl env (process env) None script >>?
+      (fun _ -> ProofEngine.forward tree) ;
   end
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/prover.mli

@@ -26,6 +26,11 @@ open VCS
 (* --- Prover Implementation against Task API                             --- *)
 (* -------------------------------------------------------------------------- *)
 
+val simplify :
+  ?start:(Wpo.t -> unit) ->
+  ?result:(Wpo.t -> prover -> result -> unit) ->
+  Wpo.t -> bool Task.task
+
 val prove : Wpo.t ->
   ?config:config ->
   ?mode:mode ->

src/plugins/wp/wpo.ml

@@ -814,8 +814,7 @@ let resolve g =
   let valid = reduce g in
   if valid then
     let result = VCS.result ~solver:(qed_time g) VCS.Valid in
-    ignore (set_result g VCS.Qed result) ;
-    true
+    ( set_result g VCS.Qed result ; true )
   else false
 
 let compute g =