runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
442 stars 145 forks source link

Inconsistency in `KLabel` on bracket productions #4434

Open tothtamas28 opened 2 months ago

tothtamas28 commented 2 months ago

Consider

module TEST
    syntax Foo ::= "foo"
    syntax Foo ::= "(" Foo ")" [bracket]
endmodule

In the kompiled definition, the production corresponding to the bracket has

If on the other hand symbol((_)) is added to the bracket production, the resulting production has

This discrepancy in KLabel seems arbitrary.

  1. Should we just drop bracketLabel, and assign a KLabel regardless of the presence of the symbol attribute?
  2. Alternatively, should we never attach a KLabel to a bracket production?

(Whatever solution we choose, an integration test should be added to pyk that checks the bracket production.)

Baltoli commented 2 months ago

The bracketLabel is only for unparsing; we probably want to keep that unconditionally and just disallow symbol + bracket.

Second part is to make sure bracketLabel is an output-only attribute. maybe not the case for Pyk, or have Pyk read syntaxDefinition.kore in the same way as the C++ implementation does.