From e141f8cf9993b4818f6fccf6f07473f6f1561d8d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 29 Nov 2021 14:14:01 +0100
Subject: [PATCH] [wp] new key to pretty print script subgoals
---
src/plugins/wp/ProverScript.ml | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index c7ae3564c95..46f3ae3cf80 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -23,6 +23,9 @@
open Tactical
open ProofScript
+let dkey_pp_allgoals =
+ Wp_parameters.register_category "script:allgoals"
+
(* -------------------------------------------------------------------------- *)
(* --- Alternatives Ordering --- *)
(* -------------------------------------------------------------------------- *)
@@ -389,12 +392,18 @@ let rec crawl env on_child node = function
(* --- Main Process --- *)
(* -------------------------------------------------------------------------- *)
+let pp_subgoal env fmt node =
+ let main = Env.goal env None in
+ let wpo = Env.goal env (Some node) in
+ Format.fprintf fmt "%s subgoal:@\n%a" (Wpo.get_gid main) Wpo.pp_goal_flow wpo
+
let schedule job =
Task.spawn (ProverTask.server ()) (Task.thread (Task.todo job))
let rec process env node =
schedule
begin fun () ->
+ Wp_parameters.debug ~dkey:dkey_pp_allgoals "%a" (pp_subgoal env) node ;
if ProofEngine.proved node then
( Env.validate env ; Task.return () )
else
@@ -407,6 +416,7 @@ let task
~depth ~width ~backtrack ~auto
~start ~progress ~result ~success wpo =
begin fun () ->
+ Wp_parameters.debug ~dkey:dkey_pp_allgoals "%a" Wpo.pp_goal_flow wpo ;
Prover.simplify ~start ~result wpo >>= fun succeed ->
if succeed
then
--
GitLab