From fc2ba2fa005ad6a6e5474d4ae8c6949edc62c348 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 13 Sep 2019 16:28:53 +0200
Subject: [PATCH] [wp/gui] simplified panel & prover selection
---
src/plugins/wp/GuiConfig.ml | 67 ----------------------------------
src/plugins/wp/GuiConfig.mli | 4 ++
src/plugins/wp/GuiNavigator.ml | 40 +++++++++++---------
src/plugins/wp/GuiPanel.ml | 46 +----------------------
src/plugins/wp/VCS.ml | 3 +-
src/plugins/wp/VCS.mli | 1 +
6 files changed, 30 insertions(+), 131 deletions(-)
diff --git a/src/plugins/wp/GuiConfig.ml b/src/plugins/wp/GuiConfig.ml
index 7974c19d95c..f5f6e9b4020 100644
--- a/src/plugins/wp/GuiConfig.ml
+++ b/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
-
-(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/GuiConfig.mli b/src/plugins/wp/GuiConfig.mli
index 4e068822df1..b2e35a7bcaa 100644
--- a/src/plugins/wp/GuiConfig.mli
+++ b/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
+*)
+
+(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 57257f3a473..f4c4a2eb52b 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/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 () =
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index da074d2311e..c71d56d3012 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/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
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 6d527714657..f71051092d0 100644
--- a/src/plugins/wp/VCS.ml
+++ b/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
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 8159ea2e4e3..ef4284710e8 100644
--- a/src/plugins/wp/VCS.mli
+++ b/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 *)
--
GitLab