Take result attributes directly from the production when resolving co…

…ntexts (#4685)

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 <[email protected]>

k-distribution/tests/regression-new/issue-4683/1.test

@@ -0,0 +1 @@
+thing(a, b)

k-distribution/tests/regression-new/issue-4683/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  .K
+</k>

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

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

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++) {