diff --git a/src/plugins/wp/gui/GuiGoal.ml b/src/plugins/wp/gui/GuiGoal.ml
index 04f83bb3faab159d63e0222325ddbe227f06cb9d..0148e3f44485bb1f35da507c9c9ed4ffbeb38aeb 100644
--- a/src/plugins/wp/gui/GuiGoal.ml
+++ b/src/plugins/wp/gui/GuiGoal.ml
@@ -117,7 +117,8 @@ class pane (gprovers : GuiConfig.provers) =
let autofocus = new autofocus in
let iformat = new iformat in
let rformat = new rformat in
- let autosearch = new GuiTactic.auto () in
+ let autosearch = new GuiTactic.autosearch () in
+ let strategies = new GuiTactic.strategies () in
object(self)
val mutable state : state = Empty
@@ -146,7 +147,9 @@ class pane (gprovers : GuiConfig.provers) =
provers <- why3_provers ;
List.iter (fun p -> palette#add_tool p#tool) provers ;
palette#add_tool autosearch#tool ;
+ palette#add_tool strategies#tool ;
Strategy.iter autosearch#register ;
+ ProofStrategy.iter strategies#register ;
Tactical.iter
(fun tac ->
let gtac = new GuiTactic.tactic tac printer#pp_selection in
@@ -381,22 +384,26 @@ class pane (gprovers : GuiConfig.provers) =
| None ->
printer#set_target Tactical.Empty ;
autosearch#connect None ;
+ strategies#connect None ;
List.iter (fun tactic -> tactic#clear) tactics
- | Some(tree,sequent,sel) ->
+ | Some(tree,wpo,sequent,sel) ->
on_proof_context tree
begin fun () ->
- autosearch#connect (Some (self#autosearch sequent)) ;
- let select (tactic : GuiTactic.tactic) =
- let process = self#apply in
- let composer = self#compose in
- let browser = self#browse in
- tactic#select ~process ~composer ~browser ~tree sel
- in
- List.iter select tactics ;
- let tgt =
- if List.exists (fun tactics -> tactics#targeted) tactics
- then sel else Tactical.Empty in
- printer#set_target tgt
+ (* configure strategies *)
+ let hints = ProofStrategy.hints wpo in
+ autosearch#connect (Some (self#autosearch sequent));
+ strategies#connect ~hints (Some self#strategies);
+ (* configure tactics *)
+ List.iter (fun (tactic : GuiTactic.tactic) ->
+ let process = self#apply in
+ let composer = self#compose in
+ let browser = self#browse in
+ tactic#select ~process ~composer ~browser ~tree sel
+ ) tactics ;
+ (* target selection feedback *)
+ printer#set_target
+ (if List.exists (fun tactics -> tactics#targeted) tactics
+ then sel else Tactical.Empty)
end ()
method private update_scriptbar =
@@ -513,7 +520,7 @@ class pane (gprovers : GuiConfig.provers) =
self#update_provers (Some wpo) ;
let sequent = printer#sequent in
let select = printer#selection in
- self#update_tactics (Some(proof,sequent,select)) ;
+ self#update_tactics (Some(proof,wpo,sequent,select)) ;
end
| Composer _ | Browser _ -> ()
@@ -692,6 +699,30 @@ class pane (gprovers : GuiConfig.provers) =
end
end
+ method private strategies ~depth strategy =
+ match state with
+ | Empty | Forking _ | Composer _ | Browser _ -> ()
+ | Proof proof ->
+ Wutil.later
+ begin fun () ->
+ ProverScript.explore
+ ~depth ?strategy
+ ~result:
+ (fun wpo prv res ->
+ text#printf "[%a] %a : %a@."
+ VCS.pp_prover prv
+ Wpo.pp_title wpo
+ VCS.pp_result res)
+ ~success:
+ (fun _ _ ->
+ ProofEngine.forward proof ;
+ self#update ;
+ text#printf "Strategie(s) Explored." )
+ proof (ProofEngine.anchor proof ()) ;
+ let server = ProverTask.server () in
+ Task.launch server
+ end
+
method private backtrack node =
match state with
| Empty | Forking _ | Composer _ | Browser _ -> ()
diff --git a/src/plugins/wp/gui/GuiTactic.ml b/src/plugins/wp/gui/GuiTactic.ml
index 4d641d16e66fdf7550b8a6ae37da790baef408c6..dcfb10b46439d25ae5d75c275dc6530fd7b8bf47 100644
--- a/src/plugins/wp/gui/GuiTactic.ml
+++ b/src/plugins/wp/gui/GuiTactic.ml
@@ -517,7 +517,7 @@ let checkbox ~(form:Wpane.form) ~default ~label ~tooltip =
type auto_callback = depth:int -> width:int -> Strategy.heuristic list -> unit
-class auto () =
+class autosearch () =
let form = new Wpane.form () in
let depth = spinner ~form ~default:1 ~label:"Depth"
~tooltip:"Limit the number of nested strategies" in
@@ -616,11 +616,10 @@ class strategies () =
button#connect (self#strategy s) ;
end
- method hints (hs: ProofStrategy.strategy list) =
- filter <- hs ; self#update
-
- method connect (cb : callback option) =
- callback <- cb ; self#update
+ method connect ?(hints=[]) (cb : callback option) =
+ callback <- cb ;
+ filter <- hints ;
+ self#update
method private strategy (s : ProofStrategy.strategy) () =
Option.iter (fun fn -> fn ~depth:depth#get (Some s)) callback
diff --git a/src/plugins/wp/gui/GuiTactic.mli b/src/plugins/wp/gui/GuiTactic.mli
index 3ea343716b676310262294b080549afe5cae9dd4..716d4620b65d0e4e0804fa1f2fa6af3ed59893d8 100644
--- a/src/plugins/wp/gui/GuiTactic.mli
+++ b/src/plugins/wp/gui/GuiTactic.mli
@@ -74,7 +74,7 @@ class tactic : Tactical.t -> (Format.formatter -> Tactical.selection -> unit) ->
type auto_callback = depth:int -> width:int -> Strategy.heuristic list -> unit
-class auto : unit ->
+class autosearch : unit ->
object
inherit Wpalette.tool
method register : Strategy.heuristic -> unit
@@ -85,15 +85,14 @@ class auto : unit ->
(* --- Strategies Dongle --- *)
(* -------------------------------------------------------------------------- *)
-
type callback = (depth:int -> ProofStrategy.strategy option -> unit)
class strategies : unit ->
object
inherit Wpalette.tool
method register : ProofStrategy.strategy -> unit
- method hints : ProofStrategy.strategy list -> unit
- method connect : callback option -> unit
+ method connect : ?hints:ProofStrategy.strategy list ->
+ callback option -> unit
end
(* -------------------------------------------------------------------------- *)