From 9739a22a3ec8779b99d2e50f97e629b1144a2f70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 24 Apr 2019 14:45:20 +0200
Subject: [PATCH] [wp/gui] fix prover selection
---
src/plugins/wp/GuiConfig.ml | 80 +++++++++++++++++++++++-----------
src/plugins/wp/GuiConfig.mli | 4 +-
src/plugins/wp/GuiNavigator.ml | 2 +-
src/plugins/wp/GuiPanel.ml | 9 ++--
src/plugins/wp/GuiPanel.mli | 1 -
src/plugins/wp/VCS.ml | 8 ++--
6 files changed, 64 insertions(+), 40 deletions(-)
diff --git a/src/plugins/wp/GuiConfig.ml b/src/plugins/wp/GuiConfig.ml
index 08942acae89..51eb58da116 100644
--- a/src/plugins/wp/GuiConfig.ml
+++ b/src/plugins/wp/GuiConfig.ml
@@ -50,8 +50,8 @@ class enabled key =
| _ -> w in
try
let data = Gtk_helper.Configuration.find key in
- self#set (List.rev (collect [] data))
- with Not_found -> ()
+ List.rev (collect [] data)
+ with Not_found -> []
method private save () =
let open Gtk_helper.Configuration in
@@ -60,7 +60,10 @@ class enabled key =
initializer
begin
- self#load () ;
+ let settings = self#load () in
+ let cmdline = Wp_parameters.Provers.get () in
+ let selection = List.sort_uniq String.compare (settings @ cmdline) in
+ self#set selection ;
self#on_event self#save ;
end
@@ -97,7 +100,7 @@ class dp_chooser
with Not_found -> false
method private entry dp =
- let text = Printf.sprintf "%s (%s)" dp.dp_name dp.dp_version in
+ let text = Pretty_utils.to_string VCS.pretty dp in
let sw = new Widget.switch () in
let lb = new Widget.label ~align:`Left ~text () in
sw#set (self#lookup dp) ;
@@ -155,39 +158,64 @@ class dp_chooser
(* --- WP Prover Switch Panel --- *)
(* ------------------------------------------------------------------------ *)
-[@@@ warning "-37-27"]
-
type mprover =
- | NoProver
- | AltErgo
- | Coq
- | Why3ide
- | Why3 of dp
+ | NONE
+ | ERGO
+ | COQ
+ | WHY of VCS.dp
-class dp_button ~(available:available) ~(enabled:enabled) =
+class dp_button ~(available:available) =
let render = function
- | NoProver -> "None"
- | AltErgo -> "Alt-Ergo (native)"
- | Coq -> "Coq (native,ide)"
- | Why3ide -> "Why3 (ide)"
- | Why3 dp -> Printf.sprintf "Why3: %s (%s)" dp.dp_name dp.dp_version
+ | NONE -> "(none)"
+ | ERGO -> "Alt-Ergo (native)"
+ | COQ -> "Coq (native)"
+ | WHY { dp_shortcuts = keys } when List.mem "alt-ergo" keys ->
+ "Alt-Ergo (why3)"
+ | WHY dp -> Pretty_utils.to_string VCS.pretty dp in
+ let select = function
+ | ERGO -> "alt-ergo"
+ | COQ -> "coq"
+ | WHY { dp_shortcuts=[] } | NONE -> "none"
+ | WHY { dp_shortcuts=key::_ } -> "why3:"^key in
+ let rec import = function
+ | [] -> ERGO
+ | spec::others ->
+ match VCS.prover_of_name spec with
+ | None | Some (Why3ide|Qed) -> NONE
+ | Some (AltErgo|Tactical) -> ERGO
+ | Some Coq -> COQ
+ | Some (Why3 s) ->
+ try
+ let dps = available#get in
+ WHY (List.find (fun dp -> List.mem s dp.dp_shortcuts) dps)
+ with Not_found -> import others
in
- let items = [ NoProver ; AltErgo ; Coq ; Why3ide ] in
- let button = new Widget.menu ~default:AltErgo ~render ~items () 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
- method update () =
- begin
- Format.eprintf "BUTTON UPDATE@." ;
- end
- initializer
+ val mutable dps = []
+
+ method update () =
+ (* called in polling mode *)
begin
- button#connect
- (fun _mp -> Format.eprintf "BUTTON SIGNAL@.") ;
+ let avl = available#get in
+ if avl != dps then
+ begin
+ dps <- avl ;
+ 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 -> Wp_parameters.Provers.set [select s])
end
+
+(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/GuiConfig.mli b/src/plugins/wp/GuiConfig.mli
index eccd95b429d..4022d25f93e 100644
--- a/src/plugins/wp/GuiConfig.mli
+++ b/src/plugins/wp/GuiConfig.mli
@@ -42,9 +42,7 @@ class dp_chooser :
method run : unit -> unit (** Edit enabled provers *)
end
-class dp_button :
- available:available ->
- enabled:enabled ->
+class dp_button : available:available ->
object
inherit Widget.widget
method update : unit -> unit
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 9173fa4b33b..28bb37c4c63 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -408,6 +408,7 @@ let make (main : main_window_extension_points) =
let available = new GuiConfig.available () in
let enabled = new GuiConfig.enabled "wp.enabled" in
+
let dp_chooser = new GuiConfig.dp_chooser ~main ~available ~enabled in
(* -------------------------------------------------------------------------- *)
@@ -502,7 +503,6 @@ let make (main : main_window_extension_points) =
main#register_source_selector popup#register ;
GuiPanel.register ~main
~available_provers:available
- ~enabled_provers:enabled
~configure_provers:dp_chooser#run ;
end
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index aa4f38bb5fd..8597f4fdf7a 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -193,7 +193,6 @@ let wp_update_script label () =
let wp_panel
~(main:Design.main_window_extension_points)
~(available_provers:GuiConfig.available)
- ~(enabled_provers:GuiConfig.enabled)
~(configure_provers:unit -> unit)
=
let vbox = GPack.vbox () in
@@ -222,9 +221,7 @@ let wp_panel
~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
- ~available:available_provers
- ~enabled:enabled_provers in
+ let prover_menu = new GuiConfig.dp_button ~available:available_provers in
form#add_field prover_menu#coerce ;
Gtk_form.register demon prover_menu#update ;
(* End Form *)
@@ -317,8 +314,8 @@ let wp_panel
"WP" , vbox#coerce , Some (Gtk_form.refresh demon) ;
end
-let register ~main ~available_provers ~enabled_provers ~configure_provers =
+let register ~main ~available_provers ~configure_provers =
main#register_panel
- (fun main -> wp_panel ~main ~available_provers ~enabled_provers ~configure_provers)
+ (fun main -> wp_panel ~main ~available_provers ~configure_provers)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/GuiPanel.mli b/src/plugins/wp/GuiPanel.mli
index 8edd57e6ebf..e68cf891b88 100644
--- a/src/plugins/wp/GuiPanel.mli
+++ b/src/plugins/wp/GuiPanel.mli
@@ -32,5 +32,4 @@ val run_and_prove :
val register :
main:Design.main_window_extension_points ->
available_provers:GuiConfig.available ->
- enabled_provers:GuiConfig.enabled ->
configure_provers:(unit -> unit) -> unit
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 37fea1aa59e..55503473e67 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -71,9 +71,11 @@ let name_of_prover = function
| Tactical -> "script"
let title_of_prover = function
- | Why3ide -> "Why3"
- | Why3 "alt-ergo" -> "altergo"
- | Why3 s -> s
+ | Why3 "cvc4" -> "CVC4"
+ | Why3 "z3" -> "Z3"
+ | Why3 ("alt-ergo" | "altergo") -> "Alt-Ergo (why3)"
+ | Why3 s -> Printf.sprintf "Why3 (%s)" s
+ | Why3ide -> "Why3 (ide)"
| AltErgo -> "Alt-Ergo"
| Coq -> "Coq"
| Qed -> "Qed"
--
GitLab