From c691fe522450077dc8b036a6cb648f5d24f1c16d Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <ekneuss@gmail.com> Date: Wed, 22 Apr 2015 15:11:47 +0200 Subject: [PATCH] Fix printing of empty lists, simplify printing of bigints --- .../scala/leon/purescala/PrettyPrinter.scala | 16 ++++++++-------- src/main/scala/leon/purescala/ScalaPrinter.scala | 1 + 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala index f5b82b8f4..44d4e90bf 100644 --- a/src/main/scala/leon/purescala/PrettyPrinter.scala +++ b/src/main/scala/leon/purescala/PrettyPrinter.scala @@ -235,18 +235,18 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe isListLiteral(e) match { case Some((tpe, elems)) => val chars = elems.collect{case CharLiteral(ch) => ch} - if (chars.length == elems.length) { + if (chars.length == elems.length && tpe == CharType) { // String literal val str = chars mkString "" val q = '"' p"$q$str$q" - } - - val elemTps = leastUpperBound(elems.map(_.getType)) - if (elemTps == Some(tpe)) { - p"List($elems)" } else { - p"List[$tpe]($elems)" + val elemTps = leastUpperBound(elems.map(_.getType)) + if (elemTps == Some(tpe)) { + p"List($elems)" + } else { + p"List[$tpe]($elems)" + } } case None => @@ -268,7 +268,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe case BVUMinus(expr) => p"-$expr" case Equals(l,r) => optP { p"$l == $r" } case IntLiteral(v) => p"$v" - case InfiniteIntegerLiteral(v) => p"BigInt($v)" + case InfiniteIntegerLiteral(v) => p"$v" case CharLiteral(v) => p"$v" case BooleanLiteral(v) => p"$v" case UnitLiteral() => p"()" diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala index f1d191196..eeca5d984 100644 --- a/src/main/scala/leon/purescala/ScalaPrinter.scala +++ b/src/main/scala/leon/purescala/ScalaPrinter.scala @@ -52,6 +52,7 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex case SetDifference(l,r) => p"$l -- $r" case SetIntersection(l,r) => p"$l & $r" case SetCardinality(s) => p"$s.size" + case InfiniteIntegerLiteral(v) => p"BigInt($v)" case a@FiniteArray(elems, oDef, size) => { import ExprOps._ -- GitLab