Parsing issues

Since we have a new implementation now, based on completely different data structures, we have to take advantage and rethink some of the parsing steps we used in SDF to parse rules.

This page tries to reference in a structured way all the issues and wiki pages currently on GitHub related to parsing and modularity:

1. Unique labels:
   #1839 Unrelated productions which had the same klabel, collided in the priority/associativity filter. We decided that we want to specify priorities external of blocks of syntax, by specifying tags or klabels: syntax priority '_*_ > '_+_. This ended up simplifying the KORE implementation but leaving out this small detail of having unique labels triggered some recurring bugs.

2. Overloaded productions:
   #1827 (examples of issues in Simple) Currently we're stuck porting examples because we haven't figured out a correct way to automatically subsort overloaded lists.
   #1772 (.K .Map .List) From #1733, I get that overloaded productions must have the same label, but all the dots in this issue have different klabels.
   #1705 (calculating automatic list subsorts) Currently done only for the parsing step. Still the issue persists when getting to the back-end.
   #1707 (List overloading, modules - again) Issue. Close when fixed.
   #1733 (proposed fix for semantic overloaded operators) Discussing possible solutions.
   Problem: we have two lists declarations

Exp  ::= Int
Ints ::= List{Int,","}
Exps ::= List{Exp,","}
Exps ::= Ints // needs to be added automatically
rule isExps(K) => true requires isInts(K) => true // alternative

and we want to automatically subsort the Ints list to Exps (second to last line). This is a lemma, or a theorem, that can be proved from the existing grammar. The problem is that if we add this production in place, the program parser will become ambiguous. The alternative solution would be to generate the predicate instead of the production which will get to the back-end without interfering with the parser. The subsort relation is still needed for sort inference in the rule parser, but that can be generated only for the rule parser.
Also, this can be extended to the more general case: G+G' where G' is a copy of G where each nonterminal Sort of G is replaced by a non-terminal Sort' (assume all productions have precisely the same corresponding KLabels). I'm not very clear on this but it's in the issue.
#1713 Close pull request and add a new/better fix.
Overloaded productions in K3 are handled as follows:

P1: S  ::= NT  T  [klabel(kl)]
P2: S' ::= NT' T' [klabel(kl')]
P1 < P2 iff S <= S' /\ NT <= NT' /\ T == T' /\ kl == kl'

During disambiguation, the parser may offer the following choice: amb(t1, t2) where t1 parsed with P1 and t2 with P2. Since I am trying to maximize the inferred sorts and terms all the time, I would eliminate t1 from the ambiguity since all the results will be included in t2. I always had the check kl == kl' for good measure, since we don't want to have interference between unrelated productions, but that always conflicted with the dots (. from .K, .Map, .List...) since they have different klabels.

Conclusion. After discussing with @dlucanu, we kind of tend to agree that we have to add automatically the inferred production Exps ::= Ints directly to the module, but annotate it with something, and exclude it when generating the program parser. We don't want it in the program parser, because it produces unwanted ambiguities, but we want it in the rest of the parsers and in the backend, because it helps with the sort inference.

3. Revise sort inference: #1587 (TODO) <:Sort needs to specify exactly the sort of the inner term, otherwise we can't disambiguate productions like ..
4. Disambiguation and modularity: #1647 (TODO)
5. Module system and module annotations: !!!-Module-System (TODO with Cosmin)