Skip to content

Commit

Permalink
Fix extraction of Array.updated
Browse files Browse the repository at this point in the history
  • Loading branch information
jad-hamza committed Mar 12, 2021
1 parent 9574673 commit 9cc2376
Show file tree
Hide file tree
Showing 3 changed files with 30 additions and 21 deletions.
29 changes: 8 additions & 21 deletions frontends/benchmarks/extraction/valid/Arrays.scala
Original file line number Diff line number Diff line change
@@ -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)
Expand All @@ -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)
Expand Down
10 changes: 10 additions & 0 deletions frontends/library/stainless/lang/package.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
Expand Down

0 comments on commit 9cc2376

Please sign in to comment.