Add KItem subsorts to the disambiguation module when parsing progra…

…ms (#3814)

Previously, when parsing programs, the subsort declarations `syntax
KItem ::= Sort` were only added to the parsing module. However, sort
inference is run in the disambiguation module, so they should be
included there as well.

This is necessary for #3601.

kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java

@@ -569,10 +569,12 @@ public static Tuple3<Module, Module, Module> getCombinedGrammarImpl(
       // if no start symbol has been defined in the configuration, then use K
       for (Sort srt : iterable(mod.allSorts())) {
         if (!isParserSort(srt) && !mod.listSorts().contains(srt)) {
-          // K ::= Sort
+          // KItem ::= Sort
           prods3.add(Production(Seq(), Sorts.KItem(), Seq(NonTerminal(srt)), Att()));
         }
       }
+      // Add KItem subsorts to disambiguation for use by sort inference
+      disambProds.addAll(prods3);
       // for each triple, generate a new pattern which works better for parsing lists in programs.
       prods3.addAll(new HashSet<>(parseProds));
       Set<Sentence> res = new HashSet<>();