From f17fb4b6853b8d2d3a6ea057bd3dbe7797e845e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9on=20Frenot?= <leon.frenot@ens-lyon.fr>
Date: Tue, 11 Feb 2025 15:24:39 +0000
Subject: [PATCH] Lean: fix lets that use tuples

---
 src/sail_lean_backend/pretty_print_lean.ml |  8 +-------
 test/lean/extern.expected.lean             |  2 +-
 test/lean/let.expected.lean                |  2 +-
 test/lean/tuples.expected.lean             | 10 ++++++++++
 test/lean/tuples.sail                      |  2 ++
 5 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index 62662e3cc..4491de58d 100644
--- a/src/sail_lean_backend/pretty_print_lean.ml
+++ b/src/sail_lean_backend/pretty_print_lean.ml
@@ -469,13 +469,7 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
       else wrap_with_pure as_monadic (parens (separate space [doc_exp false ctx e; colon; doc_typ ctx typ]))
   | E_tuple es -> wrap_with_pure as_monadic (parens (separate_map (comma ^^ space) d_of_arg es))
   | E_let (LB_aux (LB_val (lpat, lexp), _), e) ->
-      let id_typ =
-        match pat_is_plain_binder env lpat with
-        | Some (Some (Id_aux (Id id, _)), Some typ) -> string (fix_id id) ^^ space ^^ colon ^^ space ^^ doc_typ ctx typ
-        | Some (Some (Id_aux (Id id, _)), None) -> string (fix_id id)
-        | Some (None, _) -> string "x" (* TODO fresh name or wildcard instead of x *)
-        | _ -> failwith "Let pattern not translatable yet."
-      in
+      let id_typ = doc_pat lpat in
       let decl_val =
         if effectful (effect_of lexp) then [string "←"; string "do"; doc_exp true ctx lexp]
         else [coloneq; doc_exp false ctx lexp]
diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
index aa71da6b1..56ef0fc95 100644
--- a/test/lean/extern.expected.lean
+++ b/test/lean/extern.expected.lean
@@ -35,7 +35,7 @@ def extern_min (_ : Unit) : Int :=
   (Min.min 5 4)
 
 def extern_abs_int_plain (_ : Unit) : Int :=
-  let x : Int := (-5)
+  let x := (-5)
   (Sail.Int.intAbs x)
 
 def extern_eq_unit (_ : Unit) : Bool :=
diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean
index c89422abf..203fbf5f0 100644
--- a/test/lean/let.expected.lean
+++ b/test/lean/let.expected.lean
@@ -9,7 +9,7 @@ def foo (_ : Unit) : (BitVec 16) :=
   (HAnd.hAnd (0x0000 : (BitVec 16)) z)
 
 def bar (_ : Unit) : (BitVec 16) :=
-  let z : (BitVec 16) := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16)))
+  let z := (HOr.hOr (0xFFFF : (BitVec 16)) (0xABCD : (BitVec 16)))
   (HAnd.hAnd (0x0000 : (BitVec 16)) z)
 
 def initialize_registers (_ : Unit) : Unit :=
diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean
index 4cc431313..61b447c94 100644
--- a/test/lean/tuples.expected.lean
+++ b/test/lean/tuples.expected.lean
@@ -4,6 +4,16 @@ open Sail
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+def let0 := (20, 300000000000000000000000)
+
+def y :=
+  let (y, z) := let0
+  y
+
+def z :=
+  let (y, z) := let0
+  z
+
 def tuple1 (_ : Unit) : (Int × Int × ((BitVec 2) × Unit)) :=
   (3, 5, ((0b10 : (BitVec 2)), ()))
 
diff --git a/test/lean/tuples.sail b/test/lean/tuples.sail
index 66b17b474..0b7b1a588 100644
--- a/test/lean/tuples.sail
+++ b/test/lean/tuples.sail
@@ -1,5 +1,7 @@
 default Order dec
 
+let (y, z) = (20, 300000000000000000000000)
+
 function tuple1() -> (int, int, (bitvector(2), unit)) = {
   return (3, 5, (0b10, ()))
 }