Merge branch 'develop' into deprecate-symbol-klabel

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

k-distribution/tests/regression-new/issue-4114-overload-injection/1.test

@@ -0,0 +1 @@
+test(foo)

k-distribution/tests/regression-new/issue-4114-overload-injection/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  true ~> .K
+</k>

k-distribution/tests/regression-new/issue-4114-overload-injection/Makefile

@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/issue-4114-overload-injection/test.k

@@ -0,0 +1,12 @@
+module TEST
+  imports DOMAINS
+
+  syntax Foo ::= "foo"
+  syntax Bar ::= Foo | "bar"
+
+  syntax Bool ::= test(Foo) [function, overload(test)]
+                | test(Bar) [function, overload(test)]
+
+  rule test(foo) => true
+  rule test(_)   => false
+endmodule

kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

@@ -897,21 +897,33 @@ private void genOverloadedAxiom(Production lesser, Production greater, StringBui
       }
       conn = ",";
     }
-    sb.append("), inj{");
-    convert(lesser.sort(), lesser, sb);
-    sb.append(", ");
-    convert(greater.sort(), greater, sb);
-    sb.append("} (");
+
+    if (greater.sort().equals(lesser.sort())) {
+      sb.append("), ");
+    } else {
+      sb.append("), inj{");
+      convert(lesser.sort(), lesser, sb);
+      sb.append(", ");
+      convert(greater.sort(), greater, sb);
+      sb.append("} (");
+    }
+
     convert(lesser.klabel().get(), lesser, sb);
     sb.append("(");
+
     conn = "";
     for (int i = 0; i < lesser.nonterminals().size(); i++) {
       sb.append(conn);
       sb.append("K").append(i).append(":");
       convert(lesser.nonterminal(i).sort(), lesser, sb);
       conn = ",";
     }
-    sb.append("))) ");
+
+    if (greater.sort().equals(lesser.sort())) {
+      sb.append(")) ");
+    } else {
+      sb.append("))) ");
+    }
     final var args = KList(KApply(greater.klabel().get()), KApply(lesser.klabel().get()));
     final var att = Att.empty().add(Att.SYMBOL_OVERLOAD(), KList.class, args);
     convert(new HashMap<>(), att, sb, null, null);

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;