in base/src/main/java/org/arend/typechecking/implicitargs/equations/TwoStageEquations.java [678:848]
private boolean solveClassCallLowerBounds(List<Pair<InferenceVariable, List<ClassCallExpression>>> list, boolean allOK, boolean solved, CMP cmp, boolean useWrapper) {
loop:
for (Pair<InferenceVariable, List<ClassCallExpression>> pair : list) {
if (pair.proj2.size() == 1) {
solve(pair.proj1, pair.proj2.get(0), true);
solved = true;
continue;
}
ClassDefinition classDef = checkClasses(pair.proj1, pair.proj2, cmp);
if (classDef == null) {
allOK = false;
continue;
}
UniverseKind universeKind = classDef.getUniverseKind();
if (universeKind != UniverseKind.NO_UNIVERSES) {
universeKind = UniverseKind.NO_UNIVERSES;
for (ClassField field : classDef.getNotImplementedFields()) {
if (field.getUniverseKind() == UniverseKind.NO_UNIVERSES) {
continue;
}
boolean implemented = false;
for (ClassCallExpression classCall : pair.proj2) {
if (classCall.isImplementedHere(field)) {
implemented = true;
break;
}
}
if (!implemented) {
universeKind = universeKind.max(field.getUniverseKind());
if (universeKind == UniverseKind.WITH_UNIVERSES) {
break;
}
}
}
}
ClassCallExpression solution;
if (cmp == CMP.LE) {
Equations wrapper = useWrapper ? new LevelEquationsWrapper(this) : this;
Levels levels = classDef.generateInferVars(this, pair.proj1.getSourceNode());
Map<ClassField, Expression> implementations = new LinkedHashMap<>();
solution = new ClassCallExpression(classDef, levels, implementations, classDef.getSort(), universeKind);
ReferenceExpression thisExpr = new ReferenceExpression(solution.getThisBinding());
int minIndex = 0;
int minValue = Integer.MAX_VALUE;
for (int i = 0; i < pair.proj2.size(); i++) {
ClassCallExpression classCall = pair.proj2.get(i);
if (classCall.getDefinition() == classDef && classCall.getImplementedHere().size() < minValue) {
minIndex = i;
minValue = classCall.getImplementedHere().size();
}
}
ClassCallExpression minClassCall = pair.proj2.get(minIndex);
pair.proj2.remove(minIndex);
for (Map.Entry<ClassField, Expression> entry : minClassCall.getImplementedHere().entrySet()) {
implementations.put(entry.getKey(), entry.getValue().subst(minClassCall.getThisBinding(), thisExpr));
}
for (ClassCallExpression bound : pair.proj2) {
for (Iterator<Map.Entry<ClassField, Expression>> iterator = implementations.entrySet().iterator(); iterator.hasNext(); ) {
Map.Entry<ClassField, Expression> entry = iterator.next();
boolean remove = !entry.getKey().isProperty();
if (remove) {
Expression other = bound.getAbsImplementationHere(entry.getKey());
if (other != null) {
Expression expr = entry.getValue().subst(solution.getThisBinding(), new ReferenceExpression(bound.getThisBinding())).normalize(NormalizationMode.WHNF);
other = other.normalize(NormalizationMode.WHNF);
Expression type = expr.getType();
CompareVisitor cmpVisitor = new CompareVisitor(wrapper, CMP.EQ, pair.proj1.getSourceNode());
remove = !cmpVisitor.compare(type, other.getType(), Type.OMEGA, false) || !cmpVisitor.normalizedCompare(expr, other, type, true);
}
}
if (remove) {
iterator.remove();
}
}
}
if (classDef == Prelude.DEP_ARRAY) {
if (!implementations.containsKey(Prelude.ARRAY_ELEMENTS_TYPE)) {
Expression expr = minClassCall.getAbsImplementationHere(Prelude.ARRAY_ELEMENTS_TYPE);
if (expr != null) {
expr = expr.removeConstLam();
}
if (expr != null) {
boolean ok = true;
for (ClassCallExpression bound : pair.proj2) {
Expression other = bound.getAbsImplementationHere(Prelude.ARRAY_ELEMENTS_TYPE);
if (other != null) {
other = other.removeConstLam();
}
if (other != null) {
Expression type = expr.getType();
CompareVisitor cmpVisitor = new CompareVisitor(wrapper, CMP.EQ, pair.proj1.getSourceNode());
if (!(cmpVisitor.compare(type, other.getType(), Type.OMEGA, false) && cmpVisitor.normalizedCompare(expr, other, type, true))) {
ok = false;
break;
}
}
}
if (ok) {
implementations.put(Prelude.ARRAY_ELEMENTS_TYPE, new LamExpression(minClassCall.getSort(), new TypedSingleDependentLink(true, null, ExpressionFactory.Fin(ExpressionFactory.FieldCall(Prelude.ARRAY_LENGTH, new ReferenceExpression(solution.getThisBinding())))), expr));
}
}
}
} else {
solution.removeDependencies(minClassCall.getImplementedHere().keySet());
}
solution.setSort(classDef.computeSort(implementations, solution.getThisBinding()));
solution.updateHasUniverses();
if (!pair.proj2.get(0).getLevels().compare(levels, CMP.LE, this, pair.proj1.getSourceNode())) {
reportBoundsError(pair.proj1, pair.proj2, CMP.GE);
allOK = false;
continue;
}
for (ClassCallExpression lowerBound : pair.proj2) {
if (!new CompareVisitor(this, CMP.LE, pair.proj1.getSourceNode()).compareClassCallLevels(lowerBound, solution)) {
reportBoundsError(pair.proj1, pair.proj2, CMP.GE);
allOK = false;
continue loop;
}
}
} else {
solution = pair.proj2.get(0);
Map<ClassField, Expression> map = solution.getImplementedHere();
Expression thisExpr = new ReferenceExpression(solution.getThisBinding());
for (int i = 1; i < pair.proj2.size(); i++) {
Map<ClassField, Expression> otherMap = pair.proj2.get(i).getImplementedHere();
if (map.size() != otherMap.size()) {
boolean ok = true;
for (ClassField field : map.keySet()) {
if (!field.isProperty() && !otherMap.containsKey(field)) {
ok = false;
break;
}
}
for (ClassField field : otherMap.keySet()) {
if (!field.isProperty() && !map.containsKey(field)) {
ok = false;
break;
}
}
if (!ok) {
reportBoundsError(pair.proj1, pair.proj2, CMP.LE);
allOK = false;
continue loop;
}
}
for (Map.Entry<ClassField, Expression> entry : map.entrySet()) {
if (entry.getKey().isProperty()) continue;
Expression other = otherMap.get(entry.getKey());
if (other == null || !CompareVisitor.compare(this, CMP.EQ, entry.getValue(), other, solution.getDefinition().getFieldType(entry.getKey(), solution.getLevels(entry.getKey().getParentClass()), thisExpr), pair.proj1.getSourceNode())) {
reportBoundsError(pair.proj1, pair.proj2, CMP.LE);
allOK = false;
continue loop;
}
}
}
}
solve(pair.proj1, solution, true);
solved = true;
}
return allOK && solved;
}