public ConcreteExpression solve()

in meta/src/main/java/org/arend/lib/meta/equation/MonoidSolver.java [251:410]
148 lines of code
51 McCabe index (conditional complexity)

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

    // TODO: get rid of this shit with flags
    boolean oldCommutative = isCommutative;
    boolean commutative = false;
    if (isCommutative && !term1.nf.equals(term2.nf)) {
      commutative = true;
      term1.nf = CountingSort.sort(term1.nf);
      term2.nf = CountingSort.sort(term2.nf);
    }
    isCommutative = commutative;

    boolean oldSemilattice = isSemilattice;
    boolean semilattice = false;
    if (isSemilattice && commutative && !term1.nf.equals(term2.nf)) {
      semilattice = true;
      term1.nf = removeDuplicates(term1.nf);
      term2.nf = removeDuplicates(term2.nf);
    }
    isSemilattice = semilattice;

    ConcreteExpression lastArgument;
    if (!term1.nf.equals(term2.nf)) {
      if (!useHypotheses) {
        errorReporter.report(new MonoidSolverError(isMultiplicative, term1.nf, term2.nf, values.getValues(), Collections.emptyList(), Collections.emptyList(),  Collections.emptyList(), hint != null ? hint : refExpr));
        return null;
      }

      List<RuleExt> rules = new ArrayList<>();
      if (contextRules == null) {
        contextRules = new HashMap<>();
      }
      ContextHelper helper = new ContextHelper(hint);
      for (CoreBinding binding : helper.getContextBindings(typechecker)) {
        rules.addAll(contextRules.computeIfAbsent(binding, k -> {
          List<RuleExt> ctxList = new ArrayList<>();
          typeToRule(null, binding, false, ctxList);
          return ctxList;
        }));
      }
      for (CoreBinding binding : helper.getAdditionalBindings(typechecker)) {
        typeToRule(null, binding, true, rules);
      }

      if (isCommutative) {
        ComMonoidWPSolver solver = new ComMonoidWPSolver();
        var equalities = new ArrayList<Equality>();
        for (RuleExt rule : rules) {
          if (rule.direction == Direction.FORWARD || rule.direction == Direction.UNKNOWN) {
            equalities.add(new Equality(rule.binding != null ? factory.ref(rule.binding) : factory.core(rule.expression), rule.lhsTerm, rule.rhsTerm, rule.lhs, rule.rhs));
          } else {
            equalities.add(new Equality(rule.binding != null ? factory.ref(rule.binding) : factory.core(rule.expression), rule.rhsTerm, rule.lhsTerm, rule.rhs, rule.lhs));
          }
        }
        isCommutative = oldCommutative;
        isSemilattice = oldSemilattice;
        ConcreteExpression result = solver.solve(term1, term2, equalities);
        if (result == null) {
          errorReporter.report(new MonoidSolverError(isMultiplicative, term1.nf, term2.nf, values.getValues(), rules, Collections.emptyList(), Collections.emptyList(), hint != null ? hint : refExpr));
        }
        return result;
      }

      List<Step> trace1 = new ArrayList<>();
      List<Step> trace2 = new ArrayList<>();
      List<Integer> newNf1 = applyRules(term1.nf, rules, trace1);
      List<Integer> newNf2 = applyRules(term2.nf, rules, trace2);
      if (!newNf1.equals(newNf2)) {
        isCommutative = oldCommutative;
        isSemilattice = oldSemilattice;
        errorReporter.report(new MonoidSolverError(isMultiplicative, term1.nf, term2.nf, values.getValues(), rules, trace1, trace2, hint != null ? hint : refExpr));
        return null;
      }

      while (!trace1.isEmpty() && !trace2.isEmpty()) {
        if (trace1.get(trace1.size() - 1).equals(trace2.get(trace2.size() - 1))) {
          trace1.remove(trace1.size() - 1);
          trace2.remove(trace2.size() - 1);
        } else {
          break;
        }
      }

      for (Step step : trace1) {
        step.rule.count++;
      }
      for (Step step : trace2) {
        step.rule.count++;
      }
      for (RuleExt rule : rules) {
        if (rule.count > 0) {
          if (rule.rnfTerm == null) {
            rule.rnfTerm = computeNFTerm(rule.rhs);
          }
          if (rule.cExpr != null) {
            continue;
          }

          ConcreteExpression cExpr = rule.binding != null ? factory.ref(rule.binding) : factory.core(null, rule.expression);
          if (rule.direction == Direction.BACKWARD) {
            cExpr = factory.app(factory.ref(meta.ext.inv.getRef()), true, singletonList(cExpr));
          }
          if (!isNF(rule.lhsTerm) || !isNF(rule.rhsTerm)) {
            cExpr = factory.appBuilder(factory.ref(meta.termsEqConv.getRef()))
              .app(factory.ref(dataRef), false)
              .app(rule.lhsTerm)
              .app(rule.rhsTerm)
              .app(cExpr)
              .build();
          }
          if (rule.count > 1 && !(cExpr instanceof ConcreteReferenceExpression) || rule.binding == null) {
            ArendRef letClause = factory.local("rule" + letClauses.size());
            letClauses.add(factory.letClause(letClause, Collections.emptyList(), null, cExpr));
            rule.cExpr = factory.ref(letClause);
          } else {
            rule.cExpr = cExpr;
          }
        }
      }

      ConcreteExpression expr1 = trace1.isEmpty() ? null : traceToExpr(term1.nf, trace1, dataRef, factory);
      ConcreteExpression expr2 = trace2.isEmpty() ? null : factory.app(factory.ref(meta.ext.inv.getRef()), true, singletonList(traceToExpr(term2.nf, trace2, dataRef, factory)));
      if (expr1 == null && expr2 == null) {
        lastArgument = factory.ref(meta.ext.prelude.getIdp().getRef());
      } else if (expr2 == null) {
        lastArgument = expr1;
      } else if (expr1 == null) {
        lastArgument = expr2;
      } else {
        lastArgument = factory.appBuilder(factory.ref(meta.ext.concat.getRef())).app(expr1).app(expr2).build();
      }
    } else {
      lastArgument = factory.ref(meta.ext.prelude.getIdp().getRef());
    }

    ConcreteAppBuilder builder = factory.appBuilder(factory.ref((isCat ? meta.catTermsEq : semilattice ? meta.semilatticeTermsEq : commutative ? meta.commTermsEq : meta.termsEq).getRef()))
      .app(factory.ref(dataRef), false);
    if (isCat) {
      CoreExpression type = leftExpr.getType().normalize(NormalizationMode.WHNF);
      if (type instanceof CoreAppExpression) {
        CoreExpression fun = ((CoreAppExpression) type).getFunction().normalize(NormalizationMode.WHNF);
        if (fun instanceof CoreAppExpression) {
          int dom = obValues.addValue(((CoreAppExpression) fun).getArgument());
          int cod = obValues.addValue(((CoreAppExpression) type).getArgument());
          builder.app(factory.number(dom), false).app(factory.number(cod), false);
        }
      }
    }
    isCommutative = oldCommutative;
    isSemilattice = oldSemilattice;
    return builder
      .app(term1.concrete)
      .app(term2.concrete)
      .app(lastArgument)
      .build();
  }