Audit ModuleToKore for non-trivial operations

[Baltoli]

We currently do a lot of "extra" work inside ModuleToKore that would be better implemented as explicit compiler passes; Pyk doesn't need to do this, which indicates that ModuleToKore could be simplified down to a trivial Kast -> Text transformation.

The first step towards simplifying the code is to dig through it and find places where we're doing this extra work, and make it an explicit compiler pass before ModuleToKore runs.

[ehildenb]

Examples:

• Adding attributes:

  k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

  Line 249 in a017998

  for (Production prod : iterable(module.sortedProductions())) {

• Generating assoc/comm/idem/unit axioms:

  k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

  Line 440 in a017998

  private void genAssocAxiom(Production prod, StringBuilder sb) {

• Generating Ceil axioms:

  k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

  Line 566 in a017998

  private void genMapCeilAxioms(Production prod, Collection<Rule> rules) {

• Inserting priorities:

  k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

  Line 698 in a017998

  public static int getPriority(Att att) {

• Generating no-junk/overloads:

  k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

  Line 711 in a017998

  private void genNoJunkAxiom(Sort sort, StringBuilder sb) {

• Throwing errors in ModuleToKore can become checks over the Kast:

  k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

  Line 1274 in a017998

  private void assertNoExistentials(Sentence sentence, Set<KVariable> existentials) {

• Adding Kore attributes:

  k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

  Line 1493 in a017998

  private Att addKoreAttributes(Production prod, SetMultimap<KLabel, Rule> functionRules, Set<Production> overloads) {

• Converting side-conditions to ML predicates:

  k/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

  Line 1641 in a017998

  private void convertSideCondition(K k, StringBuilder sb) {

[radumereuta]

The last few commits referenced here have been reverted since they introduced noticeable performance regressions.
Please revisit when we have a better understanding of what went wrong.
The reverts: #3554 #3560

[dwightguth]

I'm pretty sure the performance regression is related to the fact that I spotted duplicate instances of certain rules in the definition before this change was reverted and now they're gone. I would suggest double checking that you didn't pass module.sentences() somewhere that module.localSentences() was appropriate. This type of duplication often happens due to a mistake where a module is transformed to include all the sentences from its recursive imports.

[Baltoli]

Closing this as superseded by @tothtamas28's recent work on translating M2K to Pyk.