From 3159bba6af43418524d167aeabb9d515d3b6f959 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 30 May 2023 14:42:47 +0200
Subject: [PATCH] [wp] better hints computation
---
src/plugins/wp/ProofEngine.ml | 3 ++-
src/plugins/wp/ProofEngine.mli | 3 ++-
src/plugins/wp/ProofStrategy.ml | 18 ++++++++++++------
src/plugins/wp/ProofStrategy.mli | 2 +-
src/plugins/wp/gui/GuiGoal.ml | 17 +++++++++--------
src/plugins/wp/register.ml | 3 +--
6 files changed, 27 insertions(+), 19 deletions(-)
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index c15320f187b..d597ee19979 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -190,7 +190,8 @@ let consolidated wpo =
(* -------------------------------------------------------------------------- *)
let main t = t.main
-let head t = match t.head with
+let head t = t.head
+let head_goal t = match t.head with
| None -> t.main
| Some n -> n.goal
let goal n = n.goal
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 33cb4ae786c..f974522b229 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -63,8 +63,9 @@ val current : tree -> current
val goto : tree -> position -> unit
val main : tree -> Wpo.t
-val head : tree -> Wpo.t
val goal : node -> Wpo.t
+val head : tree -> node option
+val head_goal : tree -> Wpo.t
val tree_context : tree -> WpContext.t
val node_context : node -> WpContext.t
diff --git a/src/plugins/wp/ProofStrategy.ml b/src/plugins/wp/ProofStrategy.ml
index 862ef1c023b..4440b768d7b 100644
--- a/src/plugins/wp/ProofStrategy.ml
+++ b/src/plugins/wp/ProofStrategy.ml
@@ -421,12 +421,18 @@ let default () =
) @@
Wp_parameters.DefaultStrategies.get ()
-let hints goal =
- let hs =
- let pid = goal.Wpo.po_pid in
- List.filter_map (fun (name,_) -> Hashtbl.find_opt strategies name) @@
- List.filter (fun (_,ps) -> WpPropId.select_by_name ps pid) !revhints
- in List.rev_append hs (default ())
+let hints ?node goal =
+ let pool = ref [] in
+ let add s = if not @@ List.memq s !pool then pool := s :: !pool in
+ let addname name = Option.iter add @@ Hashtbl.find_opt strategies name in
+ Option.iter addname (Option.bind node ProofEngine.get_hint) ;
+ let pid = goal.Wpo.po_pid in
+ List.iter
+ (fun (name,ps) ->
+ if WpPropId.select_by_name ps pid then addname name
+ ) !revhints ;
+ List.iter add @@ List.rev @@ default () ;
+ List.rev !pool
let has_hint goal =
let pid = goal.Wpo.po_pid in
diff --git a/src/plugins/wp/ProofStrategy.mli b/src/plugins/wp/ProofStrategy.mli
index 9e84f5bd61d..90c5995b1f8 100644
--- a/src/plugins/wp/ProofStrategy.mli
+++ b/src/plugins/wp/ProofStrategy.mli
@@ -34,7 +34,7 @@ val typecheck : unit -> unit
val name : strategy -> string
val loc : strategy -> Cil_types.location
val find : string -> strategy option
-val hints : Wpo.t -> strategy list
+val hints : ?node:ProofEngine.node -> Wpo.t -> strategy list
val has_hint : Wpo.t -> bool
val iter : (strategy -> unit) -> unit
diff --git a/src/plugins/wp/gui/GuiGoal.ml b/src/plugins/wp/gui/GuiGoal.ml
index 0148e3f4448..c4b555bd1ff 100644
--- a/src/plugins/wp/gui/GuiGoal.ml
+++ b/src/plugins/wp/gui/GuiGoal.ml
@@ -386,11 +386,13 @@ class pane (gprovers : GuiConfig.provers) =
autosearch#connect None ;
strategies#connect None ;
List.iter (fun tactic -> tactic#clear) tactics
- | Some(tree,wpo,sequent,sel) ->
+ | Some(tree,sequent,sel) ->
on_proof_context tree
begin fun () ->
(* configure strategies *)
- let hints = ProofStrategy.hints wpo in
+ let node = ProofEngine.head tree in
+ let wpo = ProofEngine.head_goal tree in
+ let hints = ProofStrategy.hints ?node wpo in
autosearch#connect (Some (self#autosearch sequent));
strategies#connect ~hints (Some self#strategies);
(* configure tactics *)
@@ -515,12 +517,11 @@ class pane (gprovers : GuiConfig.provers) =
self#update_provers None ;
self#update_tactics None ;
| Proof proof ->
- let wpo = ProofEngine.head proof in
begin
- self#update_provers (Some wpo) ;
+ self#update_provers (Some (ProofEngine.head_goal proof)) ;
let sequent = printer#sequent in
let select = printer#selection in
- self#update_tactics (Some(proof,wpo,sequent,select)) ;
+ self#update_tactics (Some(proof,sequent,select)) ;
end
| Composer _ | Browser _ -> ()
@@ -560,7 +561,7 @@ class pane (gprovers : GuiConfig.provers) =
text#hrule ;
scripter#tree proof ;
text#hrule ;
- text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
+ text#printf "%t@." (printer#goal (ProofEngine.head_goal proof)) ;
text#printf "@{<bf>Goal id:@} %s@." main.po_gid ;
text#printf "@{<bf>Short id:@} %s@." main.po_sid ;
text#hrule ;
@@ -576,7 +577,7 @@ class pane (gprovers : GuiConfig.provers) =
self#update in
text#printf "%t@." (composer#print cc ~quit) ;
text#hrule ;
- text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
+ text#printf "%t@." (printer#goal (ProofEngine.head_goal proof)) ;
end ()
| Browser(proof,cc,tgt) ->
on_proof_context proof
@@ -588,7 +589,7 @@ class pane (gprovers : GuiConfig.provers) =
self#update in
text#printf "%t@." (browser#print cc ~quit) ;
text#hrule ;
- text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
+ text#printf "%t@." (printer#goal (ProofEngine.head_goal proof)) ;
end ()
| Forking _ -> ()
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 597d31342dd..3b5f932999a 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -96,8 +96,7 @@ let do_print_goal_status fmt (g : Wpo.t) =
Format.fprintf fmt "%tSubgoal %d/%d:@\n" Wpo.pp_flow (succ i) n ;
ProofEngine.goto tree (`Leaf i) ;
do_print_current fmt tree ;
- let g = ProofEngine.head tree in
- Wpo.pp_goal fmt g
+ Wpo.pp_goal fmt @@ ProofEngine.head_goal tree
done
end ;
Wpo.pp_flow fmt ;
--
GitLab