Skip to content

Commit

Permalink
Finish all changes to the K frontend, LLVM backend, and Haskell backe…
Browse files Browse the repository at this point in the history 
…nd relating to multi-ary \and/\or (#3679)

Blocked on runtimeverification/llvm-backend#844

Note: this is also blocked on the changes to the Haskell backend

This change finalizes the sequence of changes used to implement
multi-ary \and and \or in the frontend. We remove the parsing of
\left-assoc and \right-assoc of \and and \or, and we emit multi-ary and
and or where previously we were using \right-assoc in ModuleToKore. We
also revert the last of the temporary changes we made.
  • Loading branch information
Dwight Guth authored Oct 12, 2023
1 parent 58eef8b commit 511541d
Show file tree
Hide file tree
Showing 4 changed files with 7 additions and 48 deletions.
4 changes: 2 additions & 2 deletions kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()))) {
Expand Down Expand Up @@ -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)");
}
Expand Down
3 changes: 1 addition & 2 deletions kore/src/main/scala/org/kframework/parser/kore/Default.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
32 changes: 0 additions & 32 deletions kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
16 changes: 4 additions & 12 deletions kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {
Expand Down

0 comments on commit 511541d

Please sign in to comment.