From 3487ca0c9f437972dcb687c528b86861cb4fb692 Mon Sep 17 00:00:00 2001
From: Dwight Guth <dwight.guth@pi2.network>
Date: Mon, 9 Sep 2024 12:51:47 -0500
Subject: [PATCH] try and fix issue with pattern matching

---
 debug/kgdb.py                                 | 23 +++++++++++++++++++
 .../llvm/matching/pattern/Pattern.scala       |  3 ++-
 2 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/debug/kgdb.py b/debug/kgdb.py
index 1e8683f11..ce9066cc5 100644
--- a/debug/kgdb.py
+++ b/debug/kgdb.py
@@ -359,6 +359,7 @@ def __init__(self, val, cat, sortName):
         self.used_var_names = set()
         self.long_int = gdb.lookup_type("long int")
         self.bool_ptr = gdb.lookup_type("bool").pointer()
+        self.char_ptr = gdb.lookup_type("unsigned char").pointer()
         self.unsigned_char = gdb.lookup_type("unsigned char")
         self.string_ptr = gdb.lookup_type("string").pointer()
         self.stringbuffer_ptr = gdb.lookup_type("stringbuffer").pointer()
@@ -483,6 +484,20 @@ def appendInt(self, val, sort):
             self.appendLimbs(size, val.dereference()['_mp_d'])
         self.result += "\")"
 
+    def appendMInt(self, val, width, sort):
+        self.result += "\\dv{" + sort + "}(\""
+        self.appendLE(val.cast(self.char_ptr), width)
+        self.result += "\")"
+
+    def appendLE(self, ptr, size):
+        accum = 0
+        for i in range(size-1,-1,-1):
+            accum <<= 8
+            byte = int(ptr[i])
+            accum |= byte
+        self.result += str(accum)
+        self.result += "p" + str(size * 8)
+
     def appendList(self, val, sort):
         length = val.dereference()['impl_']['size']
         if length == 0:
@@ -632,6 +647,14 @@ def append(self, subject, isVar, sort):
                 self.result += "\\dv{" + sort + "}(\"" + string + "\")"
             elif cat == @STRINGBUFFER_LAYOUT@:
                 self.appendStringBuffer(arg.cast(self.stringbuffer_ptr_ptr).dereference(), sort)
+            elif cat == @MINT_LAYOUT@ + 32:
+                self.appendMInt(arg, 4, sort)
+            elif cat == @MINT_LAYOUT@ + 64:
+                self.appendMInt(arg, 8, sort)
+            elif cat == @MINT_LAYOUT@ + 160:
+                self.appendMInt(arg, 20, sort)
+            elif cat == @MINT_LAYOUT@ + 256:
+                self.appendMInt(arg, 32, sort)
             else:
                 raise ValueError()
             if i != nargs - 1:
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala
index 4f8fc4f26..faa72054f 100644
--- a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala
+++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/Pattern.scala
@@ -176,10 +176,11 @@ case class ListGetP[T] private (
       maxPriority: Int
   ): Boolean =
     ix match {
-      case HasKey(_, _, Some(p)) => true
+      case HasKey(_, _, Some(_)) => true
       case HasNoKey(_, Some(p)) => !keys.map(_.canonicalize(clause)).contains(p)
       // needed for usefulness
       case HasKey(_, _, None)   => clause.action.priority <= maxPriority
+      case HasNoKey(_, None) => keys.nonEmpty && clause.action.priority > maxPriority
       case _                    => ???
     }
   def score(