Fix extraction of Array.updated

epfl-lara · Mar 12, 2021 · 9cc2376 · 9cc2376
1 parent 9574673
commit 9cc2376
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 21 deletions.
diff --git a/frontends/benchmarks/extraction/valid/Arrays.scala b/frontends/benchmarks/extraction/valid/Arrays.scala
@@ -1,12 +1,12 @@
 /* Copyright 2009-2021 EPFL, Lausanne */
 
+// use `.updated` from Stainless library
 import stainless.lang._
 
-object Arrays {
+// unimport implicit conversions for `.updated`
+import scala.Predef.{ genericArrayOps => _, genericWrapArray => _, _ }
 
-  def len[T](a: Array[T]): Boolean = {
-    a.length == a.size
-  }.holds
+object Arrays {
 
   def update[T](a: Array[T], i: Int, t: T) = {
     require(i >= 0 && i < a.length)
@@ -17,24 +17,11 @@ object Arrays {
     a.update(i, t)
   }
 
+  def updated[T](a: Array[T], i: Int, t: T): Array[T] = {
+    require(i >= 0 && i < a.length)
 
-  // ArraySeq not supported.
-  /*
-   * import scala.collection.mutable.ArraySeq
-   * def updated[T](a: Array[T], i: Int, t: T): ArraySeq[T] = {
-   *   require(i >= 0 && i < a.length)
-   *   a.updated(i, t)
-   * }
-   */
-
-  // ClassTag not supported.
-  /*
-   * import scala.reflect.ClassTag
-   * def updated[T](a: Array[T], i: Int, u: T)(implicit m: ClassTag[T]): Array[T] = {
-   *   require(i >= 0 && i < a.length)
-   *   a.updated(i, u)
-   * }
-   */
+    a.updated(i, t)
+  }
 
   def updated(a: Array[Int], i: Int, v: Int): Array[Int] = {
     require(i >= 0 && i < a.length)

diff --git a/frontends/library/stainless/lang/package.scala b/frontends/library/stainless/lang/package.scala
@@ -145,4 +145,14 @@ package object lang {
 
   @library
   def specialize[T](call: T): T = call
+
+  @ignore @library
+  implicit class ArrayUpdating[T](a: Array[T]) {
+    def updated(index: Int, value: T): Array[T] = {
+      val res = a.clone
+      res(index) = value
+      res
+    }
+  }
+
 }
diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
@@ -844,6 +844,18 @@ trait ASTExtractors {
              if (arrayOps.toString endsWith "ArrayOps") && (update.toString == "updated")
              => Some((array, index, value))
 
+        case Apply(
+          Select(
+            Apply(
+              TypeApply(ExSelected("stainless", "lang", "package", "ArrayUpdating"), tpe :: Nil),
+              array :: Nil
+            ),
+            ExNamed("updated")
+          ),
+          index :: value :: Nil) =>
+
+          Some((array, index, value))
+
         // There's no `updated` method in the Array class itself, only though implicit conversion.
         case _ => None
       }