From 5df6c4bf5d083fb70e4ce07f6b0355d3d31766b2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 2 Dec 2015 13:59:36 +0100
Subject: [PATCH] Updated the way Leon renders strings

---
 library/lang/StrOps.scala                         | 11 ++++-------
 src/main/scala/leon/purescala/PrettyPrinter.scala | 10 +++++-----
 2 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/library/lang/StrOps.scala b/library/lang/StrOps.scala
index 2c04d5dc7..3a6cfdc32 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 307d83a4b..89b58f83c 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)"
-- 
GitLab