From c71f50d7e11529a93732d19dc0dd24b606d980ba Mon Sep 17 00:00:00 2001 From: gtrepta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 29 Sep 2023 20:00:22 -0500 Subject: [PATCH] Ordering instance for Sentences (2) (#3670) fixes: #3530 This branch was merged and then reverted because of an issue that didn't get caught earlier in CI. I have since pushed a fix for the issue and tested it to make sure that it will work. So, this should be good to go. But if we really want to be sure, then we can consider this PR blocked on #3669. --------- Co-authored-by: rv-jenkins --- .../collections/test-set2list-2.col.out | 6 +- .../collections/test-set2list-3.col.out | 4 +- .../scala/org/kframework/attributes/Att.scala | 5 + .../org/kframework/definition/outer.scala | 107 +++++++++++-- .../org/kframework/definition/OuterTest.scala | 150 ++++++++++++++++++ 5 files changed, 251 insertions(+), 21 deletions(-) diff --git a/k-distribution/tests/builtins/collections/test-set2list-2.col.out b/k-distribution/tests/builtins/collections/test-set2list-2.col.out index e698f880343..ff7f12e8d9b 100644 --- a/k-distribution/tests/builtins/collections/test-set2list-2.col.out +++ b/k-distribution/tests/builtins/collections/test-set2list-2.col.out @@ -1,6 +1,6 @@ - ListItem ( 4 ) - ListItem ( 3 ) + ListItem ( 1 ) ListItem ( 2 ) - ListItem ( 1 ) ~> . + ListItem ( 3 ) + ListItem ( 4 ) ~> . diff --git a/k-distribution/tests/builtins/collections/test-set2list-3.col.out b/k-distribution/tests/builtins/collections/test-set2list-3.col.out index 42af7fc9c87..af1ebe42178 100644 --- a/k-distribution/tests/builtins/collections/test-set2list-3.col.out +++ b/k-distribution/tests/builtins/collections/test-set2list-3.col.out @@ -1,5 +1,5 @@ - ListItem ( 4 ) + ListItem ( 1 ) ListItem ( 3 ) - ListItem ( 1 ) ~> . + ListItem ( 4 ) ~> . diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index f882997bd1e..d3c3685d33f 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -414,6 +414,11 @@ object Att { val attMap = union.groupBy({ case ((name, _), _) => name}) Att(union.filter { key => attMap(key._1._1).size == 1 }.toMap) } + + implicit val ord: Ordering[Att] = { + import scala.math.Ordering.Implicits._ + Ordering.by[Att, Seq[(String, String, String)]](att => att.att.iterator.map(k => (k._1._1.key, k._1._2, k._2.toString)).toSeq.sorted) + } } trait AttributesToString { diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala index 127bb54694c..6931bc8914b 100644 --- a/kore/src/main/scala/org/kframework/definition/outer.scala +++ b/kore/src/main/scala/org/kframework/definition/outer.scala @@ -414,18 +414,66 @@ trait Sentence extends HasLocation with HasAtt with AttValue { def label: Optional[String] = att.getOptional(Att.LABEL) } +object Sentence { + implicit val ord = new Ordering[Sentence] { + def compare(a: Sentence, b: Sentence): Int = { + (a, b) match { + case (c:SyntaxSort, d:SyntaxSort) => Ordering[SyntaxSort].compare(c, d) + case (c:SortSynonym, d:SortSynonym) => Ordering[SortSynonym].compare(c, d) + case (c:SyntaxLexical, d:SyntaxLexical) => Ordering[SyntaxLexical].compare(c, d) + case (c:Production, d:Production) => Ordering[Production].compare(c, d) + case (c:SyntaxAssociativity, d:SyntaxAssociativity) => Ordering[SyntaxAssociativity].compare(c, d) + case (c:SyntaxPriority, d:SyntaxPriority) => Ordering[SyntaxPriority].compare(c, d) + case (c:ContextAlias, d:ContextAlias) => Ordering[ContextAlias].compare(c, d) + case (c:Context, d:Context) => Ordering[Context].compare(c, d) + case (c:Rule, d:Rule) => Ordering[Rule].compare(c, d) + case (c:Claim, d:Claim) => Ordering[Claim].compare(c, d) + case (_:SyntaxSort, _) => -1 + case (_, _:SyntaxSort) => 1 + case (_:SortSynonym, _) => -1 + case (_, _:SortSynonym) => 1 + case (_:SyntaxLexical, _) => -1 + case (_, _:SyntaxLexical) => 1 + case (_:Production, _) => -1 + case (_, _:Production) => 1 + case (_:SyntaxAssociativity, _) => -1 + case (_, _:SyntaxAssociativity) => 1 + case (_:SyntaxPriority, _) => -1 + case (_, _:SyntaxPriority) => 1 + case (_:ContextAlias, _) => -1 + case (_, _:ContextAlias) => 1 + case (_:Context, _) => -1 + case (_, _:Context) => 1 + case (_:Rule, _) => -1 + case (_, _:Rule) => 1 + case (_:Claim, _) => -1 + case (_, _:Claim) => 1 + case (_, _) => throw KEMException.internalError("Cannot order these sentences:\n" + a.toString() + "\n" + b.toString()) + } + } + } +} + // deprecated case class Context(body: K, requires: K, att: Att = Att.empty) extends Sentence with OuterKORE with ContextToString { override val isSyntax = false override val isNonSyntax = true override def withAtt(att: Att) = Context(body, requires, att) } +object Context { + implicit val ord: Ordering[Context] = Ordering.by[Context, (K, K, Att)](s => (s.body, s.requires, s.att)) +} case class ContextAlias(body: K, requires: K, att: Att = Att.empty) extends Sentence with OuterKORE with ContextAliasToString { override val isSyntax = true override val isNonSyntax = false override def withAtt(att: Att) = ContextAlias(body, requires, att) } +object ContextAlias { + implicit val ord: Ordering[ContextAlias] = { + Ordering.by[ContextAlias, (K, K, Att)](s => (s.body, s.requires, s.att)) + } +} abstract class RuleOrClaim extends Sentence { def body: K @@ -441,6 +489,11 @@ case class Claim(body: K, requires: K, ensures: K, att: Att = Att.empty) extends override def newInstance(body: K, requires: K, ensures: K, att: Att = Att.empty): Claim = Claim(body, requires, ensures, att) } +object Claim { + implicit val ord: Ordering[Claim] = { + Ordering.by[Claim, (K, K, K, Att)](s => (s.body, s.requires, s.ensures, s.att)) + } +} case class Rule(body: K, requires: K, ensures: K, att: Att = Att.empty) extends RuleOrClaim with RuleToString with OuterKORE { override def withAtt(att: Att): Rule = Rule(body, requires, ensures, att) @@ -449,18 +502,8 @@ case class Rule(body: K, requires: K, ensures: K, att: Att = Att.empty) extends } object Rule { - implicit val ord: Ordering[Rule] = new Ordering[Rule] { - def compare(a: Rule, b: Rule): Int = { - val c1 = Ordering[K].compare(a.body, b.body) - if (c1 == 0) { - val c2 = Ordering[K].compare(a.requires, b.requires) - if (c2 == 0) { - Ordering[K].compare(a.ensures, b.ensures) - } - c2 - } - c1 - } + implicit val ord: Ordering[Rule] = { + Ordering.by[Rule, (K, K, K, Att)](r => (r.body, r.requires, r.ensures, r.att)) } } @@ -474,6 +517,12 @@ case class SyntaxPriority(priorities: Seq[Set[Tag]], att: Att = Att.empty) override val isNonSyntax = false override def withAtt(att: Att) = SyntaxPriority(priorities, att) } +object SyntaxPriority { + implicit val ord: Ordering[SyntaxPriority] = { + import scala.math.Ordering.Implicits._ + Ordering.by[SyntaxPriority, (Seq[Seq[Tag]], Att)](s => (s.priorities.map(_.toSeq.sorted), s.att)) + } +} case class SyntaxAssociativity( assoc: Associativity, @@ -484,9 +533,19 @@ case class SyntaxAssociativity( override val isNonSyntax = false override def withAtt(att: Att) = SyntaxAssociativity(assoc, tags, att) } +object SyntaxAssociativity { + implicit val ord: Ordering[SyntaxAssociativity] = { + import scala.math.Ordering.Implicits._ + Ordering.by[SyntaxAssociativity, (Associativity, Seq[Tag], Att)](s => (s.assoc, s.tags.toSeq.sorted, s.att)) + } +} case class Tag(name: String) extends TagToString with OuterKORE +object Tag { + implicit val ord: Ordering[Tag] = Ordering.by[Tag, String](_.name) +} + //trait Production { // def sort: Sort // def att: Att @@ -503,6 +562,13 @@ case class SyntaxSort(params: Seq[Sort], sort: Sort, att: Att = Att.empty) exten override val isNonSyntax = false override def withAtt(att: Att) = SyntaxSort(params, sort, att) } +object SyntaxSort { + implicit val ord: Ordering[SyntaxSort] = { + import scala.math.Ordering.Implicits._ + Ordering.by[SyntaxSort, (Seq[String], String, Att)](s => (s.params.map(_.name), s.sort.name, s.att)) + } +} + case class SortSynonym(newSort: Sort, oldSort: Sort, att: Att = Att.empty) extends Sentence with SortSynonymToString with OuterKORE { @@ -510,6 +576,12 @@ case class SortSynonym(newSort: Sort, oldSort: Sort, att: Att = Att.empty) exten override val isNonSyntax = false override def withAtt(att: Att) = SortSynonym(newSort, oldSort, att) } +object SortSynonym { + implicit val ord: Ordering[SortSynonym] = { + Ordering.by[SortSynonym, (String, String, Att)](s => (s.newSort.name, s.oldSort.name, s.att)) + } +} + case class SyntaxLexical(name: String, regex: String, att: Att = Att.empty) extends Sentence with SyntaxLexicalToString with OuterKORE { @@ -517,6 +589,11 @@ case class SyntaxLexical(name: String, regex: String, att: Att = Att.empty) exte override val isNonSyntax = false override def withAtt(att: Att) = SyntaxLexical(name, regex, att) } +object SyntaxLexical { + implicit val ord: Ordering[SyntaxLexical] = { + Ordering.by[SyntaxLexical, (String, String, Att)](s => (s.name, s.regex, s.att)) + } +} case class Production(klabel: Option[KLabel], params: Seq[Sort], sort: Sort, items: Seq[ProductionItem], att: Att) extends Sentence with ProductionToString { @@ -638,10 +715,8 @@ case class Production(klabel: Option[KLabel], params: Seq[Sort], sort: Sort, ite } object Production { - implicit val ord: Ordering[Production] = new Ordering[Production] { - def compare(a: Production, b: Production): Int = { - Ordering[Option[String]].compare(a.klabel.map(_.name), b.klabel.map(_.name)) - } + implicit val ord: Ordering[Production] = { + Ordering.by[Production, (Option[String], Att)](s => (s.klabel.map(_.name), s.att)) } def apply(klabel: KLabel, params: Seq[Sort], sort: Sort, items: Seq[ProductionItem], att: Att = Att.empty): Production = { diff --git a/kore/src/test/scala/org/kframework/definition/OuterTest.scala b/kore/src/test/scala/org/kframework/definition/OuterTest.scala index c42cb6fa5d8..54e9beb0399 100644 --- a/kore/src/test/scala/org/kframework/definition/OuterTest.scala +++ b/kore/src/test/scala/org/kframework/definition/OuterTest.scala @@ -4,6 +4,7 @@ package org.kframework.definition import org.junit.{Assert, Test} import org.kframework.attributes.Att +import org.kframework.kore.ADT.KToken import org.kframework.kore.KORE.Sort import org.kframework.kore.KORE.KLabel @@ -90,4 +91,153 @@ class OuterTest { val prod2 = Production(Some(KLabel("foo")), Seq(), Sort("Foo"), Seq(), Att.empty.add(Att.KLABEL, "bar")) Assert.assertNotEquals(prod1, prod2) } + + // Create multiple versions of this sentence with attributes added + def toSentenceAttList(sentence: Sentence): List[Sentence] = { + val att1 = Att.empty.add(Att.ASSOC).add(Att.BAG) + val att2 = Att.empty.add(Att.ASSOC).add(Att.CELL) + val att3 = Att.empty.add(Att.BAG).add(Att.CELL) + val att4 = Att.empty.add(Att.BAG).add(Att.HOOK, "A") + val att5 = Att.empty.add(Att.BAG).add(Att.HOOK, "B") + val att6 = Att.empty.add(Att.BAG).add(Att.LABEL, "A") + val att7 = Att.empty.add(Att.BAG).add(Att.LABEL, "B") + val att8 = Att.empty.add(Att.HOOK, "A").add(Att.LABEL, "B") + val att9 = Att.empty.add(Att.HOOK, "B").add(Att.LABEL, "A") + val sentenceWithAtt1 = sentence.withAtt(att1) + val sentenceWithAtt2 = sentence.withAtt(att2) + val sentenceWithAtt3 = sentence.withAtt(att3) + val sentenceWithAtt4 = sentence.withAtt(att4) + val sentenceWithAtt5 = sentence.withAtt(att5) + val sentenceWithAtt6 = sentence.withAtt(att6) + val sentenceWithAtt7 = sentence.withAtt(att7) + val sentenceWithAtt8 = sentence.withAtt(att8) + val sentenceWithAtt9 = sentence.withAtt(att9) + + List(sentenceWithAtt1, + sentenceWithAtt2, + sentenceWithAtt3, + sentenceWithAtt4, + sentenceWithAtt5, + sentenceWithAtt6, + sentenceWithAtt7, + sentenceWithAtt8, + sentenceWithAtt9) + } + + // Asserts that S1 < S2 < ... < Sn + // Likewise, Sn > ... > S2 > S1 + // And Sx = Sx + def checkOrdering(sentences: List[Sentence]): Unit = { + val ord = Ordering[Sentence] + for (remaining <- sentences.tails.filter(_.nonEmpty)) { + val head = remaining.head + Assert.assertTrue(ord.compare(head, head) == 0) + for (sentence <- remaining.tail) { + Assert.assertTrue(ord.compare(head, sentence) < 0) + Assert.assertTrue(ord.compare(sentence, head) > 0) + } + } + } + + @Test def sentenceOrdering(): Unit = { + val sortA = Sort("A") + val sortB = Sort("B") + val sortC = Sort("C") + + val ktokenA = KToken("A", sortA) + val ktokenB = KToken("B", sortA) + val ktokenC = KToken("C", sortA) + + val tagA = Tag("A") + val tagB = Tag("B") + val tagC = Tag("C") + + val syntaxSort1 = SyntaxSort(Seq(sortA, sortC), sortA) + val syntaxSort2 = SyntaxSort(Seq(sortA, sortC), sortB) + val syntaxSort3 = SyntaxSort(Seq(sortB, sortC), sortA) + + val synonym1 = SortSynonym(sortA, sortA) + val synonym2 = SortSynonym(sortA, sortB) + val synonym3 = SortSynonym(sortB, sortC) + + val lexical1 = SyntaxLexical("A", "A") + val lexical2 = SyntaxLexical("A", "B") + val lexical3 = SyntaxLexical("B", "A") + + val production1 = Production(Seq(), sortA, Seq(), Att.empty) + val production2 = Production(KLabel("A"), Seq(), sortA, Seq(), Att.empty) + val production3 = Production(KLabel("B"), Seq(), sortA, Seq(), Att.empty) + + val syntaxAssoc1 = SyntaxAssociativity(Associativity.Left, Set(tagA)) + val syntaxAssoc2 = SyntaxAssociativity(Associativity.Left, Set(tagB)) + val syntaxAssoc3 = SyntaxAssociativity(Associativity.Right, Set(tagA)) + + val syntaxPriority1 = SyntaxPriority(Seq(Set(tagB, tagA))) + val syntaxPriority2 = SyntaxPriority(Seq(Set(tagA, tagB, tagC), Set(tagB))) + val syntaxPriority3 = SyntaxPriority(Seq(Set(tagA, tagB, tagC), Set(tagC))) + val syntaxPriority4 = SyntaxPriority(Seq(Set(tagA, tagC, tagC), Set(tagB))) + val syntaxPriority5 = SyntaxPriority(Seq(Set(tagB))) + + val contextAlias1 = ContextAlias(ktokenA, ktokenA) + val contextAlias2 = ContextAlias(ktokenA, ktokenB) + val contextAlias3 = ContextAlias(ktokenB, ktokenB) + + val context1 = Context(ktokenA, ktokenA) + val context2 = Context(ktokenA, ktokenB) + val context3 = Context(ktokenB, ktokenA) + + val rule1 = Rule(ktokenA, ktokenA, ktokenA) + val rule2 = Rule(ktokenA, ktokenA, ktokenB) + val rule3 = Rule(ktokenA, ktokenA, ktokenC) + val rule4 = Rule(ktokenA, ktokenB, ktokenA) + val rule5 = Rule(ktokenB, ktokenA, ktokenA) + + val claim1 = Claim(ktokenA, ktokenA, ktokenA) + val claim2 = Claim(ktokenA, ktokenA, ktokenB) + val claim3 = Claim(ktokenA, ktokenA, ktokenC) + val claim4 = Claim(ktokenA, ktokenB, ktokenA) + val claim5 = Claim(ktokenB, ktokenA, ktokenA) + + val sentenceList = List( + syntaxSort1, + syntaxSort2, + syntaxSort3, + synonym1, + synonym2, + synonym3, + lexical1, + lexical2, + lexical3, + production1, + production2, + production3, + syntaxAssoc1, + syntaxAssoc2, + syntaxAssoc3, + syntaxPriority1, + syntaxPriority2, + syntaxPriority3, + syntaxPriority4, + syntaxPriority5, + contextAlias1, + contextAlias2, + contextAlias3, + context1, + context2, + context3, + rule1, + rule2, + rule3, + rule4, + rule5, + claim1, + claim2, + claim3, + claim4, + claim5) + + val sentenceListWithAtts = sentenceList.flatMap(toSentenceAttList(_)) + + checkOrdering(sentenceListWithAtts) + } }