public ConcreteExpression solve()

in meta/src/main/java/org/arend/lib/meta/equation/RingSolver.java [96:149]
49 lines of code
17 McCabe index (conditional complexity)

  public ConcreteExpression solve(@Nullable ConcreteExpression hint, @NotNull TypedExpression leftExpr, @NotNull TypedExpression rightExpr, @NotNull ErrorReporter errorReporter) {
    TermCompiler.CompiledTerm term1 = lastTerm == leftExpr ? lastCompiled : termCompiler.compileTerm(leftExpr.getExpression());
    TermCompiler.CompiledTerm term2 = termCompiler.compileTerm(rightExpr.getExpression());
    lastTerm = rightExpr;
    lastCompiled = term2;

    if (isCommutative) {
      toCommutativeNF(term1.nf);
      toCommutativeNF(term2.nf);
    }

    List<Monomial> nf1 = term1.nf;
    List<Monomial> nf2 = term2.nf;
    if (termCompiler.isLattice) {
      removeDuplicates(nf1);
      removeDuplicates(nf2);
      nf1 = latticeCollapse(nf1);
      nf2 = latticeCollapse(nf2);
    }
    Collections.sort(nf1);
    Collections.sort(nf2);

    if (isCommutative && useHypotheses) {
      var rules = new ArrayList<Equality>();
      ContextHelper helper = new ContextHelper(hint);
      for (CoreBinding binding : helper.getAllBindings(typechecker)) {
        typeToRule(binding, rules);
      }

      if(!rules.isEmpty()) {
        ComRingSolver comSolver = new ComRingSolver();
        ConcreteExpression result = comSolver.solve(term1, term2, rules);
        if (result == null) {
          errorReporter.report(new EquationSolverError("Ring solver failed", nf1, nf2, values.getValues(), equalitiesToAssumptions(rules), hint != null ? hint : refExpr));
        }
        return result;
      }
    }
    if (!termCompiler.isLattice) {
      nf1 = Monomial.collapse(nf1);
      nf2 = Monomial.collapse(nf2);
    }
    if (!nf1.equals(nf2)) {
      errorReporter.report(new EquationSolverError("Ring solver failed", nf1, nf2, values.getValues(), Collections.emptyList(), hint != null ? hint : refExpr));
      return null;
    }

    return factory.appBuilder(factory.ref((termCompiler.isLattice ? meta.latticeTermsEq : (termCompiler.isRing ? (isCommutative ? meta.commRingTermsEq : meta.ringTermsEq) : (isCommutative ? meta.commSemiringTermsEq : meta.ringTermsEq))).getRef()))
      .app(factory.ref(dataRef), false)
      .app(term1.concrete)
      .app(term2.concrete)
      .app(factory.ref(meta.ext.prelude.getIdp().getRef()))
      .build();
  }