From b3d3655010b610a234f4eb67b6cfece21e845bb9 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Mon, 10 Feb 2025 16:03:12 +0000
Subject: [PATCH] fix indentation of match blocks

---
 src/sail_lean_backend/pretty_print_lean.ml |  2 +-
 test/lean/match.expected.lean              | 10 ++++++++++
 test/lean/match.sail                       | 11 +++++++++++
 3 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index 08d809f4f..ab31b6028 100644
--- a/src/sail_lean_backend/pretty_print_lean.ml
+++ b/src/sail_lean_backend/pretty_print_lean.ml
@@ -408,7 +408,7 @@ let get_fn_implicits (Typ_aux (t, _)) : bool list =
 
 let rec doc_match_clause (as_monadic : bool) ctx (Pat_aux (cl, l)) =
   match cl with
-  | Pat_exp (pat, branch) -> string "| " ^^ doc_pat pat ^^ string " =>" ^^ space ^^ doc_exp as_monadic ctx branch
+  | Pat_exp (pat, branch) -> group (nest 2 (string "| " ^^ doc_pat pat ^^ string " =>" ^^ break 1 ^^ doc_exp as_monadic ctx branch))
   | Pat_when (pat, when_, branch) -> failwith "The Lean backend does not support 'when' clauses in patterns"
 
 and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean
index fc20a4738..d9a5fca51 100644
--- a/test/lean/match.expected.lean
+++ b/test/lean/match.expected.lean
@@ -55,6 +55,16 @@ def match_reg (x : E) : SailM E := do
   | B => readReg r_B
   | C => readReg r_C
 
+/-- Type quantifiers: y : Int -/
+def match_let (x : E) (y : Int) : SailM Int := do
+  match x with
+  | A =>
+    let x := (HAdd.hAdd y y)
+    let z := (HAdd.hAdd (HAdd.hAdd y y) (← sorry))
+    (pure (HAdd.hAdd z x))
+  | B => (pure 42)
+  | C => (pure 23)
+
 def initialize_registers (lit : Unit) : SailM Unit := do
   writeReg r_A (← (undefined_E ()))
   writeReg r_B (← (undefined_E ()))
diff --git a/test/lean/match.sail b/test/lean/match.sail
index 5ead248a2..11ff1ec5d 100644
--- a/test/lean/match.sail
+++ b/test/lean/match.sail
@@ -42,4 +42,15 @@ function match_reg(x : E) -> E = {
     B => r_B,
     C => r_C,
   }
+}
+
+function match_let (x : E, y : int) -> int = {
+  match x {
+    A => 
+    let x = y + y in
+    let z = y + y + undefined_int() in
+    z + x,
+    B => 42,
+    C => 23
+  }
 }
\ No newline at end of file