private ConcreteExpression computeTerm()

in meta/src/main/java/org/arend/lib/meta/equation/TermCompiler.java [94:170]
70 lines of code
21 McCabe index (conditional complexity)

  private ConcreteExpression computeTerm(CoreExpression expression, List<Monomial> nf) {
    CoreExpression expr = expression.normalize(NormalizationMode.WHNF);
    if (zroMatcher.match(expr) != null) {
      return factory.ref(meta.zroTerm.getRef());
    }
    if (ideMatcher.match(expr) != null) {
      nf.add(new Monomial(BigInteger.ONE, Collections.emptyList()));
      return factory.ref(meta.ideTerm.getRef());
    }

    if (subTermCompiler != null && subTermCompiler.minusMatcher != null) {
      List<CoreExpression> minusArgs = subTermCompiler.minusMatcher.match(expr);
      if (minusArgs != null) {
        return getSubTermCompiler().computeMinus(minusArgs.get(0), minusArgs.get(1), nf);
      }
    }

    List<CoreExpression> addArgs = addMatcher.match(expr);
    if (addArgs != null) {
      List<ConcreteExpression> cArgs = new ArrayList<>(2);
      cArgs.add(computeTerm(addArgs.get(0), nf));
      cArgs.add(computeTerm(addArgs.get(1), nf));
      return factory.app(factory.ref(meta.addTerm.getRef()), true, cArgs);
    }

    List<CoreExpression> mulArgs = mulMatcher.match(expr);
    if (mulArgs != null) {
      List<ConcreteExpression> cArgs = new ArrayList<>(2);
      List<Monomial> nf1 = new ArrayList<>();
      List<Monomial> nf2 = new ArrayList<>();
      cArgs.add(computeTerm(mulArgs.get(0), nf1));
      cArgs.add(computeTerm(mulArgs.get(1), nf2));
      List<Monomial> newNF = new ArrayList<>();
      Monomial.multiply(nf1, nf2, newNF);
      Collections.sort(newNF);
      nf.addAll(Monomial.collapse(newNF));
      return factory.app(factory.ref(meta.mulTerm.getRef()), true, cArgs);
    }

    if (isRing) {
      List<CoreExpression> negativeArgs = negativeMatcher.match(expr);
      if (negativeArgs != null) {
        return computeNegative(negativeArgs.get(0), nf);
      }
    }

    Pair<Boolean, CoreExpression> pair = checkInt(expr);
    boolean isNeg = pair != null && pair.proj1;
    List<? extends CoreExpression> coefArgs = pair == null ? null : Collections.singletonList(pair.proj2);

    if (coefArgs == null && kind != RingKind.RAT && !isLattice) {
      coefArgs = natCoefMatcher.match(expr);
    }
    if (coefArgs != null) {
      CoreExpression arg = coefArgs.get(0).normalize(NormalizationMode.WHNF);
      if (arg instanceof CoreIntegerExpression) {
        BigInteger coef = ((CoreIntegerExpression) arg).getBigInteger();
        nf.add(new Monomial(coef, Collections.emptyList()));
        return factory.app(factory.ref(meta.coefTerm.getRef()), true, Collections.singletonList(factory.number(coef)));
      } else if (subTermCompiler != null) {
        List<Monomial> newNF = new ArrayList<>();
        ConcreteExpression term = getSubTermCompiler().computeTerm(arg, newNF);
        if (term != null) {
          if (isNeg) {
            Monomial.negate(newNF, nf);
          } else {
            nf.addAll(newNF);
          }
          return isNeg ? factory.app(factory.ref(meta.negativeTerm.getRef()), true, term) : term;
        }
      }
    }

    int index = values.addValue(expr);
    nf.add(new Monomial(BigInteger.ONE, Collections.singletonList(index)));
    return factory.app(factory.ref(meta.varTerm.getRef()), true, singletonList(factory.number(index)));
  }