Revert "Ordering instance for Sentences" (#3622)

Reverts #3590

k-distribution/tests/builtins/collections/test-set2list-2.col.out

@@ -1,6 +1,6 @@
 <k>
-  ListItem ( 1 )
-  ListItem ( 2 )
+  ListItem ( 4 )
   ListItem ( 3 )
-  ListItem ( 4 ) ~> .
+  ListItem ( 2 )
+  ListItem ( 1 ) ~> .
 </k>

k-distribution/tests/builtins/collections/test-set2list-3.col.out

@@ -1,5 +1,5 @@
 <k>
-  ListItem ( 1 )
+  ListItem ( 4 )
   ListItem ( 3 )
-  ListItem ( 4 ) ~> .
+  ListItem ( 1 ) ~> .
 </k>

kore/src/main/scala/org/kframework/attributes/Att.scala

@@ -414,11 +414,6 @@ 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 {

kore/src/main/scala/org/kframework/definition/outer.scala

@@ -414,66 +414,18 @@ 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
@@ -489,11 +441,6 @@ 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)
@@ -502,8 +449,18 @@ case class Rule(body: K, requires: K, ensures: K, att: Att = Att.empty) extends
 }
 
 object Rule {
-  implicit val ord: Ordering[Rule] = {
-    Ordering.by[Rule, (K, K, K, Att)](r => (r.body, r.requires, r.ensures, r.att))
+  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
+    }
   }
 }
 
@@ -517,12 +474,6 @@ 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,
@@ -533,19 +484,9 @@ 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
@@ -562,38 +503,20 @@ 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 {
@@ -715,8 +638,10 @@ case class Production(klabel: Option[KLabel], params: Seq[Sort], sort: Sort, ite
 }
 
 object Production {
-  implicit val ord: Ordering[Production] = {
-    Ordering.by[Production, (Option[String], Att)](s => (s.klabel.map(_.name), s.att))
+  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))
+    }
   }
 
   def apply(klabel: KLabel, params: Seq[Sort], sort: Sort, items: Seq[ProductionItem], att: Att = Att.empty): Production = {

kore/src/test/scala/org/kframework/definition/OuterTest.scala

@@ -4,7 +4,6 @@ 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
 
@@ -91,153 +90,4 @@ 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)
-  }
 }