Remove special case for array hook namespace (#4002)

For issue #3976 

The ARRAY module function symbols in `domains.md` have been hooked with
the ARRAY namespace, but no modern backends have those hooks implemented
so the frontend has been dropping the hook attributes with specific
checks, falling back to the `ARRAY-IN-K` semantics for them.

This change removes the ARRAY hook attributes in `domains.md` and the
special cases for them in the frontend.

k-distribution/include/kframework/builtin/domains.md

@@ -73,7 +73,7 @@ this module should import only the `ARRAY` module.
 module ARRAY-SYNTAX
   imports private LIST
 
-  syntax Array [hook(ARRAY.Array)]
+  syntax Array
 ```
 
 ### Array lookup
@@ -83,7 +83,7 @@ that the base of the logarithm is a relatively high number and thus the time is
 effectively constant.
 
 ```k
-  syntax KItem ::= Array "[" Int "]" [function, hook(ARRAY.lookup)]
+  syntax KItem ::= Array "[" Int "]" [function]
 ```
 
 ### Array update
@@ -92,7 +92,7 @@ You can create a new `Array` with a new value for a key in O(log(N)) time, or
 effectively constant.
 
 ```k
-  syntax Array ::= Array "[" key: Int "<-" value: KItem "]" [function, hook(ARRAY.update), klabel(_[_<-_]), symbol]
+  syntax Array ::= Array "[" key: Int "<-" value: KItem "]" [function, klabel(_[_<-_]), symbol]
 ```
 
 ### Array reset
@@ -101,7 +101,7 @@ You can create a new `Array` where a particular key is reset to its default
 value in O(log(N)) time, or effectively constant.
 
 ```k
-  syntax Array ::= Array "[" Int "<-" "undef" "]" [function, hook(ARRAY.remove)]
+  syntax Array ::= Array "[" Int "<-" "undef" "]" [function]
 ```
 
 ### Multiple array update
@@ -112,7 +112,7 @@ O(N*log(K)) time (where K is the size of the array), or effectively linear.
 Having `index + N > K` yields an exception.
 
 ```k
-  syntax Array ::= updateArray(Array, index: Int, List) [function, hook(ARRAY.updateAll)]
+  syntax Array ::= updateArray(Array, index: Int, List) [function]
 ```
 
 ### Array fill
@@ -121,15 +121,15 @@ You can create a new `Array` where the `length` elements starting at `index`
 are replaced with `value`, in O(length*log(N)) time, or effectively linear.
 
 ```k
-  syntax Array ::= fillArray(Array, index: Int, length: Int, value: KItem) [function, hook(ARRAY.fill)]
+  syntax Array ::= fillArray(Array, index: Int, length: Int, value: KItem) [function]
 ```
 
 ### Array range check
 
 You can test whether an integer is within the bounds of an array in O(1) time.
 
 ```k
-  syntax Bool ::= Int "in_keys" "(" Array ")" [function, total, hook(ARRAY.in_keys)]
+  syntax Bool ::= Int "in_keys" "(" Array ")" [function, total]
 ```
 
 ```k
@@ -153,7 +153,7 @@ may incur a one-time O(N) resizing cost, possibly amortized across multiple
 operations.
 
 ```k
-  syntax Array ::= makeArray(length: Int, value: KItem) [function, hook(ARRAY.make), public]
+  syntax Array ::= makeArray(length: Int, value: KItem) [function, public]
 ```
 
 ### Implementation of Arrays

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

@@ -22,6 +22,7 @@
 import java.util.function.Function;
 import java.util.regex.Pattern;
 import java.util.stream.Collectors;
+import java.util.stream.Stream;
 import org.kframework.Collections;
 import org.kframework.attributes.Att;
 import org.kframework.attributes.HasLocation;
@@ -201,7 +202,6 @@ public void convert(
     collectionSorts.add("SET.Set");
     collectionSorts.add("MAP.Map");
     collectionSorts.add("LIST.List");
-    collectionSorts.add("ARRAY.Array");
     collectionSorts.add("RANGEMAP.RangeMap");
     attributes.remove(Att.HAS_DOMAIN_VALUES());
     if (attributes.containsKey(Att.TOKEN())) {
@@ -423,23 +423,16 @@ private void translateSorts(
       Att att = module.sortAttributesFor().get(sort).getOrElse(() -> KORE.Att());
       if (att.contains(Att.HOOK())) {
         if (collectionSorts.contains(att.get(Att.HOOK()))) {
-          if (att.get(Att.HOOK()).equals("ARRAY.Array")) {
-            att = att.remove(Att.ELEMENT());
-            att = att.remove(Att.UNIT());
-            att = att.remove(Att.HOOK());
-          } else {
-            Production concatProd =
-                stream(module.productionsForSort().apply(sort))
-                    .filter(p -> p.att().contains(Att.ELEMENT()))
-                    .findAny()
-                    .get();
-            att =
-                att.add(
-                    Att.ELEMENT(), K.class, KApply(KLabel(concatProd.att().get(Att.ELEMENT()))));
-            att = att.add(Att.CONCAT(), K.class, KApply(concatProd.klabel().get()));
-            att = att.add(Att.UNIT(), K.class, KApply(KLabel(concatProd.att().get(Att.UNIT()))));
-            sb.append("hooked-");
-          }
+          Production concatProd =
+              stream(module.productionsForSort().apply(sort))
+                  .filter(p -> p.att().contains(Att.ELEMENT()))
+                  .findAny()
+                  .get();
+          att =
+              att.add(Att.ELEMENT(), K.class, KApply(KLabel(concatProd.att().get(Att.ELEMENT()))));
+          att = att.add(Att.CONCAT(), K.class, KApply(concatProd.klabel().get()));
+          att = att.add(Att.UNIT(), K.class, KApply(KLabel(concatProd.att().get(Att.UNIT()))));
+          sb.append("hooked-");
         } else {
           sb.append("hooked-");
         }
@@ -948,13 +941,8 @@ private void genOverloadedAxiom(Production lesser, Production greater, StringBui
 
   private boolean isRealHook(Att att) {
     String hook = att.get(Att.HOOK());
-    if (hook.startsWith("ARRAY.")) {
-      return false;
-    }
-    if (options.hookNamespaces.stream().anyMatch(ns -> hook.startsWith(ns + "."))) {
-      return true;
-    }
-    return Hooks.namespaces.stream().anyMatch(ns -> hook.startsWith(ns + "."));
+    return Stream.concat(Hooks.namespaces.stream(), options.hookNamespaces.stream())
+        .anyMatch(ns -> hook.startsWith(ns + "."));
   }
 
   private static boolean isBuiltinProduction(Production prod) {

kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java

@@ -153,7 +153,7 @@ private void checkHookedSortConstructors(Production prod) {
       return;
     }
     Att sortAtt = m.sortAttributesFor().getOrElse(prod.sort().head(), Att::empty);
-    if (sortAtt.contains(Att.HOOK()) && !sortAtt.get(Att.HOOK()).equals("ARRAY.Array")) {
+    if (sortAtt.contains(Att.HOOK())) {
       if (!prod.att().contains(Att.FUNCTION())
           && !prod.att().contains(Att.BRACKET())
           && !prod.att().contains(Att.TOKEN())

kore/src/main/java/org/kframework/builtin/Hooks.java

@@ -8,7 +8,6 @@
 import java.util.Set;
 
 public class Hooks {
-  public static final String ARRAY = "ARRAY";
   public static final String BOOL = "BOOL";
   public static final String BUFFER = "BUFFER";
   public static final String BYTES = "BYTES";
@@ -32,7 +31,6 @@ public class Hooks {
       Collections.unmodifiableSet(
           new HashSet<>(
               Arrays.asList(
-                  ARRAY,
                   BOOL,
                   BUFFER,
                   BYTES,