Add support for mutating tuples.

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),

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,

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