From c6bcd39f98881da468c49dc24834997b3944fd3f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 22 Mar 2024 15:38:22 +0100
Subject: [PATCH] [wp] refactoring code
---
src/plugins/wp/Why3Import.ml | 126 +++++++++++++----------------------
1 file changed, 46 insertions(+), 80 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 8dd6bc637b7..c9bddb69e30 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -28,91 +28,57 @@ module WConf = Why3.Whyconf
(* -------------------------------------------------------------------------- *)
-type _theory = string * string list
-
let create_why3_env loadpath =
- let main = WConf.get_main (WConf.read_config None) in
- let loadpathes = (WConf.loadpath (main))@loadpath in
- W.Env.create_env loadpathes
-
-let extract_last_segments (str_list : string list) =
- List.map (fun str ->
- let segments = String.split_on_char '.' str in
- match List.rev segments with
- | hd :: tl -> (hd, List.rev tl)
- | [] -> ("", [])
- ) str_list
-
-let get_name_from_ident (ident) =
- let ident_printer = W.Ident.create_ident_printer [] in
- W.Ident.id_unique (ident_printer) ident
-
-
-let open_theories_of_user (env) (theories) =
- List.iter
- (fun (theory_name, theory_path) ->
- try
- let theory = (W.Env.read_theory env (theory_path) (theory_name)) in
- List.iter ( fun (tdecl : T.tdecl) ->
- match tdecl.td_node with
- | Decl decl ->
- (match (decl.d_node : W.Decl.decl_node) with
- | Dtype dtype -> L.debug ~level:0 "Decl and type, named : %s.@" (get_name_from_ident dtype.ts_name);
- | Ddata ddatas ->
- List.iter (fun ((tysymbol, _) : W.Decl.data_decl) ->
- L.debug ~level:0 "Decl and dtata, named : %s.@" (get_name_from_ident tysymbol.ts_name);
- ) ddatas;
- | Dparam dparam -> L.debug ~level:0 "Decl and dparam, named : %s.@" (get_name_from_ident dparam.ls_name);
- | Dlogic dlogics ->
- List.iter (fun ((ls,_):W.Decl.logic_decl) ->
- L.debug ~level:0 "Decl and dlogic, named : %s.@" (get_name_from_ident ls.ls_name);
- ) dlogics;
- | _ -> L.debug ~level:0 "Decl but whatever")
- | Use _ -> L.debug ~level:0 "Use"
- | Clone _ -> L.debug ~level:0 "Clone"
- | Meta _ -> L.debug ~level:0 "Meta"
- ) theory.th_decls;
-
- with W.Env.LibraryNotFound paths ->
- L.debug ~level:0 "Library %s not found at %s " theory_name (String.concat "." paths);
- ) (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 main = WConf.get_main @@ WConf.read_config None in
+ W.Env.create_env @@ WConf.loadpath main @ F.to_string_list loadpath
+
+let extract_path thname =
+ let segments = String.split_on_char '.' thname in
+ match List.rev segments with
+ | hd :: tl -> hd, List.rev tl
+ | [] -> "", []
+
+(* For debug only*)
+let pp_id fmt (id: W.Ident.ident) =
+ Format.pp_print_string fmt id.id_string
+
+let import_theory env thname =
+ let theory_name, theory_path = extract_path thname in
+ try
+ let theory = W.Env.read_theory env 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 ~level:0 "Decl and type %a.@" pp_id ts.ts_name
+ | Ddata ddatas ->
+ List.iter
+ (fun ((ts, _) : W.Decl.data_decl) ->
+ L.debug ~level:0 "Decl and data %a.@" pp_id ts.ts_name
+ ) ddatas
+ | Dparam ls ->
+ L.debug ~level:0 "Decl and dparam %a.@" pp_id ls.ls_name
+ | Dlogic dlogics ->
+ List.iter
+ (fun ((ls,_):W.Decl.logic_decl) ->
+ L.debug ~level:0 "Decl and dlogic %a.@" pp_id ls.ls_name
+ ) dlogics
+ | _ -> L.debug ~level:0 "Decl but whatever"
+ end
+ | Use _ -> L.debug ~level:0 "Use"
+ | Clone _ -> L.debug ~level:0 "Clone"
+ | Meta _ -> L.debug ~level:0 "Meta"
+ ) theory.th_decls
+ with W.Env.LibraryNotFound _ ->
+ L.error "Library %s not found" thname
let () =
Boot.Main.extend
begin fun () ->
- let user_libraries = L.Library.get () in
- (* DEBUG ONLY *)
- List.iter (fun dir ->
- L.debug ~level:0 " + LIBS %s@." dir
- ) (F.to_string_list user_libraries) ;
- (* DEBUG ONLY *)
- let user_theories = L.Import.get () in
- List.iter (fun thy ->
- L.debug ~level:0 " + THY %s@." thy
- ) user_theories ;
-
- let user_libraries = L.Library.get () in
- let user_theories = L.Import.get () in
- let env = create_why3_env (F.to_string_list user_libraries) in
- open_theories_of_user (env) (user_theories);
-
-
+ let env = create_why3_env @@ L.Library.get () in
+ List.iter (import_theory env) @@ L.Import.get ()
end
(* -------------------------------------------------------------------------- *)
--
GitLab