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

Take result attributes directly from the production when resolving contexts #4685

Merged
merged 3 commits into from
Nov 27, 2024
Merged

Take result attributes directly from the production when resolving contexts #4685

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8b57108
Take result attributes directly from the production when resolving co…
virgil-serbanuta Nov 15, 2024
64dfdf7
Update k-frontend/src/main/java/org/kframework/compile/ResolveStrict.…
virgil-serbanuta Nov 27, 2024
20b7730
Fix review comments
virgil-serbanuta Nov 27, 2024
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
1 change: 1 addition & 0 deletions k-distribution/tests/regression-new/issue-4683/1.test
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
thing(a, b)
3 changes: 3 additions & 0 deletions k-distribution/tests/regression-new/issue-4683/1.test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
<k>
.K
</k>
6 changes: 6 additions & 0 deletions k-distribution/tests/regression-new/issue-4683/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
DEF=test
EXT=test
TESTDIR=.
KOMPILE_FLAGS+=--syntax-module TEST

include ../../../include/kframework/ktest.mak
17 changes: 17 additions & 0 deletions k-distribution/tests/regression-new/issue-4683/test.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
module TEST
imports BOOL

syntax KResult

syntax Stuff ::= "a" | "b" | "c"
syntax KItem ::= thing(Stuff, Stuff) [seqstrict, result(MyResult)]

rule thing(c, c) => .K

rule b => c
rule a => c

syntax Bool ::= isMyResult(K) [function, total, symbol(isMyResult)]
rule isMyResult(_) => false [owise]
rule isMyResult(c) => true
endmodule
14 changes: 10 additions & 4 deletions k-frontend/src/main/java/org/kframework/compile/ResolveStrict.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,8 +116,14 @@ private void setAliases(String attribute, Set<ContextAlias> aliases, Production
}
}

private static final ContextAlias DEFAULT_ALIAS =
ContextAlias(KVariable("HERE"), BooleanUtils.TRUE, Att.empty());
private static final ContextAlias defaultAliasFor(Production production) {
Att att = production.att();
if (!att.contains(Att.RESULT())) {
return ContextAlias(KVariable("HERE"), BooleanUtils.TRUE, Att.empty());
}
return ContextAlias(
KVariable("HERE"), BooleanUtils.TRUE, Att.empty().add(Att.RESULT(), att.get(Att.RESULT())));
}

private void resolve(
boolean sequential,
Expand Down Expand Up @@ -202,14 +208,14 @@ public Set<Sentence> resolve(Production production, boolean sequential) {
for (int i = 1; i <= arity; i++) {
strictnessPositions.add(i);
}
aliases.add(DEFAULT_ALIAS);
aliases.add(defaultAliasFor(production));
resolve(sequential, sentences, arity, strictnessPositions, allPositions, aliases, production);
allPositions.addAll(strictnessPositions);
} else {
String[] components = attribute.split(";");
if (components.length == 1) {
if (Character.isDigit(components[0].trim().charAt(0))) {
aliases.add(DEFAULT_ALIAS);
aliases.add(defaultAliasFor(production));
setPositions(components[0].trim(), strictnessPositions, arity, production);
} else {
for (int i = 1; i <= arity; i++) {
Expand Down
Loading