Fix quoting in IDs (#2968)

* Fix quoting in IDs

* Trailing whitespace

* Fix test

* Fix dependence on Id sort

* Additional test case

k-distribution/tests/regression-new/issue-2315-id-quotes/1.test

@@ -0,0 +1 @@
+test

k-distribution/tests/regression-new/issue-2315-id-quotes/1.test.out

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

k-distribution/tests/regression-new/issue-2315-id-quotes/2.test

@@ -0,0 +1 @@
+test2

k-distribution/tests/regression-new/issue-2315-id-quotes/2.test.out

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

k-distribution/tests/regression-new/issue-2315-id-quotes/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-2315-id-quotes/test.k

@@ -0,0 +1,16 @@
+module TEST
+  imports ID
+  imports BOOL
+  imports K-EQUAL
+  imports STRING
+  imports INT
+
+  syntax Bool ::= "test"  [function]
+                | "test2" [function]
+
+  // Evaluates to true if the Id constructed by String2Id contains extra quotes
+  rule test => String2Id("x") ==K #token("\"x\"", "Id")
+
+  // Test that hooks producing a result of sort String are wrapped
+  rule test2 => Int2String(2) ==K "2"
+endmodule

kernel/src/main/java/org/kframework/compile/ConstantFolding.java

@@ -24,6 +24,7 @@
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.List;
+import java.util.Objects;
 
 import static org.kframework.Collections.*;
 import static org.kframework.kore.KORE.*;
@@ -113,14 +114,17 @@ private Object unwrap(String token, String hook) {
     }
   }
 
-  private K wrap(Object result, Sort sort) {
+  private K wrap(Object result, Sort sort, Module module) {
+    String resultHookName = module.sortAttributesFor().apply(sort.head()).getOptional(Att.HOOK()).orElse("");
+    boolean hasStringHook = resultHookName.equals("STRING.String") || resultHookName.equals("BYTES.Bytes");
+
     if (result instanceof Boolean) {
       return KToken(result.toString(), sort);
     } else if (result instanceof FloatBuiltin) {
       return KToken(((FloatBuiltin)result).value(), sort);
     } else if (result instanceof BigInteger) {
       return KToken(result.toString(), sort);
-    } else if (result instanceof String) {
+    } else if (result instanceof String && hasStringHook) {
       return KToken(StringUtil.enquoteKString((String)result), sort);
     } else {
       return KToken(result.toString(), sort);
@@ -141,7 +145,7 @@ private K doFolding(String hook, List<K> args, Sort resultSort, Module module) t
     try {
       Method m = ConstantFolding.class.getDeclaredMethod(renamedHook, paramTypes.toArray(new Class<?>[args.size()]));
       Object result = m.invoke(this, unwrappedArgs.toArray(new Object[args.size()]));
-      return wrap(result, resultSort);
+      return wrap(result, resultSort, module);
     } catch (IllegalAccessException e) {
       throw KEMException.internalError("Error invoking constant folding function", e);
     } catch (InvocationTargetException e) {