[wp] Cleaned code, removed unused and/or verbose functions, removed unit from create_why3_env

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