匹配误差，同时证明功能不锈钢的终止

Question

我有此代码，该代码证明了不锈钢/leon中排序算法的终止。请注意，所采用的排名功能或措施不是正确的，因为这来自家庭作业。

import stainless.lang._
import stainless.collection._

object QuickSort {
  def isSorted(list: List[BigInt]): Boolean = list match {
    case Cons(x, xs @ Cons(y, _)) => x <= y && isSorted(xs)
    case _ => true
  }
  def quickSort(list: List[BigInt]): List[BigInt] = {
    decreases((list.size,0))
    list match {
      case Nil() => Nil[BigInt]()
      case Cons(x, xs) => par(x, Nil(), Nil(), xs)
    }
  } ensuring { res => isSorted(res) }
  def par(x: BigInt, l: List[BigInt], r: List[BigInt], ls: List[BigInt]): List[BigInt] = {
    decreases((l.size,l.size))
    ls match {
      case Nil() => quickSort(l) ++ Cons(x, quickSort(r))
      case Cons(x2, xs2) => if (x2 <= x) par(x, Cons(x2, l), r, xs2) else par(x, l, Cons(x2, r), xs2)
    }
  }
}

使用此代码，我会收到以下错误（我会说这来自Scala Frontend）：

[ Error  ] exercise.scala:14:5: error: overloaded method value decreases with alternatives:
[ Error  ]   (rank: (Int, Int, Int, Int, Int))Unit <and>
[ Error  ]   (rank: (Int, Int, Int, Int))Unit <and>
[ Error  ]   (rank: (Int, Int, Int))Unit <and>
[ Error  ]   (rank: (Int, Int))Unit <and>
[ Error  ]   (rank: Int)Unit <and>
[ Error  ]   (rank: (BigInt, BigInt, BigInt, BigInt, BigInt))Unit <and>
[ Error  ]   (rank: (BigInt, BigInt, BigInt, BigInt))Unit <and>
[ Error  ]   (rank: (BigInt, BigInt, BigInt))Unit <and>
[ Error  ]   (rank: (BigInt, BigInt))Unit <and>
[ Error  ]   (rank: BigInt)Unit
[ Error  ]  cannot be applied to ((BigInt, Int))
               decreases((list.size,0))
               ^

所以我做import scala.BigInt._并将decreases((list.size,0))转换为decreases((list.size,BigInt(0)))。最后，这给出了以下例外（来自不锈钢/Inox部分）：

Exception in thread "main" scala.MatchError: <untyped> (of class inox.ast.Types$Untyped$)
    at stainless.extraction.oo.MethodLifting$BaseTransformer$1.transform(MethodLifting.scala:139)
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:115)
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:114)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
    at scala.collection.immutable.List.map(List.scala:285)
    at inox.ast.TreeTransformer$class.transform(TreeOps.scala:114)
    at stainless.extraction.oo.MethodLifting$BaseTransformer$1.transform(MethodLifting.scala:149)
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:115)
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:114)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
    at scala.collection.immutable.List.map(List.scala:285)
    at inox.ast.TreeTransformer$class.transform(TreeOps.scala:114)
    at stainless.extraction.oo.MethodLifting$BaseTransformer$1.transform(MethodLifting.scala:149)
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:115)
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:114)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
    at scala.collection.immutable.List.map(List.scala:285)
    at inox.ast.TreeTransformer$class.transform(TreeOps.scala:114)
    at stainless.extraction.oo.MethodLifting$BaseTransformer$1.transform(MethodLifting.scala:149)
    at inox.ast.TreeTransformer$class.transform(TreeOps.scala:185)
    at stainless.extraction.oo.MethodLifting$BaseTransformer$1.transform(MethodLifting.scala:133)
    at stainless.extraction.oo.MethodLifting$$anonfun$38.apply(MethodLifting.scala:285)
    at stainless.extraction.oo.MethodLifting$$anonfun$38.apply(MethodLifting.scala:281)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
    at scala.collection.Iterator$class.foreach(Iterator.scala:893)
    at scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
    at scala.collection.MapLike$DefaultValuesIterable.foreach(MapLike.scala:206)
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
    at scala.collection.AbstractTraversable.map(Traversable.scala:104)
    at stainless.extraction.oo.MethodLifting$class.transform(MethodLifting.scala:281)
    at stainless.extraction.oo.package$extractor$.transform(package.scala:16)
    at stainless.extraction.oo.package$extractor$.transform(package.scala:16)
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262)
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262)
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262)
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262)
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262)
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262)
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262)
    at inox.Program$$anon$2.<init>(Program.scala:78)
    at inox.Program$class.transform(Program.scala:76)
    at stainless.frontends.scalac.CodeExtraction$Extraction$$anon$1.transform(CodeExtraction.scala:187)
    at stainless.SimpleComponent$class.extract(Component.scala:46)
    at stainless.termination.TerminationComponent$.extract(TerminationComponent.scala:8)
    at stainless.SimpleComponent$class.apply(Component.scala:50)
    at stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:8)
    at stainless.MainHelpers$$anonfun$main$1.apply(MainHelpers.scala:76)
    at stainless.MainHelpers$$anonfun$main$1.apply(MainHelpers.scala:76)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at stainless.MainHelpers$class.main(MainHelpers.scala:76)
    at stainless.Main$.main(Main.scala:5)
    at stainless.Main.main(Main.scala)

关于为什么会发生这种情况以及我该如何解决的任何想法？我还尝试调用decreases(list.size,BigInt(0))和其他几个版本，但它不起作用。

编辑

显然，删除行import scala.BigInt._解决了问题，所以任何想法都会发生这种情况？

Answer 1

不锈钢从Scalac Frontend提取树木的方式期望特定的树结构用于bigint提取。当从scala.BigInt._导入BigInt(_)时，此结构略有不同。

这没什么意义，可以通过使用符号而不是精确的树匹配来避免。我将考虑解决问题。