public Boolean visitConCall()

in base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java [750:898]
138 lines of code
52 McCabe index (conditional complexity)

  public Boolean visitConCall(ConCallExpression expr1, Expression expr2, Expression type) {
    ConCallExpression conCall2;
    Expression it = expr1;
    List<Pair<ConCallExpression, ConCallExpression>> stack = null;
    while (true) {
      expr1 = (ConCallExpression) it;
      if (expr2 instanceof IntegerExpression) {
        return visitInteger((IntegerExpression) expr2, expr1) || myOnlySolveVars;
      }
      conCall2 = expr2.cast(ConCallExpression.class);
      if (!compareDef(expr1, conCall2, expr2)) {
        return myOnlySolveVars;
      }

      int recursiveParam = expr1.getDefinition().getRecursiveParameter();
      if (recursiveParam < 0) {
        if (!(compareLists(expr1.getDefCallArguments(), conCall2.getDefCallArguments(), expr1.getDefinition().getParameters(), expr1.getDefinition(), null) || myOnlySolveVars)) {
          if (myResult == null) {
            initResult(expr1, conCall2);
          } else {
            if (myResult.index >= 0 && myResult.index < expr1.getDefCallArguments().size()) {
              List<Expression> args = new ArrayList<>(expr1.getDefCallArguments());
              args.set(myResult.index, myResult.wholeExpr1);
              myResult.wholeExpr1 = ConCallExpression.make(expr1.getDefinition(), expr1.getLevels(), args, expr1.getDefCallArguments());
            } else {
              myResult.wholeExpr1 = expr1;
            }
            if (myResult.index >= 0 && myResult.index < conCall2.getDefCallArguments().size()) {
              List<Expression> args = new ArrayList<>(conCall2.getDefCallArguments());
              args.set(myResult.index, myResult.wholeExpr2);
              myResult.wholeExpr2 = ConCallExpression.make(conCall2.getDefinition(), conCall2.getLevels(), args, conCall2.getDefCallArguments());
            } else {
              myResult.wholeExpr2 = conCall2;
            }
            myResult.index = -1;
            restoreConCalls(stack);
          }
          return false;
        }
        return true;
      }

      if (stack == null) {
        stack = new ArrayList<>();
      }
      stack.add(new Pair<>(expr1, conCall2));

      for (int i = 0; i < expr1.getDefCallArguments().size(); i++) {
        if (i != recursiveParam && !compare(expr1.getDefCallArguments().get(i), conCall2.getDefCallArguments().get(i), null, true)) {
          if (myOnlySolveVars) {
            return true;
          }
          if (myResult == null) {
            initResult(expr1, conCall2);
          } else {
            if (myResult.index >= 0 && myResult.index < expr1.getDefCallArguments().size()) {
              List<Expression> args = new ArrayList<>(expr1.getDefCallArguments());
              args.set(i, myResult.wholeExpr1);
              myResult.wholeExpr1 = ConCallExpression.make(expr1.getDefinition(), expr1.getLevels(), expr1.getDataTypeArguments(), args);
            } else {
              myResult.wholeExpr1 = expr1;
            }
            if (myResult.index >= 0 && myResult.index < conCall2.getDefCallArguments().size()) {
              List<Expression> args = new ArrayList<>(conCall2.getDefCallArguments());
              args.set(i, myResult.wholeExpr2);
              myResult.wholeExpr2 = ConCallExpression.make(conCall2.getDefinition(), conCall2.getLevels(), conCall2.getDataTypeArguments(), args);
            } else {
              myResult.wholeExpr2 = conCall2;
            }
          }
          if (myResult != null) {
            restoreConCalls(stack);
          }
          return false;
        }
      }

      it = expr1.getDefCallArguments().get(recursiveParam).getUnderlyingExpression();
      expr2 = conCall2.getDefCallArguments().get(recursiveParam).getUnderlyingExpression();
      if (it == expr2) {
        return true;
      }
      it = it.normalize(NormalizationMode.WHNF);
      expr2 = expr2.normalize(NormalizationMode.WHNF);
      if (!(it instanceof ConCallExpression)) {
        break;
      }

      // compare(it, expr2, null)
      InferenceReferenceExpression infRefExpr2 = expr2.cast(InferenceReferenceExpression.class);
      if (infRefExpr2 != null && infRefExpr2.getVariable() != null) {
        if (!(myNormalCompare && myEquations.addEquation(it, infRefExpr2, type, myCMP, infRefExpr2.getVariable().getSourceNode(), it.getStuckInferenceVariable(), infRefExpr2.getVariable()) || myOnlySolveVars)) {
          if (initResult(expr1, expr2)) {
            restoreConCalls(stack);
          }
          return false;
        }
        return true;
      }
      InferenceVariable stuckVar2 = expr2.getStuckInferenceVariable();
      if (stuckVar2 != null && (!myNormalCompare || myEquations == DummyEquations.getInstance())) {
        if (!myOnlySolveVars) {
          if (initResult(expr1, expr2)) {
            restoreConCalls(stack);
          }
          return false;
        }
        return true;
      }

      if (myOnlySolveVars && stuckVar2 != null) {
        return true;
      }

      if (!myNormalCompare || !myNormalize) {
        if (initResult(expr1, expr2)) {
          restoreConCalls(stack);
        }
        return false;
      }

      // normalizedCompare(it, expr2, null)
      if (expr2 instanceof ErrorExpression) {
        return true;
      }
      Expression stuck2 = expr2.getStuckExpression();
      if (stuck2 != null && stuck2.isError()) {
        return true;
      }
      stuckVar2 = expr2.getInferenceVariable();
      if (stuckVar2 != null) {
        if (!(myNormalCompare && myEquations.addEquation(it, substitute(expr2), type, myCMP, stuckVar2.getSourceNode(), null, stuckVar2) || myOnlySolveVars)) {
          if (initResult(expr1, expr2)) {
            restoreConCalls(stack);
          }
          return false;
        }
        return true;
      }
    }

    if (!compare(it, expr2, null, true)) {
      if (initResult(it, expr2)) {
        restoreConCalls(stack);
      }
      return false;
    }
    return true;
  }