[wp/gui] simplified panel & prover selection

src/plugins/wp/GuiConfig.ml

@@ -156,70 +156,3 @@ class dp_chooser
   end
 
 (* ------------------------------------------------------------------------ *)
-(* ---  WP Prover Switch Panel                                          --- *)
-(* ------------------------------------------------------------------------ *)
-
-type mprover =
-  | NONE
-  | ERGO
-  | COQ
-  | WHY of Why3Provers.t
-
-class dp_button () =
-  let render = function
-    | NONE -> "(none)"
-    | ERGO -> "Alt-Ergo (native)"
-    | COQ -> "Coq (native)"
-    | WHY p when Why3Provers.has_shortcut p "alt-ergo" ->
-        "Alt-Ergo (why3)"
-    | WHY dp -> Why3Provers.title dp in
-  let select = function
-    | ERGO -> VCS.NativeAltErgo
-    | COQ -> VCS.NativeCoq
-    | NONE -> VCS.Qed
-    | WHY p -> VCS.Why3 p in
-  let rec import = function
-    | [] -> ERGO
-    | spec::others ->
-        match VCS.prover_of_name spec with
-        | None | Some VCS.Qed -> NONE
-        | Some (VCS.NativeAltErgo|VCS.Tactical) -> ERGO
-        | Some VCS.NativeCoq -> COQ
-        | Some (VCS.Why3 p) ->
-            if Why3.Whyconf.Sprover.mem p (Why3Provers.provers_set ())
-            then WHY p
-            else import others
-  in
-  let items = [ NONE ; ERGO ; COQ ] in
-  let button = new Widget.menu ~default:ERGO ~render ~items () in
-  object(self)
-    method coerce = button#coerce
-    method widget = (self :> Widget.t)
-    method set_enabled = button#set_enabled
-    method set_visible = button#set_visible
-    val mutable dps = Why3.Whyconf.Sprover.empty
-
-    method update () =
-      (* called in polling mode *)
-      begin
-        let avl = Why3Provers.provers_set () in
-        if Why3.Whyconf.Sprover.equal avl dps then
-          begin
-            dps <- avl ;
-            let dps = Why3.Whyconf.Sprover.elements dps in
-            let items = [NONE;ERGO] @ List.map (fun p -> WHY p) dps @ [COQ] in
-            button#set_items items
-          end ;
-        let cur = Wp_parameters.Provers.get () |> import in
-        if cur <> button#get then button#set cur ;
-      end
-
-    initializer button#connect
-        (fun s ->
-           let p = select s in
-           let p = VCS.name_of_prover p in
-           Wp_parameters.Provers.set [p]
-        )
-  end
-
-(* ------------------------------------------------------------------------ *)

src/plugins/wp/GuiConfig.mli

@@ -33,8 +33,12 @@ class dp_chooser :
     method run : unit -> unit (** Edit enabled provers *)
   end
 
+(*
 class dp_button : unit ->
   object
     inherit Widget.widget
     method update : unit -> unit
   end
+*)
+
+(* ------------------------------------------------------------------------ *)

src/plugins/wp/GuiNavigator.ml

@@ -238,24 +238,28 @@ class behavior
           let server = ProverTask.server () in
           Task.spawn server thread ;
           Task.launch server in
-        match prover with
-        | VCS.Tactical ->
-            begin
-              match mode , ProverScript.get w with
-              | (None | Some VCS.BatchMode) , `Script ->
-                  schedule (ProverScript.prove ~success w)
-              | _ ->
-                  card#set `Goal ;
-                  clear#set_enabled false ;
-                  self#navigator true (Some w) ;
-            end
-        | _ ->
-            let mode = match mode , prover with
-              | Some m , _ -> m
-              | None , VCS.NativeCoq -> VCS.EditMode
-              | None , VCS.NativeAltErgo -> VCS.FixMode
-              | _ -> VCS.BatchMode in
-            schedule (Prover.prove w ~mode ~result prover)
+        if not (VCS.is_valid (Wpo.get_result w VCS.Qed)) &&
+           not (VCS.is_computing (Wpo.get_result w prover))
+        then
+          match prover with
+          | VCS.Tactical ->
+              begin
+                match mode , ProverScript.get w with
+                | (None | Some VCS.BatchMode) , `Script ->
+                    schedule (ProverScript.prove ~success w)
+                | _ ->
+                    card#set `Goal ;
+                    clear#set_enabled false ;
+                    self#navigator true (Some w) ;
+              end
+          | _ ->
+              let mode = match mode , prover with
+                | Some m , _ -> m
+                | None , VCS.NativeCoq -> VCS.EditMode
+                | None , VCS.NativeAltErgo -> VCS.FixMode
+                | _ -> VCS.BatchMode in
+              schedule (Prover.prove w ~mode ~result prover) ;
+              refresh w
       end
 
     method private clear () =

src/plugins/wp/GuiPanel.ml

@@ -164,17 +164,6 @@ class model_selector (main : Design.main_window_extension_points) =
 (* ---  WP Panel                                                        --- *)
 (* ------------------------------------------------------------------------ *)
 
-let wp_dir = ref (Sys.getcwd())
-
-let wp_script () =
-  let file = Gtk_helper.select_file
-      ~title:"Script File for Coq proofs"
-      ~dir:wp_dir ~filename:"wp.script" ()
-  in
-  match file with
-  | Some f -> Wp_parameters.Script.set f
-  | None -> ()
-
 let wp_update_model label () =
   let s = Factory.parse (Wp_parameters.Model.get ()) in
   label#set_text (Factory.descr s)
@@ -185,11 +174,6 @@ let wp_configure_model main label () =
     wp_update_model label () ;
   end
 
-let wp_update_script label () =
-  let file = Wp_parameters.Script.get () in
-  let text = if file = "" then "(None)" else Filename.basename file in
-  label#set_text text
-
 let wp_panel
     ~(main:Design.main_window_extension_points)
     ~(configure_provers:unit -> unit)
@@ -199,6 +183,7 @@ let wp_panel
   let packing = vbox#pack in
 
   let form = new Wpane.form () in
+
   (* Model Row *)
   let model_cfg = new Widget.button
     ~label:"Model..." ~tooltip:"Configure WP Model" () in
@@ -207,42 +192,13 @@ let wp_panel
   model_cfg#connect (wp_configure_model main model_lbl) ;
   form#add_label_widget model_cfg#coerce ;
   form#add_field model_lbl#coerce ;
-  (* Script Row *)
-  let script_cfg = new Widget.button
-    ~label:"Script..." ~tooltip:"Load/Save User Scripts file" () in
-  let script_lbl = GMisc.label ~xalign:0.0 () in
-  Gtk_form.register demon (wp_update_script script_lbl) ;
-  script_cfg#connect wp_script ;
-  form#add_label_widget script_cfg#coerce ;
-  form#add_field script_lbl#coerce ;
-  (* Prover Row *)
   let prover_cfg = new Widget.button
     ~label:"Provers..." ~tooltip:"Detect WP Provers" () in
   prover_cfg#connect configure_provers ;
   form#add_label_widget prover_cfg#coerce ;
-  let prover_menu = new GuiConfig.dp_button () in
-  form#add_field prover_menu#coerce ;
-  Gtk_form.register demon prover_menu#update ;
   (* End Form *)
   packing form#coerce ;
 
-  let options = GPack.hbox ~spacing:16 ~packing () in
-
-  Gtk_form.check ~label:"RTE"
-    ~tooltip:"Generates RTE guards for WP"
-    ~packing:options#pack
-    Wp_parameters.RTE.get Wp_parameters.RTE.set demon ;
-
-  Gtk_form.check ~label:"Split"
-    ~tooltip:"Splits conjunctions into sub-goals"
-    ~packing:options#pack
-    Wp_parameters.Split.get Wp_parameters.Split.set demon ;
-
-  Gtk_form.check ~label:"Trace"
-    ~tooltip:"Reports proof information from provers"
-    ~packing:options#pack
-    Wp_parameters.ProofTrace.get Wp_parameters.ProofTrace.set demon ;
-
   let control = GPack.table ~columns:2 ~col_spacings:8 ~rows:4 ~packing () in
   let addcontrol line col w = control#attach ~left:(col-1) ~top:(line-1) ~expand:`NONE w in
 

src/plugins/wp/VCS.ml

@@ -207,7 +207,8 @@ let is_verdict r = match r.verdict with
   | Valid | Checked | Unknown | Invalid | Timeout | Stepout | Failed -> true
   | NoResult | Computing _ -> false
 
-let is_valid r = r.verdict = Valid
+let is_valid = function { verdict = Valid } -> true | _ -> false
+let is_computing = function { verdict=Computing _ } -> true | _ -> false
 
 let configure r =
   let valid = (r.verdict = Valid) in

src/plugins/wp/VCS.mli

@@ -111,6 +111,7 @@ val result : ?cached:bool -> ?solver:float -> ?time:float -> ?steps:int -> verdi
 val is_auto : prover -> bool
 val is_verdict : result -> bool
 val is_valid: result -> bool
+val is_computing: result -> bool
 val configure : result -> config
 val autofit : result -> bool (** Result that fits the default configuration *)