diff --git a/library/lang/string/String.scala b/library/lang/string/String.scala index e0a591f011a0035dba2fb0ad4398e4db27632526..0a3e72bd1a6f234a79eba234a646b2c0844ecfaf 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 0741d2b4bfa2131c7445c5638ac330c578763c06..101e572ee83f3d41c1978e385730e98453615e2b 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)