From 94c954051cdb91c48da776b1bd0a0c97d32eff1b Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Fri, 13 Dec 2024 12:30:41 +0100 Subject: [PATCH] fix generated lean project --- src/bin/dune | 4 ++-- src/sail_lean_backend/Sail/{sail.lean => Sail.lean} | 0 src/sail_lean_backend/pretty_print_lean.ml | 9 ++++----- src/sail_lean_backend/sail_plugin_lean.ml | 11 +++++++---- test/lean/struct.expected.lean | 3 +-- 5 files changed, 14 insertions(+), 13 deletions(-) rename src/sail_lean_backend/Sail/{sail.lean => Sail.lean} (100%) diff --git a/src/bin/dune b/src/bin/dune index d30ef9052..01f943c48 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -241,6 +241,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 2c19acb7f..05af01dae 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -260,17 +260,17 @@ let doc_typdef (TD_aux (td, tannot) as full_typdef) = let derivers = if List.length fields > 0 then [string "Inhabited"] else [] in let fields = List.map doc_id_ctor fields in let fields = List.map (fun i -> space ^^ pipe ^^ space ^^ i) fields in - let enums_doc = concat fields in + let fields_doc = concat fields in nest 2 (flow (break 1) [string "inductive"; string id; string "where"] - ^^ enums_doc ^^ hardline ^^ string "deriving" ^^ space + ^^ fields_doc ^^ hardline ^^ string "deriving" ^^ space ^^ separate (comma ^^ space) derivers ) | TD_record (Id_aux (Id id, _), TypQ_aux (tq, _), fields, _) -> let fields = List.map doc_typ_id fields in - let enums_doc = concat fields in + let fields_doc = concat fields in let rectyp = doc_typ_quant tq in - nest 2 (flow (break 1) [string "structure"; string id; rectyp; string "where"] ^^ hardline ^^ enums_doc) + nest 2 (flow (break 1) [string "structure"; string id; string "where"] ^^ hardline ^^ fields_doc) | _ -> failwith ("Type definition " ^ string_of_type_def_con full_typdef ^ " not translatable yet.") let doc_def (DEF_aux (aux, def_annot) as def) = @@ -290,6 +290,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 007b999f5..48e35b3ac 100644 --- a/src/sail_lean_backend/sail_plugin_lean.ml +++ b/src/sail_lean_backend/sail_plugin_lean.ml @@ -157,7 +157,7 @@ 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 ( + if !opt_lean_force_output && Sys.file_exists project_dir && Sys.is_directory project_dir then ( let _ = Unix.system ("rm -r " ^ project_dir ^ "/*") in () ) @@ -174,13 +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 " ^ sail_dir ^ "/src/sail_lean_backend/Sail " ^ 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 ce4046905..6b54fe561 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 := () -