Revisiting "unfold" and renaming it to unfolding

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

@@ -261,7 +261,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
         // * `selectResult` selects the first element of the tuple returned by the transformed function
         // (the others elements are the "updated" version of the mutated parameters).
         // By default, it should be set to `true`.
-        // However, in the particular case of `unfold(fn(...))`, we would like *not* to have this selection be performed
+        // However, in the particular case of `unfolding(fn(...))`, we would like *not* to have this selection be performed
         // due to the following. `AntiAliasing` will transform this call to:
         //   unfold {
         //      val res = fn(...)
@@ -1055,7 +1055,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
 
         object UnfoldOpaque {
           def unapply(e: Expr): Option[(Identifier, FunctionInvocation)] = e match {
-            case FunctionInvocation(id @ ast.SymbolIdentifier("stainless.lang.unfold"), Seq(_), Seq(fi: s.FunctionInvocation)) =>
+            case FunctionInvocation(id @ ast.SymbolIdentifier("stainless.lang.unfolding"), Seq(_), Seq(fi: s.FunctionInvocation)) =>
               Some((id, fi))
             case _ => None
           }

core/src/main/scala/stainless/extraction/inlining/UnfoldOpaque.scala

@@ -24,7 +24,7 @@ class UnfoldOpaque(override val s: Trees, override val t: Trees)
 
     override def transform(e: Expr, env: Env): t.Expr = {
       e match {
-        case s.FunctionInvocation(ast.SymbolIdentifier("stainless.lang.unfold"), Seq(_), Seq(maybeFi)) =>
+        case s.FunctionInvocation(ast.SymbolIdentifier("stainless.lang.unfolding"), Seq(_), Seq(maybeFi)) =>
           // Lookup the bindings recursively to unveil a call to a function which we would need to unfold
           val r = dealiasedAndStripped(maybeFi, env)
           r match {

frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala

@@ -14,8 +14,8 @@ object OpaqueMutation1 {
       @ghost val oldBox = snapshot(this)
       cnt += 1
       ghostExpr {
-        unfold(secretSauce(other))
-        unfold(oldBox.secretSauce(other))
+        unfolding(secretSauce(other))
+        unfolding(oldBox.secretSauce(other))
         check(oldBox.secretSauce(other) + 1 == this.secretSauce(other))
       }
     }.ensuring(_ => old(this).secretSauce(other) + 1 == this.secretSauce(other))
@@ -29,4 +29,4 @@ object OpaqueMutation1 {
     // Therefore, the following is incorrect (but it holds for `b.other`, see the other `valid/OpaqueMutation`)
     assert(oldBox.secretSauce(oldBox.other) + 1 == b.secretSauce(oldBox.other))
   }
-}
+}

frontends/benchmarks/imperative/invalid/OpaqueMutation2.scala

@@ -15,8 +15,8 @@ object OpaqueMutation2 {
       @ghost val oldBox = snapshot(this)
       cnt += 1
       ghostExpr {
-        unfold(secretSauce(smallerBox.otherCnt))
-        unfold(oldBox.secretSauce(smallerBox.otherCnt))
+        unfolding(secretSauce(smallerBox.otherCnt))
+        unfolding(oldBox.secretSauce(smallerBox.otherCnt))
         check(oldBox.secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt))
       }
     }.ensuring(_ => old(this).secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt))
@@ -30,4 +30,4 @@ object OpaqueMutation2 {
     // Therefore, the following is incorrect (but it holds for `b.other`, see the other `valid/OpaqueMutation`)
     assert(oldBox.secretSauce(oldBox.smallerBox.otherCnt) + 1 == b.secretSauce(oldBox.smallerBox.otherCnt))
   }
-}
+}

frontends/benchmarks/imperative/valid/OpaqueMutation1.scala

@@ -13,8 +13,8 @@ object OpaqueMutation1 {
       @ghost val oldBox = snapshot(this)
       cnt += 1
       ghostExpr {
-        unfold(secretSauce(other))
-        unfold(oldBox.secretSauce(other))
+        unfolding(secretSauce(other))
+        unfolding(oldBox.secretSauce(other))
         check(oldBox.secretSauce(other) + 1 == this.secretSauce(other))
       }
     }.ensuring(_ => old(this).secretSauce(other) + 1 == this.secretSauce(other))
@@ -24,8 +24,8 @@ object OpaqueMutation1 {
     def incrementPure(): (Unit, Box) = {
       val newThis = Box(cnt + 1, other)
       ghostExpr {
-        unfold(newThis.secretSauce(other))
-        unfold(this.secretSauce(other))
+        unfolding(newThis.secretSauce(other))
+        unfolding(this.secretSauce(other))
         check(this.secretSauce(other) + 1 == newThis.secretSauce(other))
       }
       ((), newThis)
@@ -67,4 +67,4 @@ object OpaqueMutation1 {
     assert(oldB2.secretSauce(newB2.other) + 1 == newB2.secretSauce(newB2.other))
     assert(cond ==> (oldB2.secretSauce(newB.other) + 1 == newB.secretSauce(newB.other)))
   }
-}
+}

frontends/benchmarks/imperative/valid/OpaqueMutation2.scala

@@ -15,8 +15,8 @@ object OpaqueMutation2 {
       @ghost val oldBox = snapshot(this)
       cnt += 1
       ghostExpr {
-        unfold(secretSauce(smallerBox.otherCnt))
-        unfold(oldBox.secretSauce(smallerBox.otherCnt))
+        unfolding(secretSauce(smallerBox.otherCnt))
+        unfolding(oldBox.secretSauce(smallerBox.otherCnt))
         check(oldBox.secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt))
       }
     }.ensuring(_ => old(this).secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt))
@@ -41,4 +41,4 @@ object OpaqueMutation2 {
     assert(oldB2.secretSauce(b2.smallerBox.otherCnt) + 1 == b2.secretSauce(b2.smallerBox.otherCnt))
     assert(cond ==> (oldB2.secretSauce(b.smallerBox.otherCnt) + 1 == b.secretSauce(b.smallerBox.otherCnt)))
   }
-}
+}

frontends/benchmarks/imperative/valid/UnfoldOpaqueMutate.scala

@@ -19,12 +19,12 @@ object UnfoldOpaqueMutate {
 
   def test1(wb: WrappedBox, x: BigInt): Unit = {
     @ghost val oldWb = snapshot(wb)
-    unfold(wb.opaqueMutMeth1(x))
+    unfolding(wb.opaqueMutMeth1(x))
     assert(wb.box.cnt == oldWb.box.cnt + x)
   }
 
   def test2(wb: WrappedBox, x: BigInt): Unit = {
-    unfold(wb.opaqueMutMeth2(x))
+    unfolding(wb.opaqueMutMeth2(x))
     assert(wb.box == Box(x * 2))
   }
-}
+}

frontends/benchmarks/verification/valid/MicroTests/VisibleOpaque.scala

@@ -1,11 +1,11 @@
 import stainless.annotation._
-import stainless.lang.unfold
+import stainless.lang.unfolding
 
 object VisibleOpaque {
   @opaque def p(x: Int) = x > 0
 
   def test(x: Int): Unit = {
-    unfold(p(x))
+    unfolding(p(x))
     assert(p(x) == x > 0)
   }
 }

frontends/benchmarks/verification/valid/UnfoldOpaqueVal.scala

@@ -7,7 +7,7 @@ object UnfoldOpaqueVal {
 
   def test(x: BigInt): Unit = {
     val y = opaqueFn(x)
-    unfold(y)
+    unfolding(y)
     assert(y == x + 1)
   }
-}
+}

frontends/library/stainless/lang/package.scala

@@ -179,7 +179,7 @@ package object lang {
   // typically used when `call` invokes an `opaque` function
   // this adds an equality between the call, and the inlined call
   @library
-  def unfold[T](call: T): Unit = ()
+  def unfolding[T](call: T): Unit = ()
 
   @ignore @library
   implicit class ArrayUpdating[T](a: Array[T]) {