Ordering instance for Sentences

[gtrepta]

fixes: #3530

[Robertorosmaninho]

@gtrepta This Ordering.by is the same as using Compare to compare 2 elements to sort them?

[gtrepta]

This Ordering.by is the same as using Compare to compare 2 elements to sort them?

I'm not sure what the Compare you're referring to is. But Ordering.by allows you to define a sorting strategy for a (normally ADT) type T in terms of a type S, and you give it a function T => S.

ex. For the case class Tag(name: String) you can make an ordering for it using its name field with Ordering.by[Tag, String](t: Tag => t.name), so you use Scala's implicit ordering for String to sort the Tag datatype.

https://www.scala-lang.org/api/2.12.14/scala/math/Ordering.html

[Robertorosmaninho]

This Ordering.by is the same as using Compare to compare 2 elements to sort them?

I'm not sure what the Compare you're referring to is. But Ordering.by allows you to define a sorting strategy for a (normally ADT) type T in terms of a type S, and you give it a function T => S.

ex. For the case class Tag(name: String) you can make an ordering for it using its name field with Ordering.by[Tag, String](t: Tag => t.name), so you use Scala's implicit ordering for String to sort the Tag datatype.

https://www.scala-lang.org/api/2.12.14/scala/math/Ordering.html

Got it! But I'm not sure yet how we (or Scala implicitly) decide how to compare and sort the type K.
Also, we're missing the sorting of Attributes. TBH, this is a key feature that we really want to have here.

[Robertorosmaninho]

We really need to consider the Att on the objects to sort them. Even though it can be costly, it will be worse to sort them later regarding the Att.

By considering the Att, we can safely compare two objects for equality, and we can safely enable decoupling the Add Kore Attribute function on ModuleToKore.

[gtrepta]

@Robertorosmaninho

Ordering for K is here:

k/kore/src/main/scala/org/kframework/kore/interface.scala

Lines 33 to 61 in ab225b2

	implicit val ord = new Ordering[K] {
	def compare(a: K, b: K): Int = {
	import scala.math.Ordering.Implicits._
	(a, b) match {
	case (c: KToken, d: KToken) => Ordering.Tuple2(Ordering[String], Ordering[Sort]).compare((c.s, c.sort), (d.s, d.sort))
	case (c: KApply, d: KApply) => Ordering.Tuple2(KLabelOrdering, seqDerivedOrdering[Seq, K](this)).compare((c.klabel, c.klist.items.asScala), (d.klabel, d.klist.items.asScala))
	case (c: KSequence, d: KSequence) => seqDerivedOrdering(this).compare(c.items.asScala, d.items.asScala)
	case (c: KVariable, d: KVariable) => Ordering[String].compare(c.name, d.name)
	case (c: KAs, d: KAs) => Ordering.Tuple2(this, this).compare((c.pattern, c.alias), (d.pattern, d.alias))
	case (c: KRewrite, d: KRewrite) => Ordering.Tuple2(this, this).compare((c.left, c.right), (d.left, d.right))
	case (c: InjectedKLabel, d: InjectedKLabel) => KLabelOrdering.compare(c.klabel, d.klabel)
	case (_:KToken, _) => 1
	case (_, _:KToken) => -1
	case (_:KApply, _) => 1
	case (_, _:KApply) => -1
	case (_:KSequence, _) => 1
	case (_, _:KSequence) => -1
	case (_:KVariable, _) => 1
	case (_, _:KVariable) => -1
	case (_:KAs, _) => 1
	case (_, _:KAs) => -1
	case (_:KRewrite, _) => 1
	case (_, _:KRewrite) => -1
	case (_:InjectedKLabel, _) => 1
	case (_, _:InjectedKLabel) => -1
	case (_, _) => throw KEMException.internalError("Cannot order these terms:\n" + a.toString() + "\n" + b.toString())
	}
	}
	}

I can create an ordering for attributes as well. But, are you thinking about the attributes being factored in when ordering sentences? Because I can't think of an occurrence where it would come down to that. Just saw the change request, I'll implement it.

[Robertorosmaninho]

I can create an ordering for attributes as well. But, are you thinking about the attributes being factored in when ordering sentences? Because I can't think of an occurrence where it would come down to that. Just saw the change request, I'll implement it.

To give you more context, we had to revert these 2 PRs(#3523, #3522) due to the slowdown in the kompile time. One of the main reasons was that we had to do a linear pass to all productions and compare every attribute list just to check if we had or not to apply the compiler pass.

[Robertorosmaninho]

Nevertheless, @gtrepta, I would like to have a third opinion on this, perhaps @dwightguth or @radumereuta can help us on this.

[dwightguth]

This doesn't feel quite right. Shouldn't it have a case where both are the same and it compares their contents?

[gtrepta]

I had them there but removing them didn't break the unit tests I wrote, so I figured when they're the same type then the ordering for that specific type is used instead of going up the type heirarchy.

[gtrepta]

Looks like we do need those extra cases. I pushed the fix.

[radumereuta]

Can you remind me why the ordering is needed? To make comparisons faster?
This code touches the core data structures of kompile, and they are very sensitive to performance losses.
Before we merge this, it needs to be tested with the c-semantics and the evm-semantics.
Run kompile -v. The step Apply compile pipeline should not be slower.

[gtrepta]

@radumereuta The compile pipeline didn't run any slower on those semantics.

[Robertorosmaninho]

Hey @gtrepta, this test is failing rn, any ideas on the reason?

[exec] make[1]: Entering directory '/opt/workspace/k-distribution/tests/builtins/collections'
     [exec] set -o pipefail; (cat test-set2list-2.col.in 2>/dev/null || true) | /opt/workspace/k-distribution/bin/krun test-set2list-2.col --no-exc-wrap  --definition ./collections-test-kompiled | diff - test-set2list-2.col.out
     [exec] 2,3c2
     [exec] <   ListItem ( 1 )
     [exec] <   ListItem ( 2 )
     [exec] ---
     [exec] >   ListItem ( 4 )
     [exec] 5c4,5
     [exec] <   ListItem ( 4 ) ~> .
     [exec] ---
     [exec] >   ListItem ( 2 )
     [exec] >   ListItem ( 1 ) ~> .
     [exec] make[1]: Leaving directory '/opt/workspace/k-distribution/tests/builtins/collections'

[gtrepta]

Hey @gtrepta, this test is failing rn, any ideas on the reason? ...

It's most likely some nondeterminism from printing/converting sets, the expected output only recognizes one of multiple possible outcomes. I've seen plenty of tests break in this fashion, normally we just update the expected output in the PR that it's breaking in.

[Robertorosmaninho]

LGTM! Thanks for your contribution on this @gtrepta!