Merge remote-tracking branch 'origin/develop'

runtimeverification · Oct 12, 2023 · d74da5e · d74da5e
2 parents be14737 + 511541d
commit d74da5e
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 48 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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 = {