From dd5e6f79eec4d1f46383c3639e9502d8ccc02807 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 15 Apr 2016 22:42:33 +0200
Subject: [PATCH] improve printing blocks
---
.../frontends/scalac/CodeExtraction.scala | 3 +-
.../scala/leon/purescala/PrettyPrinter.scala | 5 +++
src/main/scala/leon/xlang/Constructors.scala | 36 +++++++++++++++++++
src/main/scala/leon/xlang/Expressions.scala | 4 +--
4 files changed, 45 insertions(+), 3 deletions(-)
create mode 100644 src/main/scala/leon/xlang/Constructors.scala
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 0a80b3b53..4efc43706 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -25,6 +25,7 @@ import ExprOps._
import TypeOps.{leastUpperBound, typesCompatible, typeParamsOf, canBeSubtypeOf}
import xlang.Expressions.{Block => LeonBlock, _}
import xlang.ExprOps._
+import xlang.Constructors.{block => leonBlock}
import leon.utils.{Position => LeonPosition, OffsetPosition => LeonOffsetPosition, RangePosition => LeonRangePosition, Bijection, DefinedPosition}
@@ -1916,7 +1917,7 @@ trait CodeExtraction extends ASTExtractors {
rest match {
case Some(r) =>
- LeonBlock(Seq(res), extractTree(r))
+ leonBlock(Seq(res, extractTree(r)))
case None =>
res
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 0dbf1aba9..04e32eb31 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -633,6 +633,7 @@ class PrettyPrinter(opts: PrinterOptions,
protected def noBracesSub(e: Expr): Seq[Expr] = e match {
case Assert(_, _, bd) => Seq(bd)
case Let(_, _, bd) => Seq(bd)
+ case xlang.Expressions.LetVar(_, _, bd) => Seq(bd)
case LetDef(_, bd) => Seq(bd)
case LetPattern(_, _, bd) => Seq(bd)
case Require(_, bd) => Seq(bd)
@@ -646,6 +647,10 @@ class PrettyPrinter(opts: PrinterOptions,
case (e: Expr, Some(within: Expr)) if noBracesSub(within) contains e => false
case (_: Expr, Some(_: MatchCase)) => false
case (_: LetDef, Some(_: LetDef)) => false
+ case (_: Expr, Some(_: xlang.Expressions.Block)) => false
+ case (_: xlang.Expressions.Block, Some(_: xlang.Expressions.While)) => false
+ case (_: xlang.Expressions.Block, Some(_: FunDef)) => false
+ case (_: xlang.Expressions.Block, Some(_: LetDef)) => false
case (e: Expr, Some(_)) => true
case _ => false
}
diff --git a/src/main/scala/leon/xlang/Constructors.scala b/src/main/scala/leon/xlang/Constructors.scala
new file mode 100644
index 000000000..c55842f92
--- /dev/null
+++ b/src/main/scala/leon/xlang/Constructors.scala
@@ -0,0 +1,36 @@
+package leon
+package xlang
+
+import purescala.Expressions._
+import purescala.Types._
+import xlang.Expressions._
+import xlang.ExprOps._
+
+object Constructors {
+
+ def block(exprs: Seq[Expr]): Expr = {
+ require(exprs.nonEmpty)
+
+ val flat = exprs.flatMap{
+ case Block(es2, el) => es2 :+ el
+ case e2 => Seq(e2)
+ }
+
+ val init = flat.init
+ val last = flat.last
+ val filtered = init.filter{
+ case UnitLiteral() => false
+ case _ => true
+ }
+
+ val finalSeq =
+ if(last == UnitLiteral() && filtered.last.getType == UnitType) filtered else (filtered :+ last)
+
+ finalSeq match {
+ case Seq() => UnitLiteral()
+ case Seq(e) => e
+ case es => Block(es.init, es.last)
+ }
+ }
+
+}
diff --git a/src/main/scala/leon/xlang/Expressions.scala b/src/main/scala/leon/xlang/Expressions.scala
index c0e2d4deb..e8dd17c3d 100644
--- a/src/main/scala/leon/xlang/Expressions.scala
+++ b/src/main/scala/leon/xlang/Expressions.scala
@@ -50,7 +50,7 @@ object Expressions {
}
def printWith(implicit pctx: PrinterContext) {
- p"$varId = $expr;"
+ p"$varId = $expr"
}
}
@@ -62,7 +62,7 @@ object Expressions {
}
def printWith(implicit pctx: PrinterContext) {
- p"${obj}.${varId} = ${expr};"
+ p"${obj}.${varId} = ${expr}"
}
}
--
GitLab