Audit uses of simplifyCondition

[ttuegel]

I am auditing the uses of simplifyCondition to identify places where it might be used inappropriately.

• Kore.Step.Simplification.Simplify: OK, class defined here.
• Kore.Step.Simplification.Condition: OK, implemented here.
• Kore.Step.Simplification.Data: OK, implementation hooked into instance here.
• Kore.Builtin.KEqual: called within unification, might not be OK.
• Kore.Equation.Application: OK, used to requirements of equations.
• Kore.Step.Step: OK, used to simplify requirements of rewrite rules.
• Kore.Step.RewriteStep: OK, used to simplify requirements of rewrite rules.
• Kore.Step.Substitution: used to implement mergePredicatesAndSubstitutions; should probably be deprecated.
• Kore.Step.Function.Evaluator: essentially used to reimplement the Pattern simplifier; should not be used here.
• Kore.Step.Rule.Combine: OK, used to simplify requirements of merged rules.
• Kore.Step.Simplification.Exists: not OK, should be rewritten so that re-simplifying child patterns is not required.
• Kore.Step.Simplification.OrPattern: not OK, should not be used multiple times here.
• Kore.Step.Simplification.Pattern: OK, used to implement the Pattern simplifier.
• Kore.Step.Simplification.TermLike: not OK, the TermLike simplifier should not need to simplify conditions.
• Kore.Unification.Procedure: OK, used to simplify the result of solving \in.
• Kore.Unification.UnifierT: OK, implementation hooked into instance here.
• Kore.Unification.SubstitutionSimplifier: OK, used to simplify the result of solving \and.

[ttuegel]

Because the condition simplifier is used inappropriately in the term simplifier, many uses of the latter should be changed to use the pattern simplifier.

[ttuegel]

1. Move Condition.simplifyPredicate to its own module and implement a Predicate.simplify similar to TermLike.simplify. It must not call simplifyCondition or simplifyTermLike.
2. Add simplifyPattern to MonadSimplify.
3. Pattern.simplify may call TermLike.simplify directly.
4. The remaining calls to simplifyTermLike should become simplifyPattern instead.
5. TermLike.simplify must also not call simplifyCondition.
6. Remove simplifyTermLike.