From 3c0b34dede2c5c9014146f6b72049b14dc4463c9 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Thu, 21 Mar 2024 12:21:20 +0100
Subject: [PATCH] [wp] Cache pattern for theory retrieval, to be corrected
---
src/plugins/wp/Why3Import.ml | 17 +++++++++++++++--
1 file changed, 15 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 4fbebc17147..129d596bb0f 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -59,6 +59,17 @@ let extract_theory_path struc_theories =
let ty = tys.tysymbol in
tymap <- Mty.add tys.tysymbol tymap; *)
+let get_name_from_ident (ident) =
+ let ident_printer = W.Ident.create_ident_printer [] in
+ W.Ident.id_unique (ident_printer) ident
+
+let get_theory_from_user (env) (path) (name) (map) =
+ let theory = W.Env.read_theory env ([String.concat "." path]) name in
+ let theory_uid = (get_name_from_ident(theory.th_name)) in
+ try W.Wstdlib.Mstr.find theory_uid map in map
+with Not_found ->
+ W.Wstdlib.Mstr.add (theory_uid) (theory) map
+
let () =
Boot.Main.extend
@@ -91,6 +102,7 @@ let () =
let libs = L.Library.get () in
let thys = L.Import.get () in
+ let theories_map : W.Theory.theory W.Wstdlib.Mstr.t = W.Wstdlib.Mstr.empty in
let env = create_why3_env (F.to_string_list libs) () in
let loadpath = W.Env.get_loadpath env in
List.iter
@@ -100,8 +112,9 @@ let () =
List.iter
(fun (thy_n, thy_p) ->
try
- let _ns = (W.Env.read_theory env ([String.concat "." thy_p]) (thy_n)) in
- W.Pretty.print_theory Format.std_formatter _ns;
+ let theory = (W.Env.read_theory env ([String.concat "." thy_p]) (thy_n)) in
+ in
+ W.Pretty.print_theory Format.std_formatter theory;
L.debug ~level:0 "INTHY %s" thy_n;
with W.Env.LibraryNotFound paths ->
--
GitLab