From d5134d0f00bc5ef58443dafa1b993dd31813dc5e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 21 Dec 2023 06:53:25 +0100
Subject: [PATCH] [wp] debug key
---
src/plugins/wp/ProofStrategy.ml | 12 ++++++++++--
1 file changed, 10 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/ProofStrategy.ml b/src/plugins/wp/ProofStrategy.ml
index 35482547db2..73b4be3ac2b 100644
--- a/src/plugins/wp/ProofStrategy.ml
+++ b/src/plugins/wp/ProofStrategy.ml
@@ -469,6 +469,8 @@ let auto = function
(* --- Strategy Tactical Step --- *)
(* -------------------------------------------------------------------------- *)
+let dkey_tactical = Wp_parameters.register_category "tactical"
+
let tactical a =
match resolve_tactic a with None -> raise Not_found | Some t -> t
@@ -483,8 +485,14 @@ let rec bind sigma sequent = function
| [] -> sigma
| lookup::binders ->
match Pattern.psequent lookup sigma sequent with
- | None -> raise Not_found
- | Some sigma -> bind sigma sequent binders
+ | None ->
+ Wp_parameters.debug ~dkey:dkey_tactical "[failed] %a@."
+ pp_lookup lookup ;
+ raise Not_found
+ | Some sigma ->
+ Wp_parameters.debug ~dkey:dkey_tactical "[found] %a@."
+ pp_lookup lookup ;
+ bind sigma sequent binders
let select sigma ?goal = function
| [] ->
--
GitLab