Merge pull request #616 from viperproject/meilers_pretty_printer_linebreaks

Breaking up long lines when pretty-printing

Author: marcoeilers

src/main/scala/viper/silver/ast/Expression.scala

@@ -47,6 +47,13 @@ sealed trait Exp extends Hashable with Typed with Positioned with Infoed with Tr
    */
  // lazy val proofObligations = Expressions.proofObligations(this)
 
+  override def toString() = {
+   // Carbon relies on expression pretty-printing resulting in a string without line breaks,
+   // so for the special case of directly converting an expression to a string,, we remove all line breaks
+   // the pretty printer might have inserted.
+   super.toString.replaceAll("\n", " ")
+ }
+
 }
 
 // --- Simple integer and boolean expressions (binary and unary operations, literals)

src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala

@@ -484,7 +484,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
     case v: LocalVarDecl => showVar(v)
     case dm: DomainMember => showDomainMember(dm)
     case Trigger(exps) =>
-      text("{") <+> ssep(exps map show, char (',')) <+> "}"
+      text("{") <+> ssep(exps map show, group(char (',') <> line)) <+> "}"
     case null => uninitialized
   }
 
@@ -526,10 +526,10 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
       case Field(name, typ) =>
         text("field") <+> name <> ":" <+> show(typ)
       case Method(name, formalArgs, formalReturns, pres, posts, body) =>
-        text("method") <+> name <> parens(showVars(formalArgs)) <> {
+        group(text("method") <+> name <> nest(defaultIndent, parens(showVars(formalArgs))) <> {
           if (formalReturns.isEmpty) nil
-          else nil <+> "returns" <+> parens(showVars(formalReturns))
-        } <>
+          else nest(defaultIndent, line <> "returns" <+> parens(showVars(formalReturns)))
+        }) <>
           nest(defaultIndent,
             showContracts("requires", pres) <>
             showContracts("ensures", posts)
@@ -545,12 +545,12 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
               ) <> line)
           })
       case Predicate(name, formalArgs, body) =>
-        text("predicate") <+> name <> parens(showVars(formalArgs)) <+> (body match {
+        text("predicate") <+> name <> nest(defaultIndent, parens(showVars(formalArgs))) <+> (body match {
           case None => nil
           case Some(exp) => braces(nest(defaultIndent, line <> show(exp)) <> line)
         })
       case Function(name, formalArgs, typ, pres, posts, optBody) =>
-        text("function") <+> name <> parens(showVars(formalArgs)) <>
+        text("function") <+> name <> nest(defaultIndent, parens(showVars(formalArgs))) <>
           ":" <+> show(typ) <>
           nest(defaultIndent,
             showContracts("requires", pres) <>
@@ -574,7 +574,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
     if (contracts == null)
       line <> name <+> uninitialized
     else
-      lineIfSomeNonEmpty(contracts) <> ssep(contracts map (text(name) <+> show(_)), line)
+      lineIfSomeNonEmpty(contracts) <> ssep(contracts.map(c => text(name) <+> nest(defaultIndent, show(c))), line)
   }
 
   /** Returns `n` lines if at least one element of `s` is non-empty, and an empty document otherwise. */
@@ -588,7 +588,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
   }
 
   /** Show a list of formal arguments. */
-  def showVars(vars: Seq[AnyLocalVarDecl]): Cont = ssep(vars map showVar, char (',') <> space)
+  def showVars(vars: Seq[AnyLocalVarDecl]): Cont = ssep(vars map showVar, group(char (',') <> line))
   /** Show a variable name with the type of the variable (e.g. to be used in formal argument lists). */
   def showVar(v: AnyLocalVarDecl): Cont = v match {
     case l: LocalVarDecl => text(l.name) <> ":" <+> showType(l.typ)
@@ -644,18 +644,18 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
     val stmtDoc = stmt match {
       case NewStmt(target, fields) =>
         show(target) <+> ":=" <+> "new(" <> ssep(fields map (f => value(f.name)), char(',') <> space) <> ")"
-      case LocalVarAssign(lhs, rhs) => show(lhs) <+> ":=" <+> show(rhs)
-      case FieldAssign(lhs, rhs) => show(lhs) <+> ":=" <+> show(rhs)
-      case Fold(e) => text("fold") <+> show(e)
-      case Unfold(e) => text("unfold") <+> show(e)
+      case LocalVarAssign(lhs, rhs) => show(lhs) <+> ":=" <+> nest(defaultIndent, show(rhs))
+      case FieldAssign(lhs, rhs) => show(lhs) <+> ":=" <+> nest(defaultIndent, show(rhs))
+      case Fold(e) => text("fold") <+> nest(defaultIndent, show(e))
+      case Unfold(e) => text("unfold") <+> nest(defaultIndent, show(e))
       case Package(e, proofScript) => text("package") <+> show(e) <+> showBlock(proofScript)
-      case Apply(e) => text("apply") <+> show(e)
-      case Inhale(e) => text("inhale") <+> show(e)
-      case Assume(e) => text("assume") <+> show(e)
-      case Exhale(e) => text("exhale") <+> show(e)
-      case Assert(e) => text("assert") <+> show(e)
+      case Apply(e) => text("apply") <+> nest(defaultIndent, show(e))
+      case Inhale(e) => text("inhale") <+> nest(defaultIndent, show(e))
+      case Assume(e) => text("assume") <+> nest(defaultIndent, show(e))
+      case Exhale(e) => text("exhale") <+> nest(defaultIndent, show(e))
+      case Assert(e) => text("assert") <+> nest(defaultIndent, show(e))
       case MethodCall(mname, args, targets) =>
-        val call = text(mname) <> parens(ssep(args map show, char(',') <> space))
+        val call = text(mname) <> nest(defaultIndent, parens(ssep(args map show, group(char(',') <> line))))
         targets match {
           case Nil => call
           case _ => ssep(targets map show, char(',') <> space) <+> ":=" <+> call
@@ -725,34 +725,35 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
     case FieldAccess(rcv, field) =>
       show(rcv) <> "." <> field.name
     case PredicateAccess(params, predicateName) =>
-      text(predicateName) <> parens(ssep(params map show, char (',') <> space))
+      text(predicateName) <> parens(ssep(params map show, group(char (',') <> line)))
     case Unfolding(acc, exp) =>
-      parens(text("unfolding") <+> show(acc) <+> "in" <+> show(exp))
+      group(parens(text("unfolding") <+> nest(defaultIndent, show(acc)) <+> "in" <> nest(defaultIndent, line <> show(exp))))
     case Applying(wand, exp) =>
-      parens(text("applying") <+> show(wand) <+> "in" <+> show(exp))
+      parens(text("applying") <+> nest(defaultIndent, show(wand)) <+> "in" <> nest(defaultIndent, line <> show(exp)))
     case Old(exp) =>
       text("old") <> parens(show(exp))
     case LabelledOld(exp,label) =>
       text("old") <> brackets(label) <> parens(show(exp))
     case Let(v, exp, body) =>
-      parens(text("let") <+> text(v.name) <+> "==" <+> parens(show(exp)) <+> "in" <+> show(body))
+      parens(text("let") <+> text(v.name) <+> "==" <> nest(defaultIndent, line <> parens(show(exp))) <+>
+        "in" <> nest(defaultIndent, line <> show(body)))
     case CondExp(cond, thn, els) =>
-      parens(show(cond) <+> "?" <+> show(thn) <+> ":" <+> show(els))
+      group(parens(show(cond) <+> "?" <> nest(defaultIndent, line <> show(thn) <+> ":" <@> show(els))))
     case Exists(v, triggers, exp) =>
       parens(text("exists") <+> showVars(v) <+> "::" <>
-        (if (triggers.isEmpty) nil else space <> ssep(triggers map show, space)) <+>
-        show(exp))
+        nest(defaultIndent, (if (triggers.isEmpty) nil else space <> ssep(triggers map show, space)) <+>
+          show(exp)))
     case Forall(v, triggers, exp) =>
-      parens(text("forall") <+> showVars(v) <+> "::" <>
-        (if (triggers.isEmpty) nil else space <> ssep(triggers map show, space)) <+>
-        show(exp))
+      group(parens(text("forall") <+> showVars(v) <+> "::" <>
+        nest(defaultIndent, (if (triggers.isEmpty) nil else line <> ssep(triggers map show, line)) <@>
+          show(exp))))
     case ForPerm(vars, resource, exp) =>
-      parens(text("forperm")
-        <+> showVars(vars)
-        <+> brackets(show(resource)) <+> "::" <+> show(exp))
+      group(parens(text("forperm")
+        <> nest(defaultIndent, line <> showVars(vars)
+          <+> brackets(show(resource)) <+> "::" <+> show(exp))))
 
     case InhaleExhaleExp(in, ex) =>
-      brackets(show(in) <> char (',') <+> show(ex))
+      group(brackets(show(in) <> char (',') <@> show(ex)))
     case WildcardPerm() =>
       "wildcard"
     case FullPerm() =>
@@ -771,19 +772,19 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
     case AccessPredicate(loc, perm) =>
       text("acc") <> parens(show(loc) <> "," <+> show(perm))
     case FuncApp(funcname, args) =>
-      text(funcname) <> parens(ssep(args map show, char (',') <> space))
+      text(funcname) <> parens(ssep(args map show, group(char (',') <> line)))
     case dfa@DomainFuncApp(funcname, args, tvMap) =>
       if (tvMap.nonEmpty)
         // Type may be underconstrained, so to be safe we explicitly print out the type.
-        parens(text(funcname) <> parens(ssep(args map show, char (',') <> space)) <> char(':') <+> show(dfa.typ))
+        parens(text(funcname) <> parens(ssep(args map show, group(char (',') <> line))) <> char(':') <+> show(dfa.typ))
       else
-        text(funcname) <> parens(ssep(args map show, char (',') <> space))
+        text(funcname) <> parens(ssep(args map show, group(char (',') <> line)))
     case BackendFuncApp(func, args) =>
-      text(func.name) <> parens(ssep(args map show, char(',') <> space))
+      text(func.name) <> parens(ssep(args map show, group(char(',') <> line)))
     case EmptySeq(elemTyp) =>
       text("Seq[") <> showType(elemTyp) <> "]()"
     case ExplicitSeq(elems) =>
-      text("Seq") <> parens(ssep(elems map show, char (',') <> space))
+      text("Seq") <> parens(ssep(elems map show, group(char (',') <> line)))
     case RangeSeq(low, high) =>
       text("[") <> show(low) <> ".." <> show(high) <> ")"
     case si@SeqIndex(seq: PrettyOperatorExpression, idx) =>
@@ -801,47 +802,47 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
     case SeqDrop(seq, n) =>
       show(seq) <> brackets(show(n) <> "..")
     case SeqUpdate(seq, idx, elem) =>
-      show(seq) <> brackets(show(idx) <+> ":=" <+> show(elem))
+      show(seq) <> group(brackets(show(idx) <+> ":=" <@> show(elem)))
     case SeqLength(seq) =>
       surround(show(seq),char ('|'))
     case SeqContains(elem, seq) =>
-      parens(show(elem) <+> "in" <+> show(seq))
+      group(parens(show(elem) <+> "in" <@> show(seq)))
 
     case EmptySet(elemTyp) =>
       text("Set[") <> showType(elemTyp) <> "]()"
     case ExplicitSet(elems) =>
-      text("Set") <> parens(ssep(elems map show, char (',') <> space))
+      text("Set") <> parens(ssep(elems map show, group(char (',') <> line)))
     case EmptyMultiset(elemTyp) =>
       text("Multiset[") <> showType(elemTyp) <> "]()"
     case ExplicitMultiset(elems) =>
-      text("Multiset") <> parens(ssep(elems map show, char (',') <> space))
+      text("Multiset") <> parens(ssep(elems map show, group(char (',') <> line)))
     case AnySetUnion(left, right) =>
-      parens(show(left) <+> "union" <+> show(right))
+      group(parens(show(left) <+> "union" <@> show(right)))
     case AnySetIntersection(left, right) =>
-      parens(show(left) <+> "intersection" <+> show(right))
+      group(parens(show(left) <+> "intersection" <@> show(right)))
     case AnySetSubset(left, right) =>
-      parens(show(left) <+> "subset" <+> show(right))
+      group(parens(show(left) <+> "subset" <@> show(right)))
     case AnySetMinus(left, right) =>
-      parens(show(left) <+> "setminus" <+> show(right))
+      group(parens(show(left) <+> "setminus" <@> show(right)))
     case AnySetContains(elem, s) =>
-      parens(show(elem) <+> "in" <+> show(s))
+      group(parens(show(elem) <+> "in" <@> show(s)))
     case AnySetCardinality(s) =>
       surround(show(s),char ('|'))
 
     case EmptyMap(keyType, valueType) =>
       text("Map") <> brackets(showType(keyType) <> "," <> showType(valueType)) <> "()"
     case ExplicitMap(elems) =>
-      text("Map") <> parens(ssep(elems map show, char(',') <> space))
+      text("Map") <> parens(ssep(elems map show, group(char(',') <> line)))
     case Maplet(key, value) =>
       show(key) <+> ":=" <+> show(value)
     case MapLookup(base, key) =>
       show(base) <> brackets(show(key))
     case MapContains(key, base) =>
-      parens(show(key) <+> "in" <+> show(base))
+      group(parens(show(key) <+> "in" <@> show(base)))
     case MapCardinality(base) =>
       surround(show(base), char('|'))
     case MapUpdate(base, key, value) =>
-      show(base) <> brackets(show(key) <+> ":=" <+> show(value))
+      show(base) <> group(brackets(show(key) <+> ":=" <@> show(value)))
     case MapDomain(base) =>
       text("domain") <> parens(show(base))
     case MapRange(base) =>
@@ -886,6 +887,6 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
           toParenDoc(r)
       }
 
-    ld <+> text(b.op) <+> rd
+    group(ld <+> text(b.op) <@> rd)
   }
 }