From 523c16efe332245691cf3669e93960ecf6198533 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9on=20Frenot?= <leon.frenot@ens-lyon.fr>
Date: Thu, 16 Jan 2025 15:35:00 +0000
Subject: [PATCH] Lean style update

---
 src/sail_lean_backend/pretty_print_lean.ml | 4 ++--
 test/lean/struct.expected.lean             | 9 +++++++--
 test/lean/struct.sail                      | 5 +++++
 3 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index d3c449b58..624ba7fab 100644
--- 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
index 7b1cc29e5..60424c7cc 100644
--- 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
index 4d249a4ee..9853b7d11 100644
--- 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 {