Mutable fields with generics

[yannbolliger]

After solving #154, the next step is to make the same work for generic ADTs.

#[var(field)]
struct S {
  field: i32,
}
struct Gen<T>(T);

fn set_gen_field(mut g: Gen<S>) -> Gen<S> {
  g.0.field = 131415;
  g = Gen(S { field: 161718 });
  g
}

Ideas, roadmap

• All fields should be @var without annotation
• (try this first without generics)
• Then also, all type parameters should be @mutable by default
• However, as we only have consuming, mutable paramters, all methods can be @pure
• and arguments with mutable type parameters as type, that are not mut in Rust, can swap the @mutable flag with @pure.
• Otherwise, one might try to freshCopy all the type parameter-typed args.

[yannbolliger]

The above might work, as is suggested by these examples:

case class Ref[@mutable T](var x:T)
def add(a: @pure Ref[Int], b: Ref[Int]) = { b.x = a.x }

import stainless.lang._
import stainless.annotation._

object Test {
  case class Foo(var i: Int)

  @extern
  def mystery(x: Foo, @pure y: Foo) = {
    ()
  }

  def test = {
    val a = Foo(0)
    val b = Foo(1)

    mystery(a, b)

    assert(a.i == 0) // fails
    assert(b.i == 1) // passes
  }
}