From 0ff6402c618dbf1f3af4dec46acf0b0141e85dc8 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Mon, 16 Dec 2024 16:55:49 +0100 Subject: [PATCH] fix generated lean project --- src/bin/dune | 4 ++-- .../Sail/{sail.lean => Sail.lean} | 0 src/sail_lean_backend/pretty_print_lean.ml | 3 ++- src/sail_lean_backend/sail_plugin_lean.ml | 15 ++++++++------- test/lean/struct.expected.lean | 3 +-- 5 files changed, 13 insertions(+), 12 deletions(-) rename src/sail_lean_backend/Sail/{sail.lean => Sail.lean} (100%) diff --git a/src/bin/dune b/src/bin/dune index 1eed938e3..38c3f278c 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -242,6 +242,6 @@ (%{workspace_root}/src/gen_lib/sail2_values.lem as src/gen_lib/sail2_values.lem) - (%{workspace_root}/src/sail_lean_backend/Sail/sail.lean + (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean as - src/sail_lean_backend/Sail/sail.lean))) + src/sail_lean_backend/Sail/Sail.lean))) diff --git a/src/sail_lean_backend/Sail/sail.lean b/src/sail_lean_backend/Sail/Sail.lean similarity index 100% rename from src/sail_lean_backend/Sail/sail.lean rename to src/sail_lean_backend/Sail/Sail.lean diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index 5944f5b4f..bd49c7009 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -10,8 +10,10 @@ open PPrint open Pretty_print_common let implicit_parens x = enclose (string "{") (string "}") x + let doc_id_ctor (Id_aux (i, _)) = match i with Id i -> string i | Operator x -> string (Util.zencode_string ("op " ^ x)) + let doc_kid (Kid_aux (Var x, _)) = string ("k_" ^ String.sub x 1 (String.length x - 1)) (* TODO do a proper renaming and keep track of it *) @@ -298,6 +300,5 @@ let rec remove_imports (defs : (Libsail.Type_check.tannot, Libsail.Type_check.en let pp_ast_lean ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o = let defs = remove_imports defs 0 in let output : document = separate_map empty doc_def defs in - output_string o "import Sail.sail\n\n"; print o output; () diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml index 5d4d2f1e8..48e35b3ac 100644 --- a/src/sail_lean_backend/sail_plugin_lean.ml +++ b/src/sail_lean_backend/sail_plugin_lean.ml @@ -157,8 +157,8 @@ let create_lake_project (out_name : string) default_sail_dir = (* Change the base directory if the option '--lean-output-dir' is set *) let base_dir = match !opt_lean_output_dir with Some dir -> dir | None -> "." in let project_dir = Filename.concat base_dir out_name in - if !opt_lean_force_output && Sys.is_directory project_dir then ( - let _ = Unix.system ("rm -r " ^ Filename.quote project_dir ^ "/*") in + if !opt_lean_force_output && Sys.file_exists project_dir && Sys.is_directory project_dir then ( + let _ = Unix.system ("rm -r " ^ project_dir ^ "/*") in () ) else Unix.mkdir project_dir 0o775; @@ -174,15 +174,16 @@ let create_lake_project (out_name : string) default_sail_dir = let out_name_camel = Libsail.Util.to_upper_camel_case out_name in let lakefile = open_out (Filename.concat project_dir "lakefile.toml") in output_string lakefile - ("name = \"" ^ out_name ^ "\"\ndefaultTargets = [\"" ^ out_name_camel - ^ "\"]\n\n[[lean_lib]]\nname = \"Sail\"\n\n[[lean_lib]]\nname = \"" ^ out_name_camel ^ "\"" + ("name = \"" ^ out_name ^ "\"\ndefaultTargets = [\"" ^ out_name_camel ^ "\"]\n\n[[lean_lib]]\nname = \"" + ^ out_name_camel ^ "\"" ); close_out lakefile; + let lean_src_dir = Filename.concat project_dir out_name_camel in + if not (Sys.file_exists lean_src_dir) then Unix.mkdir lean_src_dir 0o775; let sail_dir = Reporting.get_sail_dir default_sail_dir in - let _ = - Unix.system ("cp -r " ^ Filename.quote (sail_dir ^ "/src/sail_lean_backend/Sail") ^ " " ^ Filename.quote project_dir) - in + let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/sail_lean_backend/Sail " ^ lean_src_dir) in let project_main = open_out (Filename.concat project_dir (out_name_camel ^ ".lean")) in + output_string project_main ("import " ^ out_name_camel ^ ".Sail.Sail\n\n"); project_main let output (out_name : string) ast default_sail_dir = diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean index 37529f301..38d801fcd 100644 --- a/test/lean/struct.expected.lean +++ b/test/lean/struct.expected.lean @@ -1,4 +1,4 @@ -import Sail.sail +import My_Project.Sail.sail structure My_struct where field1 : Int @@ -10,4 +10,3 @@ def undefined_My_struct (lit : Unit) : My_struct := def initialize_registers : Unit := () -