From e95b7dc47e15a30f54fe92698d51e319769133a2 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 30 Oct 2012 16:51:21 +0100
Subject: [PATCH] Extract leon.Utils.error[T] calls correctly
---
src/main/scala/leon/plugin/CodeExtraction.scala | 4 ++--
src/main/scala/leon/plugin/Extractors.scala | 6 +++---
testcases/Errors.scala | 6 ++++++
3 files changed, 11 insertions(+), 5 deletions(-)
create mode 100644 testcases/Errors.scala
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 5ada9b223..67071a6d0 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -534,8 +534,8 @@ trait CodeExtraction extends Extractors {
val tupleType = TupleType(tupleExprs.map(expr => bestRealType(expr.getType)))
Tuple(tupleExprs).setType(tupleType)
}
- case ExErrorExpression(str) =>
- Error(str).setType(scalaType2PureScala(unit, silent)(nextExpr.tpe))
+ case ExErrorExpression(str, tpe) =>
+ Error(str).setType(scalaType2PureScala(unit, silent)(tpe))
case ExTupleExtract(tuple, index) => {
val tupleExpr = rec(tuple)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index e736f7536..8b3eebd4b 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -183,9 +183,9 @@ trait Extractors {
}
object ExErrorExpression {
- def unapply(tree: Apply) : Option[String] = tree match {
- case a @ Apply(Select(Select(Select(ExIdNamed("scala"), ExNamed("sys")), ExNamed("package")), ExNamed("error")), List(lit : Literal)) =>
- Some(lit.value.stringValue)
+ def unapply(tree: Apply) : Option[(String, Type)] = tree match {
+ case a @ Apply(TypeApply(Select(Select(ExIdNamed("leon"), ExNamed("Utils")), ExNamed("error")), List(tpe)), List(lit : Literal)) =>
+ Some((lit.value.stringValue, tpe.tpe))
case _ =>
None
}
diff --git a/testcases/Errors.scala b/testcases/Errors.scala
new file mode 100644
index 000000000..b6d7dc74e
--- /dev/null
+++ b/testcases/Errors.scala
@@ -0,0 +1,6 @@
+import leon.Utils._
+
+object Errors {
+ def a(a: Int): Int = error[Int]("This is an error")
+}
+
--
GitLab