Revert

epfl-lara · Mar 12, 2021 · 1fdf28f · 1fdf28f
1 parent 11a0071
commit 1fdf28f
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 30 deletions.
diff --git a/frontends/benchmarks/extraction/valid/Arrays.scala b/frontends/benchmarks/extraction/valid/Arrays.scala
@@ -1,13 +1,13 @@
 /* Copyright 2009-2021 EPFL, Lausanne */
 
-// use `.updated` from Stainless library
 import stainless.lang._
 
-// unimport implicit conversions for `.updated`
-import scala.Predef.{ genericArrayOps => _, genericWrapArray => _, _ }
-
 object Arrays {
 
+  def len[T](a: Array[T]): Boolean = {
+    a.length == a.size
+  }.holds
+
   def update[T](a: Array[T], i: Int, t: T) = {
     require(i >= 0 && i < a.length)
     val array: Array[Int] = Array(0, 1)
@@ -17,11 +17,24 @@ object Arrays {
     a.update(i, t)
   }
 
-  def updated[T](a: Array[T], i: Int, t: T): Array[T] = {
-    require(i >= 0 && i < a.length)
 
-    a.updated(i, t)
-  }
+  // 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)
+   * }
+   */
 
   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,14 +145,4 @@ 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,18 +844,6 @@ 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
       }