Skip to content

Commit

Permalink
Add test with mutable pattern match.
Browse files Browse the repository at this point in the history
  • Loading branch information
yannbolliger committed Jun 4, 2021
1 parent 6dda86f commit d3e243c
Show file tree
Hide file tree
Showing 2 changed files with 44 additions and 0 deletions.
1 change: 1 addition & 0 deletions stainless_frontend/tests/extraction_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,7 @@ define_tests!(
pass: mut_ref_borrow_6,
pass: mut_ref_borrow_7,
pass: mut_ref_borrow_8,
pass: mut_ref_borrow_9,
pass: mut_ref_immut_borrow,
pass: mut_return,
pass: nested_spec,
Expand Down
43 changes: 43 additions & 0 deletions stainless_frontend/tests/pass/mut_ref_borrow_9.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
extern crate stainless;

struct S<T>(T);
struct Container<T> {
s: S<T>,
}

pub fn main() {
let mut c = Container { s: S("hello") };

match &mut c.s {
S(v) if *v == "hello" => *v = "world",
_ => {}
};

assert!(c.s.0 == "world")
}

/*
Desired Scala translation:
import stainless.annotation._
object Fields {
case class S[@mutable T](_0: MutCell[T])
case class MutCell[@mutable T](var value: T)
case class Container[@mutable T](s: MutCell[S[T]])
def main: Unit = {
var c: Container[String] = Container(MutCell(S(MutCell("hello"))))
(c.s match {
case MutCell(S(v)) if v.value == "hello" =>
v.value = "world"
case _ =>
()
})
assert(c.s.value._0.value == "world")
}
}
*/

0 comments on commit d3e243c

Please sign in to comment.