From 2fa1c55f9d9dc4867e4347d430584b2ac265da1b Mon Sep 17 00:00:00 2001
From: Samuel Chassot <14821693+samuelchassot@users.noreply.github.com>
Date: Mon, 13 Nov 2023 12:58:37 +0100
Subject: [PATCH] Add mutable map TR (#1484)

* add mutable map TR

* move to dotty specific
---
 .../dotty-specific/valid/MutableMapTR.scala   | 40 +++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 frontends/benchmarks/dotty-specific/valid/MutableMapTR.scala

diff --git a/frontends/benchmarks/dotty-specific/valid/MutableMapTR.scala b/frontends/benchmarks/dotty-specific/valid/MutableMapTR.scala
new file mode 100644
index 000000000..04ce8e378
--- /dev/null
+++ b/frontends/benchmarks/dotty-specific/valid/MutableMapTR.scala
@@ -0,0 +1,40 @@
+import scala.annotation.tailrec
+import stainless.lang.*
+import stainless.collection.*
+import stainless.annotation.*
+
+object MTailList:
+  sealed abstract class MutableList[T]  
+  case class MNil[T]() extends MutableList[T]
+  case class MCons[T](val hd: T, var tail: MutableList[T]) extends MutableList[T]
+
+  extension[T] (ml: MutableList[T])
+    @pure
+    def toList: List[T] =
+      ml match
+        case MNil() => Nil()
+        case MCons(h, t) => Cons(h, t.toList)
+
+  def mapTR[T,U](l: MutableList[T], f: T => U): MutableList[U] = {
+    l match
+      case MNil() => MNil[U]()
+      case MCons(hd, tl) =>
+        val acc: MCons[U] = MCons[U](f(hd), MNil())
+        mapTRWorker[T,U](tl, f, acc)
+        acc
+  } ensuring(_.toList == l.toList.map(f))
+
+  @tailrec
+  def mapTRWorker[T,U](
+      l: MutableList[T],
+      f: T => U,
+      acc: MCons[U]
+  ): Unit = {
+    require(acc.tail == MNil[U]())
+    l match
+      case MNil() => ()
+      case MCons(h, t) => 
+        acc.tail = MCons[U](f(h), MNil())      
+        mapTRWorker(t, f, acc.tail.asInstanceOf[MCons[U]])
+        assert(acc.tail.asInstanceOf[MCons[U]].toList == f(h) :: t.toList.map(f))
+  } ensuring(_ => acc.toList == old(acc).hd :: l.toList.map(f))
\ No newline at end of file