From fc7e99bac1f44d54b9f4b685f935b558604f3ad4 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 14 Oct 2022 15:52:26 +0200 Subject: [PATCH 1/4] Actually enforce max line width and indent subexpressions in pretty printer --- .../silver/ast/pretty/PrettyPrinter.scala | 81 ++++++++++--------- 1 file changed, 42 insertions(+), 39 deletions(-) diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala index 6cc2f8484..72bb7c331 100644 --- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala +++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala @@ -373,6 +373,9 @@ trait FastPrettyPrinterBase extends PrettyPrintPrimitives { def <+> (dr : Cont) : Cont = dl <> space <> dr + def <++>(dr: Cont): Cont = + dl <> line <> dr + def <@> (dr: Cont) : Cont = if (dl == nil) dr else if (dr == nil) dl else dl <> line <> dr } @@ -526,10 +529,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 <> parens(showVars(formalArgs)) <> { if (formalReturns.isEmpty) nil - else nil <+> "returns" <+> parens(showVars(formalReturns)) - } <> + else nest(defaultIndent, nil <++> "returns" <+> parens(showVars(formalReturns))) + }) <> nest(defaultIndent, showContracts("requires", pres) <> showContracts("ensures", posts) @@ -574,7 +577,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. */ @@ -644,18 +647,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 @@ -727,7 +730,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter case PredicateAccess(params, predicateName) => text(predicateName) <> parens(ssep(params map show, char (',') <> space)) 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)) case Old(exp) => @@ -737,22 +740,22 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter case Let(v, exp, body) => parens(text("let") <+> text(v.name) <+> "==" <+> parens(show(exp)) <+> "in" <+> 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, group(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,13 +774,13 @@ 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)) case EmptySeq(elemTyp) => @@ -810,38 +813,38 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter 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 +889,6 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter toParenDoc(r) } - ld <+> text(b.op) <+> rd + group(ld <+> text(b.op) <++> rd) } } From 883a07956641886184b1c0d9c004618517ef4dbe Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 14 Oct 2022 20:03:04 +0200 Subject: [PATCH 2/4] Dropped unnecessary function, added potential line breaks for remaining cases --- .../silver/ast/pretty/PrettyPrinter.scala | 54 +++++++++---------- 1 file changed, 26 insertions(+), 28 deletions(-) diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala index 72bb7c331..54fdbdd11 100644 --- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala +++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala @@ -373,9 +373,6 @@ trait FastPrettyPrinterBase extends PrettyPrintPrimitives { def <+> (dr : Cont) : Cont = dl <> space <> dr - def <++>(dr: Cont): Cont = - dl <> line <> dr - def <@> (dr: Cont) : Cont = if (dl == nil) dr else if (dr == nil) dl else dl <> line <> dr } @@ -487,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 } @@ -529,9 +526,9 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter case Field(name, typ) => text("field") <+> name <> ":" <+> show(typ) case Method(name, formalArgs, formalReturns, pres, posts, body) => - group(text("method") <+> name <> parens(showVars(formalArgs)) <> { + group(text("method") <+> name <> nest(defaultIndent, parens(showVars(formalArgs))) <> { if (formalReturns.isEmpty) nil - else nest(defaultIndent, nil <++> "returns" <+> parens(showVars(formalReturns))) + else nest(defaultIndent, nil <@> "returns" <+> parens(showVars(formalReturns))) }) <> nest(defaultIndent, showContracts("requires", pres) <> @@ -548,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) <> @@ -591,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) @@ -728,26 +725,27 @@ 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) => 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) => - group(parens(show(cond) <+> "?" <> nest(defaultIndent, line <> 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) <+> "::" <> nest(defaultIndent, (if (triggers.isEmpty) nil else space <> ssep(triggers map show, space)) <+> - show(exp))) + show(exp))) case Forall(v, triggers, exp) => group(parens(text("forall") <+> showVars(v) <+> "::" <> - nest(defaultIndent, (if (triggers.isEmpty) nil else line <> ssep(triggers map show, group(line))) <++> + nest(defaultIndent, (if (triggers.isEmpty) nil else line <> ssep(triggers map show, line)) <@> show(exp)))) case ForPerm(vars, resource, exp) => group(parens(text("forperm") @@ -755,7 +753,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter <+> brackets(show(resource)) <+> "::" <+> show(exp)))) case InhaleExhaleExp(in, ex) => - group(brackets(show(in) <> char (',') <++> show(ex))) + group(brackets(show(in) <> char (',') <@> show(ex))) case WildcardPerm() => "wildcard" case FullPerm() => @@ -782,11 +780,11 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter else 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) => @@ -804,11 +802,11 @@ 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) <> "]()" @@ -819,15 +817,15 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter case ExplicitMultiset(elems) => text("Multiset") <> parens(ssep(elems map show, group(char (',') <> line))) case AnySetUnion(left, right) => - group(parens(show(left) <+> "union" <++> show(right))) + group(parens(show(left) <+> "union" <@> show(right))) case AnySetIntersection(left, right) => - group(parens(show(left) <+> "intersection" <++> show(right))) + group(parens(show(left) <+> "intersection" <@> show(right))) case AnySetSubset(left, right) => - group(parens(show(left) <+> "subset" <++> show(right))) + group(parens(show(left) <+> "subset" <@> show(right))) case AnySetMinus(left, right) => - group(parens(show(left) <+> "setminus" <++> show(right))) + group(parens(show(left) <+> "setminus" <@> show(right))) case AnySetContains(elem, s) => - group(parens(show(elem) <+> "in" <++> show(s))) + group(parens(show(elem) <+> "in" <@> show(s))) case AnySetCardinality(s) => surround(show(s),char ('|')) @@ -840,11 +838,11 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter case MapLookup(base, key) => show(base) <> brackets(show(key)) case MapContains(key, base) => - group(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) <> group(brackets(show(key) <+> ":=" <++> show(value))) + show(base) <> group(brackets(show(key) <+> ":=" <@> show(value))) case MapDomain(base) => text("domain") <> parens(show(base)) case MapRange(base) => @@ -889,6 +887,6 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter toParenDoc(r) } - group(ld <+> text(b.op) <++> rd) + group(ld <+> text(b.op) <@> rd) } } From c46cc87553ce172ab2819a071de39097cde12a2a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 14 Oct 2022 20:12:24 +0200 Subject: [PATCH 3/4] Fixed return parameter list --- src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala index 54fdbdd11..d896b93ee 100644 --- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala +++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala @@ -528,7 +528,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter case Method(name, formalArgs, formalReturns, pres, posts, body) => group(text("method") <+> name <> nest(defaultIndent, parens(showVars(formalArgs))) <> { if (formalReturns.isEmpty) nil - else nest(defaultIndent, nil <@> "returns" <+> parens(showVars(formalReturns))) + else nest(defaultIndent, line <> "returns" <+> parens(showVars(formalReturns))) }) <> nest(defaultIndent, showContracts("requires", pres) <> From ae365effe1a29cc8dcb0a5ed573916ceb47360ba Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 14 Oct 2022 20:58:01 +0200 Subject: [PATCH 4/4] Removing line breaks from directly pretty-printed expressions to fix Carbon --- src/main/scala/viper/silver/ast/Expression.scala | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala index 71c83a0ba..0a5422262 100644 --- a/src/main/scala/viper/silver/ast/Expression.scala +++ b/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)