diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index c7cc6a103c5d62a3ac523fe3a092edf6d6180833..78b75cf4600f6906ebf03ff33333d7a8fc2c9a92 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -763,8 +763,32 @@ trait CodeExtraction extends Extractors {
case ExEmptyMap(ft, tt) => {
val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
- EmptyMap(fromUnderlying, toUnderlying).setType(MapType(fromUnderlying, toUnderlying))
+ val tpe = MapType(fromUnderlying, toUnderlying)
+
+ EmptyMap(fromUnderlying, toUnderlying).setType(tpe)
+ }
+ case ExLiteralMap(ft, tt, elems) => {
+ val fromUnderlying = scalaType2PureScala(unit, silent)(ft.tpe)
+ val toUnderlying = scalaType2PureScala(unit, silent)(tt.tpe)
+ val tpe = MapType(fromUnderlying, toUnderlying)
+
+ if (elems.isEmpty) {
+ EmptyMap(fromUnderlying, toUnderlying).setType(tpe)
+ } else {
+ val singletons = elems.collect { case ExTuple(tpes, trees) if (trees.size == 2) =>
+ SingletonMap(rec(trees(0)), rec(trees(1))).setType(tpe)
+ }
+
+
+ if (singletons.size != elems.size) {
+ unit.error(nextExpr.pos, "Some map elements could not be extracted as Tuple2")
+ throw ImpureCodeEncounteredException(nextExpr)
+ }
+
+ FiniteMap(singletons).setType(tpe)
+ }
}
+
case ExSetMin(t) => {
val set = rec(t)
if(!set.getType.isInstanceOf[SetType]) {
@@ -1009,7 +1033,6 @@ trait CodeExtraction extends Extractors {
// default behaviour is to complain :)
case _ => {
if(!silent) {
- println(tr)
reporter.info(tr.pos, "Could not extract as PureScala.", true)
}
throw ImpureCodeEncounteredException(tree)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 8b3eebd4b27da35614412acaad96428477311278..978b6d8337b44f71c07592e8c13601acf4e65662 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -20,30 +20,41 @@ trait Extractors {
private lazy val multisetTraitSym = definitions.getClass("scala.collection.immutable.Multiset")
private lazy val optionClassSym = definitions.getClass("scala.Option")
- object StructuralExtractors {
- object ScalaPredef {
- /** Extracts method calls from scala.Predef. */
- def unapply(tree: Select): Option[String] = tree match {
- case Select(Select(This(scalaName),predefName),symName)
- if("scala".equals(scalaName.toString) && "Predef".equals(predefName.toString)) =>
- Some(symName.toString)
- case _ => None
+ object ExtractorHelpers {
+ object ExIdNamed {
+ def unapply(id: Ident): Option[String] = Some(id.toString)
+ }
+ object ExNamed {
+ def unapply(name: Name): Option[String] = Some(name.toString)
+ }
+
+ object ExSelected {
+ def unapplySeq(select: Select): Option[Seq[String]] = select match {
+ case Select(This(scalaName), name) =>
+ Some(Seq(scalaName.toString, name.toString))
+
+ case Select(from: Select, name) =>
+ unapplySeq(from).map(prefix => prefix :+ name.toString)
+
+ case Select(from: Ident, name) =>
+ Some(Seq(from.toString, name.toString))
+
+ case _ =>
+ None
}
}
+ }
+
+ object StructuralExtractors {
+ import ExtractorHelpers._
object ExEnsuredExpression {
/** Extracts the 'ensuring' contract from an expression. */
def unapply(tree: Apply): Option[(Tree,Symbol,Tree)] = tree match {
- case Apply(
- Select(
- Apply(
- TypeApply(
- ScalaPredef("any2Ensuring"),
- TypeTree() :: Nil),
- body :: Nil),
- ensuringName),
+ case Apply(Select(Apply(TypeApply(ExSelected("scala", "Predef", "any2Ensuring"), TypeTree() :: Nil),
+ body :: Nil), ExNamed("ensuring")),
(Function((vd @ ValDef(_, _, _, EmptyTree)) :: Nil, contractBody)) :: Nil)
- if("ensuring".equals(ensuringName.toString)) => Some((body, vd.symbol, contractBody))
+ => Some((body, vd.symbol, contractBody))
case _ => None
}
}
@@ -62,7 +73,7 @@ trait Extractors {
/** Extracts the 'require' contract from an expression (only if it's the
* first call in the block). */
def unapply(tree: Block): Option[(Tree,Tree)] = tree match {
- case Block(Apply(ScalaPredef("require"), contractBody :: Nil) :: rest, body) =>
+ case Block(Apply(ExSelected("scala", "Predef", "require"), contractBody :: Nil) :: rest, body) =>
if(rest.isEmpty)
Some((body,contractBody))
else
@@ -147,6 +158,7 @@ trait Extractors {
}
object ExpressionExtractors {
+ import ExtractorHelpers._
//object ExLocalFunctionDef {
// def unapply(tree: Block): Option[(DefDef,String,Seq[ValDef],Tree,Tree,Tree)] = tree match {
@@ -175,16 +187,9 @@ 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, Type)] = tree match {
- case a @ Apply(TypeApply(Select(Select(ExIdNamed("leon"), ExNamed("Utils")), ExNamed("error")), List(tpe)), List(lit : Literal)) =>
+ case a @ Apply(TypeApply(ExSelected("leon", "Utils", "error"), List(tpe)), List(lit : Literal)) =>
Some((lit.value.stringValue, tpe.tpe))
case _ =>
None
@@ -291,6 +296,10 @@ trait Extractors {
case TypeRef(_, sym, List(t1, t2, t3, t4, t5)) => Some((Seq(t1, t2, t3, t4, t5), Seq(e1, e2, e3, e4, e5)))
case _ => None
}
+ // Match e1 -> e2
+ case Apply(TypeApply(Select(Apply(TypeApply(ExSelected("scala", "Predef", "any2ArrowAssoc"), List(tpeFrom)), List(from)), ExNamed("$minus$greater")), List(tpeTo)), List(to)) =>
+
+ Some((Seq(tpeFrom.tpe, tpeTo.tpe), Seq(from, to)))
case _ => None
}
}
@@ -570,20 +579,22 @@ trait Extractors {
}
}
+ object ExLiteralMap {
+ def unapply(tree: Apply): Option[(Tree, Tree, Seq[Tree])] = tree match {
+ case Apply(TypeApply(ExSelected("scala", "Predef", "Map", "apply"), fromTypeTree :: toTypeTree :: Nil), args) =>
+ Some((fromTypeTree, toTypeTree, args))
+ case _ =>
+ None
+ }
+ }
object ExEmptyMap {
- def unapply(tree: TypeApply): Option[(Tree,Tree)] = tree match {
- case TypeApply(
- Select(
- Select(
- Select(
- Select(Ident(s), collectionName),
- immutableName),
- mapName),
- emptyName), fromTypeTree :: toTypeTree :: Nil) if (
- collectionName.toString == "collection" && immutableName.toString == "immutable" && mapName.toString == "Map" && emptyName.toString == "empty"
- ) => Some((fromTypeTree, toTypeTree))
- case TypeApply(Select(Select(Select(This(scalaName), predefName), mapName), emptyName), fromTypeTree :: toTypeTree :: Nil) if (scalaName.toString == "scala" && predefName.toString == "Predef" && emptyName.toString == "empty") => Some((fromTypeTree, toTypeTree))
- case _ => None
+ def unapply(tree: TypeApply): Option[(Tree, Tree)] = tree match {
+ case TypeApply(ExSelected("scala", "collection", "immutable", "Map", "empty"), fromTypeTree :: toTypeTree :: Nil) =>
+ Some((fromTypeTree, toTypeTree))
+ case TypeApply(ExSelected("scala", "Predef", "Map", "empty"), fromTypeTree :: toTypeTree :: Nil) =>
+ Some((fromTypeTree, toTypeTree))
+ case _ =>
+ None
}
}
diff --git a/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala b/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dab0d37412a50b2db1293391dc955c4cf7df9dbb
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala
@@ -0,0 +1,21 @@
+object LiteralMaps {
+ def test(): Map[Int, Int] = {
+ Map(1 -> 2, 3 -> 4, (5, 6))
+ }
+
+ def test2(): (Int, Int) = {
+ 1 -> 2
+ }
+
+ def test3(): Map[Int, Int] = {
+ Map()
+ }
+
+ def test4(): Map[Int, Int] = {
+ Map.empty[Int, Int]
+ }
+
+ def test5(): Map[Int, Int] = {
+ Map.empty[Int, Int]
+ }
+}