From 38a50d2eeadf467ce77557e80ca5dabe085c3a7e Mon Sep 17 00:00:00 2001
From: gtrepta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 19 Feb 2024 05:03:15 -0600
Subject: [PATCH] Remove array namespace check (#988)

For https://github.com/runtimeverification/k/issues/3976

There's a special case for a hook namespace in `ARRAY` which falls back
to K semantics for those symbols. The frontend wont emit any hook
attributes in that namespace for the ARRAY module anyway so it can
safely be removed.
---
 lib/ast/AST.cpp            |  3 ---
 lib/codegen/CreateTerm.cpp | 11 ++---------
 2 files changed, 2 insertions(+), 12 deletions(-)

diff --git a/lib/ast/AST.cpp b/lib/ast/AST.cpp
index 905dd3430..69730a725 100644
--- a/lib/ast/AST.cpp
+++ b/lib/ast/AST.cpp
@@ -218,9 +218,6 @@ ValueType KORECompositeSort::getCategory(std::string const &hookName) {
     category = SortCategory::MInt;
     bits = std::stoi(hookName.substr(10));
   } else {
-    // ARRAY.Array is implemented in K and therefore should fall through to the
-    // default category. Should it one day be implemented as a fully hooked
-    // sort, a check needs to be added to the list above.
     category = SortCategory::Symbol;
   }
   return {category, bits};
diff --git a/lib/codegen/CreateTerm.cpp b/lib/codegen/CreateTerm.cpp
index 06073c0eb..0af4a213e 100644
--- a/lib/codegen/CreateTerm.cpp
+++ b/lib/codegen/CreateTerm.cpp
@@ -648,15 +648,8 @@ llvm::Value *CreateTerm::createHook(
     assert(false && "not implemented yet: MInt");
     abort();
   }
-  std::string domain = name.substr(0, name.find('.'));
-  if (domain == "ARRAY") {
-    // array is not really hooked in llvm, it's implemented in K
-    auto fn_name = fmt::format(
-        "eval_{}", ast_to_string(*pattern->getConstructor(), 0, false));
-    return createFunctionCall(fn_name, pattern, false, true, locationStack);
-  }
-  std::string hookName
-      = "hook_" + domain + "_" + name.substr(name.find('.') + 1);
+  std::string hookName = "hook_" + name.substr(0, name.find('.')) + "_"
+                         + name.substr(name.find('.') + 1);
   return createFunctionCall(hookName, pattern, true, false, locationStack);
 }