如何使用Leon的库构建scalac？

Question

我正在尝试使用scalac直接编译我的Leon代码。不幸的是，我无法正确构建代码所依赖的Leon库。

例如，我运行了

scalac $(find ~/my-path/leon/library/ -name "*.scala" | xargs) Queue.scala 

但这实际上会返回错误：

.../leon/library/collection/List.scala:81: error: missing parameter type for expanded function ((x$2) => x$2.size.$eq$eq(if (i.$less$eq(0))
  BigInt(0)
else
  if (i.$greater$eq(this.size))
    this.size
  else
    i))
  }} ensuring { _.size == (
                ^

应该向scalac传递什么才能避免库中的这些错误，并最终编译我自己的源文件？

谢谢!

Answer 1

首先，我怀疑这里的尝试是执行Leon程序，如果是这样的话，有一个名为--eval的新选项，它将评估所有地面函数(您可以像往常一样通过--functions进一步过滤它)。这应该可以防止框架实现出现不可执行的问题。

关于编译问题:它现在应该在https://github.com/epfl-lara/leon/commit/3d73c6447916516d0ad56806fe0febf7b30a71ad中得到修复

这是由于类型推断无法跟踪从声明的返回类型通过非类型化的ensuring到函数体的类型。这会导致Nil()在正文中的类型不精确，进而导致无类型闭包被拒绝。

为什么这会在Leon内部起作用？Leon在类型检查之前在Scala编译器流水线中插入一个阶段，以注入使这种推断成为可能(并且方便)的提示，因为模式

def foo(a: A): B = { a match {
   case ..
   case ..
}} ensuring { .. }

在里昂项目中是如此频繁。

Answer 2

奇怪的是，编写类似这样的代码：

def take(i: BigInt): List[T] = { val res: List[T] = (this, i) match {
    case (Nil(), _) => Nil()
    case (Cons(h, t), i) =>
      if (i <= BigInt(0)) {
        Nil()
      } else {
        Cons(h, t.take(i-1))
      }
  }; res} ensuring { _.size == (
    if      (i <= 0)         BigInt(0)
    else if (i >= this.size) this.size 
    else                     i
  )}

明确地...makes它。Scalac无法推断正确的参数类型，但这使得第一个块的返回类型足够明确。但是请注意，直接使用Leon不是问题，这是整个Leon库中使用的通用语法，而不是我的代码。

通过更改上面解释的所有函数，我能够编译Leon库-但不能使用标准的scala语法运行项目，因为在https://github.com/epfl-lara/leon/blob/master/library/lang/Set.scala中缺少set实现，而Leon不知何故没有使用它。

Answer 3

以下是Etienne帖子：

这是可行的，但我们仍然需要在https://github.com/epfl-lara/leon/blob/master/library/lang/Set.scala中实现集合。我是这样做的：

package leon.lang
import leon.annotation._
import scala.collection.{ immutable => imm }

object Set {
  @library
  def empty[T] = Set[T]()
  protected[Set] def apply[T](elems: imm.Set[T]): Set[T] = Set(elems.toSeq :_*)
}

@ignore
case class Set[T](elems: T*) {
  def +(a: T): Set[T] = Set(elems.toSet + a)
  def ++(a: Set[T]): Set[T] = Set(elems.toSet ++ a.elems.toSet) //Set.trim(elems ++ a.elems) //Set((elems.toSeq ++ a.elems.toSeq).toSet.toSeq :_*)
  def -(a: T): Set[T] = Set(elems.toSet - a)
  def --(a: Set[T]): Set[T] = Set(elems.toSet -- a.elems.toSet)
  def contains(a: T): Boolean = elems.toSet.contains(a)
  def isEmpty: Boolean = this == Set.empty
  def subsetOf(b: Set[T]): Boolean = elems.toSet.forall(e => b.elems.toSet.contains(e))
  def &(a: Set[T]): Set[T] = Set(elems.toSet & a.elems.toSet)
}

不幸的是，这不能像在Leon中那样直接使用：

[ Error  ] 8:31: Scala's Set API is no longer extracted. Make sure you import leon.lang.Set that defines supported Set operations.
         protected[Set] def apply[T](elems: imm.Set[T]): Set[T] = Set(elems.toSeq :_*)
                                     ^^^^^^^^^^^^^^^^^

但是它在使用scalac编译和使用scala运行时工作得很好：

scalac $(find ~/my-path/leon/library/ -name "*.scala" | xargs) Queue.scala

无论如何，如果--eval成功了，我们就使用它吧！

谢谢!