Merge remote-tracking branch 'origin/develop'

k-distribution/tests/regression-new/checks/checkNoSymbolOverload.k

@@ -0,0 +1,13 @@
+module CHECKNOSYMBOLOVERLOAD-SYNTAX
+endmodule
+
+module CHECKNOSYMBOLOVERLOAD
+  syntax LVal
+  syntax RVal
+  syntax Val ::= LVal | RVal
+  syntax Exp ::= Val
+
+  syntax RVals ::= RVal [overload(arg)]
+  syntax Vals  ::= Val  [overload(arg), symbol(val)]
+  syntax Exps  ::= Exp  [overload(arg)]
+endmodule

k-distribution/tests/regression-new/checks/checkNoSymbolOverload.k.out

@@ -0,0 +1,11 @@
+[Error] Compiler: Production would not be a KORE symbol and therefore cannot be overloaded. Add a `symbol(_)` attribute to the production.
+	Source(checkNoSymbolOverload.k)
+	Location(10,20,10,40)
+	10 |	  syntax RVals ::= RVal [overload(arg)]
+	   .	                   ^~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Production would not be a KORE symbol and therefore cannot be overloaded. Add a `symbol(_)` attribute to the production.
+	Source(checkNoSymbolOverload.k)
+	Location(12,20,12,40)
+	12 |	  syntax Exps  ::= Exp  [overload(arg)]
+	   .	                   ^~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 2 structural errors.

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/Makefile

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

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/exps.test

@@ -0,0 +1 @@
+rv(0), rv(1), rv(2), (1, 2)

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/exps.test.out

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

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/rvals.test

@@ -0,0 +1 @@
+rv(0), rv(1), rv(2)

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/rvals.test.out

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

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/test.k

@@ -0,0 +1,39 @@
+module TEST
+  imports DOMAINS
+
+  syntax LVal ::= lv(Int) | lv(Id)
+  syntax RVal ::= rv(Int)
+  syntax Val  ::= LVal | RVal
+
+  syntax Exp  ::= Int
+                | Id
+                | Val
+                | "(" Exp ")" [bracket]
+                > left:
+                  Exp "," Exp [group(comma)]
+
+  syntax RVals ::= RVal           [overload(arg),  group(assignExp), symbol(rval), avoid]
+                 | RVals "," RVal [overload(exps), group(assignExp)]
+
+  syntax Vals  ::= Val            [overload(arg),  group(assignExp), symbol(val),  avoid]
+                 | Vals "," Val   [overload(exps), group(assignExp)]
+
+  syntax Exps  ::= Exp            [overload(arg),  group(assignExp), symbol(exp),  avoid]
+                 | Exps "," Exp   [overload(exps), group(assignExp)]
+
+  syntax Exps ::= Vals
+  syntax Vals ::= RVals
+
+  syntax priority assignExp > comma
+
+  syntax KItem ::= "rvals"
+                 | "vals"
+                 | "exps"
+
+  configuration
+    <k> $PGM:Exps </k>
+
+  rule _:RVals => rvals
+  rule _:Vals  => vals
+  rule _:Exps  => exps  [owise]
+endmodule

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/vals.test

@@ -0,0 +1 @@
+rv(0), lv(x), rv(2)

k-distribution/tests/regression-new/issue-4142-no-symbol-overload/vals.test.out

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

kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java

@@ -73,6 +73,7 @@ private void checkProduction(Production prod) {
     checkSymbolKLabel(prod);
     checkKLabelOverload(prod);
     checkNullarySymbol(prod);
+    checkNoSymbolOverload(prod);
   }
 
   private <T extends HasAtt & HasLocation> void checkUnrecognizedAtts(T term) {
@@ -360,6 +361,15 @@ private void checkKLabelOverload(Production prod) {
     }
   }
 
+  private void checkNoSymbolOverload(Production prod) {
+    if (prod.klabel().isEmpty() && prod.att().contains(Att.OVERLOAD())) {
+      errors.add(
+          KEMException.compilerError(
+              "Production would not be a KORE symbol and therefore cannot be overloaded. Add a `symbol(_)` attribute to the production.",
+              prod));
+    }
+  }
+
   private void checkNullarySymbol(Production prod) {
     if (prod.att().contains(Att.SYMBOL()) && !prod.att().contains(Att.KLABEL())) {
       if (prod.att().get(Att.SYMBOL()).isEmpty()) {