public static Pair findInstanceWithClassCall()

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;
    });
  }