Skip to content

Commit

Permalink
Refactor addKoreAttributes (#4145)
Browse files Browse the repository at this point in the history 
Preparatory refactoring for:
* #4134

Changes:
* Extract method `semanticAttributes`
* Extract method `syntaxAttributes`
* Several small changes
  • Loading branch information
@tothtamas28
tothtamas28 committed Apr 2, 2024
1 parent 050837a commit 953b0b9
Showing 1 changed file with 76 additions and 66 deletions.
142 changes: 76 additions & 66 deletions kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
View file
Expand Up @@ -298,7 +298,7 @@ public void convert(
if (isFunction(prod) && prod.att().contains(Att.UNIT())) {
genUnitAxiom(prod, semantics);
}
if (isFunctional(prod, functionRules)) {
if (isFunctional(prod)) {
genFunctionalAxiom(prod, semantics);
}
if (isConstructor(prod, functionRules)) {
Expand Down Expand Up @@ -458,7 +458,7 @@ private void translateSymbol(
Production prod,
StringBuilder sb) {
sb.append(" ");
if (isFunction(prod) && prod.att().contains(Att.HOOK()) && isRealHook(prod.att())) {
if (isFunction(prod) && isHook(prod)) {
sb.append("hooked-");
}
sb.append("symbol ");
Expand All @@ -475,7 +475,7 @@ private void translateSymbol(
sb.append(") : ");
convert(prod.sort(), prod, sb);
sb.append(" ");
Att koreAtt = addKoreAttributes(prod, functionRules, overloads);
Att koreAtt = koreAttributes(prod, functionRules, overloads);
convert(attributes, koreAtt, sb, null, null);
sb.append("\n");
}
Expand Down Expand Up @@ -930,16 +930,6 @@ private void genOverloadedAxiom(Production lesser, Production greater, StringBui
sb.append(" // overloaded production\n");
}

private boolean isRealHook(Att att) {
String hook = att.get(Att.HOOK());
return Stream.concat(Hooks.namespaces.stream(), options.hookNamespaces.stream())
.anyMatch(ns -> hook.startsWith(ns + "."));
}

private static boolean isBuiltinProduction(Production prod) {
return prod.klabel().nonEmpty() && ConstructorChecks.isBuiltinLabel(prod.klabel().get());
}

public String convertSpecificationModule(
Module definition, Module spec, SentenceType defaultSentenceType, StringBuilder sb) {
SentenceType sentenceType = getSentenceType(spec.att()).orElse(defaultSentenceType);
Expand Down Expand Up @@ -1625,13 +1615,30 @@ private void convertParams(Option<KLabel> maybeKLabel, boolean hasR, StringBuild
}

private boolean isConstructor(Production prod, SetMultimap<KLabel, Rule> functionRules) {
Att att = addKoreAttributes(prod, functionRules, java.util.Collections.emptySet());
Att att = semanticAttributes(prod, functionRules, java.util.Collections.emptySet());
return att.contains(Att.CONSTRUCTOR());
}

private boolean isFunctional(Production prod, SetMultimap<KLabel, Rule> functionRules) {
Att att = addKoreAttributes(prod, functionRules, java.util.Collections.emptySet());
return att.contains(Att.FUNCTIONAL());
private static boolean isFunctional(Production prod) {
return !isFunction(prod) || prod.att().contains(Att.TOTAL());
}

private static boolean isFunction(Production prod) {
return prod.att().contains(Att.FUNCTION());
}

private boolean isHook(Production prod) {
return prod.att().contains(Att.HOOK()) && isRealHook(prod.att());
}

private boolean isRealHook(Att att) {
String hook = att.get(Att.HOOK());
return Stream.concat(Hooks.namespaces.stream(), options.hookNamespaces.stream())
.anyMatch(ns -> hook.startsWith(ns + "."));
}

private static boolean isBuiltinProduction(Production prod) {
return prod.klabel().nonEmpty() && ConstructorChecks.isBuiltinLabel(prod.klabel().get());
}

private boolean isGeneratedInKeysOp(Production prod) {
Expand All @@ -1641,9 +1648,16 @@ private boolean isGeneratedInKeysOp(Production prod) {
return (!prod.klabel().isEmpty());
}

private Att addKoreAttributes(
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());
att = att.addAll(semanticAttributes(prod, functionRules, overloads));
att = att.addAll(syntaxAttributes(prod));
return att;
}

private Att semanticAttributes(
Production prod, SetMultimap<KLabel, Rule> functionRules, Set<Production> overloads) {
boolean isFunctional = !isFunction(prod) || prod.att().contains(Att.TOTAL());
boolean isConstructor = !isFunction(prod);
isConstructor &= !prod.att().contains(Att.ASSOC());
isConstructor &= !prod.att().contains(Att.COMM());
Expand All @@ -1667,14 +1681,14 @@ private Att addKoreAttributes(
isConstructor &= !isMacro;
isConstructor &= !isAnywhere;

Att att = prod.att().remove(Att.CONSTRUCTOR());
if (att.contains(Att.HOOK()) && !isRealHook(att)) {
att = att.remove(Att.HOOK());
Att att = Att.empty();
if (isHook(prod)) {
att = att.add(Att.HOOK(), prod.att().get(att.HOOK()));
}
if (isConstructor) {
att = att.add(Att.CONSTRUCTOR());
}
if (isFunctional) {
if (isFunctional(prod)) {
att = att.add(Att.FUNCTIONAL());
}
if (isAnywhere) {
Expand All @@ -1686,10 +1700,13 @@ private Att addKoreAttributes(
if (isMacro) {
att = att.add(Att.MACRO());
}
return att;
}

private Att syntaxAttributes(Production prod) {
// update format attribute with structure expected by backend
String format = att.getOptional(Att.FORMAT()).orElse(prod.defaultFormat());
String format = prod.att().getOptional(Att.FORMAT()).orElse(prod.defaultFormat());
int nt = 1;
boolean hasFormat = true;

for (int i = 0; i < prod.items().size(); i++) {
if (prod.items().apply(i) instanceof NonTerminal) {
Expand All @@ -1707,48 +1724,45 @@ private Att addKoreAttributes(
.replace("%", "%%")
+ "%r");
} else {
hasFormat = false;
return Att.empty();
}
}
if (hasFormat) {
att = att.add(Att.FORMAT(), format);
if (att.contains(Att.COLOR())) {
boolean escape = false;
StringBuilder colors = new StringBuilder();
String conn = "";
for (int i = 0; i < format.length(); i++) {
if (escape && format.charAt(i) == 'c') {
colors.append(conn).append(att.get(Att.COLOR()));
conn = ",";
}
escape = format.charAt(i) == '%';
}
att = att.add(Att.COLORS(), colors.toString());
}
StringBuilder sb = new StringBuilder();
for (ProductionItem pi : iterable(prod.items())) {
if (pi instanceof NonTerminal) {
sb.append('0');
} else {
sb.append('1');

Att att = Att.empty();
att = att.add(Att.FORMAT(), format);
if (prod.att().contains(Att.COLOR())) {
String color = prod.att().get(Att.COLOR());
boolean escape = false;
StringBuilder colors = new StringBuilder();
String conn = "";
for (int i = 0; i < format.length(); i++) {
if (escape && format.charAt(i) == 'c') {
colors.append(conn).append(color);
conn = ",";
}
escape = format.charAt(i) == '%';
}
att = att.add(Att.TERMINALS(), sb.toString());
if (prod.klabel().isDefined()) {
att = att.add(Att.PRIORITIES(), KList.class, getPriorities(prod.klabel().get()));
att =
att.add(
Att.LEFT_INTERNAL(),
KList.class,
getAssoc(module.leftAssoc(), prod.klabel().get()));
att =
att.add(
Att.RIGHT_INTERNAL(),
KList.class,
getAssoc(module.rightAssoc(), prod.klabel().get()));
att = att.add(Att.COLORS(), colors.toString());
}
StringBuilder sb = new StringBuilder();
for (ProductionItem pi : iterable(prod.items())) {
if (pi instanceof NonTerminal) {
sb.append('0');
} else {
sb.append('1');
}
} else {
att = att.remove(Att.FORMAT());
}
att = att.add(Att.TERMINALS(), sb.toString());
if (prod.klabel().isDefined()) {
att = att.add(Att.PRIORITIES(), KList.class, getPriorities(prod.klabel().get()));
att =
att.add(
Att.LEFT_INTERNAL(), KList.class, getAssoc(module.leftAssoc(), prod.klabel().get()));
att =
att.add(
Att.RIGHT_INTERNAL(),
KList.class,
getAssoc(module.rightAssoc(), prod.klabel().get()));
}
return att;
}
Expand Down Expand Up @@ -1781,10 +1795,6 @@ private KList getAssoc(scala.collection.Set<Tuple2<Tag, Tag>> assoc, KLabel klab
.collect(Collectors.toList()));
}

private boolean isFunction(Production prod) {
return prod.att().contains(Att.FUNCTION());
}

// Assume that there is no quantifiers
private Set<KVariable> collectLHSFreeVariables(K requires, K left) {
Set<KVariable> res = new HashSet<>();
Expand Down

0 comments on commit 953b0b9

Please sign in to comment.