Open vkuncak opened 9 months ago
This uses equality between wrong types in _ == t1.toList ++ t2.toList, but throws off function specialization:
_ == t1.toList ++ t2.toList
info Finished compiling info Preprocessing finished info Running phase FunctionSpecialization error: Lookup failed for adt with symbol `Conc$27`
Here is the entire code.
import stainless.lang._ import stainless.collection._ object SimpleConc: sealed abstract class Conc[T] case class Empty[T]() extends Conc[T] case class Single[T](x: T) extends Conc[T] case class CC[T](left: Conc[T], right: Conc[T], csize: BigInt) extends Conc[T] { require(csize == left.size + right.size) } extension[T](t1: Conc[T]) def <>(t2: Conc[T]) = CC(t1, t2, t1.size + t2.size) def toList: List[T] = t1 match case Empty() => Nil[T]() case Single(x) => x :: Nil[T]() case CC(l, r, _) => l.toList ++ r.toList def size: BigInt = { t1 match case Empty() => BigInt(0) case Single(_) => BigInt(1) case CC(_, _, csize) => csize }.ensuring(_ == t1.toList.size) def ++(t2: Conc[T]): Conc[T] = { t1 match case Empty() => t2 case Single(_) => t1 <> t2 case CC(l, r, _) => l ++ (r ++ t2) }.ensuring(_ == t1.toList ++ t2.toList) end SimpleConc
Should we add a check that ensures equality is only applied to comparable types?
This uses equality between wrong types in
_ == t1.toList ++ t2.toList
, but throws off function specialization:Here is the entire code.