diff --git a/library/lang/StrOps.scala b/library/lang/StrOps.scala index 2c04d5dc7fc7cede6018c66e10653eef24b9d43e..3a6cfdc324b14c175062cd49ba4fc5473cfaa011 100644 --- a/library/lang/StrOps.scala +++ b/library/lang/StrOps.scala @@ -18,22 +18,19 @@ object StrOps { def substring(a: String, start: BigInt, end: BigInt): String = { if(start > end || start >= length(a) || end <= 0) "" else a.substring(start.toInt, end.toInt) } - @ignore + @library def bigIntToString(a: BigInt): String = { a.toString } - @ignore + @library def intToString(a: Int): String = { a.toString } - @ignore - def doubleToString(a: Double): String = { - a.toString - } + @library def booleanToString(a: Boolean): String = { if(a) "true" else "false" } - @ignore + @library def charToString(a: Char): String = { a.toString } diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala index 307d83a4bbf0d8b36bb4aba3c203e860e3af75be..89b58f83ce45af7ee5845def6ae0dff636d6967b 100644 --- a/src/main/scala/leon/purescala/PrettyPrinter.scala +++ b/src/main/scala/leon/purescala/PrettyPrinter.scala @@ -167,11 +167,11 @@ class PrettyPrinter(opts: PrinterOptions, case Equals(l,r) => optP { p"$l == $r" } - case Int32ToString(expr) => p"StrOps.intToString($expr)" - case BooleanToString(expr) => p"StrOps.booleanToString($expr)" - case IntegerToString(expr) => p"StrOps.bigIntToString($expr)" - case CharToString(expr) => p"StrOps.charToString($expr)" - case RealToString(expr) => p"StrOps.realToString($expr)" + case Int32ToString(expr) => p"$expr.toString" + case BooleanToString(expr) => p"$expr.toString" + case IntegerToString(expr) => p"$expr.toString" + case CharToString(expr) => p"$expr.toString" + case RealToString(expr) => p"$expr.toString" case StringConcat(lhs, rhs) => optP { p"$lhs + $rhs" } case SubString(expr, start, end) => p"StrOps.substring($expr, $start, $end)"