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 index 0fbc763a6..67f3dfb85 100644 --- 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 index 92f1e3d7a..72101d48f 100644 --- 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,