Only generate syntactic attributes for syntaxDefinition.kore

k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-11-spec.k.out

@@ -12,8 +12,8 @@
 #And
   <k>
     assignmentResult ( ( MAP
-    X:MyId |-> 1 ) [ Z:MyId <- 3 ]
-    Y:MyId |-> 2 ) ~> .K
+    X:MyId |-> 1
+    Y:MyId |-> 2 ) [ Z:MyId <- 3 ] ) ~> .K
   </k>
 #And
   {

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

@@ -239,10 +239,12 @@ public void convert(
     for (Production lesser : module.overloads().elements()) {
       overloads.addAll(module.overloads().relations().getOrDefault(lesser, Set.of()));
     }
-    translateSymbols(attributes, functionRules, overloads, semantics);
 
-    // print syntax definition
     syntax.append(semantics);
+    translateSymbols(attributes, functionRules, overloads, semantics, false);
+    translateSymbols(attributes, functionRules, overloads, syntax, true);
+
+    // print syntax definition
     for (Tuple2<Sort, scala.collection.immutable.List<Production>> sort :
         iterable(module.bracketProductionsFor())) {
       for (Production prod : iterable(sort._2())) {
@@ -252,7 +254,8 @@ public void convert(
             overloads,
             prod.att().get(Att.BRACKET_LABEL(), KLabel.class),
             prod,
-            syntax);
+            syntax,
+            true);
       }
     }
     for (Production prod : iterable(module.sortedProductions())) {
@@ -438,15 +441,17 @@ private void translateSymbols(
       Map<Att.Key, Boolean> attributes,
       SetMultimap<KLabel, Rule> functionRules,
       Set<Production> overloads,
-      StringBuilder sb) {
+      StringBuilder sb,
+      boolean withSyntaxAtts) {
     for (Production prod : iterable(module.sortedProductions())) {
       if (isBuiltinProduction(prod)) {
         continue;
       }
       if (prod.klabel().isEmpty()) {
         continue;
       }
-      translateSymbol(attributes, functionRules, overloads, prod.klabel().get(), prod, sb);
+      translateSymbol(
+          attributes, functionRules, overloads, prod.klabel().get(), prod, sb, withSyntaxAtts);
     }
   }
 
@@ -456,7 +461,8 @@ private void translateSymbol(
       Set<Production> overloads,
       KLabel label,
       Production prod,
-      StringBuilder sb) {
+      StringBuilder sb,
+      boolean withSyntaxAtts) {
     sb.append("  ");
     if (isFunction(prod) && isHook(prod)) {
       sb.append("hooked-");
@@ -475,7 +481,7 @@ private void translateSymbol(
     sb.append(") : ");
     convert(prod.sort(), prod, sb);
     sb.append(" ");
-    Att koreAtt = koreAttributes(prod, functionRules, overloads);
+    Att koreAtt = koreAttributes(prod, functionRules, overloads, withSyntaxAtts);
     convert(attributes, koreAtt, sb, null, null);
     sb.append("\n");
   }
@@ -1649,10 +1655,29 @@ private boolean isGeneratedInKeysOp(Production prod) {
   }
 
   private Att koreAttributes(
-      Production prod, SetMultimap<KLabel, Rule> functionRules, Set<Production> overloads) {
-    Att att = prod.att().remove(Att.CONSTRUCTOR()).remove(Att.HOOK()).remove(Att.FORMAT());
+      Production prod,
+      SetMultimap<KLabel, Rule> functionRules,
+      Set<Production> overloads,
+      boolean withSyntaxAtts) {
+    Att att = prod.att();
+    List<Att.Key> attsToRemove =
+        List.of(
+            // semantics
+            Att.CONSTRUCTOR(),
+            Att.HOOK(),
+            // syntax
+            Att.ASSOC(),
+            Att.BRACKET(),
+            Att.COLORS(),
+            Att.COMM(),
+            Att.FORMAT());
+    for (Att.Key key : attsToRemove) {
+      att = att.remove(key);
+    }
     att = att.addAll(semanticAttributes(prod, functionRules, overloads));
-    att = att.addAll(syntaxAttributes(prod));
+    if (withSyntaxAtts) {
+      att = att.addAll(syntaxAttributes(prod));
+    }
     return att;
   }
 
@@ -1730,6 +1755,14 @@ private Att syntaxAttributes(Production prod) {
 
     Att att = Att.empty();
     att = att.add(Att.FORMAT(), format);
+
+    List<Att.Key> attsToCopy = List.of(Att.ASSOC(), Att.BRACKET(), Att.COLORS(), Att.COMM());
+    for (Att.Key key : attsToCopy) {
+      if (prod.att().contains(key)) {
+        att = att.add(key, prod.att().get(key));
+      }
+    }
+
     if (prod.att().contains(Att.COLOR())) {
       String color = prod.att().get(Att.COLOR());
       boolean escape = false;