public SubexprOccurrences matchSubexpr()

in meta/src/main/java/org/arend/lib/meta/equation/MonoidSolver.java [149:248]
81 lines of code
24 McCabe index (conditional complexity)

  public SubexprOccurrences matchSubexpr(@NotNull TypedExpression subExpr, @NotNull TypedExpression expr, @NotNull ErrorReporter errorReporter, List<Integer> occurrences) {
    if (isCommutative || isSemilattice) return super.matchSubexpr(subExpr, expr, errorReporter, occurrences);

    CompiledTerm subExTerm = compileTerm(subExpr.getExpression());
    CompiledTerm term = compileTerm(expr.getExpression());
    SubexprOccurrences result = new SubexprOccurrences();

    result.occurrenceVar = factory.local("occurVar");
    result.subExprMissed = term.nf.size() == 1 && (expr.getExpression() instanceof CoreAppExpression);

    if (term.nf.isEmpty()) {
      if (!subExTerm.nf.isEmpty()) {
        result.occurrenceVar = null;
        return result;
      }
      return super.matchSubexpr(subExpr, expr, errorReporter, occurrences);
    }

    if (subExTerm.nf.isEmpty()) {
      result.occurrenceVar = null;
      return result;
    }

    // Now this check is not needed, but keep it for the future
    if (!isCommutative) {
      var exprSplitting = cutAccordingToOccurrences(subExTerm.nf, term.nf, occurrences);
      var pieces = exprSplitting.proj1;

      result.numOccurrencesSkipped = exprSplitting.proj2;

      if (pieces.size() == 1 && pieces.get(0) != null) {
        result.occurrenceVar = null;
        return result;
      }

      for (List<Integer> piece : pieces) {
        if (piece == null) {
          ++result.numOccurrences;
        }
      }

      var mul = isCat ? factory.ref(meta.catMul.getRef()) : factory.ref(meta.mul.getRef());
      var interpretNF = isCat ? factory.ref(meta.catInterpretNF.getRef()) : factory.ref(meta.monoidInterpretNF.getRef());
      var subExprNF = computeNFTerm(subExTerm.nf);
      var constructedExprNF = pieces.get(0) == null ? new ArrayList<>(subExTerm.nf) : new ArrayList<>(pieces.get(0));
      ConcreteExpression concatNFsProof = null;

      result.exprWithOccurrences = pieces.get(0) == null ? factory.ref(result.occurrenceVar) : factory.app(interpretNF, true, computeNFTerm(pieces.get(0)));

      for (int i = 1; i < pieces.size(); ++i) {
        var piece = pieces.get(i);
        var pieceNFTerm = piece == null ? subExprNF : computeNFTerm(piece);
        var pieceTerm = piece == null ? factory.ref(result.occurrenceVar) : factory.app(interpretNF, true, pieceNFTerm);
        var pieceTermSubExpr = piece == null ? factory.core(subExpr) : factory.app(interpretNF, true, pieceNFTerm);
        result.exprWithOccurrences = factory.appBuilder(mul).app(result.exprWithOccurrences).app(pieceTerm).build();
        concatNFsProof = appendRightNFProof(computeNFTerm(constructedExprNF), pieceNFTerm, concatNFsProof);
        if (piece == null) constructedExprNF.addAll(subExTerm.nf); else constructedExprNF.addAll(piece);
      }

      var normConsist = isCat ? meta.catNormConsist.getRef() : meta.monoidNormConsist.getRef();

      ConcreteExpression normConsistSubExpr;
      ConcreteExpression normConsistExpr;

      if (!isCat) {
        normConsistSubExpr = factory.appBuilder(factory.ref(normConsist)).app(subExTerm.concrete).build();
        normConsistExpr = factory.appBuilder(factory.ref(normConsist)).app(term.concrete).build();
      } else {
        int subExprDom = domMap.get(subExTerm.nf.get(subExTerm.nf.size() - 1));
        int subExprCod = codomMap.get(subExTerm.nf.get(0));
        int exprDom = domMap.get(term.nf.get(term.nf.size() - 1));
        int exprCod = codomMap.get(term.nf.get(0));
        normConsistSubExpr = factory.appBuilder(factory.ref(normConsist))
                .app(factory.ref(dataRef), false)
                .app(factory.number(subExprDom), false).app(factory.number(subExprCod), false)
                .app(subExTerm.concrete).build();
        normConsistExpr = factory.appBuilder(factory.ref(normConsist))
                .app(factory.hole(), false)
                .app(factory.number(exprDom), false).app(factory.number(exprCod), false)
                .app(term.concrete).build();
      }

      var occLambda = factory.lam(Collections.singletonList(factory.param(result.occurrenceVar)), result.exprWithOccurrences);
              // factory.lam(Collections.singletonList(factory.param(Collections.singletonList(result.occurrenceVar), factory.core(subExpr.getType().computeTyped()))), result.exprWithOccurrences);
      var pmapOccurrence = factory.appBuilder(factory.ref(meta.ext.pmap.getRef()))
              .app(occLambda).app(factory.appBuilder(factory.ref(meta.ext.inv.getRef())).app(normConsistSubExpr).build()).build();
      if (concatNFsProof == null) {
      //  return new SubexprOccurrences(null, null, null, allOccurrences.size());
        result.equalityProof = factory.appBuilder(factory.ref(meta.ext.concat.getRef())).app(normConsistExpr)
                .app(pmapOccurrence).build();
      } else {
        result.equalityProof = factory.appBuilder(factory.ref(meta.ext.concat.getRef())).app(normConsistExpr)
                .app(factory.appBuilder(factory.ref(meta.ext.concat.getRef())).app(concatNFsProof).app(pmapOccurrence).build()).build();
      }
      result.wrapExprWithOccurrences(factory.core(subExpr.getType().computeTyped()), factory);
      return result;
    }

    return null;
  }