[wp] added update and fixup modes

src/plugins/wp/GuiGoal.ml

@@ -616,7 +616,7 @@ class pane (gprovers : GuiConfig.provers) =
               VCS.pp_prover prv Wpo.pp_title wpo VCS.pp_result res
           end
         ~success:(fun _ _ -> Wutil.later self#commit)
-        ~pool (List.map (fun dp -> VCS.BatchMode , dp) provers)
+        ~pool (List.map (fun dp -> VCS.Batch , dp) provers)
 
     method private fork proof fork =
       Wutil.later

src/plugins/wp/GuiNavigator.ml

@@ -251,7 +251,7 @@ class behavior
           | VCS.Tactical ->
               begin
                 match mode , ProverScript.get w with
-                | (None | Some VCS.BatchMode) , `Script ->
+                | (None | Some VCS.Batch) , `Script ->
                     schedule (ProverScript.prove ~success w)
                 | _ ->
                     card#set `Goal ;
@@ -261,9 +261,9 @@ class behavior
           | _ ->
               let mode = match mode , prover with
                 | Some m , _ -> m
-                | None , VCS.NativeCoq -> VCS.EditMode
-                | None , VCS.NativeAltErgo -> VCS.FixMode
-                | _ -> if VCS.is_auto prover then VCS.BatchMode else VCS.FixMode in
+                | None , VCS.NativeCoq -> VCS.Edit
+                | None , VCS.NativeAltErgo -> VCS.Fix
+                | _ -> if VCS.is_auto prover then VCS.Batch else VCS.Fix in
               schedule (Prover.prove w ~mode ~result prover) ;
               refresh w
       end
@@ -325,17 +325,17 @@ class behavior
     initializer
       let open VCS in
       begin
-        popup_tip#add_item ~label:"Run Script" ~callback:(self#popup_run BatchMode) ;
-        popup_tip#add_item ~label:"Edit Proof" ~callback:(self#popup_run EditMode) ;
+        popup_tip#add_item ~label:"Run Script" ~callback:(self#popup_run Batch) ;
+        popup_tip#add_item ~label:"Edit Proof" ~callback:(self#popup_run Edit) ;
         popup_tip#add_item ~label:"Delete Script" ~callback:(self#popup_delete_script) ;
-        popup_why3_auto#add_item ~label:"Run Prover" ~callback:(self#popup_run VCS.BatchMode) ;
-        popup_why3_inter#add_item ~label:"Check Script" ~callback:(self#popup_run VCS.BatchMode) ;
-        popup_why3_inter#add_item ~label:"Edit Script" ~callback:(self#popup_run VCS.EditMode) ;
-        popup_why3_inter#add_item ~label:"Fixup Script" ~callback:(self#popup_run VCS.FixMode) ;
+        popup_why3_auto#add_item ~label:"Run Prover" ~callback:(self#popup_run VCS.Batch) ;
+        popup_why3_inter#add_item ~label:"Check Script" ~callback:(self#popup_run VCS.Batch) ;
+        popup_why3_inter#add_item ~label:"Edit Script" ~callback:(self#popup_run VCS.Edit) ;
+        popup_why3_inter#add_item ~label:"Fixup Script" ~callback:(self#popup_run VCS.FixUpdate) ;
         self#add_popup_proofmodes popup_ergo
-          [ "Run",BatchMode ; "Open Altgr-Ergo on Fail",EditMode ; "Open Altgr-Ergo",EditMode ] ;
+          [ "Run",Batch ; "Open Altgr-Ergo on Fail",Edit ; "Open Altgr-Ergo",Edit ] ;
         self#add_popup_proofmodes popup_coq
-          [ "Check Proof",BatchMode ; "Edit on Fail",EditMode ; "Edit Proof",EditMode ] ;
+          [ "Check Proof",Batch ; "Edit on Fail",Edit ; "Edit Proof",Edit ] ;
       end
 
     method private popup w p =

src/plugins/wp/ProverCoq.ml

@@ -599,9 +599,9 @@ let prove_session ~mode w =
     compile_headers w.cw_includes false w.cw_headers >>=
     begin fun () ->
       match mode with
-      | BatchMode -> try_prove w
-      | EditMode -> try_coqide w
-      | FixMode ->
+      | Batch | Update -> try_prove w
+      | Edit -> try_coqide w
+      | Fix | FixUpdate ->
           begin
             try_prove w >>> function
             | Task.Result true -> Task.return true

src/plugins/wp/ProverErgo.ml

@@ -455,11 +455,11 @@ let try_prove ~config ~pid ~gui ~file ~lines ~logout ~logerr =
 
 let prove_file ~config ~pid ~mode ~file ~lines ~logout ~logerr =
   let gui = match mode with
-    | EditMode -> Lazy.force altergo_gui
-    | BatchMode | FixMode -> false in
+    | Edit -> Lazy.force altergo_gui
+    | Batch | Update | Fix | FixUpdate -> false in
   try_prove ~config ~pid ~gui ~file ~lines ~logout ~logerr >>= function
   | { verdict=(VCS.Unknown|VCS.Timeout|VCS.Stepout) }
-    when mode = FixMode && Lazy.force altergo_gui ->
+    when (mode = Fix || mode = FixUpdate) && Lazy.force altergo_gui ->
       try_prove ~config ~pid ~gui:true ~file ~lines ~logout ~logerr
   | r -> Task.return r
 

src/plugins/wp/ProverScript.ml

@@ -162,7 +162,7 @@ struct
     | None -> ProofEngine.main env.tree
 
   let prove env wpo ?config prover =
-    Prover.prove wpo ?config ~mode:VCS.BatchMode
+    Prover.prove wpo ?config ~mode:VCS.Batch
       ~progress:env.progress prover
 
   let backtracking env =

src/plugins/wp/ProverWhy3.ml

@@ -1276,22 +1276,25 @@ let scriptfile ~force ~ext wpo =
   let dir = Wp_parameters.get_session_dir ~force "interactive" in
   Format.sprintf "%s/%s%s" (dir :> string) wpo.Wpo.po_sid ext
 
+let updatescript ~script driver task =
+  let backup = script ^ ".bak" in
+  Sys.rename script backup ;
+  let old = open_in backup in
+  Command.pp_to_file script
+    (fun fmt ->
+       ignore @@ Why3.Driver.print_task_prepared ~old driver fmt task
+    );
+  close_in old ;
+  let d_old = Digest.file backup in
+  let d_new = Digest.file script in
+  if String.equal d_new d_old then Extlib.safe_remove backup
+
 let editor ~script ~merge wpo pconf driver prover task =
   Task.sync editor_mutex
     begin fun () ->
       Wp_parameters.feedback ~ontty:`Transient "Editing %S..." script ;
       Cache.clear_result ~digest:(digest wpo driver) prover task ;
-      if merge then
-        begin
-          let backup = script ^ ".bak" in
-          Sys.rename script backup ;
-          let old = open_in backup in
-          Command.pp_to_file script
-            (fun fmt ->
-               ignore @@ Why3.Driver.print_task_prepared ~old driver fmt task
-            );
-          close_in old ;
-        end ;
+      if merge then updatescript ~script driver task ;
       let command = editor_command pconf in
       let call = Why3.Call_provers.call_editor ~command script in
       call_prover_task ~timeout:None ~steps:None pconf.prover call
@@ -1304,7 +1307,7 @@ let compile ~script ~timeout wpo pconf driver prover task =
 
 let prepare ~mode wpo driver task =
   let ext = Filename.extension (Why3.Driver.file_of_task driver "S" "T" task) in
-  let force = mode <> VCS.BatchMode in
+  let force = mode <> VCS.Batch in
   let script = scriptfile ~force wpo ~ext in
   if Sys.file_exists script then Some (script, true) else
   if force then
@@ -1324,16 +1327,27 @@ let interactive ~mode wpo pconf driver prover task =
   | None -> Task.return VCS.unknown
   | Some (script, merge) ->
       match mode with
-      | VCS.BatchMode ->
+      | VCS.Batch ->
           compile ~script ~timeout wpo pconf driver prover task
-      | VCS.EditMode ->
+      | VCS.Update ->
+          if merge then updatescript ~script driver task ;
+          compile ~script ~timeout wpo pconf driver prover task
+      | VCS.Edit ->
           let open Task in
           editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
           compile ~script ~timeout wpo pconf driver prover task
-      | VCS.FixMode ->
+      | VCS.Fix ->
+          let open Task in
+          compile ~script ~timeout wpo pconf driver prover task >>= fun r ->
+          if VCS.is_valid r then return r else
+            editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
+            compile ~script ~timeout wpo pconf driver prover task
+      | VCS.FixUpdate ->
           let open Task in
+          if merge then updatescript ~script driver task ;
           compile ~script ~timeout wpo pconf driver prover task >>= fun r ->
           if VCS.is_valid r then return r else
+            let merge = false in
             editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
             compile ~script ~timeout wpo pconf driver prover task
 
@@ -1345,7 +1359,7 @@ let is_trivial (t : Why3.Task.task) =
   let goal = Why3.Task.task_goal_fmla t in
   Why3.Term.t_equal goal Why3.Term.t_true
 
-let build_proof_task ?(mode=VCS.BatchMode) ?timeout ?steplimit ~prover wpo () =
+let build_proof_task ?(mode=VCS.Batch) ?timeout ?steplimit ~prover wpo () =
   try
     (* Always generate common task *)
     let context = Wpo.get_context wpo in

src/plugins/wp/VCS.ml

@@ -34,9 +34,11 @@ type prover =
   | Tactical      (* Interactive Prover *)
 
 type mode =
-  | BatchMode (* Only check scripts *)
-  | EditMode  (* Edit then check scripts *)
-  | FixMode   (* Try check script, then edit script on non-success *)
+  | Batch (* Only check scripts *)
+  | Update (* Check and update scripts *)
+  | Edit  (* Edit then check scripts *)
+  | Fix   (* Try to check script, then edit script on non-success *)
+  | FixUpdate (* Update and fix *)
 
 let parse_prover = function
   | "" | "none" -> None
@@ -76,13 +78,15 @@ let parse_prover = function
 
 let parse_mode m =
   match String.lowercase_ascii m with
-  | "fix" -> FixMode
-  | "edit" -> EditMode
-  | "batch" -> BatchMode
+  | "fix" -> Fix
+  | "edit" -> Edit
+  | "batch" -> Batch
+  | "update" -> Update
+  | "fixup" -> FixUpdate
   | _ ->
       Wp_parameters.error ~once:true
         "Unrecognized mode %S (use 'batch' instead)" m ;
-      BatchMode
+      Batch
 
 let name_of_prover = function
   | Why3 s -> Why3Provers.print_wp s
@@ -102,9 +106,11 @@ let title_of_prover = function
   | Tactical -> "Script"
 
 let title_of_mode = function
-  | FixMode -> "Fix"
-  | EditMode -> "Edit"
-  | BatchMode -> "Batch"
+  | Fix -> "Fix"
+  | Edit -> "Edit"
+  | Batch -> "Batch"
+  | Update -> "Update"
+  | FixUpdate -> "Fix Update"
 
 let sanitize_why3 s =
   let buffer = Buffer.create 80 in

src/plugins/wp/VCS.mli

@@ -27,16 +27,18 @@
 (** {2 Prover} *)
 
 type prover =
-  | Why3 of Why3Provers.t (* Prover via WHY *)
-  | NativeAltErgo (* Direct Alt-Ergo *)
-  | NativeCoq     (* Direct Coq and Coqide *)
-  | Qed           (* Qed Solver *)
-  | Tactical      (* Interactive Prover *)
+  | Why3 of Why3Provers.t (** Prover via WHY *)
+  | NativeAltErgo (** Direct Alt-Ergo *)
+  | NativeCoq     (** Direct Coq and Coqide *)
+  | Qed           (** Qed Solver *)
+  | Tactical      (** Interactive Prover *)
 
 type mode =
-  | BatchMode (* Only check scripts *)
-  | EditMode  (* Edit then check scripts *)
-  | FixMode   (* Try check script, then edit script on non-success *)
+  | Batch  (** Only check scripts *)
+  | Update (** Check and update scripts *)
+  | Edit   (** Edit then check scripts *)
+  | Fix    (** Try check script, then edit script on non-success *)
+  | FixUpdate (** Update & Fix *)
 
 module Pset : Set.S with type elt = prover
 module Pmap : Map.S with type key = prover

src/plugins/wp/prover.ml

@@ -59,7 +59,7 @@ let update ?result wpo prover res =
   | None -> ()
   | Some f -> f wpo prover res
 
-let run_prover wpo ?config ?(mode=BatchMode) ?progress ?result prover =
+let run_prover wpo ?config ?(mode=Batch) ?progress ?result prover =
   signal ?progress wpo (VCS.name_of_prover prover) ;
   dispatch ?config mode prover wpo >>>
   fun status ->

src/plugins/wp/register.ml

@@ -615,7 +615,7 @@ let compute_provers ~mode ~script =
               script.update <- true ;
             prvs
         | Some prover ->
-            let pmode = if VCS.is_auto prover then VCS.BatchMode else mode in
+            let pmode = if VCS.is_auto prover then VCS.Batch else mode in
             (pmode , prover) :: prvs
       end (get_prover_names ()) []
 
@@ -720,7 +720,7 @@ let do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) =
   compute_provers ~mode ~script ;
   compute_auto ~script ;
   begin match provers with None -> () | Some prvs ->
-    script.provers <- List.map (fun dp -> VCS.BatchMode , VCS.Why3 dp) prvs
+    script.provers <- List.map (fun dp -> VCS.Batch , VCS.Why3 dp) prvs
   end ;
   begin match tip with None -> () | Some tip ->
     script.tactical <- tip ;