From 0c5212a80204da01c36f10623d0f9c1f8d26de61 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Wed, 13 Mar 2024 14:58:12 +0100
Subject: [PATCH] [wp] PoC for opening module from command lines arguments
---
src/plugins/wp/Why3Import.ml | 32 ++++++++++++++++++++++++++++++--
1 file changed, 30 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index dc44b223a86..570067c07b1 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -21,22 +21,50 @@
(**************************************************************************)
module L = Wp_parameters
+module P = Why3.Pmodule
+module F = Filepath.Normalized
+module W = Why3
+module WConf = Why3.Whyconf
(* -------------------------------------------------------------------------- *)
+let create_why3_env =
+ begin fun () ->
+ W.Env.create_env (WConf.loadpath (WConf.get_main (WConf.read_config None)))
+ end
+
let () =
Boot.Main.extend
begin fun () ->
let libs = L.Library.get () in
List.iter
(fun dir ->
- L.debug ~level:0 " + LIB %a@." Filepath.Normalized.pretty dir
- ) libs ;
+ L.debug ~level:0 " + LIBS %s@." dir
+ ) (F.to_string_list libs) ;
let thys = L.Import.get () in
List.iter
(fun thy ->
L.debug ~level:0 " + THY %s@." thy
) thys ;
+
+ let libs = L.Library.get () in
+ let thys = L.Import.get () in
+ let env = create_why3_env () in
+ List.iter
+ (fun thy ->
+ let ns = (P.read_module env (F.to_string_list libs) thy).mod_export in
+ let _t = List.map (fun (ity : W.Ity.itysymbol) -> ity.its_ts) (W.Wstdlib.Mstr.values (ns.ns_ts)) in
+ List.iter (
+ fun _ty ->
+ match W.Ty.ts_hash _ty with
+ | 1 -> L.debug "NoDef %s@." thy
+ | _ -> L.debug "Otr %s@." thy
+ ) _t;
+ ) thys ;
+ (* let _ns = (P.read_module env (F.to_string_list libs) (List.hd thys)).mod_export in
+ L.debug ""; *)
+
+
end
(* -------------------------------------------------------------------------- *)
--
GitLab