private int compareExpressions()

in base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java [3569:3697]
114 lines of code
52 McCabe index (conditional complexity)

  private int compareExpressions(Expression expr1, Expression expr2, Expression type) {
    if (expr2 instanceof ErrorExpression) {
      return 1;
    }
    expr1 = expr1.normalize(NormalizationMode.WHNF);

    while (expr2 instanceof LamExpression) {
      expr2 = ((LamExpression) expr2).getBody();
    }

    if (expr2 instanceof UniverseExpression) {
      return expr1 instanceof UniverseExpression && ((UniverseExpression) expr1).getSort().equals(((UniverseExpression) expr2).getSort()) ? 0 : 1;
    }

    if (expr2 instanceof IntegerExpression) {
      return expr1 instanceof IntegerExpression ? ((IntegerExpression) expr1).compare((IntegerExpression) expr2) : 1;
    }

    if (expr2 instanceof DataCallExpression || expr2 instanceof FunCallExpression && ((FunCallExpression) expr2).getDefinition().getKind() == CoreFunctionDefinition.Kind.TYPE) {
      int cmp = 0;
      if (expr1 instanceof DefCallExpression && ((DefCallExpression) expr1).getDefinition() == ((DefCallExpression) expr2).getDefinition()) {
        ExprSubstitution substitution = new ExprSubstitution();
        DependentLink link = ((DefCallExpression) expr1).getDefinition().getParameters();
        List<? extends Expression> args1 = ((DefCallExpression) expr1).getDefCallArguments();
        List<? extends Expression> args2 = ((DefCallExpression) expr2).getDefCallArguments();
        for (int i = 0; i < args1.size(); i++) {
          int argCmp = compareExpressions(args1.get(i), args2.get(i), link.getTypeExpr().subst(substitution));
          if (argCmp == 1) {
            cmp = 1;
            break;
          }
          if (argCmp == -1) {
            cmp = -1;
          }

          substitution.add(link, args1.get(i));
          link = link.getNext();
        }
        if (cmp == -1) {
          return -1;
        }
      }

      for (Expression arg : ((DefCallExpression) expr2).getDefCallArguments()) {
        if (compareExpressions(expr1, arg, null) != 1) {
          return -1;
        }
      }

      return cmp;
    }

    if (expr2 instanceof SigmaExpression || expr2 instanceof PiExpression) {
      int cmp = 0;
      if (expr1 instanceof SigmaExpression && expr2 instanceof SigmaExpression || expr1 instanceof PiExpression && expr2 instanceof PiExpression) {
        DependentLink param1 = getExprParameters(expr1);
        DependentLink param2 = getExprParameters(expr2);
        if (DependentLink.Helper.size(param1) == DependentLink.Helper.size(param2)) {
          for (; param1.hasNext(); param1 = param1.getNext(), param2 = param2.getNext()) {
            int argCmp = compareExpressions(param1.getTypeExpr(), param2.getTypeExpr(), Type.OMEGA);
            if (argCmp == 1) {
              cmp = 1;
              break;
            }
            if (argCmp == -1) {
              cmp = -1;
            }
          }
          if (cmp != 1 && expr1 instanceof PiExpression) {
            int codCmp = compareExpressions(((PiExpression) expr1).getCodomain(), ((PiExpression) expr2).getCodomain(), Type.OMEGA);
            if (codCmp != 0) cmp = codCmp;
          }
          if (cmp == -1) {
            return -1;
          }
        }
      }

      for (DependentLink param = getExprParameters(expr2); param.hasNext(); param = param.getNext()) {
        param = param.getNextTyped(null);
        if (compareExpressions(expr1, param.getTypeExpr(), Type.OMEGA) != 1) {
          return -1;
        }
      }
      if (expr2 instanceof PiExpression && compareExpressions(expr1, ((PiExpression) expr2).getCodomain(), Type.OMEGA) != 1) {
        return -1;
      }

      return cmp;
    }

    if (expr2 instanceof ClassCallExpression) {
      int cmp = 0;
      if (expr1 instanceof ClassCallExpression && ((ClassCallExpression) expr1).getDefinition() == ((ClassCallExpression) expr2).getDefinition() && ((ClassCallExpression) expr1).getImplementedHere().size() == ((ClassCallExpression) expr2).getImplementedHere().size()) {
        for (Map.Entry<ClassField, Expression> entry : ((ClassCallExpression) expr1).getImplementedHere().entrySet()) {
          Expression impl2 = ((ClassCallExpression) expr2).getAbsImplementationHere(entry.getKey());
          if (impl2 == null) {
            cmp = 1;
            break;
          }

          int argCmp = compareExpressions(entry.getValue(), impl2, null);
          if (argCmp == 1) {
            cmp = 1;
            break;
          }
          if (argCmp == -1) {
            cmp = -1;
          }
        }
        if (cmp == -1) {
          return -1;
        }
      }

      for (Expression arg : ((ClassCallExpression) expr2).getImplementedHere().values()) {
        if (compareExpressions(expr1, arg, null) != 1) {
          return -1;
        }
      }

      return cmp;
    }

    while (expr1 instanceof FieldCallExpression && !(expr2 instanceof FieldCallExpression && ((FieldCallExpression) expr2).getDefinition() == ((FieldCallExpression) expr1).getDefinition())) {
      expr1 = ((FieldCallExpression) expr1).getArgument();
    }
    return Expression.compare(expr1, expr2, type, CMP.EQ) ? 0 : 1;
  }