Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Refactor addKoreAttributes #4145

Merged
merged 14 commits into from Apr 2, 2024
Merged

Refactor addKoreAttributes #4145

Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
f770709
Extract method `syntaxAttributes`
tothtamas28 Mar 28, 2024
7a9bdc1
Eliminate `hasFormat`
tothtamas28 Mar 28, 2024
384d100
Reverse call between `addKoreAttributes` and `isFunctional`
tothtamas28 Mar 28, 2024
a6aaeb7
Slide `isFunction`
tothtamas28 Mar 28, 2024
a10f98c
Add `HOOK`
tothtamas28 Mar 28, 2024
1b37469
Extract method `isHook`
tothtamas28 Mar 28, 2024
2f3d597
Group calls to `remove`
tothtamas28 Mar 28, 2024
02e1f87
Slide statement
tothtamas28 Mar 28, 2024
901166f
Slide methods
tothtamas28 Mar 28, 2024
4c35fcb
Make methods `static`
tothtamas28 Mar 28, 2024
a3d4125
Extract method `semanticAttributes`
tothtamas28 Mar 28, 2024
93a4e26
Replace call
tothtamas28 Mar 28, 2024
85eb022
Rename method
tothtamas28 Mar 28, 2024
9c1ef56
Merge branch 'develop' into refactor-kore-attributes
tothtamas28 Apr 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
142 changes: 76 additions & 66 deletions kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
View file
Open in desktop
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