From cb1df8c004954a6682abbfd41186a2cce9291c37 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Thu, 21 Mar 2024 15:30:48 +0100
Subject: [PATCH] [wp] Cleaned code, removed unused and/or verbose functions,
removed unit from create_why3_env
---
src/plugins/wp/Why3Import.ml | 107 +++++++++--------------------------
1 file changed, 27 insertions(+), 80 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 129d596bb0f..c0fe6fa3216 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -32,43 +32,32 @@ module WConf = Why3.Whyconf
type _theory = string * string list
let create_why3_env loadpath =
- begin fun () ->
- let main = WConf.get_main (WConf.read_config None) in
- let loadpathes = (WConf.loadpath (main))@loadpath in
- W.Env.create_env loadpathes
- end
-let extract_last_segment (str : string) =
- let segments = String.split_on_char '.' str in
- match List.rev segments with
- | hd :: tl -> (hd, List.rev tl)
- | [] -> ("", [])
+ 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 extract_last_segment str_list
-let extract_theory_name struc_theories =
- let t = extract_last_segments struc_theories in
- List.map (fun (theory_name, _) -> theory_name) t
-
-let extract_theory_path struc_theories =
- let t = extract_last_segments struc_theories in
- List.map (fun (_, theory_path) -> theory_path) t
-
-(* let rec get_ty_symbols_from_ty (tys : W.Ty.tysymbol) (tymap) =
- try W.Wstdlib.Mstr.find tymap tys
- with Not_found ->
- let ty = tys.tysymbol in
- tymap <- Mty.add tys.tysymbol tymap; *)
-
-let get_name_from_ident (ident) =
- let ident_printer = W.Ident.create_ident_printer [] in
- W.Ident.id_unique (ident_printer) ident
-
-let get_theory_from_user (env) (path) (name) (map) =
- let theory = W.Env.read_theory env ([String.concat "." path]) name in
- let theory_uid = (get_name_from_ident(theory.th_name)) in
- try W.Wstdlib.Mstr.find theory_uid map in map
-with Not_found ->
- W.Wstdlib.Mstr.add (theory_uid) (theory) map
+ 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 open_theory (env) (theories) =
+ List.iter
+ (fun (thy_n, thy_p) ->
+ try
+ let theory = (W.Env.read_theory env (thy_p) (thy_n)) in
+ W.Pretty.print_theory Format.std_formatter theory;
+ L.debug ~level:0 "INTHY %s" thy_n;
+
+ with W.Env.LibraryNotFound paths ->
+ List.iter (
+ fun path ->
+ L.debug ~level:0 "Library not found at %s " path;
+ ) paths;
+ ) (extract_last_segments theories)
let () =
@@ -77,7 +66,7 @@ let () =
let libs = L.Library.get () in
List.iter
(fun dir ->
- L.debug ~level:0 " + LIBS %s@." dir
+ L.debug ~level:0 " + LIBS %s@." dir
) (F.to_string_list libs) ;
let thys = L.Import.get () in
List.iter
@@ -85,52 +74,10 @@ let () =
L.debug ~level:0 " + THY %s@." thy
) thys ;
- List.iter
- (fun thy ->
- L.debug ~level:0 " + Extracted theory name %s@." thy
- ) (extract_theory_name thys) ;
-
- List.iter
- (fun thy ->
- List.iter
- (fun p ->
- L.debug ~level:0 " + Extracted theory path %s@." p
- ) (thy);
- ) (extract_theory_path thys) ;
-
-
-
let libs = L.Library.get () in
let thys = L.Import.get () in
- let theories_map : W.Theory.theory W.Wstdlib.Mstr.t = W.Wstdlib.Mstr.empty in
- let env = create_why3_env (F.to_string_list libs) () in
- let loadpath = W.Env.get_loadpath env in
- List.iter
- (fun lpath ->
- L.debug ~level:0 " Loadpath %s@." lpath
- ) loadpath ;
- List.iter
- (fun (thy_n, thy_p) ->
- try
- let theory = (W.Env.read_theory env ([String.concat "." thy_p]) (thy_n)) in
- in
- W.Pretty.print_theory Format.std_formatter theory;
- L.debug ~level:0 "INTHY %s" thy_n;
-
- with W.Env.LibraryNotFound paths ->
- List.iter (
- fun path ->
- L.debug ~level:0 "Library not found at %s " path;
- ) paths;
-
- (* let _ns = (W.Env.read_theory env (F.to_string_list libs) thy).th_export in *)
-
- (* let _t = (W.Wstdlib.Mstr.values (_ns.ns_ts)) in
- L.debug "Nombres de itys trucs : %d" (List.length _t); *)
- ) (extract_last_segments thys) ;
- (* let env = create_why3_env () in
- let _ns = (W.Env.read_theory env ["summodule"] "Sum") in
- L.debug ""; *)
+ let env = create_why3_env (F.to_string_list libs) in
+ open_theory (env) (thys);
end
--
GitLab