Lean: fix generated lean projects (#829)

rems-project · Dec 17, 2024 · 52d292a · 52d292a
1 parent 725cbde
commit 52d292a
Show file tree

Hide file tree

Showing 13 changed files with 21 additions and 16 deletions.
diff --git 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 → src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/sail.lean → 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
@@ -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
@@ -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 " ^ Filename.quote project_dir ^ "/*") in
     ()
   )
@@ -174,15 +174,19 @@ 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)
+    Unix.system
+      ("cp -r " ^ Filename.quote (sail_dir ^ "/src/sail_lean_backend/Sail") ^ " " ^ Filename.quote 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/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
@@ -1,4 +1,4 @@
-import Sail.sail
+import Out.Sail.Sail
 
 def bitvector_eq (x : BitVec 16) (y : BitVec 16) : Bool :=
   (Eq x y)

diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
@@ -1,4 +1,4 @@
-import Sail.sail
+import Out.Sail.Sail
 
 inductive E where | A | B | C
   deriving Inhabited

diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
@@ -1,4 +1,4 @@
-import Sail.sail
+import Out.Sail.Sail
 
 def extern_add : Int :=
   (Int.add 5 4)

diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean
@@ -1,4 +1,4 @@
-import Sail.sail
+import Out.Sail.Sail
 
 def extern_const : BitVec 64 :=
   (0xFFFF000012340000 : BitVec 64)

diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean
@@ -1,4 +1,4 @@
-import Sail.sail
+import Out.Sail.Sail
 
 def foo : BitVec 16 :=
   let z := (HOr.hOr (0xFFFF : BitVec 16) (0xABCD : BitVec 16))

diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
@@ -1,4 +1,4 @@
-import Sail.sail
+import Out.Sail.Sail
 
 structure My_struct where
   field1 : Int

diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean
@@ -1,4 +1,4 @@
-import Sail.sail
+import Out.Sail.Sail
 
 def foo (y : Unit) : Unit :=
   y

diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean
@@ -1,4 +1,4 @@
-import Sail.sail
+import Out.Sail.Sail
 
 def tuple1 : (Int × Int × (BitVec 2 × Unit)) :=
   (3, 5, ((0b10 : BitVec 2), ()))

diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
@@ -1,4 +1,4 @@
-import Sail.sail
+import Out.Sail.Sail
 
 def foo (n : Int) : BitVec 4 :=
   (0xF : BitVec 4)