Merge remote-tracking branch 'origin/develop'

k-distribution/tests/regression-new/checkWarns/singletonOverload.k

@@ -1,11 +1,32 @@
 module SINGLETONOVERLOAD-SYNTAX
 endmodule
 
-module SINGLETONOVERLOAD
+module WARNS
   imports ID
 
   syntax LVal ::= L() [unused]
                 | LVal "." Id [unused, overload(_.)]
   syntax Exp  ::= LVal
                 | Exp  "." Id [unused, overload(_._)]
 endmodule
+
+module NOWARNS
+  imports BOOL
+
+  syntax Foo  ::= "foo" | "bar"
+  syntax Foos ::= List{Foo, ","}
+
+  syntax Bool ::= test(Foo)   [function, overload(test)]
+                | test(Foos)  [function, overload(test)]
+
+  rule test(foo) => true
+  rule test(bar) => false
+
+  rule test(F, Rest) => test(F) andBool test(Rest)
+  rule test(.Foos) => true
+endmodule
+
+module SINGLETONOVERLOAD
+  imports WARNS
+  imports NOWARNS
+endmodule

kernel/src/main/java/org/kframework/kompile/Kompile.java

@@ -3,7 +3,6 @@
 
 import static org.kframework.Collections.*;
 import static org.kframework.definition.Constructors.*;
-import static org.kframework.kore.KORE.*;
 
 import com.google.inject.Inject;
 import java.io.File;
@@ -634,12 +633,23 @@ public void structuralChecks(
   }
 
   private void checkSingletonOverload(Module module) {
-    var withOverload = module.productions().filter(p -> p.att().contains(Att.OVERLOAD())).toSeq();
+    // When disambiguating, an extra production `Es ::= E` is added for every user list
+    // sort `Es`.
+    //
+    // This means that productions that reference a user list sort (or the child sort of
+    // one) can behave as overloads at disambiguation, even if they look like singletons
+    // from the perspective. We therefore need to use the disambiguation module to implement this
+    // check.
+    //
+    // See `RuleGrammarGenerator::getCombinedGrammarImpl`.
+    var disambMod = RuleGrammarGenerator.getCombinedGrammarImpl(module, false, false, true)._2();
+    var withOverload =
+        disambMod.productions().filter(p -> p.att().contains(Att.OVERLOAD())).toSeq();
 
     stream(withOverload)
         .forEach(
             p -> {
-              if (!module.overloads().elements().contains(p)) {
+              if (!disambMod.overloads().elements().contains(p)) {
                 kem.registerCompilerWarning(
                     KException.ExceptionType.SINGLETON_OVERLOAD,
                     errors,

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

@@ -167,7 +167,7 @@ public Module getExtensionModule() {
     Module extM = extensionModule;
     if (extM == null) {
       Tuple3<Module, Module, Module> mods =
-          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner);
+          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner, false);
       extM = mods._1();
       disambModule = mods._2();
       parsingModule = mods._3();
@@ -180,7 +180,7 @@ public Module getParsingModule() {
     Module parseM = parsingModule;
     if (parseM == null) {
       Tuple3<Module, Module, Module> mods =
-          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner);
+          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner, false);
       extensionModule = mods._1();
       disambModule = mods._2();
       parseM = mods._3();
@@ -193,7 +193,7 @@ public Module getDisambiguationModule() {
     Module disambM = disambModule;
     if (disambM == null) {
       Tuple3<Module, Module, Module> mods =
-          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner);
+          RuleGrammarGenerator.getCombinedGrammarImpl(seedModule, isBison, forGlobalScanner, false);
       extensionModule = mods._1();
       disambM = mods._2();
       parsingModule = mods._3();

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

@@ -333,8 +333,25 @@ public static ParseInModule getCombinedGrammar(
         partialParseDebug);
   }
 
+  /**
+   * Generate the derived extension, disambiguation and parsing modules from a user module.
+   *
+   * <p>When performing different parts of the compilation pipeline, we need to use derived modules
+   * with different properties to the user-supplied source module. This method adds additional
+   * syntax to the user module to do so.
+   *
+   * <p>TODO: analysis of the properties of these modules: K Issue #1278
+   *
+   * @param mod The user module to transform.
+   * @param isBison If true, modules with the `not-lr1` attribute will be dropped.
+   * @param forGlobalScanner If false, only the public signature of the user module is considered
+   *     (i.e. private imports are dropped).
+   * @param subsortUserLists If true, a subsorting production `Es ::= E` is added to the
+   *     disambiguation module for each user list sort `Es`.
+   * @return A tuple `(extension, disambiguation, parsing)` of derived modules.
+   */
   public static Tuple3<Module, Module, Module> getCombinedGrammarImpl(
-      Module mod, boolean isBison, boolean forGlobalScanner) {
+      Module mod, boolean isBison, boolean forGlobalScanner, boolean subsortUserLists) {
     Set<Sentence> prods = new HashSet<>();
     Set<Sentence> extensionProds = new HashSet<>();
     Set<Sentence> disambProds;
@@ -730,7 +747,7 @@ public static Tuple3<Module, Module, Module> getCombinedGrammarImpl(
       parseProds = res;
     }
 
-    if (mod.importedModuleNames().contains(RULE_LISTS)) {
+    if (mod.importedModuleNames().contains(RULE_LISTS) || subsortUserLists) {
       Set<Sentence> res = new HashSet<>();
       for (UserList ul : UserList.getLists(parseProds)) {
         Production prod1;