more bug fixes

runtimeverification · Sep 9, 2024 · 9f62a71 · 9f62a71
1 parent c0505f7
commit 9f62a71
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 3 deletions.
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala
@@ -307,7 +307,7 @@ class SortInfo private (sort: Sort, symlib: Parser.SymLib) {
   val exactLength: Int = category.length(exactConstructors.size)
   val isCollection: Boolean =
     category match {
-      case MapS() | SetS() => true
+      case MapS() | SetS() | ListS() => true
       case _               => false
     }
 }

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
@@ -189,7 +189,7 @@ case class ListGetP[T] private (
       key: Option[Pattern[Option[Occurrence]]],
       isEmpty: Boolean
   ): Double = h.scoreListGet(this, f, c, key, isEmpty)
-  override def isChoice: Boolean = false
+  override def isChoice: Boolean = keys.nonEmpty
   def bindings(
       ix: Option[Constructor],
       residual: Option[Pattern[String]],

diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala
@@ -268,7 +268,9 @@ case class ListS() extends SortCategory {
     } else {
       val key = matrix.bestCol.bestKey
       key match {
-        case None => ???
+        case None => throw new MatchingException(
+          MatchingException.Type.COMPILER_ERROR,
+          "LLVM backend does not support random access list patterns with unbound keys.")
         case Some(k) =>
           MakePattern(
             newO,