private Integer splitIntoSubterms()

in meta/src/main/java/org/arend/lib/meta/closure/CongruenceClosure.java [74:135]
53 lines of code
12 McCabe index (conditional complexity)

  private Integer splitIntoSubterms(V term) {
    Queue<Pair<CoreExpression, Integer>> termsToSplit = new ArrayDeque<>();
    Set<VarId> toBeAddedToCongrTable = new HashSet<>();

    int inputTermVar = addTerm(term, null, termsToSplit);

    while (!termsToSplit.isEmpty()) {
      Pair<CoreExpression, Integer> subtermPair = termsToSplit.poll();
      CoreExpression subterm = subtermPair.proj1;
      int var = subtermPair.proj2;

      toBeAddedToCongrTable.add(new VarId(var, -1));
      if (subterm instanceof CoreAppExpression) {
        CoreExpression func = ((CoreAppExpression) subterm).getFunction();
        CoreExpression arg = ((CoreAppExpression) subterm).getArgument();
        CoreExpression funcType = func.computeType();
        boolean doSplitting = true;

        if (funcType instanceof CorePiExpression) {
          doSplitting = !((CorePiExpression) funcType).getCodomain().findFreeBinding(((CorePiExpression) funcType).getParameters().getBinding());
        }

        if (doSplitting) {
          int funcVar = addTerm(func, new VarId(var, -1), termsToSplit);
          int argVar = addTerm(arg, new VarId(var, -1), termsToSplit);

          varDefs.put(new VarId(var, -1), new Pair<>(new VarId(funcVar, -1), new VarId(argVar, -1)));
        }
      } else if (subterm instanceof CoreDefCallExpression && !(subterm instanceof CoreFieldCallExpression)) {
        int numArgs = ((CoreDefCallExpression) subterm).getDefCallArguments().size();
        List<VarId> prefixVars = terms.getVarIds(subterm);
        VarId appVar = prefixVars.get(0);

        for (int i = 0; i < numArgs; ++i) {
          int argVar = addTerm(((CoreDefCallExpression) subterm).getDefCallArguments().get(numArgs - 1 - i), appVar, termsToSplit);
          VarId funcVar = prefixVars.get(i + 1);
          boolean stop = funcVar != null;
          if (funcVar == null) {
            funcVar = new VarId(var, i);
          }
          varDefs.put(appVar, new Pair<>(funcVar, new VarId(argVar, -1)));
          initAppExprVar(funcVar, appVar);
          toBeAddedToCongrTable.add(appVar);
          if (stop) {
            break;
          }
          if (i == numArgs - 1) {
            toBeAddedToCongrTable.add(funcVar);
          }
          appVar = funcVar;
        }
      }
    }

    Queue<Equality> pending = new ArrayDeque<>();
    for (VarId var : toBeAddedToCongrTable) {
      addToCongrTable(var, pending);
    }

    addEqualities(pending);
    return inputTermVar;
  }