From 0826a0d7db8b698abacd8c59f1efc73ee5536a79 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Fri, 5 Jul 2024 17:56:41 +0200
Subject: [PATCH] [wp] Importing logic_info and logic_type_info from parsed
@import clauses
---
src/plugins/wp/Why3Import.ml | 116 +++++++++++++++++++----------------
1 file changed, 64 insertions(+), 52 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 16a3a2ab2da..c644d56a0a8 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -69,11 +69,11 @@ let pp_id fmt (id: W.Ident.ident) =
Format.pp_print_string fmt id.id_string
(* For debug only*)
-let pp_tys fmt (tys: W.Ty.tysymbol) =
+let _pp_tys fmt (tys: W.Ty.tysymbol) =
W.Pretty.print_ty_decl fmt tys
(* For debug only*)
-let pp_ls fmt ls =
+let _pp_ls fmt ls =
W.Pretty.print_ls fmt ls
(* For debug only*)
@@ -91,7 +91,7 @@ let pp_li fmt (li : C.logic_info) =
Cpp.pp_logic_info fmt li
(* For debug only*)
-let pp_lvs fmt (lvs : C.logic_var list) =
+let _pp_lvs fmt (lvs : C.logic_var list) =
List.iter (fun (lv: C.logic_var) ->
Format.fprintf fmt "@ %a: %a"
Cpp.pp_logic_var lv Cpp.pp_logic_type lv.lv_type
@@ -180,7 +180,7 @@ let convert_location (wloc : Why3.Loc.position option) : C.location =
(* For debug use only *)
-let pp_cil_loc fmt (id : W.Ident.ident) =
+let _pp_cil_loc fmt (id : W.Ident.ident) =
Cpp.pp_location fmt @@ convert_location id.id_loc
@@ -267,45 +267,50 @@ let li_of_ls (env:env) (menv : menv) (ls : W.Term.lsymbol) : C.logic_info =
let import_theory (env : env) thname =
let theory_name, theory_path = extract_path thname in
try
- let menv : menv = {li = []; lti = []} in
- let theory = W.Env.read_theory env.wenv theory_path theory_name in
- List.iter (fun (tdecl : T.tdecl) ->
- match tdecl.td_node with
- | Decl decl ->
- begin
- match decl.d_node with
- | Dtype ts ->
- L.debug ~dkey "Decl and type %a" pp_id ts.ts_name;
- L.debug ~dkey "Location %a" pp_id_loc ts.ts_name;
- let lti = lti_of_ts env menv ts in
- L.debug ~dkey "Correspondign LTI %a" pp_lti lti;
- | Ddata ddatas ->
- List.iter
- (fun ((ts, _) : W.Decl.data_decl) ->
- L.debug ~dkey "Decl and data %a" pp_id ts.ts_name;
- L.debug ~dkey "Location %a" pp_id_loc ts.ts_name;
- let lti = lti_of_ts env menv ts in
- L.debug ~dkey "Correspondign data LTI %a" pp_lti lti;
- ) ddatas
- | Dparam ls ->
- L.debug ~dkey "Decl and dparam %a" pp_id ls.ls_name;
- L.debug ~dkey "Location %a" pp_id_loc ls.ls_name
- | Dlogic dlogics ->
- List.iter
- (fun ((ls,_):W.Decl.logic_decl) ->
- L.debug ~dkey "Decl and dlogic %a" pp_id ls.ls_name;
- L.debug ~dkey "Location %a" pp_id_loc ls.ls_name;
- let li = li_of_ls env menv ls in
- L.debug ~dkey "Corresponding dlogic LTI %a" pp_li li;
- ) dlogics
- | _ -> L.debug ~dkey "Other type of Decl"
- end
- | Use _| Clone _| Meta _ -> L.debug ~dkey ""
- ) theory.th_decls;
- Datatype.String.Hashtbl.add env.menv thname
- { logics = List.rev menv.li;
- types = List.rev menv.lti;
- paths = theory_path };
+ if not (Datatype.String.Hashtbl.mem env.menv thname) then
+ begin
+ let menv : menv = {li = []; lti = []} in
+ let theory = W.Env.read_theory env.wenv theory_path theory_name in
+ List.iter (fun (tdecl : T.tdecl) ->
+ match tdecl.td_node with
+ | Decl decl ->
+ begin
+ match decl.d_node with
+ | Dtype ts ->
+ L.debug ~dkey "Decl and type %a" pp_id ts.ts_name;
+ L.debug ~dkey "Location %a" pp_id_loc ts.ts_name;
+ let lti = lti_of_ts env menv ts in
+ L.debug ~dkey "Correspondign LTI %a" pp_lti lti;
+ | Ddata ddatas ->
+ List.iter
+ (fun ((ts, _) : W.Decl.data_decl) ->
+ L.debug ~dkey "Decl and data %a" pp_id ts.ts_name;
+ L.debug ~dkey "Location %a" pp_id_loc ts.ts_name;
+ let lti = lti_of_ts env menv ts in
+ L.debug ~dkey "Correspondign data LTI %a" pp_lti lti;
+ ) ddatas
+ | Dparam ls ->
+ L.debug ~dkey "Decl and dparam %a" pp_id ls.ls_name;
+ L.debug ~dkey "Location %a" pp_id_loc ls.ls_name
+ | Dlogic dlogics ->
+ List.iter
+ (fun ((ls,_):W.Decl.logic_decl) ->
+ L.debug ~dkey "Decl and dlogic %a" pp_id ls.ls_name;
+ L.debug ~dkey "Location %a" pp_id_loc ls.ls_name;
+ let li = li_of_ls env menv ls in
+ L.debug ~dkey "Corresponding dlogic LTI %a" pp_li li;
+ ) dlogics
+ | _ -> L.debug ~dkey "Other type of Decl"
+ end
+ | Use _| Clone _| Meta _ -> L.debug ~dkey ""
+ ) theory.th_decls;
+ Datatype.String.Hashtbl.add env.menv thname
+ { logics = List.rev menv.li;
+ types = List.rev menv.lti;
+ paths = theory_path };
+ end
+ else
+ L.error "Trying to register %s a second time, ignoring" thname;
with W.Env.LibraryNotFound _ ->
L.error "Library %s not found" thname
@@ -324,21 +329,28 @@ module Env = WpContext.StaticGenerator
add_builtins env ; env
end)
-let loader (ctxt: Logic_typing.module_builder) (loc: C.location) (m: string list) =
+let loader (ctxt: Logic_typing.module_builder) (_: C.location) (m: string list) =
begin
(* Use Env.get () to obtain the global env of the current project *)
(* Use import_theory if the module is not in the hashtbl *)
(* Register logics in ctxt for the imported (or cached) module *)
- L.result "[test-import:%d] Loading %s.@." (fst loc).pos_lnum (String.concat "::" m) ;
- let t = Cil_const.make_logic_type "t" in
- let check = Cil_const.make_logic_info "check" in
- let x = Cil_const.make_logic_var_formal "x" (Ltype(t,[])) in
- let k = Cil_const.make_logic_var_formal "k" Linteger in
- check.l_profile <- [x;k] ;
- ctxt.add_logic_type loc t ;
- ctxt.add_logic_function loc check ;
+
+ L.result "Importing Why3 theory %s.@." (String.concat "::" m) ;
+ let thname = String.concat "." m in
+ import_theory (Env.get ()) thname;
+ let env = Env.get () in
+ let current_module = Datatype.String.Hashtbl.find env.menv thname in
+ List.iter (fun (lti,loc) ->
+ ctxt.add_logic_type loc lti;
+ ) current_module.types;
+ List.iter (fun (li, loc) ->
+ ctxt.add_logic_function loc li;
+ ) current_module.logics;
+ L.result "Successfully imported theory at %s"
+ @@ String.concat "::" current_module.paths;
+
end
let () =
--
GitLab