From 248f89d6a36008c94674cb1d099a13e2aca8039e Mon Sep 17 00:00:00 2001
From: Yann Bolliger <yann.bolliger@epfl.ch>
Date: Fri, 25 Jun 2021 21:30:24 +0200
Subject: [PATCH] Add support for mutating tuples.

---
 stainless_extraction/src/expr/field.rs       | 9 +++++++++
 stainless_frontend/tests/extraction_tests.rs | 1 +
 stainless_frontend/tests/pass/mut_tuple.rs   | 8 ++++++++
 3 files changed, 18 insertions(+)
 create mode 100644 stainless_frontend/tests/pass/mut_tuple.rs

diff --git a/stainless_extraction/src/expr/field.rs b/stainless_extraction/src/expr/field.rs
index 8e75368f..50ec74b8 100644
--- a/stainless_extraction/src/expr/field.rs
+++ b/stainless_extraction/src/expr/field.rs
@@ -36,6 +36,15 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
           )
           .into()
         }
+        TyKind::Tuple(substs) => {
+          let lhs = self.extract_expr(lhs);
+          f.FieldAssignment(
+            self.synth().tuple_select(substs.len(), lhs, name.index()),
+            self.synth().mut_cell_value_id(),
+            value,
+          )
+          .into()
+        }
         ref t => self.unsupported_expr(
           lhs.span,
           format!("Cannot extract assignment to type {:?}", t),
diff --git a/stainless_frontend/tests/extraction_tests.rs b/stainless_frontend/tests/extraction_tests.rs
index 7ed18508..248bf11c 100644
--- a/stainless_frontend/tests/extraction_tests.rs
+++ b/stainless_frontend/tests/extraction_tests.rs
@@ -138,6 +138,7 @@ define_tests!(
   pass: mut_ref_immut_borrow,
   pass: mut_ref_tuple,
   pass: mut_return,
+  pass: mut_tuple,
   pass: nested_spec,
   pass: nested_spec_impl,
   pass: panic_type,
diff --git a/stainless_frontend/tests/pass/mut_tuple.rs b/stainless_frontend/tests/pass/mut_tuple.rs
new file mode 100644
index 00000000..ceb2ef41
--- /dev/null
+++ b/stainless_frontend/tests/pass/mut_tuple.rs
@@ -0,0 +1,8 @@
+extern crate stainless;
+
+pub fn main() {
+  let mut x = (123, false);
+  let y = x;
+  x.1 = true;
+  assert!(!y.1 && x.1)
+}