Skip to content

Breaking up long lines when pretty-printing #616

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
marcoeilers merged 5 commits into from
Oct 18, 2022
Merged

Breaking up long lines when pretty-printing #616

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
fc7e99b
Actually enforce max line width and indent subexpressions in pretty p…
marcoeilers Oct 14, 2022
883a079
Dropped unnecessary function, added potential line breaks for remaini…
marcoeilers Oct 14, 2022
c46cc87
Fixed return parameter list
marcoeilers Oct 14, 2022
ae365ef
Removing line breaks from directly pretty-printed expressions to fix …
marcoeilers Oct 14, 2022
360cc44
Merge branch 'master' into meilers_pretty_printer_linebreaks
jcp19 Oct 18, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions src/main/scala/viper/silver/ast/Expression.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
101 changes: 51 additions & 50 deletions src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

Expand Down Expand Up @@ -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)
Expand All @@ -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) <>
Expand All @@ -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. */
Expand All @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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() =>
Expand All @@ -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) =>
Expand All @@ -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) =>
Expand Down Expand Up @@ -886,6 +887,6 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
toParenDoc(r)
}

ld <+> text(b.op) <+> rd
group(ld <+> text(b.op) <@> rd)
}
}
⚡