Pretty-printing has priority issue for SeqIndex

[pieter-bos]

If I pretty-print an expression that indexes a sequence, where the sequence is not a simple expression, the requires parentheses around the sequence disappear:

function concatFirst(xs: Seq[Int], ys: Seq[Int]): Int { 
    (xs ++ ys)[0]
}

when parsed and pretty-printed (with viper.silver.ast.Node.toString) turns into:

function concatFirst(xs: Seq[Int], ys: Seq[Int]): Int
{
  xs ++ ys[0]
}

We (the VerCors team) use pretty printing to diagnose the output of VerCors in vscode quite often, so it would be nice if this can be fixed. Thanks!

Here is the code I used to parse+print the example for completeness sake

package viper.api

import viper.silver.frontend.{SilFrontend, SilFrontendConfig}
import viper.silver.verifier.{NoVerifier, Verifier}

import java.io.{File, FileOutputStream, OutputStreamWriter}

object EmptyFrontend extends SilFrontend() {
  val NO_VERIFIER = new NoVerifier

  override def createVerifier(fullCmd: String): Verifier = NO_VERIFIER
  override def configureVerifier(args: Seq[String]): SilFrontendConfig = ???
}

object TestSubscriptBug {
  def main(args: Array[String]): Unit = {
    val tmp = File.createTempFile("vercors-output-", ".sil")
    tmp.deleteOnExit()

    val writer = new OutputStreamWriter(new FileOutputStream(tmp))
    writer.write("""function concatFirst(xs: Seq[Int], ys: Seq[Int]): Int { (xs ++ ys)[0] }""")
    writer.close()

    val frontend = EmptyFrontend
    frontend.init(EmptyFrontend.NO_VERIFIER)
    frontend.reset(tmp.toPath)
    frontend.parsing()
    frontend.semanticAnalysis()
    frontend.translation()

    assert(frontend.errors.isEmpty)

    println(frontend.translationResult.toString())
  }
}

[JonasAlaif]

If this is a big issue for you I could just hardcode brackets around the lhs when prettyprinting (...)[0], but this would be ugly with simple cases such as seq[0] -> (seq)[0]. A proper fix would be to have a binding strength defined at each AST Node and pass that down when pretty printing, generating brackets only when binding_strength(current_ast_node) < parent_binding) - that might take some time to implement though.

[marcoeilers]

Silver's pretty printer actually has something like this implemented here:

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

Line 434 in 3039635

def noparens (inner : PrettyOperatorExpression, outer : PrettyOperatorExpression,

Not sure how easy it is to extend it to cover this case though. Seems like SeqAppend already implements PrettyOperatorExpression, so maybe it'd be enough to make SeqIndex implement it as well?

[marcoeilers]

Should be fixed in a03adc2