try and fix issue with pattern matching

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:

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(