Swap operation on references

[vkuncak]

This code is unfortunately not accepted by alias analysis.

import stainless.lang.*
object Tree {
  sealed abstract class Tree
  case class Node(var left: Tree, var x: Int, var right: Tree) extends Tree
  case class Leaf() extends Tree

  def flip(t: Tree): Unit = {
    t match 
      case Leaf() => ()
      case _ =>
        val n: Node = t.asInstanceOf[Node]
        val tmp = n.right
        n.right = n.left
        n.left = tmp
  }
}

If this is inherent to how we track aliases, maybe we can come up with a primitive to do a swap, like the one we have with the arrays. One question is how to refer to a pair of an object and a field.

[vkuncak]

Given that we have array swap, one could try

  sealed abstract class Tree
  case class Node(var x: Int, children: Array[Tree]) extends Tree
  case class Leaf() extends Tree

but this is not accepted as a valid recursive definition:

[ Fatal  ] Tree.scala:3:25: ADT Tree must appear only in strictly positive positions of Tree
             sealed abstract class Tree
                                   ^

even though there is nothing wrong with such recursion over arrays, it is still covariant.

[vkuncak]

One possible approach is to suggest systematically using vals to mutable cells, in the style of ML.

import stainless.lang.*
import stainless.annotation.*
object TreeCell {
  sealed case class Cell[@mutable T](var v: T)

  sealed abstract class Tree
  case class Node(left: Cell[Tree], var x: Int, right: Cell[Tree]) extends Tree
  case class Leaf() extends Tree

  def swap[@mutable T](c1: Cell[T], c2: Cell[T]): Unit = {
    val v1 = c1.v
    val v2 = c2.v
    c1.v = freshCopy(v2)
    c2.v = freshCopy(v1)
  }

  def flip(t: Tree): Unit = {
    t match 
      case Leaf() => ()
      case Node(l,_,r) =>
        flip(l.v)
        flip(r.v)
        swap(l, r)
  }

  def elem(x: Int): Tree =
    Node(Cell[Tree](Leaf()), x, Cell[Tree](Leaf()))

  def node(t1: Tree, x: Int, t2: Tree): Tree =
    Node(Cell[Tree](t1), x, Cell[Tree](t2))
  
  val t: Tree = node(node(elem(3), 4, elem(5)), 6,
                     node(elem(7), 8, elem(9)))

This works in Stainless. It crashes in Scala because freshCopy is defined as ???, but we could redefine it as identity function.

[vkuncak]

So, my proposal is to:

• redefine freshCopy to make it executable
• introduce into the library Cell[@mutable T](var v: T)
• introduce into the library swap[@mutable T](c1: Cell[T], c2: Cell[T]): Unit

[vkuncak]

I actually tried to mimic swap defined on arrays to introduce swapCells into the library in the same way as the swap for arrays, but with that Stainless reports that the new reference swapCells is undefined:

[ Error  ] flip$0 depends on missing dependencies: swapCells$0.
[ Fatal  ] Cannot recover from missing dependencies

[vkuncak]

@samuelchassot this seems of interest

[samuelchassot]

Implemented in #1461