epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 51 forks source link

Classes with multiple parameter groups #1086

Open jad-hamza opened 3 years ago

jad-hamza commented 3 years ago

This is currently not supported by Stainless:

case class C(var x: Int)(var y: Int = x) { }
Variables are only allowed within functions and as constructor parameters in Stainless.
vkuncak commented 2 years ago

Are there uses of such constructors that do not involve partial application? If we need to support partial application, what does C(3) even mean, what is its type?

mario-bucev commented 2 years ago

Mostly for dependent types such as:

case class C(t: MyTrait)(a: MyTrait.A) 

As for C(3), Scala 3 types it as Int => C (as we would expect)

vkuncak commented 2 years ago

I see, so partial application would probably be desugared in Stainless into a partial constructor:

  case class C(var x: Int, var y: Int)

  // replace all C constructor calls with makeC
  def makeC(x: Int)(y: Int) = C(x, y)

  def test: C =
    val pC = makeC(3)
    pC(42)