Add Scala translation for mut-from-start approach.

stainless_frontend/tests/fail/mut_ref_borrow_4.rs

@@ -23,3 +23,30 @@ fn main() {
   assert!(*x.0 == 789);
   assert!(int == 789)
 }
+
+/*
+Desired Scala translation:
+
+import stainless.annotation._
+
+object Mutable {
+  final case class Mut[@mutable T](var t: T)
+  final case class S(var s: Mut[Int])
+
+  def main() = {
+    val int = Mut(123)
+    val x = Mut(S(int))
+
+    val y = x
+    assert(y.t.s.t == 123 && x.t.s.t == 123)
+
+    val z = x
+    assert(z.t.s.t == 123)
+
+    z.t.s.t = 789
+    assert(z.t.s.t == 789)
+    assert(x.t.s.t == 789)
+    assert(int.t == 789)
+  }
+}
+*/

stainless_frontend/tests/pass/mut_ref_borrow_0.rs

@@ -9,3 +9,23 @@ pub fn main() {
 
   assert!(x == 2)
 }
+
+/*
+Desired Scala translation:
+
+import stainless.annotation._
+
+object Mutable {
+  final case class Mut[@mutable T](var t: T)
+
+  def main() = {
+    var x = Mut(1)
+
+    val y = x
+    assert(y.t == 1)
+    y.t = 2
+
+    assert(x.t == 2)
+  }
+}
+*/

stainless_frontend/tests/pass/mut_ref_borrow_1.rs

@@ -10,3 +10,23 @@ pub fn main() {
 
   assert!(a.0 == 100 && a.1 == 200)
 }
+
+/*
+Desired Scala translation:
+
+import stainless.annotation._
+
+object Mutable {
+  final case class Mut[@mutable T](var t: T)
+  final case class S(var s1: Int, var s2: Int)
+
+  def main() = {
+    var a = Mut(S(1, 2))
+
+    val b = a
+    b.t = S(100, 200)
+
+    assert(a.t.s1 == 100 && a.t.s2 == 200)
+  }
+}
+*/

stainless_frontend/tests/pass/mut_ref_borrow_2.rs

@@ -11,3 +11,26 @@ pub fn main() {
   b.0 = 100;
   assert!(b.0 == a.0 && a.0 == 100)
 }
+
+/*
+Desired Scala translation:
+
+import stainless.annotation._
+
+object Mutable {
+  final case class Mut[@mutable T](var t: T)
+  final case class S(var s: Int)
+
+  def main() = {
+    var a = Mut(S(1))
+
+    val b = {
+      a.t.s = 10
+      a
+    }
+    b.t.s = 100
+
+    assert(b.t.s == a.t.s && a.t.s == 100)
+  }
+}
+*/

stainless_frontend/tests/pass/mut_ref_borrow_3.rs

@@ -12,3 +12,25 @@ pub fn main() {
   b.0 = 100;
   assert!(b.0 == a.0 && a.0 == 100)
 }
+
+/*
+Desired Scala translation:
+
+import stainless.annotation._
+
+object Mutable {
+  final case class Mut[@mutable T](var t: T)
+  final case class S(var s: Int)
+
+  def borrows_mutably[@mutable T](t: Mut[T]): Mut[T] = t
+
+  def main() = {
+    var a = Mut(S(1))
+
+    val b = borrows_mutably(a)
+    b.t.s = 100
+
+    assert(b.t.s == a.t.s && a.t.s == 100)
+  }
+}
+*/

stainless_frontend/tests/pass/mut_ref_borrow_5.rs

@@ -21,3 +21,33 @@ pub fn main() {
   *thing3 = Thing { field: 0 };
   assert!(thing.field == 0);
 }
+
+/*
+Desired Scala translation:
+
+import stainless.lang._
+import stainless.annotation._
+
+object Mutable {
+  final case class Mut[@mutable T](var t: T)
+  final case class Thing[@mutable T](var field: T)
+
+  def change_thing[@mutable T](thing: Mut[Thing[T]], t: T) = {
+    thing.t = Thing(freshCopy(t))
+  }
+
+  def main() = {
+    val thing = Mut(Thing(123))
+    change_thing(thing, 456)
+    assert(thing.t.field == 456)
+
+    val thing2 = thing
+    change_thing(thing2, 789)
+    assert(thing.t.field == 789)
+
+    val thing3 = thing
+    thing3.t = Thing(0)
+    assert(thing.t.field == 0)
+  }
+}
+*/