epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 50 forks source link

Cell swap (#2) #1461

Closed samuelchassot closed 9 months ago

samuelchassot commented 9 months ago

Add a new Cell feature with a swap to support more mutability, notably swapping 2 variables.

This adds a new Cell class in the library, and a swap function exchanging their values:

case class Cell[@mutable T](var v: T) 

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

These can be used as follows:

import stainless.lang._

object Test {

  def f(c1: Cell[Int], c2: Cell[Int]): Unit = {
    require(c1.v == 1)
    require(c2.v == 2)

    c1.v = 3
    swap(c1, c2)
    assert(c1.v == 2)
    assert(c2.v == 3)
  }
}
samuelchassot commented 9 months ago

Closes #1356

samuelchassot commented 9 months ago

Looks good 👍 ! Just minor details :) There is also a missing case for CellSwap in AntiAliasing#doNormalize:

case swp @ CellSwap(cell1, cell2) =>
  val (ctxCell1, normCell1) = normalizeForTarget(cell1)
  val (ctxCell2, normCell2) = normalizeForTarget(cell2)
  (ctxCell1 compose ctxCell2, CellSwap(normCell1, normCell2).copiedFrom(swp))

Whoops, I added it!

samuelchassot commented 9 months ago

@mario-bucev I applied the fixes according to your comments!

vkuncak commented 9 months ago

Awesome!