From 307e256870651673ab2e739f66ec8605f868d3c9 Mon Sep 17 00:00:00 2001
From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com>
Date: Wed, 27 Nov 2024 22:43:38 +0200
Subject: [PATCH] Take result attributes directly from the production when
 resolving contexts (#4685)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A declaration like
```syntax KItem ::= thing(Stuff, Stuff)  [seqstrict, result(Evaluated)]```
should consider tems that are `Evaluated` as evaluated. Right now, this happens only for the argument being heated/cooled, while the previous arguments are checked for being `KResult`. As an example, when heating the second argument above, the heating rule looks something like this:
```
rule thing(A, B) => B ~> thingFreezer(A) requires isKResult(A) andBool
notBool isEvaluated(B)
```

With this PR, the rule becomes
```
rule thing(A, B) => B ~> thingFreezer(A) requires isEvaluated(A) andBool
notBool isEvaluated(B)
```

Fixes #4683

---------

Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
---
 .../tests/regression-new/issue-4683/1.test      |  1 +
 .../tests/regression-new/issue-4683/1.test.out  |  3 +++
 .../tests/regression-new/issue-4683/Makefile    |  6 ++++++
 .../tests/regression-new/issue-4683/test.k      | 17 +++++++++++++++++
 .../org/kframework/compile/ResolveStrict.java   | 14 ++++++++++----
 5 files changed, 37 insertions(+), 4 deletions(-)
 create mode 100644 k-distribution/tests/regression-new/issue-4683/1.test
 create mode 100644 k-distribution/tests/regression-new/issue-4683/1.test.out
 create mode 100644 k-distribution/tests/regression-new/issue-4683/Makefile
 create mode 100644 k-distribution/tests/regression-new/issue-4683/test.k

diff --git a/k-distribution/tests/regression-new/issue-4683/1.test b/k-distribution/tests/regression-new/issue-4683/1.test
new file mode 100644
index 00000000000..d4b7157b64e
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4683/1.test
@@ -0,0 +1 @@
+thing(a, b)
diff --git a/k-distribution/tests/regression-new/issue-4683/1.test.out b/k-distribution/tests/regression-new/issue-4683/1.test.out
new file mode 100644
index 00000000000..3983fd868e3
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4683/1.test.out
@@ -0,0 +1,3 @@
+<k>
+  .K
+</k>
diff --git a/k-distribution/tests/regression-new/issue-4683/Makefile b/k-distribution/tests/regression-new/issue-4683/Makefile
new file mode 100644
index 00000000000..7f1f1f3cf18
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4683/Makefile
@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_FLAGS+=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/issue-4683/test.k b/k-distribution/tests/regression-new/issue-4683/test.k
new file mode 100644
index 00000000000..8aac863152f
--- /dev/null
+++ b/k-distribution/tests/regression-new/issue-4683/test.k
@@ -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
diff --git a/k-frontend/src/main/java/org/kframework/compile/ResolveStrict.java b/k-frontend/src/main/java/org/kframework/compile/ResolveStrict.java
index 628be2bcc5a..504e390cd4f 100644
--- a/k-frontend/src/main/java/org/kframework/compile/ResolveStrict.java
+++ b/k-frontend/src/main/java/org/kframework/compile/ResolveStrict.java
@@ -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,
@@ -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++) {