private ConcreteExpression computeTerm()

in meta/src/main/java/org/arend/lib/meta/linear/TermCompiler.java [189:325]
127 lines of code
60 McCabe index (conditional complexity)

  private ConcreteExpression computeTerm(CoreExpression expression, Map<Integer, Ring> coefficients, Ring[] freeCoef, Set<Integer> vars) {
    CoreExpression expr = expression.getUnderlyingExpression();
    if (expr instanceof CoreAppExpression || expr instanceof CoreFieldCallExpression) {
      CoreFieldCallExpression fieldCall = null;
      CoreExpression arg1 = null;
      CoreExpression arg2 = null;
      if (expr instanceof CoreFieldCallExpression) {
        fieldCall = (CoreFieldCallExpression) expr;
      } else {
        CoreExpression fun = ((CoreAppExpression) expr).getFunction().getUnderlyingExpression();
        if (fun instanceof CoreFieldCallExpression) {
          fieldCall = (CoreFieldCallExpression) fun;
          arg1 = ((CoreAppExpression) expr).getArgument();
        } else if (fun instanceof CoreAppExpression) {
          CoreExpression fun2 = ((CoreAppExpression) fun).getFunction().getUnderlyingExpression();
          if (fun2 instanceof CoreFieldCallExpression) {
            fieldCall = (CoreFieldCallExpression) fun2;
            arg1 = ((CoreAppExpression) fun).getArgument();
            arg2 = ((CoreAppExpression) expr).getArgument();
          }
        }
      }
      if (fieldCall != null) {
        CoreClassField field = fieldCall.getDefinition();
        if (((field == meta.ext.zro || field == meta.ext.ide) && arg1 == null || (field == meta.plus || field == meta.mul) && arg2 != null || field == meta.negative && arg1 != null && arg2 == null) && typechecker.compare(fieldCall.getArgument(), instance, CMP.EQ, marker, false, true, false)) {
          if (field == meta.ext.zro) {
            return factory.ref(meta.zroTerm.getRef());
          } else if (field == meta.ext.ide) {
            freeCoef[0] = freeCoef[0].add(getOne());
            return factory.ref(meta.ideTerm.getRef());
          } else if (field == meta.negative) {
            return computeNegative(arg1, coefficients, freeCoef, vars);
          } else if (field == meta.plus) {
            return computePlus(arg1, arg2, coefficients, freeCoef, vars);
          } else if (field == meta.mul) {
            return computeMul(arg1, arg2, expr, coefficients, freeCoef, vars);
          }
        }
      }
    }
    expr = expr.normalize(NormalizationMode.WHNF);

    if (zroMatcher.match(expr) != null) {
      return factory.ref(meta.zroTerm.getRef());
    }

    List<CoreExpression> addArgs = addMatcher.match(expr);
    if (addArgs != null) {
      return computePlus(addArgs.get(addArgs.size() - 2), addArgs.get(addArgs.size() - 1), coefficients, freeCoef, vars);
    }

    if (ideMatcher.match(expr) != null) {
      freeCoef[0] = freeCoef[0].add(getOne());
      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), coefficients, freeCoef, vars);
      }
    }

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

    CoreExpression expr1 = kind == RingKind.RAT ? expr : null;
    if (ratAlgebraMatcher != null) {
      List<CoreExpression> ratAlgebraArgs = ratAlgebraMatcher.match(expr);
      if (ratAlgebraArgs != null) {
        expr1 = ratAlgebraArgs.get(0).normalize(NormalizationMode.WHNF);
      }
    }
    if (expr1 instanceof CoreConCallExpression conCall) {
      TypedExpression typedExpr = expr1.computeTyped();
      CoreExpression nomExpr = conCall.getDefCallArguments().get(0).normalize(NormalizationMode.WHNF);
      CoreExpression denomExpr = conCall.getDefCallArguments().get(1).normalize(NormalizationMode.WHNF);
      BigInteger nom = getInt(nomExpr);
      BigInteger denom = getInt(denomExpr);
      if (nom != null && denom != null) {
        freeCoef[0] = freeCoef[0].add(BigRational.make(nom, denom));
        return factory.app(factory.ref(meta.coefTerm.getRef()), true, factory.core(typedExpr));
      }
      if (denom != null && denom.equals(BigInteger.ONE) && subTermCompiler != null) {
        Map<Integer, Ring> newCoefficients = new HashMap<>();
        Ring[] newFreeCoef = new Ring[] { IntRing.ZERO };
        ConcreteExpression term = getSubTermCompiler().computeTerm(nomExpr, newCoefficients, newFreeCoef, vars);
        if (term != null) {
          for (Map.Entry<Integer, Ring> entry : newCoefficients.entrySet()) {
            BigRational value = BigRational.makeInt(((IntRing) entry.getValue()).number);
            coefficients.compute(entry.getKey(), (k,v) -> v == null ? value : v.add(value));
          }
          freeCoef[0] = freeCoef[0].add(BigRational.makeInt(((IntRing) newFreeCoef[0]).number));
          return term;
        }
      }
    }

    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 && kind != RingKind.RAT_ALG) {
      coefArgs = natCoefMatcher.match(expr);
    }
    if (coefArgs != null) {
      CoreExpression arg = coefArgs.get(0).normalize(NormalizationMode.WHNF);
      if (arg instanceof CoreIntegerExpression) {
        BigInteger coef = ((CoreIntegerExpression) arg).getBigInteger();
        if (isNeg) coef = coef.negate();
        freeCoef[0] = freeCoef[0].add(new IntRing(coef));
        return factory.app(factory.ref(meta.coefTerm.getRef()), true, factory.number(coef));
      } else if (subTermCompiler != null) {
        Map<Integer, Ring> newCoefficients = new HashMap<>();
        Ring[] newFreeCoef = new Ring[] { getZero() };
        ConcreteExpression term = getSubTermCompiler().computeTerm(arg, newCoefficients, newFreeCoef, vars);
        if (term != null) {
          for (Map.Entry<Integer, Ring> entry : newCoefficients.entrySet()) {
            coefficients.compute(entry.getKey(), (k,v) -> v == null ? (isNeg ? entry.getValue().negate() : entry.getValue()) : isNeg ? v.subtract(entry.getValue()) : v.add(entry.getValue()));
          }
          freeCoef[0] = isNeg ? freeCoef[0].subtract(newFreeCoef[0]) : freeCoef[0].add(newFreeCoef[0]);
          return isNeg ? factory.app(factory.ref(meta.negativeTerm.getRef()), true, term) : term;
        }
      }
    }

    List<CoreExpression> mulArgs = mulMatcher.match(expr);
    if (mulArgs != null) {
      return computeMul(mulArgs.get(mulArgs.size() - 2), mulArgs.get(mulArgs.size() - 1), expr, coefficients, freeCoef, vars);
    }

    return computeVal(expr, coefficients, vars);
  }