From dc5041b86345e1b2ba036f37335799976237bc3c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 29 Oct 2019 11:56:51 +0100
Subject: [PATCH] [wp/gui] use prover selection to run command
---
src/plugins/wp/GuiConfig.mli | 8 --------
src/plugins/wp/GuiNavigator.ml | 5 +++--
src/plugins/wp/GuiPanel.ml | 12 +++++++++---
src/plugins/wp/GuiPanel.mli | 3 ++-
src/plugins/wp/VC.ml | 3 ++-
src/plugins/wp/VC.mli | 6 ++++--
src/plugins/wp/register.ml | 14 ++++++++++----
7 files changed, 30 insertions(+), 21 deletions(-)
diff --git a/src/plugins/wp/GuiConfig.mli b/src/plugins/wp/GuiConfig.mli
index 68df00a85d9..d812b88b23b 100644
--- a/src/plugins/wp/GuiConfig.mli
+++ b/src/plugins/wp/GuiConfig.mli
@@ -33,12 +33,4 @@ 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 6a97990c81c..eed9d0dbb42 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -91,6 +91,7 @@ class behavior
~(clear : Widget.button)
~(card : card Widget.selector)
~(list : GuiList.pane)
+ ~(provers : GuiConfig.provers)
~(goal : GuiGoal.pane)
~(source : GuiSource.highlighter)
~(popup : GuiSource.popup)
@@ -380,7 +381,7 @@ class behavior
card#connect (fun _ -> self#details) ;
scope#connect self#set_scope ;
popup#on_click self#set_selection ;
- popup#on_prove (GuiPanel.run_and_prove main) ;
+ popup#on_prove (GuiPanel.run_and_prove main provers) ;
clear#connect self#clear ;
end
@@ -505,7 +506,7 @@ let make (main : main_window_extension_points) =
let filter = (filter :> _ Widget.selector) in
let behavior = new behavior ~main
~next ~prev ~index ~scope ~filter ~clear
- ~list ~card ~goal ~source ~popup in
+ ~list ~provers ~card ~goal ~source ~popup in
GuiPanel.on_reload behavior#reload ;
GuiPanel.on_update behavior#update ;
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index 078ddb311e1..c8e6c9759ee 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -63,8 +63,14 @@ let wp_rte_generated s =
not mem
else false
+let spawn provers vcs =
+ if not (Bag.is_empty vcs) then
+ let provers = Why3.Whyconf.Sprover.elements provers#get in
+ VC.command ~provers ~tip:true vcs
+
let run_and_prove
(main:Design.main_window_extension_points)
+ (provers:GuiConfig.provers)
(selection:GuiSource.selection)
=
begin
@@ -72,9 +78,9 @@ let run_and_prove
begin
match selection with
| S_none -> raise Stop
- | S_fun kf -> VC.(command (generate_kf kf))
- | S_prop ip -> VC.(command (generate_ip ip))
- | S_call s -> VC.(command (generate_call s.s_stmt))
+ | S_fun kf -> spawn provers (VC.generate_kf kf)
+ | S_prop ip -> spawn provers (VC.generate_ip ip)
+ | S_call s -> spawn provers (VC.generate_call s.s_stmt)
end ;
if wp_rte_generated selection then
main#redisplay ()
diff --git a/src/plugins/wp/GuiPanel.mli b/src/plugins/wp/GuiPanel.mli
index 25219a0c506..83642c83d9c 100644
--- a/src/plugins/wp/GuiPanel.mli
+++ b/src/plugins/wp/GuiPanel.mli
@@ -27,7 +27,8 @@ val reload : unit -> unit
val on_reload : (unit -> unit) -> unit
val run_and_prove :
- Design.main_window_extension_points -> GuiSource.selection -> unit
+ Design.main_window_extension_points ->
+ GuiConfig.provers -> GuiSource.selection -> unit
val register :
main:Design.main_window_extension_points ->
diff --git a/src/plugins/wp/VC.ml b/src/plugins/wp/VC.ml
index eed3642e3f0..506deb1860a 100644
--- a/src/plugins/wp/VC.ml
+++ b/src/plugins/wp/VC.ml
@@ -96,6 +96,7 @@ let prove = Prover.prove
let spawn = Prover.spawn ~delayed:true
let server = ProverTask.server
-let command vcs = Register.do_wp_proofs_iter (fun f -> Bag.iter f vcs)
+let command ?provers ?tip vcs =
+ Register.do_wp_proofs_iter ?provers ?tip (fun f -> Bag.iter f vcs)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli
index eb916875fb6..630be0e0e50 100644
--- a/src/plugins/wp/VC.mli
+++ b/src/plugins/wp/VC.mli
@@ -98,7 +98,9 @@ val server : ?procs:int -> unit -> Task.server
The returned server is global to Frama-C, but the number of parallel task
allowed will be updated to fit the [~procs] or command-line options. *)
-val command : t Bag.t -> unit
-(** Run the provers with the command-line interface *)
+val command : ?provers:Why3.Whyconf.prover list -> ?tip:bool -> t Bag.t -> unit
+(** Run the provers with the command-line interface.
+ If [~provers] is set, it is used for computing the list of provers to spawn.
+ If [~tip] is set, it is used to compute the script execution mode. *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index bbf63ea8913..e9b9477243e 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -511,7 +511,6 @@ let do_list_scheduled_result () =
(* ------------------------------------------------------------------------ *)
type mode = {
- mutable why3ide : bool ;
mutable tactical : bool ;
mutable update : bool ;
mutable depth : int ;
@@ -585,7 +584,7 @@ let dump_strategies =
)))
let default_mode () = {
- why3ide = false ; tactical = false ; update=false ; provers = [] ;
+ tactical = false ; update=false ; provers = [] ;
depth=0 ; width = 0 ; auto=[] ; backtrack = 0 ;
}
@@ -668,11 +667,18 @@ let do_update_session mode iter =
Wp_parameters.result "Updated session with %d new script%s to complete." f s );
end
-let do_wp_proofs_iter iter =
+let do_wp_proofs_iter ?provers ?tip iter =
let mode = default_mode () in
compute_provers ~mode ;
compute_auto ~mode ;
- let spawned = mode.why3ide || mode.tactical || mode.provers <> [] in
+ begin match provers with None -> () | Some prvs ->
+ mode.provers <- List.map (fun dp -> VCS.BatchMode , VCS.Why3 dp) prvs
+ end ;
+ begin match tip with None -> () | Some tip ->
+ mode.tactical <- tip ;
+ mode.update <- tip ;
+ end ;
+ let spawned = mode.tactical || mode.provers <> [] in
begin
if spawned then do_list_scheduled iter ;
spawn_wp_proofs_iter ~mode iter ;
--
GitLab