From b75e4cf0a0e3a2f2a5a0501174f7c18fb77e3ecd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 9 May 2023 15:59:50 +0200
Subject: [PATCH] [wp/gui] connecting strategies
---
src/plugins/wp/gui/GuiGoal.ml | 61 ++++++++++++++++++++++++--------
src/plugins/wp/gui/GuiTactic.ml | 11 +++---
src/plugins/wp/gui/GuiTactic.mli | 7 ++--
3 files changed, 54 insertions(+), 25 deletions(-)
diff --git a/src/plugins/wp/gui/GuiGoal.ml b/src/plugins/wp/gui/GuiGoal.ml
index 04f83bb3faa..0148e3f4448 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 4d641d16e66..dcfb10b4643 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 3ea343716b6..716d4620b65 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
(* -------------------------------------------------------------------------- *)
--
GitLab