Lean: fix indentation of match blocks (#966)

src/sail_lean_backend/pretty_print_lean.ml

@@ -409,7 +409,8 @@ 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) =

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) (← (undefined_int ())))
+    (pure (HAdd.hAdd z x))
+  | B => (pure 42)
+  | C => (pure 23)
+
 def initialize_registers (_ : Unit) : SailM Unit := do
   writeReg r_A (← (undefined_E ()))
   writeReg r_B (← (undefined_E ()))

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
+  }
 }