diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java index 10fa815fecb..a00ac5b32a8 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -713,7 +713,7 @@ private void genNoJunkAxiom(Sort sort, StringBuilder sb) { sbTemp.append(" axiom{} "); boolean hasToken = false; int numTerms = 0; - sbTemp.append("\\right-assoc{}(\\or{"); + sbTemp.append("\\or{"); convert(sort, sbTemp); sbTemp.append("} ("); for (Production prod : iterable(mutable(module.productionsForSort()).getOrDefault(sort.head(), Set()).toSeq().sorted(Production.ord()))) { @@ -776,7 +776,7 @@ private void genNoJunkAxiom(Sort sort, StringBuilder sb) { } sbTemp.append("\\bottom{"); convert(sort, sbTemp); - sbTemp.append("}())) [constructor{}()] // no junk"); + sbTemp.append("}()) [constructor{}()] // no junk"); if (hasToken && !METAVAR) { sbTemp.append(" (TODO: fix bug with \\dv)"); } diff --git a/kore/src/main/scala/org/kframework/parser/kore/Default.scala b/kore/src/main/scala/org/kframework/parser/kore/Default.scala index 01df2ccf620..c7c2b2b9e47 100644 --- a/kore/src/main/scala/org/kframework/parser/kore/Default.scala +++ b/kore/src/main/scala/org/kframework/parser/kore/Default.scala @@ -5,8 +5,7 @@ import org.kframework.parser.{kore => i} object implementation { - // TODO: make private again - object ConcreteClasses { + private object ConcreteClasses { case class Definition(att: i.Attributes, modules: Seq[i.Module]) extends i.Definition diff --git a/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala b/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala index ef16e75c7e3..6aebc0de4ac 100644 --- a/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala +++ b/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala @@ -524,22 +524,6 @@ class TextToKore(b: Builders = DefaultBuilders) { consumeWithLeadingWhitespaces("}") consumeWithLeadingWhitespaces("(") val ctr = scanner.nextWithSkippingWhitespaces() match { - case '\\' => - val c1 = scanner.next() - val c2 = scanner.next() - (c1, c2) match { - case ('a', 'n') => // and - consume("d") - consumeWithLeadingWhitespaces("{") - val s = parseSort() - consumeWithLeadingWhitespaces("}") - (p1: kore.Pattern, p2: kore.Pattern) => b.And(s, p1, p2) - case ('o', 'r') => // or - consumeWithLeadingWhitespaces("{") - val s = parseSort() - consumeWithLeadingWhitespaces("}") - (p1: kore.Pattern, p2: kore.Pattern) => b.Or(s, p1, p2) - } case c => // variable or application scanner.putback(c) val id = parseId() // previousParsingLevel is set here @@ -559,22 +543,6 @@ class TextToKore(b: Builders = DefaultBuilders) { consumeWithLeadingWhitespaces("}") consumeWithLeadingWhitespaces("(") val ctr = scanner.nextWithSkippingWhitespaces() match { - case '\\' => - val c1 = scanner.next() - val c2 = scanner.next() - (c1, c2) match { - case ('a', 'n') => // and - consume("d") - consumeWithLeadingWhitespaces("{") - val s = parseSort() - consumeWithLeadingWhitespaces("}") - (p1: kore.Pattern, p2: kore.Pattern) => b.And(s, p1, p2) - case ('o', 'r') => // or - consumeWithLeadingWhitespaces("{") - val s = parseSort() - consumeWithLeadingWhitespaces("}") - (p1: kore.Pattern, p2: kore.Pattern) => b.Or(s, p1, p2) - } case c => // variable or application scanner.putback(c) val id = parseId() // previousParsingLevel is set here diff --git a/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala b/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala index 4cee235b858..48eebe0788a 100644 --- a/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala +++ b/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala @@ -8,27 +8,19 @@ import org.kframework.parser.kore.implementation.{DefaultBuilders => b} class TextToKoreTest { @Test def testMultiOr(): Unit = { - val kore1 = "\\left-assoc{}(\\or{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\")))" + val kore1 = "\\or{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\"))" val parser = new TextToKore() val ast1 = parser.parsePattern(kore1) val int = b.CompoundSort("SortInt", Seq()) - Assert.assertEquals(b.Or(int, b.Or(int, b.DomainValue(int, "1"), b.DomainValue(int, "2")), b.DomainValue(int, "3")), ast1) - - val kore2 = "\\right-assoc{}(\\or{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\")))" - val ast2 = parser.parsePattern(kore2) - Assert.assertEquals(b.Or(int, b.DomainValue(int, "1"), b.Or(int, b.DomainValue(int, "2"), b.DomainValue(int, "3"))), ast2) + Assert.assertEquals(b.Or(int, Seq(b.DomainValue(int, "1"), b.DomainValue(int, "2"), b.DomainValue(int, "3"))), ast1) } @Test def testMultiAnd(): Unit = { - val kore1 = "\\left-assoc{}(\\and{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\")))" + val kore1 = "\\and{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\"))" val parser = new TextToKore() val ast1 = parser.parsePattern(kore1) val int = b.CompoundSort("SortInt", Seq()) - Assert.assertEquals(b.And(int, b.And(int, b.DomainValue(int, "1"), b.DomainValue(int, "2")), b.DomainValue(int, "3")), ast1) - - val kore2 = "\\right-assoc{}(\\and{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\")))" - val ast2 = parser.parsePattern(kore2) - Assert.assertEquals(b.And(int, b.DomainValue(int, "1"), b.And(int, b.DomainValue(int, "2"), b.DomainValue(int, "3"))), ast2) + Assert.assertEquals(b.And(int, Seq(b.DomainValue(int, "1"), b.DomainValue(int, "2"), b.DomainValue(int, "3"))), ast1) } @Test def testAssocApplication(): Unit = {