From 105e2905914ea18c087c50d329f350a6b987021d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 30 Oct 2012 15:53:23 +0100
Subject: [PATCH] Extract sys.error into purescala trees
---
src/main/scala/leon/plugin/CodeExtraction.scala | 4 ++++
src/main/scala/leon/plugin/Extractors.scala | 16 ++++++++++++++++
src/main/scala/leon/purescala/ScalaPrinter.scala | 2 +-
src/main/scala/leon/purescala/TreeOps.scala | 4 ++++
.../scala/leon/synthesis/FileInterface.scala | 2 +-
5 files changed, 26 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 8f48d8629..5ada9b223 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -534,6 +534,9 @@ 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 ExTupleExtract(tuple, index) => {
val tupleExpr = rec(tuple)
val TupleType(tpes) = tupleExpr.getType
@@ -1051,6 +1054,7 @@ trait CodeExtraction extends Extractors {
case tpe if tpe == IntClass.tpe => Int32Type
case tpe if tpe == BooleanClass.tpe => BooleanType
case tpe if tpe == UnitClass.tpe => UnitType
+ case tpe if tpe == NothingClass.tpe => BottomType
case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) => SetType(rec(btt))
case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) => MultisetType(rec(btt))
case TypeRef(_, sym, btt :: Nil) if isOptionClassSym(sym) => OptionType(rec(btt))
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 824519548..e736f7536 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -175,6 +175,22 @@ trait Extractors {
}
}
+ object ExIdNamed {
+ def unapply(id: Ident): Option[String] = Some(id.toString)
+ }
+ object ExNamed {
+ def unapply(name: Name): Option[String] = Some(name.toString)
+ }
+
+ 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)
+ case _ =>
+ None
+ }
+ }
+
object ExChooseExpression {
def unapply(tree: Apply) : Option[(List[(Type, Symbol)], Type, Tree, Tree)] = tree match {
case a @ Apply(
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 31f3e7305..fb1e14785 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -426,7 +426,7 @@ object ScalaPrinter {
case e @ Error(desc) => {
var nsb = sb
- nsb.append("error(\"" + desc + "\")")
+ nsb.append("sys.error(\"" + desc + "\")")
nsb
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 2b5cda8ed..d00857b9c 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1173,6 +1173,10 @@ object TreeOps {
(scrutinees.head, patterns.head)
}
+ // We use searchAndReplace to replace the biggest match first
+ // (topdown).
+ // So replaceing using Map(a => b, CC(a) => d) will replace
+ // "CC(a)" by "d" and not by "CC(b)"
val newThen = searchAndReplace(substMap.get)(then)
MatchExpr(scrutinee, Seq(SimpleCase(pattern, newThen), SimpleCase(WildcardPattern(None), elze)))
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index ad19ba6c7..b76184182 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -14,7 +14,7 @@ class FileInterface(reporter: Reporter, origFile: File) {
origFile.getAbsolutePath() match {
case FileExt(path, "scala") =>
var i = 0
- def savePath = path+"."+i+".scala"
+ def savePath = path+".scala."+i
while (new File(savePath).isFile()) {
i += 1
}
--
GitLab