Lean: fix lets that use tuples

rems-project · Feb 11, 2025 · f17fb4b · f17fb4b
1 parent c8020d3
commit f17fb4b
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -1,5 +1,7 @@
 default Order dec
 
+let (y, z) = (20, 300000000000000000000000)
+
 function tuple1() -> (int, int, (bitvector(2), unit)) = {
   return (3, 5, (0b10, ()))
 }