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

Make new-format rules without antileft the default #3391

Merged
merged 3 commits into from
May 4, 2023
Merged

Make new-format rules without antileft the default #3391

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1e6c85c
Make new-format rules the default
Baltoli May 4, 2023
0a375a5
Not deprecated
Baltoli May 4, 2023
466afa5
Merge branch 'develop' into default-antileft
rv-jenkins May 4, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/issue-3035-antileft/haskell/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@ DEF=test
EXT=test
TESTDIR=.
KOMPILE_BACKEND=haskell
KOMPILE_FLAGS=--syntax-module TEST --disable-kore-antileft
KOMPILE_FLAGS=--syntax-module TEST

include ../../../../include/kframework/ktest.mak
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/issue-3035-antileft/llvm/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@ DEF=test
EXT=test
TESTDIR=.
KOMPILE_BACKEND=llvm
KOMPILE_FLAGS=--syntax-module TEST --disable-kore-antileft
KOMPILE_FLAGS=--syntax-module TEST

include ../../../../include/kframework/ktest.mak
4 changes: 2 additions & 2 deletions k-distribution/tests/regression-new/map-symbolic-tests-haskell/assignment-11-spec.k.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@
#And
<k>
assignmentResult ( ( MAP
X:MyId |-> 1 ) [ Z:MyId <- 3 ]
Y:MyId |-> 2 ) ~> .
X:MyId |-> 1
Y:MyId |-> 2 ) [ Z:MyId <- 3 ] ) ~> .
</k>
#And
{
Expand Down
23 changes: 12 additions & 11 deletions kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -302,7 +302,7 @@ public void convert(boolean heatCoolEq, String prelude, StringBuilder semantics,
ruleIndex++;
}

if (!options.disableKoreAntileft) {
if (options.enableKoreAntileft) {
semantics.append("\n// priority groups\n");
genPriorityGroups(priorityList, priorityToPreviousGroup, priorityToAlias, topCellSortStr, semantics);
}
Expand Down Expand Up @@ -1175,7 +1175,7 @@ private void convertRule(RuleOrClaim rule, int ruleIndex, boolean heatCoolEq, St
Comparator<KVariable> compareByName = (KVariable v1, KVariable v2) -> v1.name().compareTo(v2.name());
java.util.Collections.sort(freeVars, compareByName);

if (!options.disableKoreAntileft) {
if (options.enableKoreAntileft) {
genAliasForSemanticsRuleLHS(requires, left, ruleAliasName, freeVars, topCellSortStr,
priority, priorityToAlias, sb);
sb.append("\n");
Expand All @@ -1184,13 +1184,13 @@ private void convertRule(RuleOrClaim rule, int ruleIndex, boolean heatCoolEq, St
sb.append(" axiom{} ");
sb.append(String.format("\\rewrites{%s} (\n ", topCellSortStr));

if (options.disableKoreAntileft) {
genSemanticsRuleLHSNoAlias(requires, left, freeVars, topCellSortStr, priorityToPreviousGroup.get(priority), sb);
sb.append(",\n ");
} else {
if (options.enableKoreAntileft) {
genSemanticsRuleLHSWithAlias(ruleAliasName, freeVars, topCellSortStr,
priorityToPreviousGroup.get(priority), sb);
sb.append(",\n ");
} else {
genSemanticsRuleLHSNoAlias(requires, left, freeVars, topCellSortStr, priorityToPreviousGroup.get(priority), sb);
sb.append(",\n ");
}
} else {
// LHS for claims
Expand Down Expand Up @@ -1219,14 +1219,15 @@ private void convertRule(RuleOrClaim rule, int ruleIndex, boolean heatCoolEq, St
}
sb.append(String.format("\\and{%s} (\n ", topCellSortStr));

if (options.disableKoreAntileft) {
convert(right, sb);
sb.append(", ");
convertSideCondition(ensures, topCellSortStr, sb);
} else {
if (options.enableKoreAntileft) {
convertSideCondition(ensures, topCellSortStr, sb);
sb.append(", ");
convert(right, sb);
} else {
convert(right, sb);
sb.append(", ");
convertSideCondition(ensures, topCellSortStr, sb);

}

sb.append(')');
Expand Down
4 changes: 2 additions & 2 deletions kernel/src/main/java/org/kframework/kompile/KompileOptions.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,6 +142,6 @@ public String syntaxModule(FileUtil files) {
@Parameter(names={"--allow-anywhere-haskell"}, description="Disable error message for anywhere rules on the Haskell backend.")
public boolean allowAnywhereRulesHaskell;

@Parameter(names="--disable-kore-antileft", description="[EXPERIMENTAL] Disable generation of antileft priority predicates ")
public boolean disableKoreAntileft;
@Parameter(names="--enable-kore-antileft", description="[DEPRECATED] Enable generation of legacy antileft priority predicates ")
public boolean enableKoreAntileft;
}