MinimizeTermConstruction's behavior intersecting GuardOrPattern's functionality

[gtrepta]

Following up on discussions in #3973

GuardOrPatterns, introduced in #340, wraps #Or terms on the RHS of rules in #as patterns to remove ambiguity. A regression test, or-llvm was updated to exercise the case that this pass is meant to cover.

Today, if the pass is removed from the compiler pipeline, those tests still pass, and the #Or terms in the RHS of rules in the generated kore are still wrapped up in #as patterns. It happens here, in MinimizeTermConstruction, sometime after the KoreBackend.steps transformation:

k/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java

Lines 169 to 176 in ef56dd9

	if (isLHS() && !isRHS() && !inBad) {
	if (usedOnRhs.contains(k)) {
	return KAs(
	super.apply(k),
	cache.get(k),
	Att.empty()
	.add(Att.SORT(), Sort.class, cache.get(k).att().get(Att.SORT(), Sort.class)));
	}

I believe this isn't intended. It looks as if #Or patterns are explicitly meant to not be operated on:

k/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java

Lines 186 to 188 in ef56dd9

	if (k.klabel().head().equals(KLabels.ML_OR)) {
	inBad = true;
	}

So somehow the bookkeeping done by this Transformer as it traverses the terms gets messed up and the value of inBad is wrong when visiting the #Or term.

[gtrepta]

After discussing with Dwight, I've learned that MinimizeTermConstruction is meant as an optimization to reduce the number of constructors in a rewrite, and is likely doing what it's supposed to. GuardOrPatterns is to ensure correctness. It's possible that there's a case that GuardOrPatterns handles that MinimizeTermConstruction doesn't handle, but it would probably be pretty difficult to find.

I've created a PR to add a little documentation to MinimizeTermConstruction, and we can close this.