Recommendation for handling comments?

[FedericoPonzi]

I think/hope this is the last big issue I should be facing :) I'd like to know if there is a recommended strategy for handling comments.

In the TLA's AST, the comments are attached to the first node right after the comment. When building the Doc of that node, I'll first prefix the comment to it. In TLA+ specs people like to make comment blocks like this: (from file: TowerOfHanoi.tla)

(***************************************************************************)
(* TRUE iff i is a power of two                                            *)
(***************************************************************************)
PowerOfTwo(i) == i & (i-1) = 0

This is problematic because the comment block gets included as a text in the same group that contains PowerOfTwo. This causes the formatter to produce:

(***************************************************************************)
  (* TRUE iff i is a power of two                                            *)
  (***************************************************************************)
  PowerOfTwo(i) == i & ( i - 1 ) = 0

Do you have any recommendation on how to best handle this? According to https://prettier.io/docs/rationale.html it's also a challenge for prettier.

Update: this commit seems to be working for tlaplus-formatter though I haven't tested it a lot: main...FedericoPonzi:prettier4j:issue-156

[DavidGregory084]

Hmm that's interesting, can you describe what the Doc AST looks like in this scenario?

I don't think we should need to add any new primitives to prettier4j to handle this - each line of the comment should be a single Doc.text element (preferably trimmed of any whitespace) separated by hard Doc.lines.

[DavidGregory084]

In the TLA's AST, the comments are attached to the first node right after the comment. When building the Doc of that node, I'll first prefix the comment to it.

This is useful context - what I would suggest is that the top-level node could be something along these lines:

Doc.intersperse(Doc.line(), <a list of Doc.text comment lines followed by your declaration node Doc>)

In general, I would suggest that you try to push down group and indent to the elements that need to be able to flatten onto one line and to be subject to indentation.

I don't think that you want the comment lines to attempt to flatten onto one line (unless you are doing something advanced like reflowing comments), so they shouldn't be part of the group.

Each group introduces a choice about layout, so the more groups that you use, the more alternative layouts prettier4j needs to consider.

As a result, I tend to use group only around argument lists, control structures, and other elements that need to "break open" when they are too long for a single line.

For indentation, I am not so familiar with how TLA+ is normally formatted, but there are some examples of using prettier4j in one of my personal repositories here and here.

As you can see, I tend to use indent implicitly via bracket, so new indented scopes are usually introduced only with syntactic elements that introduce indentation.

One thing that catches me out frequently is that the lineOr element before a new indented scope must belong to that indented document. That is the motivation for the indented helper in the MetaNodePrinter.

[FedericoPonzi]

I see, then I've been too generous with my groups :) but the reason why I was thinking of a new api is the following scenario:

if condition {
// this is a very long comment that breaks the max width
if a { 1 } else {  3 }
} else {
condition
}

Assuming that I've put the body of the if in a group: Doc.group(buildThenBody(node)), then the if a inside the body will end up wrapped because the width of the body is broken by the inline comment - that's my understanding. I'll need some time to experiment with what you shared (I haven't tried intersperse before), I'll share an update later

[FedericoPonzi]

By the way, can you please publish a new version when you have a moment? I can then bump the library version to use the align combinator.

[DavidGregory084]

Assuming that I've put the body of the if in a group: Doc.group(buildThenBody(node)), then the if a inside the body will end up wrapped because the width of the body is broken by the inline comment - that's my understanding.

I think that if there is a hard line after your long comment, then there will be no need to break open the if, because the line position will be reset. I presume you will have to add hard lines after line comments in any case to ensure that you don't accidentally comment out code. 😁

By the way, can you please publish a new version when you have a moment?

Yep no prob, 0.3.2 is on its way to Central now 👍