From bf883726d771988c838bc6a6e1c012dfb008769c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 11 Jun 2024 13:59:39 +0200
Subject: Update the tests for tuples

---
 tests/lean/NoNestedBorrows.lean | 31 ++++++++++++++++++++++++-------
 1 file changed, 24 insertions(+), 7 deletions(-)

(limited to 'tests/lean/NoNestedBorrows.lean')

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index b8fbcff0..262fc79e 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -538,27 +538,44 @@ def read_then_incr (x : U32) : Result (U32 × U32) :=
    Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 -/
 def Tuple (T1 T2 : Type) := T1 × T2
 
-/- [no_nested_borrows::use_tuple_struct]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 -/
-def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
+/- [no_nested_borrows::read_tuple]:
+   Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:40 -/
+def read_tuple (x : (U32 × U32)) : Result U32 :=
+  let (i, _) := x
+  Result.ok i
+
+/- [no_nested_borrows::update_tuple]:
+   Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 -/
+def update_tuple (x : (U32 × U32)) : Result (U32 × U32) :=
+  let (_, i) := x
+  Result.ok (1#u32, i)
+
+/- [no_nested_borrows::read_tuple_struct]:
+   Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 -/
+def read_tuple_struct (x : Tuple U32 U32) : Result U32 :=
+  Result.ok x.#0
+
+/- [no_nested_borrows::update_tuple_struct]:
+   Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 -/
+def update_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
   Result.ok (1#u32, x.#1)
 
 /- [no_nested_borrows::create_tuple_struct]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 -/
 def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) :=
   Result.ok (x, y)
 
 /- [no_nested_borrows::IdType]
-   Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 503:0-503:20 -/
 @[reducible] def IdType (T : Type) := T
 
 /- [no_nested_borrows::use_id_type]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 505:0-505:40 -/
 def use_id_type (T : Type) (x : IdType T) : Result T :=
   Result.ok x
 
 /- [no_nested_borrows::create_id_type]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 509:0-509:43 -/
 def create_id_type (T : Type) (x : T) : Result (IdType T) :=
   Result.ok x
 
-- 
cgit v1.2.3


From 2e91b90e332c473253c2ff91fd65da34eb709572 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 11 Jun 2024 14:06:23 +0200
Subject: Deactivate the use of tuple projectors in the Lean backend

---
 tests/lean/NoNestedBorrows.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'tests/lean/NoNestedBorrows.lean')

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 262fc79e..f0438050 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -553,12 +553,14 @@ def update_tuple (x : (U32 × U32)) : Result (U32 × U32) :=
 /- [no_nested_borrows::read_tuple_struct]:
    Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 -/
 def read_tuple_struct (x : Tuple U32 U32) : Result U32 :=
-  Result.ok x.#0
+  let (i, _) := x
+  Result.ok i
 
 /- [no_nested_borrows::update_tuple_struct]:
    Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 -/
 def update_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
-  Result.ok (1#u32, x.#1)
+  let (_, i) := x
+  Result.ok (1#u32, i)
 
 /- [no_nested_borrows::create_tuple_struct]:
    Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 -/
-- 
cgit v1.2.3