Pretty printer using wrong unparsing module for rules

[radumereuta]

Fixes: #1509

[ehildenb]

@radumereuta can you check if any of these changes are corrections that need to be applied regardless of the source issue? If so, can you provide examples? Otherwise, I think we need to close this until the discussion on the attached issue is finished.

[radumereuta]

@dwightguth please have another look.
I've changed the test from json to kore, and it fails on master with:

kast --input kore --output kore out.kore --debug
java.util.NoSuchElementException: key not found: #SemanticCastToK
	at scala.collection.MapLike.default(MapLike.scala:232)
	at scala.collection.MapLike.default$(MapLike.scala:231)
	at scala.collection.AbstractMap.default(Map.scala:59)
	at scala.collection.MapLike.apply(MapLike.scala:141)
	at scala.collection.MapLike.apply$(MapLike.scala:140)
	at scala.collection.AbstractMap.apply(Map.scala:59)
	at org.kframework.compile.AddSortInjections.production(AddSortInjections.java:409)
	at org.kframework.compile.AddSortInjections.visitChildren(AddSortInjections.java:178)
	at org.kframework.compile.AddSortInjections.internalAddSortInjections(AddSortInjections.java:152)
	at org.kframework.compile.AddSortInjections.visitChildren(AddSortInjections.java:189)
	at org.kframework.compile.AddSortInjections.internalAddSortInjections(AddSortInjections.java:125)
	at org.kframework.compile.AddSortInjections.visitChildren(AddSortInjections.java:189)
	at org.kframework.compile.AddSortInjections.internalAddSortInjections(AddSortInjections.java:125)
	at org.kframework.compile.AddSortInjections.visitChildren(AddSortInjections.java:189)
	at org.kframework.compile.AddSortInjections.internalAddSortInjections(AddSortInjections.java:125)
	at org.kframework.compile.AddSortInjections.addSortInjections(AddSortInjections.java:87)
	at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:182)
	at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:152)
	at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:140)
	at org.kframework.kast.KastFrontEnd.run(KastFrontEnd.java:147)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:62)
	at org.kframework.main.Main.runApplication(Main.java:119)
	at org.kframework.main.Main.runApplication(Main.java:109)
	at org.kframework.main.Main.main(Main.java:57)
[Error] Internal: Uncaught exception thrown of type NoSuchElementException
(NoSuchElementException: key not found: #SemanticCastToK)

[ehildenb]

It looks OK to me, looks like the major change is just that with PROGRAM unparser, you use a different module than with the other ones. Looks like you've also made the example test as a Kore-to-Kore test, which is good for avoiding any problems with the JSON KAST format.

Would still like @dwightguth to have a look though.

[radumereuta]

This PR doesn't actually fix the original issue. It fixes the kore to kore transformations (should be considered more of a validation) which was also broken.
The problem with JSON still remains since it's a lossy transformation, and during unparsing it fails to reproduce the proper terms.
So I guess @dwightguth should also have a look.

[dwightguth]

If we're just talking about kast -i kore -o kore, I don't like this as a solution. It would be better to make AddSortInjections aware of the semantic casts when they are applied to variables and use it to construct the correctly sorted variable. as it currently stands, I don't believe you're going to end up with the right output AST.

[radumereuta]

Now that you mention it, the input and output are significantly different sort wise.
So the most likely culprit is AddSortInjections? (just so I know where to look first)