From c2626cea6e8bd28cb08ba7973eef7dc48b3cd86a Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Fri, 17 May 2024 11:02:14 +0200
Subject: [PATCH] [wp] proof of concept of adding module linked logic_info to
global, to be refactored
---
src/plugins/wp/Why3Import.ml | 21 +++++++++++++++++----
1 file changed, 17 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index cfa181d07be..4388a3c8c0c 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -64,6 +64,9 @@ let construct_acsl_name (id : W.Ident.ident) =
String.concat "::" (paths @ name :: List.rev_append q [of_infix t])
| [] -> ""
+let recover_module (id : W.Ident.ident) =
+ let (paths,name,_) = T.restore_path id in
+ String.concat "." paths ^ "." ^ name
(* For debug only*)
let pp_id fmt (id: W.Ident.ident) =
@@ -98,6 +101,10 @@ let pp_lvs fmt (lvs : C.logic_var list) =
Cpp.pp_logic_var lv Cpp.pp_logic_type lv.lv_type
) lvs;
+ (* let pp_id_path (id : W.Ident.ident) =
+ Format.printf "@ %s " @@ construct_acsl_name id in
+ assert false *)
+
(* -------------------------------------------------------------------------- *)
(* --- Types --- *)
(* -------------------------------------------------------------------------- *)
@@ -106,7 +113,7 @@ let pp_lvs fmt (lvs : C.logic_var list) =
type tvars = C.logic_type W.Ty.Mtv.t
type why3module = {
- _paths : string list;
+ paths : string list;
_types : C.logic_type_info list;
_logics : C.logic_info list;
}
@@ -219,7 +226,10 @@ let li_of_ls (env:env) (ls : W.Term.lsymbol) : C.logic_info =
l_body = C.LBnone;
} in W.Term.Hls.add env.lenv ls li;
Logic_info.Hashtbl.add env.lils li ls;
-
+ L.debug ~level:0 "Module is : %s" @@ recover_module ls.ls_name;
+ let o = Datatype.String.Hashtbl.find env._menv @@ recover_module ls.ls_name in
+ Datatype.String.Hashtbl.replace env._menv (recover_module ls.ls_name)
+ {o with _logics = o._logics @ [li]};
li
@@ -231,7 +241,7 @@ let import_theory (env : env) thname =
let theory_name, theory_path = extract_path thname in
try
Datatype.String.Hashtbl.add env._menv thname
- { _logics = []; _types = []; _paths = theory_path};
+ { _logics = []; _types = []; paths = theory_path};
let theory = W.Env.read_theory env.wenv theory_path theory_name in
List.iter (fun (tdecl : T.tdecl) ->
match tdecl.td_node with
@@ -300,7 +310,10 @@ let () =
L.result "Associated parameters : @[<hov2>%a@]" pp_lvs li.l_profile;
) env.lenv;
Datatype.String.Hashtbl.iter (fun (s) (why3mod) ->
- L.result "Encoutered %s at %s" s (String.concat "::" why3mod._paths)
+ L.result "Encoutered %s at %s" s (String.concat "::" why3mod.paths);
+ List.iter (fun (li) ->
+ L.result "%a" pp_li li)
+ why3mod._logics;
) env._menv
end
--
GitLab