diff --git a/src/plugins/wp/ProofStrategy.ml b/src/plugins/wp/ProofStrategy.ml
index 4e02e13ce3903ea2e5f7dbbe637a576f885b3a56..dcc6d56000d0a40bc76c846708e6d343596d741a 100644
--- a/src/plugins/wp/ProofStrategy.ml
+++ b/src/plugins/wp/ProofStrategy.ml
@@ -345,11 +345,14 @@ let typecheck () =
(* --- Strategy Hints --- *)
(* -------------------------------------------------------------------------- *)
-let hints pid =
+let hints goal =
+ let pid = goal.Wpo.po_pid in
List.map (fun (name,_) -> Strategies.find name) @@
- List.filter (fun (_,ps) ->
- WpPropId.select_by_name ps pid
- ) (Hints.get ())
+ List.filter (fun (_,ps) -> WpPropId.select_by_name ps pid) @@ Hints.get ()
+
+let has_hint goal =
+ let pid = goal.Wpo.po_pid in
+ List.exists (fun (_,ps) -> WpPropId.select_by_name ps pid) @@ Hints.get ()
(* -------------------------------------------------------------------------- *)
(* --- Strategy Forward Step --- *)
@@ -478,7 +481,7 @@ let tactic tree node strategy = function
let sigma = bind Pattern.empty sequent t.lookup in
List.iter (configure tactic sigma) t.params ;
let selection = select sigma t.select in
- match tactic#select console selection with
+ match Lang.local ~pool (tactic#select console) selection with
| exception (Not_found | Exit) -> raise Not_found
| Not_applicable ->
raise Not_found
diff --git a/src/plugins/wp/ProofStrategy.mli b/src/plugins/wp/ProofStrategy.mli
index ecb0929fc9324a41a593b9262c6f400828292522..178dec978d2411bf1d9e4777f5b2f99130086dbb 100644
--- a/src/plugins/wp/ProofStrategy.mli
+++ b/src/plugins/wp/ProofStrategy.mli
@@ -33,7 +33,8 @@ val typecheck : unit -> unit
val name : strategy -> string
val find : string -> strategy option
-val hints : WpPropId.prop_id -> strategy list
+val hints : Wpo.t -> strategy list
+val has_hint : Wpo.t -> bool
val alternatives : strategy -> alternative list
val provers : alternative -> VCS.prover list * float
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index e146dc0edfb113d1094b7eddd70b2c182bee66d0..e3089d47e5c06eace2b9a075abbf1e3afb464be0 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -23,8 +23,7 @@
open Tactical
open ProofScript
-let dkey_pp_allgoals =
- Wp_parameters.register_category "script:allgoals"
+let dkey_pp_allgoals = Wp_parameters.register_category "script:allgoals"
(* -------------------------------------------------------------------------- *)
(* --- Alternatives Ordering --- *)
@@ -330,7 +329,7 @@ let rec sequence (f : 'a -> solver) = function
| [] -> unknown
| x::xs -> f x +>> sequence f xs
-let rec explore_strategie env p s : solver =
+let rec explore_strategy env p s : solver =
sequence
(explore_alternative env p s)
(ProofStrategy.alternatives s)
@@ -371,7 +370,7 @@ and explore_auto env process a node =
and explore_fallback env process a node =
match ProofStrategy.fallback a with
| None -> failed
- | Some s -> explore_strategie env process s node
+ | Some s -> explore_strategy env process s node
let explore_hint env process node =
if ProofEngine.depth node > env.Env.depth then failed
@@ -381,18 +380,18 @@ let explore_hint env process node =
| Some s ->
match ProofStrategy.find s with
| None -> failed
- | Some s -> explore_strategie env process s node
+ | Some s -> explore_strategy env process s node
let explore_further env process strategy node =
let marked =
match ProofEngine.get_hint node with
| None -> false
| Some s -> ProofStrategy.name strategy = s
- in if marked then failed else explore_strategie env process strategy node
+ in if marked then failed else explore_strategy env process strategy node
let explore_further_hints env process =
let wpo = ProofEngine.main env.Env.tree in
- sequence (explore_further env process) (ProofStrategy.hints wpo.po_pid)
+ sequence (explore_further env process) (ProofStrategy.hints wpo)
(* -------------------------------------------------------------------------- *)
(* --- Automated Solving --- *)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 2ba6ede5b061334619054cb439a92eba62004989..80b340b303602b92d8099dda09a27c4465bcdada 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -66,35 +66,50 @@ let do_print_index fmt = function
| Wpo.Axiomatic ax -> Wpo.pp_axiomatics fmt ax
| Wpo.Function(kf,bhv) -> Wpo.pp_function fmt kf bhv
+let rec do_print_parents fmt (node : ProofEngine.node) =
+ Option.iter (do_print_parents fmt) (ProofEngine.parent node) ;
+ Format.fprintf fmt " - %s@\n" (ProofEngine.title node)
+
+let do_print_current fmt tree =
+ match ProofEngine.current tree with
+ | `Main -> ()
+ | `Internal node | `Leaf(_,node) -> do_print_parents fmt node
+
let do_print_goal_status fmt (g : Wpo.t) =
if not (Wpo.is_valid g || Wpo.is_smoke_test g) then
begin
do_print_index fmt g.po_idx ;
if ProofSession.exists g then
- Format.printf "Script %a@\n" ProofSession.pp_file
+ Format.fprintf fmt "Script %a@\n" ProofSession.pp_file
(ProofSession.filename ~force:false g) ;
- match ProofEngine.get g with
- | `None | `Script ->
- Wpo.pp_goal fmt g
- | `Proof | `Saved ->
- let tree = ProofEngine.proof ~main:g in
- match ProofEngine.status tree with
- | `Unproved | `Invalid | `Proved | `Passed ->
+ begin
+ match ProofEngine.get g with
+ | `None | `Script ->
Wpo.pp_goal fmt g
- | `Pending n | `StillResist n ->
- for i = 0 to n-1 do
- Format.fprintf fmt "Subgoal %d/%d:@\n" (succ i) n ;
- ProofEngine.goto tree (`Leaf i) ;
- let g = ProofEngine.head tree in
+ | `Proof | `Saved ->
+ let tree = ProofEngine.proof ~main:g in
+ match ProofEngine.status tree with
+ | `Unproved | `Invalid | `Proved | `Passed ->
Wpo.pp_goal fmt g
- done
+ | `Pending n | `StillResist n ->
+ for i = 0 to n-1 do
+ Format.fprintf fmt "Subgoal %d/%d:@\n" (succ i) n ;
+ ProofEngine.goto tree (`Leaf i) ;
+ do_print_current fmt tree ;
+ let g = ProofEngine.head tree in
+ Wpo.pp_goal fmt g
+ done
+ end ;
+ Format.pp_print_newline fmt () ;
end
let do_wp_print_status () =
- Log.print_on_output
- (fun fmt ->
- Wpo.iter
- ~on_goal:(do_print_goal_status fmt) ())
+ begin
+ Log.print_on_output
+ (fun fmt ->
+ Wpo.iter
+ ~on_goal:(do_print_goal_status fmt) ()) ;
+ end
let do_wp_print () =
(* Printing *)
@@ -487,7 +502,9 @@ let spawn_wp_proofs ~script goals =
(fun goal ->
if script.tactical
&& not (Wpo.is_trivial goal)
- && (script.auto <> [] || ProofSession.exists goal)
+ && (script.auto <> [] ||
+ ProofSession.exists goal ||
+ ProofStrategy.has_hint goal)
then
ProverScript.spawn
~failed:false