From 9c3b251ee9ac686fe0a9606da1d5dbc467d554c5 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Mon, 18 Mar 2024 18:21:18 +0100
Subject: [PATCH] [wp] Working theory reading for one theory, no folder depth
---
src/plugins/wp/Why3Import.ml | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 0ffa6f99ac4..4fbebc17147 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -98,11 +98,11 @@ let () =
L.debug ~level:0 " Loadpath %s@." lpath
) loadpath ;
List.iter
- (fun _thy ->
+ (fun (thy_n, thy_p) ->
try
- (* let _ns = (W.Env.read_theory env (F.to_string_list libs) _thy) in
- W.Pretty.print_theory Format.std_formatter _ns; *)
- L.debug ~level:0 "INTHY %s" _thy;
+ let _ns = (W.Env.read_theory env ([String.concat "." thy_p]) (thy_n)) in
+ W.Pretty.print_theory Format.std_formatter _ns;
+ L.debug ~level:0 "INTHY %s" thy_n;
with W.Env.LibraryNotFound paths ->
List.iter (
@@ -114,7 +114,7 @@ let () =
(* let _t = (W.Wstdlib.Mstr.values (_ns.ns_ts)) in
L.debug "Nombres de itys trucs : %d" (List.length _t); *)
- ) (extract_theory_name thys) ;
+ ) (extract_last_segments thys) ;
(* let env = create_why3_env () in
let _ns = (W.Env.read_theory env ["summodule"] "Sum") in
L.debug ""; *)
--
GitLab