Skip to content

Commit

Permalink
Ordering instance for Sentences (2) (#3670)
Browse files Browse the repository at this point in the history 
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 <[email protected]>
  • Loading branch information
@gtrepta @rv-jenkins
gtrepta and rv-jenkins authored Sep 30, 2023
1 parent 3a2ffbe commit c71f50d
Show file tree
Hide file tree
Showing 5 changed files with 251 additions and 21 deletions.
6 changes: 3 additions & 3 deletions k-distribution/tests/builtins/collections/test-set2list-2.col.out
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
<k>
ListItem ( 4 )
ListItem ( 3 )
ListItem ( 1 )
ListItem ( 2 )
ListItem ( 1 ) ~> .
ListItem ( 3 )
ListItem ( 4 ) ~> .
</k>
4 changes: 2 additions & 2 deletions k-distribution/tests/builtins/collections/test-set2list-3.col.out
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
<k>
ListItem ( 4 )
ListItem ( 1 )
ListItem ( 3 )
ListItem ( 1 ) ~> .
ListItem ( 4 ) ~> .
</k>
5 changes: 5 additions & 0 deletions kore/src/main/scala/org/kframework/attributes/Att.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
107 changes: 91 additions & 16 deletions kore/src/main/scala/org/kframework/definition/outer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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))
}
}

Expand All @@ -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,
Expand All @@ -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
Expand All @@ -503,20 +562,38 @@ 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 {

override val isSyntax = true
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 {

override val isSyntax = true
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 {
Expand Down Expand Up @@ -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 = {
Expand Down
150 changes: 150 additions & 0 deletions kore/src/test/scala/org/kframework/definition/OuterTest.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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)
}
}

0 comments on commit c71f50d

Please sign in to comment.