Add warning for syntax priority / associativity mismatch

USER_MANUAL.md

@@ -756,6 +756,13 @@ syntax left mult
 syntax right add
 ```
 
+Note that `syntax [left|right|non-assoc]` should not be used to group together
+productions with different priorities. For example, this code would be invalid:
+```k
+syntax priorities mult > add
+syntax left mult add
+```
+
 Note that there is one other way to describe associativity, but it is
 prone to a very common mistake. You can apply the attribute `left`, `right`,
 or `non-assoc` directly to a production to indicate that it is, by itself,

k-distribution/k-tutorial/1_basic/04_disambiguation/README.md

@@ -225,6 +225,17 @@ the productions with at least one of the attributes in that group, and each
 `syntax left`, `syntax right`, or `syntax non-assoc` sentence defines an
 associativity relation connecting all the productions with one of the target
 attributes together into a left-, right-, or non-associative grouping.
+Specifically, this means that:
+```
+syntax left a b
+```
+is _different_ to:
+```
+syntax left a
+syntax left b
+```
+As a consequence of this, `syntax [left|right|non-assoc]` should not be used to
+group together labels with different priority.
 
 ## Prefer/avoid
 

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

@@ -0,0 +1,10 @@
+module SYNTAXGROUPS-SYNTAX
+  syntax Exp  ::= Exp "*" Exp [times, unused]
+                > Exp "+" Exp [plus,  unused]
+
+  syntax left times plus
+endmodule
+
+module SYNTAXGROUPS
+  imports SYNTAXGROUPS-SYNTAX
+endmodule

k-distribution/tests/regression-new/checkWarns/syntaxGroups.k.out

@@ -0,0 +1,6 @@
+[Error] Compiler: Symbols _+__SYNTAXGROUPS-SYNTAX_Exp_Exp_Exp and _*__SYNTAXGROUPS-SYNTAX_Exp_Exp_Exp are in the same associativity group, but have different priorities.
+	Source(syntaxGroups.k)
+	Location(5,3,5,25)
+	5 |	  syntax left times plus
+	  .	  ^~~~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 1 structural errors.

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

@@ -0,0 +1,46 @@
+package org.kframework.compile.checks;
+
+import org.kframework.definition.Sentence;
+import org.kframework.definition.SyntaxAssociativity;
+import org.kframework.definition.Tag;
+import org.kframework.utils.errorsystem.KEMException;
+import org.kframework.utils.errorsystem.KException;
+import org.kframework.utils.errorsystem.KExceptionManager;
+import org.kframework.definition.Module;
+import static org.kframework.Collections.*;
+
+import java.util.List;
+import java.util.ArrayList;
+import java.util.Set;
+
+public class CheckSyntaxGroups {
+
+    private final Set<KEMException> errors;
+    private final KExceptionManager kem;
+    private final Module module;
+
+    public CheckSyntaxGroups(Set<KEMException> errors, Module module, KExceptionManager kem) {
+        this.errors = errors;
+        this.kem = kem;
+        this.module = module;
+    }
+
+    public void check(Sentence s) {
+        if(s instanceof SyntaxAssociativity) {
+            Set<Tag> tags = mutable(((SyntaxAssociativity) s).tags());
+            List<Tag> tagList = new ArrayList(tags);
+
+            for(int i = 0; i < tagList.size(); ++i) {
+                for(int j = i + 1; j < tagList.size(); ++j) {
+                    Tag t1 = tagList.get(i);
+                    Tag t2 = tagList.get(j);
+
+                    if(this.module.priorities().inSomeRelation(t1, t2)) {
+                        String message = "Symbols " + t1 + " and " + t2 + " are in the same associativity group, but have different priorities.";
+                        kem.registerCompilerWarning(KException.ExceptionType.INVALID_ASSOCIATIVITY, errors, message, s);
+                    }
+                }
+            }
+        }
+    }
+}

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

@@ -22,6 +22,7 @@
 import org.kframework.compile.checks.CheckRewrite;
 import org.kframework.compile.checks.CheckSortTopUniqueness;
 import org.kframework.compile.checks.CheckStreams;
+import org.kframework.compile.checks.CheckSyntaxGroups;
 import org.kframework.compile.checks.CheckTokens;
 import org.kframework.definition.*;
 import org.kframework.definition.Module;
@@ -491,6 +492,8 @@ public void structuralChecks(scala.collection.Set<Module> modules, Module mainMo
 
         stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckAnonymous(errors, m, kem)::check));
 
+        stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckSyntaxGroups(errors, m, kem)::check));
+
         Set<String> moduleNames = new HashSet<>();
         stream(modules).forEach(m -> {
             if (moduleNames.contains(m.name())) {

kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java

@@ -142,7 +142,7 @@ public org.kframework.definition.SyntaxAssociativity apply(PriorityExtendedAssoc
         scala.collection.Set<Tag> tags = toTags(ii.getTags(), ii);
         String assocOrig = ii.getAssoc();
         Associativity assoc = applyAssoc(assocOrig);
-        return SyntaxAssociativity(assoc, tags);
+        return SyntaxAssociativity(assoc, tags, convertAttributes(ii));
     }
 
     public Associativity applyAssoc(String assocOrig) {

kore/src/main/java/org/kframework/utils/errorsystem/KException.java

@@ -115,6 +115,7 @@ public enum ExceptionType {
         MISSING_SYNTAX_MODULE,
         INVALID_EXIT_CODE,
         INVALID_CONFIG_VAR,
+        INVALID_ASSOCIATIVITY,
         FUTURE_ERROR,
         UNUSED_VAR,
         PROOF_LINT,