diff --git a/k-distribution/tests/regression-new/checks/checkParametricSort.k b/k-distribution/tests/regression-new/checks/checkParametricSort.k new file mode 100644 index 00000000000..85bc2a174e3 --- /dev/null +++ b/k-distribution/tests/regression-new/checks/checkParametricSort.k @@ -0,0 +1,8 @@ +// Copyright (c) Runtime Verification, Inc. All Rights Reserved. +module CHECKPARAMETRICSORT +imports MINT +imports INT + +syntax MInt{6} +syntax {S} Foo{S} +endmodule diff --git a/k-distribution/tests/regression-new/checks/checkParametricSort.k.out b/k-distribution/tests/regression-new/checks/checkParametricSort.k.out new file mode 100644 index 00000000000..04b183f486a --- /dev/null +++ b/k-distribution/tests/regression-new/checks/checkParametricSort.k.out @@ -0,0 +1,5 @@ +[Error] Compiler: User-defined parametric sorts are currently unsupported: Foo{S} + Source(checkParametricSort.k) + Location(7,1,7,18) + 7 | syntax {S} Foo{S} + . ^~~~~~~~~~~~~~~~~ diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala index 81673ae59b0..660477e2e9a 100644 --- a/kore/src/main/scala/org/kframework/definition/outer.scala +++ b/kore/src/main/scala/org/kframework/definition/outer.scala @@ -427,9 +427,21 @@ case class Module( set.head } - // check that non-terminals have a defined sort + private def throwIfUserParametricSort(sort: Sort, loc: HasLocation): Unit = + if (sort.head.params != 0 && sort.name != Sorts.MInt.name) + throw KEMException.compilerError( + "User-defined parametric sorts are currently " + + "unsupported: " + sort, + loc + ) + + // Check that user-defined sorts are non-parametric and that + // each non-terminal has a defined sort def checkSorts(): Unit = localSentences.foreach { - case p @ Production(_, params, _, items, _) => + case s @ SyntaxSort(_, sort, _) => throwIfUserParametricSort(sort, s) + case s @ SortSynonym(newSort, _, _) => throwIfUserParametricSort(newSort, s) + case p @ Production(_, params, sort, items, _) => + throwIfUserParametricSort(sort, p) val res = items.collect { case nt: NonTerminal if !p.isSortVariable(nt.sort) && !definedSorts.contains(nt.sort.head) && !sortSynonymMap