From c54017e6bd14be55afa599ed81ff66d50bd346c4 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Thu, 21 Mar 2024 18:26:59 +0100
Subject: [PATCH] [wp] Clarified vars and functions name
---
src/plugins/wp/Why3Import.ml | 40 ++++++++++++++++++------------------
1 file changed, 20 insertions(+), 20 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 9a4ed549cc6..3af3a7f66d5 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -48,15 +48,15 @@ let get_name_from_ident (ident) =
W.Ident.id_unique (ident_printer) ident
-let open_theory (env) (theories) =
+let open_theories_of_user (env) (theories) =
List.iter
- (fun (thy_n, thy_p) ->
+ (fun (theory_name, theory_path) ->
try
- let theory = (W.Env.read_theory env (thy_p) (thy_n)) in
+ let theory = (W.Env.read_theory env (theory_path) (theory_name)) in
List.iter ( fun (tdecl : T.tdecl) ->
match tdecl.td_node with
- | Decl d ->
- (match (d.d_node : W.Decl.decl_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 _ -> L.debug ~level:0 "Decl and ddata"
| Dparam _ -> L.debug ~level:0 "Decl and dparam"
@@ -68,28 +68,28 @@ let open_theory (env) (theories) =
) theory.th_decls;
with W.Env.LibraryNotFound paths ->
- L.debug ~level:0 "Library %s not found at %s " thy_n (String.concat "." paths);
+ L.debug ~level:0 "Library %s not found at %s " theory_name (String.concat "." paths);
) (extract_last_segments theories)
let () =
Boot.Main.extend
begin fun () ->
- let libs = L.Library.get () in
- List.iter
- (fun dir ->
- L.debug ~level:0 " + LIBS %s@." dir
- ) (F.to_string_list libs) ;
- let thys = L.Import.get () in
- List.iter
- (fun thy ->
- L.debug ~level:0 " + THY %s@." thy
- ) thys ;
+ 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 libs = L.Library.get () in
- let thys = L.Import.get () in
- let env = create_why3_env (F.to_string_list libs) in
- open_theory (env) (thys);
+ 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);
end
--
GitLab