public void solve()

in meta/src/main/java/org/arend/lib/goal/ConstructorGoalSolver.java [49:126]
75 lines of code
20 McCabe index (conditional complexity)

  public void solve(@NotNull ExpressionTypechecker typechecker, @NotNull ConcreteGoalExpression goalExpression, @Nullable CoreExpression expectedType, @NotNull ArendUI ui, @NotNull Consumer<ConcreteExpression> callback) {
    CoreExpression type = expectedType == null ? null : Utils.unfoldType(expectedType.normalize(NormalizationMode.WHNF));
    ConcreteFactory factory = ext.factory.withData(goalExpression.getData());

    ConcreteExpression result;
    if (type instanceof CoreSigmaExpression) {
      List<ConcreteExpression> goals = new ArrayList<>();
      for (CoreParameter param = ((CoreSigmaExpression) type).getParameters(); param.hasNext(); param = param.getNext()) {
        goals.add(factory.goal());
      }
      result = factory.tuple(goals);
    } else if (type instanceof CorePiExpression) {
      List<CoreParameter> params = new ArrayList<>();
      type.getPiParameters(params);
      List<ConcreteParameter> cParams = new ArrayList<>(params.size());
      VariableRenamer renamer = ext.renamerFactory.variableRenamer();
      List<CoreBinding> freeVars = typechecker.getFreeBindingsList();
      for (CoreParameter param : params) {
        cParams.add(factory.param(param.isExplicit(), factory.local(renamer.generateFreshName(param.getBinding(), freeVars))));
        freeVars.add(param.getBinding());
      }
      result = factory.lam(cParams, factory.goal());
    } else if (type instanceof CoreClassCallExpression) {
      Boolean isEmptyArray = Utils.isArrayEmpty(type, ext);
      if (isEmptyArray == null) {
        CoreClassCallExpression classCall = (CoreClassCallExpression) type;
        List<ConcreteClassElement> classElements = new ArrayList<>();
        for (CoreClassField field : classCall.getDefinition().getNotImplementedFields()) {
          if (!classCall.isImplementedHere(field)) {
            classElements.add(factory.implementation(field.getRef(), factory.goal()));
          }
        }
        result = factory.newExpr(factory.classExt(factory.ref(classCall.getDefinition().getRef()), classElements));
      } else if (isEmptyArray) {
        result = factory.ref(ext.prelude.getEmptyArray().getRef());
      } else {
        result = factory.app(factory.ref(ext.prelude.getArrayCons().getRef()), true, Arrays.asList(factory.goal(), factory.goal()));
      }
    } else if (type instanceof CoreDataCallExpression dataCall) {
      if (dataCall.getDefinition() == ext.prelude.getPath()) {
        CoreFunCallExpression eq = dataCall.toEquality();
        if (eq != null && eq.getDefCallArguments().get(1).compare(eq.getDefCallArguments().get(2), CMP.EQ)) {
          callback.accept(factory.ref(ext.prelude.getIdp().getRef()));
          return;
        }
      }

      List<CoreConstructor> constructors = new ArrayList<>();
      dataCall.computeMatchedConstructors(constructors);
      if (constructors.isEmpty()) {
        result = null;
      } else if (constructors.size() == 1) {
        result = Utils.addArguments(factory.ref(constructors.get(0).getRef()), factory, Utils.numberOfExplicitParameters(constructors.get(0)), true);
      } else {
        ArendSession session = ui.newSession();
        session.setDescription("Goal");
        ArendQuery<CoreConstructor> query = session.listQuery("Choose constructor", constructors, null);
        session.setCallback(ok -> {
          if (ok) {
            CoreConstructor constructor = query.getResult();
            if (constructor != null) {
              callback.accept(Utils.addArguments(factory.ref(constructor.getRef()), factory, Utils.numberOfExplicitParameters(constructor), true));
            }
          }
        });
        session.startSession();
        return;
      }
    } else {
      result = null;
    }

    if (result != null) {
      callback.accept(result);
    } else {
      ui.showErrorMessage(null, "Goal type does not have constructors");
    }
  }