fix bugs

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

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Constructor.scala
@@ -88,7 +88,7 @@ case class HasKey(
             Some(
               immutable.Seq(
                 Fringe(f.symlib, sorts(2), Value(k, f.occurrence), isExact = false),
-                Fringe(f.symlib, f.sort, Rem(k, f.occurrence), isExact = false),
+                Fringe(f.symlib, f.sort, f.occurrence, isExact = false),
                 f
               )
             )

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
@@ -265,12 +265,14 @@ case class ListS() extends SortCategory {
             .map(expandListPatternDefault(_, listO, maxList))
         )
       )
+    } else if (matrix.bestCol.isChoice) {
+      throw new MatchingException(
+          MatchingException.Type.COMPILER_ERROR,
+          "LLVM backend does not support random access list patterns with unbound keys.")
     } else {
       val key = matrix.bestCol.bestKey
       key match {
-        case None => throw new MatchingException(
-          MatchingException.Type.COMPILER_ERROR,
-          "LLVM backend does not support random access list patterns with unbound keys.")
+        case None => Switch(listO, hookAtt, matrix.compiledCases, matrix.compiledDefault)
         case Some(k) =>
           MakePattern(
             newO,