From fe1158fedff529efbc86c5a8eadc623b58c9bdea Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 12 Jun 2015 01:32:17 +0200
Subject: [PATCH] Make Leon strings a bit more scala-friendly
---
library/lang/string/String.scala | 14 +++++++++++++-
.../leon/frontends/scalac/CodeExtraction.scala | 3 +++
2 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/library/lang/string/String.scala b/library/lang/string/String.scala
index e0a591f01..0a3e72bd1 100644
--- a/library/lang/string/String.scala
+++ b/library/lang/string/String.scala
@@ -3,9 +3,10 @@
package leon.lang.string
import leon.annotation._
+import leon.collection._
@library
-case class String(chars: leon.collection.List[Char]) {
+case class String(chars: List[Char]) {
def +(that: String): String = {
String(this.chars ++ that.chars)
}
@@ -13,4 +14,15 @@ case class String(chars: leon.collection.List[Char]) {
def size = chars.size
def length = size
+
+ @ignore
+ override def toString = {
+
+ "\""+charsToString(chars)+"\""
+ }
+ @ignore
+ def charsToString(chars: List[Char]): java.lang.String = chars match {
+ case Cons(h, t) => h + charsToString(t)
+ case Nil() => ""
+ }
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 0741d2b4b..101e572ee 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -721,6 +721,9 @@ trait CodeExtraction extends ASTExtractors {
val ctparamsMap = ctparams zip cd.tparams.map(_.tp)
for (d <- tmpl.body) d match {
+ case t if isIgnored(t.symbol) =>
+ //ignore
+
case ExFunctionDef(sym, tparams, params, _, body) =>
val fd = defsToDefs(sym)
--
GitLab