From 1ddf072e372616c207c7326bc234ded939190662 Mon Sep 17 00:00:00 2001
From: Scott Guest <scott.guest@runtimeverification.com>
Date: Wed, 15 Nov 2023 15:04:47 +0200
Subject: [PATCH] Add `KItem` subsorts to the disambiguation module when
 parsing programs (#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.
---
 .../org/kframework/parser/inner/RuleGrammarGenerator.java     | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java
index 93163bba47b..bf15b74d1a1 100644
--- a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java
+++ b/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<>();