in meta/src/main/java/org/arend/lib/util/Utils.java [268:300]
public static Pair<TypedExpression, CoreClassCallExpression> findInstanceWithClassCall(InstanceSearchParameters parameters, CoreClassField classifyingField, CoreExpression classifyingExpr, ExpressionTypechecker typechecker, ConcreteSourceNode marker, CoreClassDefinition forcedClass) {
return typechecker.withCurrentState(tc -> {
Pair<TypedExpression, CoreClassCallExpression> result = findInstanceWithClassCall(parameters, classifyingField, classifyingExpr, typechecker, marker);
if (result == null) {
if (forcedClass != null) {
typechecker.getErrorReporter().report(new InstanceInferenceError(typechecker.getExpressionPrettifier(), forcedClass.getRef(), classifyingExpr, marker));
} else {
tc.loadSavedState();
}
return null;
}
CoreExpression classifyingImpl = result.proj2.getImplementation(classifyingField, result.proj1);
if (classifyingImpl != null && !Boolean.TRUE.equals(tryWithSavedState(tc, tc2 -> tc2.compare(classifyingImpl, classifyingExpr, CMP.LE, marker, true, true, false)))) {
if (forcedClass != null) {
typechecker.getErrorReporter().report(new InstanceInferenceError(typechecker.getExpressionPrettifier(), forcedClass.getRef(), classifyingExpr, marker, new CoreExpression[]{result.proj1.getExpression()}));
} else {
tc.loadSavedState();
}
return null;
}
CoreExpression expr = result.proj1.getExpression();
if (expr instanceof CoreFunCallExpression funCall) {
for (CoreExpression argument : funCall.getDefCallArguments()) {
if (argument instanceof CoreInferenceReferenceExpression infExpr && infExpr.getSubstExpression() == null) {
tc.loadSavedState();
return null;
}
}
}
return result;
});
}