Don't generate inj{S, S} when symbol overloads have the same sort (#…

…4136)

It is valid for two overloaded symbols to have the same sort; a
motivating case for doing so is to select a _more specific function
implementation_ based on more specific arguments, rather than to make
the sort of a constructor more specific. We do this a few times in the C
semantics, for example.

Previously, such overloads would generate spurious injections `inj{S,
S}` in the "overloaded symbol" axioms. Because we don't actually rewrite
based on these axioms (but rather just read off the relevant
attributes), this behaviour went unrecognised for a long time.

For consistency, this PR amends ModuleToKore such that it will not
generate the injection when the sort of the two productions is the same.
We're in the process of porting this code to Python, and so I have not
made any effort to clean up the code here; doing so is really outside
the scope of this change. I have added a test that minimally exercises
this part of the KORE generator, and verifies that the overload set
induced works correctly to disambiguate a parse.

Fixes: #4114

k-distribution/tests/regression-new/issue-4114-overload-injection/1.test

@@ -0,0 +1 @@
+test(foo)

k-distribution/tests/regression-new/issue-4114-overload-injection/1.test.out

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

k-distribution/tests/regression-new/issue-4114-overload-injection/Makefile

@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/issue-4114-overload-injection/test.k

@@ -0,0 +1,12 @@
+module TEST
+  imports DOMAINS
+
+  syntax Foo ::= "foo"
+  syntax Bar ::= Foo | "bar"
+
+  syntax Bool ::= test(Foo) [function, overload(test)]
+                | test(Bar) [function, overload(test)]
+
+  rule test(foo) => true
+  rule test(_)   => false
+endmodule

kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

@@ -897,21 +897,33 @@ private void genOverloadedAxiom(Production lesser, Production greater, StringBui
       }
       conn = ",";
     }
-    sb.append("), inj{");
-    convert(lesser.sort(), lesser, sb);
-    sb.append(", ");
-    convert(greater.sort(), greater, sb);
-    sb.append("} (");
+
+    if (greater.sort().equals(lesser.sort())) {
+      sb.append("), ");
+    } else {
+      sb.append("), inj{");
+      convert(lesser.sort(), lesser, sb);
+      sb.append(", ");
+      convert(greater.sort(), greater, sb);
+      sb.append("} (");
+    }
+
     convert(lesser.klabel().get(), lesser, sb);
     sb.append("(");
+
     conn = "";
     for (int i = 0; i < lesser.nonterminals().size(); i++) {
       sb.append(conn);
       sb.append("K").append(i).append(":");
       convert(lesser.nonterminal(i).sort(), lesser, sb);
       conn = ",";
     }
-    sb.append("))) ");
+
+    if (greater.sort().equals(lesser.sort())) {
+      sb.append(")) ");
+    } else {
+      sb.append("))) ");
+    }
     final var args = KList(KApply(greater.klabel().get()), KApply(lesser.klabel().get()));
     final var att = Att.empty().add(Att.SYMBOL_OVERLOAD(), KList.class, args);
     convert(new HashMap<>(), att, sb, null, null);