From 885b044b575133f5eae7af4cdf2cbd60747d45e5 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Fri, 22 Mar 2024 14:59:24 +0100
Subject: [PATCH] [wp] PoC for opening module, TBD
---
src/plugins/wp/Why3Import.ml | 15 +++++++++++++++
1 file changed, 15 insertions(+)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 265f9013f37..8dd6bc637b7 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -78,6 +78,21 @@ let open_theories_of_user (env) (theories) =
) (extract_last_segments theories)
+let open_modules_of_user (env) (modules) =
+ List.iter
+ (fun (theory_name, theory_path) ->
+ try
+ let pmodule = (W.Pmodule.read_module env (theory_path) (theory_name)) in
+ List.iter ( fun (modunit : W.Pmodule.mod_unit) ->
+ L.debug ~level:0 "Meta";
+ ) pmodule.mod_units;
+
+ with W.Env.LibraryNotFound paths ->
+ L.debug ~level:0 "Library %s not found at %s " theory_name (String.concat "." paths);
+ ) (extract_last_segments modules)
+
+
+
let () =
Boot.Main.extend
begin fun () ->
--
GitLab