Lean style update

rems-project · Jan 16, 2025 · 523c16e · 523c16e
1 parent ab6fefd
commit 523c16e
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 4 deletions.
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -285,11 +285,11 @@ let rec doc_exp ctxt (E_aux (e, (l, annot)) as full_exp) =
       nest 2 (flow (break 1) [string "let"; string id; coloneq; doc_exp ctxt lexp]) ^^ hardline ^^ doc_exp ctxt e
   | E_struct fexps ->
       let args = List.map (doc_fexp ctxt) fexps in
-      braces (separate (comma ^^ space) args)
+      braces (space ^^ nest 2 (separate hardline args) ^^ space)
   | E_field (exp, id) -> doc_exp ctxt exp ^^ dot ^^ doc_id_ctor id
   | E_struct_update (exp, fexps) ->
       let args = List.map (doc_fexp ctxt) fexps in
-      braces (doc_exp ctxt exp ^^ string " with " ^^ separate comma args)
+      braces (space ^^ doc_exp ctxt exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space)
   | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.")
 
 and doc_fexp ctxt (FE_aux (FE_fexp (field, exp), _)) = doc_id_ctor field ^^ string " := " ^^ doc_exp ctxt exp

diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
@@ -13,11 +13,16 @@ def struct_field2 (s : My_struct) : (BitVec 1) :=
   s.field2
 
 def struct_update_field2 (s : My_struct) (b : (BitVec 1)) : My_struct :=
-  {s with field2 := b}
+  { s with field2 := b }
+
+/-- Type quantifiers: i : Int -/
+def struct_update_both_fields (s : My_struct) (i : Int) (b : (BitVec 1)) : My_struct :=
+  { s with field1 := i, field2 := b }
 
 /-- Type quantifiers: i : Int -/
 def mk_struct (i : Int) (b : (BitVec 1)) : My_struct :=
-  {field1 := i, field2 := b}
+  { field1 := i
+    field2 := b }
 
 def initialize_registers : Unit :=
   ()

diff --git a/test/lean/struct.sail b/test/lean/struct.sail
@@ -17,6 +17,11 @@ function struct_update_field2(s, b) = {
   { s with field2 = b }
 }
 
+val struct_update_both_fields : (My_struct, int, bit) -> My_struct
+function struct_update_both_fields(s, i, b) = {
+  { s with field1 = i, field2 = b }
+}
+
 val mk_struct : (int, bit) -> My_struct
 function mk_struct(i, b) = {
   struct {