diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala index 914636ed1c0b25f31050a0235359ff0787d8f44c..c3f9eed0f0d55b0f75628d491a998facd29aa346 100644 --- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala +++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala @@ -631,11 +631,11 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int None } case (up @ UnapplyPattern(ob, _, subs), scrut) => - e(FunctionInvocation(up.unapplyFun, Seq(scrut))) match { - case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.Nil.get => + e(functionInvocation(up.unapplyFun.fd, Seq(scrut))) match { + case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.None.get => None - case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Cons.get => - val res = subs zip unwrapTuple(arg, up.unapplyFun.returnType.isInstanceOf[TupleType]) map { + case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Some.get => + val res = subs zip unwrapTuple(arg, subs.size) map { case (s,a) => matchesPattern(s,a) } if (res.forall(_.isDefined)) { diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala index f9ef63bdd9ad8650d44877ad03ff109fbd387200..9cc6dd132036ffdde4a5ef70e2be87e6276f9f3c 100644 --- a/src/main/scala/leon/evaluators/StreamEvaluator.scala +++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala @@ -252,12 +252,12 @@ class StreamEvaluator(ctx: LeonContext, prog: Program) } else { Stream() } - case (up @ UnapplyPattern(ob, _, subs), scrut) => - e(FunctionInvocation(up.unapplyFun, Seq(scrut))) flatMap { - case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.Nil.get => + case (UnapplyPattern(ob, unapplyFun, subs), scrut) => + e(functionInvocation(unapplyFun.fd, Seq(scrut))) flatMap { + case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.None.get => None - case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Cons.get => - val subMaps = subs zip unwrapTuple(arg, up.unapplyFun.returnType.isInstanceOf[TupleType]) map { + case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Some.get => + val subMaps = subs zip unwrapTuple(arg, subs.size) map { case (s,a) => matchesPattern(s,a) } cartesianProduct(subMaps).map( _.flatten.toMap ++ obind(ob, expr)) @@ -305,7 +305,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program) Some(step(expr, es)) } catch { case _: RuntimeError => - // EvalErrors stop the computation alltogether + // EvalErrors stop the computation altogether None } } diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala index ff882c96157cb6b85b02e101a3c0b84e0cfe058f..84b0087caee305b66e16d82ad2adcd9f4b10e06d 100644 --- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala +++ b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala @@ -187,6 +187,38 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL { | def f3 = C(42).isInstanceOf[A] |}""".stripMargin, + """import leon.lang._ + |import leon.collection._ + | + |object Foo { + | def unapply(i: BigInt): Option[BigInt] = if (i > 0) Some(i) else None() + |} + | + |object Unapply { + | def foo = + | (BigInt(1) match { + | case Foo(i) => i + | case _ => BigInt(0) + | }) + (BigInt(-12) match { + | case Foo(i) => i + | case _ => BigInt(2) + | }) + | + | def size[A](l: List[A]): BigInt = l match { + | case _ :: _ :: _ :: Nil() => 3 + | case _ :: _ :: Nil() => 2 + | case _ :: Nil() => 1 + | case Nil() => 0 + | case _ :: _ => 42 + | } + | + | def s1 = size(1 :: 2 :: 3 :: Nil[Int]()) + | def s2 = size(Nil[Int]()) + | def s3 = size(List(1,2,3,4,5,6,7,8)) + | + |} + """.stripMargin, + """object Casts1 { | abstract class Foo | case class Bar1(v: BigInt) extends Foo @@ -371,6 +403,15 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL { } } + test("Unapply") { implicit fix => + for(e <- allEvaluators) { + eval(e, fcall("Unapply.foo")()) === bi(3) + eval(e, fcall("Unapply.s1")()) === bi(3) + eval(e, fcall("Unapply.s2")()) === bi(0) + eval(e, fcall("Unapply.s3")()) === bi(42) + } + } + test("Casts1") { implicit fix => def bar1(es: Expr*) = cc("Casts1.Bar1")(es: _*) def bar2(es: Expr*) = cc("Casts1.Bar2")(es: _*)