From fa6e5ee1b5bbbd87212105c8ffba289ce7f7896f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Thu, 9 Oct 2014 13:44:54 +0200
Subject: [PATCH] List literals
---
library/collection/List.scala | 5 +++
.../leon/frontends/scalac/ASTExtractors.scala | 11 +++++++
.../frontends/scalac/CodeExtraction.scala | 9 ++++++
.../scala/leon/purescala/PrettyPrinter.scala | 31 +++++++++++++------
src/main/scala/leon/purescala/TreeOps.scala | 12 +++----
5 files changed, 52 insertions(+), 16 deletions(-)
diff --git a/library/collection/List.scala b/library/collection/List.scala
index 521a573a1..26355f8e7 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -287,6 +287,11 @@ sealed abstract class List[T] {
}
+@ignore
+object List {
+ def apply[T](elems: T*): List[T] = ???
+}
+
@library
object ListOps {
def flatten[T](ls: List[List[T]]): List[T] = ls match {
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 559dc93a0..00f039d29 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -164,6 +164,17 @@ trait ASTExtractors {
}
}
+ object ExListLiteral {
+ def unapply(tree: Apply): Option[(Type, List[Tree])] = tree match {
+ case Apply(
+ TypeApply(ExSelected("leon", "collection", "List", "apply"), tpe :: Nil),
+ args) =>
+ Some((tpe.tpe, args))
+ case _ =>
+ None
+ }
+ }
+
object ExAssertExpression {
/** Extracts the 'assert' contract from an expression (only if it's the
* first call in the block). */
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 40e3a6117..b79616a39 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1378,6 +1378,15 @@ trait CodeExtraction extends ASTExtractors {
ArrayUpdated(rar, rk, rv)
+ case l @ ExListLiteral(tpe, elems) =>
+ val rtpe = extractType(l)
+ val cons = CaseClassType(libraryCaseClass(l.pos, "leon.collection.Cons"), Seq(rtpe));
+ val nil = CaseClassType(libraryCaseClass(l.pos, "leon.collection.Nil"), Seq(rtpe));
+
+ elems.foldRight(CaseClass(nil, Seq())) {
+ case (e, ls) => CaseClass(cons, Seq(extractTree(e), ls))
+ }
+
case chr @ ExCharLiteral(c) =>
CharLiteral(c)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index a00e2d245..fca74d262 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -13,7 +13,8 @@ import utils._
import java.lang.StringBuffer
import PrinterHelpers._
-import TreeOps.isStringLiteral
+import TreeOps.{isStringLiteral, isListLiteral}
+import TypeTreeOps.leastUpperBound
case class PrinterContext(
current: Tree,
@@ -230,17 +231,27 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
p"""|?($es)"""
}
case e @ CaseClass(cct, args) =>
-
- isStringLiteral(e) match {
- case Some(str) =>
- val q = '"';
- p"$q$str$q"
+ isListLiteral(e) match {
+ case Some((tpe, elems)) =>
+ val elemTps = leastUpperBound(elems.map(_.getType))
+ if (elemTps == Some(tpe)) {
+ p"List($elems)"
+ } else {
+ p"List[$tpe]($elems)"
+ }
case None =>
- if (cct.classDef.isCaseObject) {
- p"$cct"
- } else {
- p"$cct($args)"
+ isStringLiteral(e) match {
+ case Some(str) =>
+ val q = '"';
+ p"$q$str$q"
+
+ case None =>
+ if (cct.classDef.isCaseObject) {
+ p"$cct"
+ } else {
+ p"$cct($args)"
+ }
}
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index a98519e19..8e8b831ec 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1995,8 +1995,8 @@ object TreeOps {
val lib = inProgram(cct.classDef).library
if (Some(cct.classDef) == lib.String) {
- listLiteralToList(args(0)) match {
- case Some(chars) =>
+ isListLiteral(args(0)) match {
+ case Some((_, chars)) =>
val str = chars.map {
case CharLiteral(c) => Some(c)
case _ => None
@@ -2018,15 +2018,15 @@ object TreeOps {
None
}
- def listLiteralToList(e: Expr): Option[List[Expr]] = e match {
+ def isListLiteral(e: Expr): Option[(TypeTree, List[Expr])] = e match {
case CaseClass(cct, args) =>
val lib = inProgram(cct.classDef).library
if (Some(cct.classDef) == lib.Nil) {
- Some(Nil)
+ Some((cct.tps.head, Nil))
} else if (Some(cct.classDef) == lib.Cons) {
- listLiteralToList(args(1)).map { t =>
- args(0) :: t
+ isListLiteral(args(1)).map { case (_, t) =>
+ (cct.tps.head, args(0) :: t)
}
} else {
None
--
GitLab