in meta/src/main/java/org/arend/lib/meta/equation/MonoidSolver.java [587:627]
private List<Integer> applyRules(List<Integer> term, List<RuleExt> rules, List<Step> trace) {
boolean hasBadRules = false;
for (RuleExt rule : rules) {
if (rule.isIncreasing()) {
hasBadRules = true;
break;
}
}
int i = 0;
boolean found;
do {
found = false;
for (RuleExt rule : rules) {
int pos = Collections.indexOfSubList(term, rule.lhs);
if (rule.direction == Direction.UNKNOWN) {
if (pos < 0) {
pos = Collections.indexOfSubList(term, rule.rhs);
if (pos >= 0) {
rule.setBackward();
}
} else {
rule.direction = Direction.FORWARD;
}
if (rule.isIncreasing()) {
hasBadRules = true;
}
}
if (pos >= 0) {
Step step = new Step(rule, pos);
trace.add(step);
term = step.apply(term);
found = true;
break;
}
}
i++;
} while (found && (!hasBadRules || i < MAX_STEPS));
return term;
}