From ef2f1c595d645451552aadad88de7ee03b4213cf Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Thu, 21 Mar 2024 18:40:13 +0100
Subject: [PATCH] [wp] Printed the name of all the possible Decl patterns
---
src/plugins/wp/Why3Import.ml | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 3af3a7f66d5..265f9013f37 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -58,9 +58,15 @@ let open_theories_of_user (env) (theories) =
| Decl decl ->
(match (decl.d_node : W.Decl.decl_node) with
| Dtype dtype -> L.debug ~level:0 "Decl and type, named : %s.@" (get_name_from_ident dtype.ts_name);
- | Ddata _ -> L.debug ~level:0 "Decl and ddata"
- | Dparam _ -> L.debug ~level:0 "Decl and dparam"
- | Dlogic _ -> L.debug ~level:0 "Decl and dlogic"
+ | Ddata ddatas ->
+ List.iter (fun ((tysymbol, _) : W.Decl.data_decl) ->
+ L.debug ~level:0 "Decl and dtata, named : %s.@" (get_name_from_ident tysymbol.ts_name);
+ ) ddatas;
+ | Dparam dparam -> L.debug ~level:0 "Decl and dparam, named : %s.@" (get_name_from_ident dparam.ls_name);
+ | Dlogic dlogics ->
+ List.iter (fun ((ls,_):W.Decl.logic_decl) ->
+ L.debug ~level:0 "Decl and dlogic, named : %s.@" (get_name_from_ident ls.ls_name);
+ ) dlogics;
| _ -> L.debug ~level:0 "Decl but whatever")
| Use _ -> L.debug ~level:0 "Use"
| Clone _ -> L.debug ~level:0 "Clone"
--
GitLab