public boolean normalizedCompare()

in base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java [234:386]
141 lines of code
126 McCabe index (conditional complexity)

  public boolean normalizedCompare(Expression expr1, Expression expr2, Expression type, boolean useType) {
    Expression stuck1 = expr1.getStuckExpression();
    Expression stuck2 = expr2.getStuckExpression();
    if (stuck1 != null) stuck1 = stuck1.getUnderlyingExpression();
    if (stuck2 != null) stuck2 = stuck2.getUnderlyingExpression();
    if (stuck1 instanceof ErrorExpression && !(stuck2 instanceof InferenceReferenceExpression) ||
        stuck2 instanceof ErrorExpression && !(stuck1 instanceof InferenceReferenceExpression)) {
      return true;
    }

    if ((stuck1 instanceof InferenceReferenceExpression || stuck2 instanceof InferenceReferenceExpression) && myAllowEquations) {
      InferenceVariable var1 = stuck1 instanceof InferenceReferenceExpression ? ((InferenceReferenceExpression) stuck1).getVariable() : null;
      InferenceVariable var2 = stuck2 instanceof InferenceReferenceExpression ? ((InferenceReferenceExpression) stuck2).getVariable() : null;
      if (var1 instanceof MetaInferenceVariable || var2 instanceof MetaInferenceVariable || var1 != null && var2 != null && !(expr1 instanceof DefCallExpression && !(expr1 instanceof FieldCallExpression) && expr2 instanceof DefCallExpression && ((DefCallExpression) expr1).getDefinition() == ((DefCallExpression) expr2).getDefinition())) {
        if (!myEquations.addEquation(expr1, substitute(expr2), type, myCMP, (var1 != null ? var1 : var2).getSourceNode(), var1, var2)) {
          initResult(expr1, expr2);
          return false;
        }
        return true;
      }
    }

    InferenceVariable stuckVar1 = expr1.getInferenceVariable(true);
    InferenceVariable stuckVar2 = expr2.getInferenceVariable(true);
    if (stuckVar1 != null || stuckVar2 != null) {
      if (!(myNormalCompare && myEquations.addEquation(expr1, substitute(expr2), type, myCMP, stuckVar1 != null ? stuckVar1.getSourceNode() : stuckVar2.getSourceNode(), stuckVar1, stuckVar2))) {
        initResult(expr1, expr2);
        return false;
      }
      return true;
    }

    if (expr1 instanceof FieldCallExpression && ((FieldCallExpression) expr1).getDefinition().isProperty() && expr2 instanceof FieldCallExpression && ((FieldCallExpression) expr2).getDefinition().isProperty()) {
      return true;
    }

    boolean onlySolveVars = myOnlySolveVars;
    if (myNormalCompare && !myOnlySolveVars && expr1.isBoxed() && expr2.isBoxed() && (type != null || compare(expr1.getType(), expr2.getType(), Type.OMEGA, true))) {
      myOnlySolveVars = true;
    }
    if (useType && myNormalCompare && !myOnlySolveVars) {
      Expression normType = type == null ? null : type.getUnderlyingExpression();
      boolean allowProp = normType instanceof DataCallExpression && ((DataCallExpression) normType).getDefinition().getConstructors().isEmpty() || !expr1.canBeConstructor() && !expr2.canBeConstructor();
      if (normType instanceof SigmaExpression && !((SigmaExpression) normType).getParameters().hasNext() ||
          normType instanceof ClassCallExpression && (((ClassCallExpression) normType).getNumberOfNotImplementedFields() == 0 || Boolean.TRUE.equals(ConstructorExpressionPattern.isArrayEmpty(normType)) && ((ClassCallExpression) normType).isImplemented(Prelude.ARRAY_ELEMENTS_TYPE)) ||
          allowProp && normType != null && Sort.PROP.equals(normType.getSortOfType())) {
        myOnlySolveVars = true;
      }

      if (!myOnlySolveVars && (normType == null || normType.getStuckInferenceVariable() != null || normType instanceof ClassCallExpression)) {
        Expression type1 = expr1.getType();
        if (type1 != null && type1.getStuckInferenceVariable() != null) {
          type1 = null;
        }
        if (type1 != null) {
          type1 = myNormalize ? type1.normalize(NormalizationMode.WHNF) : type1;
          if (allowProp) {
            Sort sort1 = type1.getSortOfType();
            if (sort1 != null && sort1.isProp() && !type1.isInstance(ClassCallExpression.class)) {
              myOnlySolveVars = true;
            }
          }
        }

        if (!myOnlySolveVars && type1 != null) {
          Expression type2 = expr2.getType();
          if (type2 != null && type2.getStuckInferenceVariable() != null) {
            type2 = null;
          }
          if (type2 != null) {
            type2 = myNormalize ? type2.normalize(NormalizationMode.WHNF) : type2;
            if (allowProp) {
              Sort sort2 = type2.getSortOfType();
              if (sort2 != null && sort2.isProp() && !type2.isInstance(ClassCallExpression.class)) {
                myOnlySolveVars = true;
              }
            }
          }

          if (!myOnlySolveVars && type2 != null) {
            ClassCallExpression classCall1 = type1.cast(ClassCallExpression.class);
            ClassCallExpression classCall2 = type2.cast(ClassCallExpression.class);
            if (classCall1 != null && classCall2 != null && compareClassInstances(expr1, classCall1, expr2, classCall2, normType)) {
              return true;
            }
          }
        }
      }
    }

    CMP origCMP = myCMP;
    if (!myOnlySolveVars && myAllowEquations) {
      Boolean dataAndApp = checkDefCallAndApp(expr1, expr2, true);
      if (dataAndApp != null) {
        if (!dataAndApp) initResult(expr1, expr2);
        return dataAndApp;
      }
      dataAndApp = checkDefCallAndApp(expr2, expr1, false);
      if (dataAndApp != null) {
        if (!dataAndApp) initResult(expr1, expr2);
        return dataAndApp;
      }
    }

    if (!myOnlySolveVars && myNormalCompare) {
      Boolean result = expr1 instanceof AppExpression && (stuck2 == null || stuck2.getInferenceVariable() == null) ? checkApp((AppExpression) expr1, expr2, true) : null;
      if (result != null) {
        if (!result) initResult(expr1, expr2);
        return result;
      }
      result = expr2 instanceof AppExpression && (stuck1 == null || stuck1.getInferenceVariable() == null) ? checkApp((AppExpression) expr2, expr1, false) : null;
      if (result != null) {
        if (!result) initResult(expr1, expr2);
        return result;
      }
    }

    if (expr1 instanceof ErrorExpression) {
      return true;
    }
    if (!(expr1 instanceof UniverseExpression || expr1 instanceof PiExpression || expr1 instanceof ClassCallExpression || expr1 instanceof DataCallExpression || expr1 instanceof AppExpression || expr1 instanceof SigmaExpression || expr1 instanceof LamExpression)) {
      myCMP = CMP.EQ;
    }

    boolean ok;
    if (expr2 instanceof ErrorExpression) {
      return true;
    }
    if (expr2 instanceof PathExpression && !(expr1 instanceof PathExpression)) {
      ok = comparePathEta((PathExpression) expr2, expr1, type, false);
    } else if (expr2 instanceof LamExpression) {
      ok = visitLam((LamExpression) expr2, expr1, type, false);
    } else if (expr2 instanceof TupleExpression) {
      ok = visitTuple((TupleExpression) expr2, expr1, false);
    } else if (expr2 instanceof TypeConstructorExpression) {
      ok = visitTypeConstructor((TypeConstructorExpression) expr2, expr1, false);
    } else if (expr2 instanceof FunCallExpression && ((FunCallExpression) expr2).getDefinition() == Prelude.ARRAY_INDEX && !(expr1 instanceof FunCallExpression && ((FunCallExpression) expr1).getDefinition() == Prelude.ARRAY_INDEX)) {
      ok = compareConstArray((FunCallExpression) expr2, expr1, type, false);
    } else {
      ok = expr1.accept(this, expr2, type);
    }

    if (!ok && !myOnlySolveVars && myAllowEquations) {
      InferenceVariable variable1 = stuck1 == null ? null : stuck1.getInferenceVariable();
      InferenceVariable variable2 = stuck2 == null ? null : stuck2.getInferenceVariable();
      ok = (variable1 != null || variable2 != null) && myNormalCompare && myEquations.addEquation(expr1, substitute(expr2), type, origCMP, variable1 != null ? variable1.getSourceNode() : variable2.getSourceNode(), variable1, variable2);
    }
    if (myOnlySolveVars) {
      ok = true;
    }
    myOnlySolveVars = onlySolveVars;
    return ok;
  }