diff --git a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-11-spec.k.out b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-11-spec.k.out
index 194b181bb6..e20ff09994 100644
--- a/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-11-spec.k.out
+++ b/k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-11-spec.k.out
@@ -12,8 +12,8 @@
#And
assignmentResult ( ( MAP
- X:MyId |-> 1 ) [ Z:MyId <- 3 ]
- Y:MyId |-> 2 ) ~> .K
+ X:MyId |-> 1
+ Y:MyId |-> 2 ) [ Z:MyId <- 3 ] ) ~> .K
#And
{
diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
index 6a932e9b83..ba37d97f09 100644
--- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
+++ b/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 :
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,7 +441,8 @@ private void translateSymbols(
Map attributes,
SetMultimap functionRules,
Set overloads,
- StringBuilder sb) {
+ StringBuilder sb,
+ boolean withSyntaxAtts) {
for (Production prod : iterable(module.sortedProductions())) {
if (isBuiltinProduction(prod)) {
continue;
@@ -446,7 +450,8 @@ private void translateSymbols(
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 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 functionRules, Set overloads) {
- Att att = prod.att().remove(Att.CONSTRUCTOR()).remove(Att.HOOK()).remove(Att.FORMAT());
+ Production prod,
+ SetMultimap functionRules,
+ Set overloads,
+ boolean withSyntaxAtts) {
+ Att att = prod.att();
+ List 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 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;