Term printer error

[msaaltink]

It is somewhat perplexing that these two expressions, with different types and structure, print almost exactly the same:

sawscript> {{ \ (x:Integer) -> [(x,x)] }}
[19:23:38.879] \(x : Prelude.Integer) -> [x,x]
sawscript> {{ \ (x:Integer) -> [x,x] }}
[19:23:49.800] \(x : Prelude.Integer) -> [x, x]

What happened to the parentheses around the tuple?

A very careful reader could check for whitespace after a comma to distinguish these two, but that's an easily missed distinction.

[brianhuffman]

This is probably just a mistake in the use of precedence levels in the saw-core pretty printer.

[msaaltink]

I occasionally see this in the let-binding list, but it seems hard to reproduce in a small example. Seen recently, in a large formula

x@44 = x@37,x@38,x@23

Not too bad here, but in another case there are line breaks coupled with an ill-chosen left margin:

  x@63 = x@60,
  [email protected] ([email protected] ([email protected] (x@59,x@60),x@55),[email protected] (x@62,x@62)),
  [email protected] ([email protected] (x@21,x@21),x@48)

To be sure, though, putting the parentheses in and indenting properly will do little to improve the readability of that!

[robdockins]

I bumped into this recently. I think the problem is here:

https://github.com/GaloisInc/saw-core/blob/ea914a9eea8e484189ee6e4c4dcdfc7db831d987/saw-core/src/Verifier/SAW/Term/Pretty.hs#L349

There should probably be a precendence level between None and whatever is next that corresponds to constructing the right-tail of a compound tuple so we don't forget to put the outermost parens around a tuple.