diff --git a/frontends/benchmarks/extraction/valid/Arrays.scala b/frontends/benchmarks/extraction/valid/Arrays.scala index a10538cf82..e2e94b2e4b 100644 --- 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 index 5d7e8fff89..75f749b3e7 100644 --- 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 index 6b310c785d..e86b0f9308 100644 --- 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 }