Uniqueness of `symbol` not enforced

[tothtamas28]

kast.md defines #Top as

k/k-distribution/include/kframework/builtin/kast.md

Line 141 in 01b4a38

syntax {Sort} Sort ::= "#Top" [klabel(#Top), symbol, group(mlUnary)]

and #True as

k/k-distribution/include/kframework/builtin/kast.md

Line 143 in 01b4a38

| "#True" [klabel(#Top), symbol, group(mlUnary), unparseAvoid]

(Similarly for #Bottom and #False.)

Both productions have the same klabel and are symbol-s. However, according to the K User Manual,

The symbol provided must be unique to this definition. This is enforced by K.

In this case, it is not enforced. As a consequence, there are productions in compiled.json that have the same klabel (field, not the attribute), which makes processing productions more difficult.

---

Possible fixes:

1. [If this is a bug] Add the missing check for symbol uniqueness. Drop #True and #False as they do not seem to be indispensable.
2. [If this is a feature] Adjust the documentation. Add a new kompiler pass that eliminates the duplicate production from compiled.json.

[Baltoli]

These are special-cased because there are multiple ways to write the symbols; this is for historical compatibility. We should be able to drop #True and #False and similar cases then make the check stricter. Possible that we rely on this somewhere, so be careful when removing cases.

Trickiest case is the empty K sequence; we are definitely using this.

[Baltoli]

There is a consensus among the K development team that we should standardise on .K as the canonical unit element of K sequences, and deprecate .. This will require a migration process for downstream code.

[Baltoli]

Blocked on actually removing . in favour of .K; that's a pretty breaking change so I want to leave warnings on for a little while before doing so. Once it's gone, we can finish removing the special-casing.