public List getMatchingExpressionArguments()

in base/src/main/java/org/arend/core/pattern/ConstructorExpressionPattern.java [275:373]


  public List<? extends Expression> getMatchingExpressionArguments(Expression expression, boolean normalize) {
    Expression dataExpr = getDataExpression();
    if (dataExpr instanceof SigmaExpression) {
      TupleExpression tuple = expression.cast(TupleExpression.class);
      return tuple == null ? null : tuple.getFields();
    }

    if (dataExpr instanceof FunCallExpression) {
      FunctionDefinition function = ((FunCallExpression) dataExpr).getDefinition();
      expression = expression.getUnderlyingExpression();
      if (function == Prelude.EMPTY_ARRAY) {
        if (expression instanceof ArrayExpression array && array.getElements().isEmpty() && array.getTail() == null) {
          return array.getConstructorArguments(getArrayElementsType() == null, getArrayLength() == null, normalize);
        }
        ClassCallExpression classCall = expression.getType().normalize(NormalizationMode.WHNF).cast(ClassCallExpression.class);
        if (classCall != null && classCall.getDefinition() == Prelude.DEP_ARRAY) {
          Expression length = classCall.getImplementationHere(Prelude.ARRAY_LENGTH, expression);
          if (length != null) {
            length = length.normalize(NormalizationMode.WHNF);
            if (length instanceof IntegerExpression && ((IntegerExpression) length).isZero()) {
              return getArrayElementsType() == null ? Collections.singletonList(FieldCallExpression.make(Prelude.ARRAY_ELEMENTS_TYPE, expression)) : Collections.emptyList();
            }
          }
        }
        return null;
      }
      if (function == Prelude.ARRAY_CONS) {
        if (expression instanceof ArrayExpression array && !array.getElements().isEmpty()) {
          return array.getConstructorArguments(getArrayElementsType() == null, getArrayLength() == null, normalize);
        }
        ClassCallExpression classCall = expression.getType().normalize(NormalizationMode.WHNF).cast(ClassCallExpression.class);
        if (classCall != null && classCall.getDefinition() == Prelude.DEP_ARRAY) {
          Expression length = classCall.getImplementationHere(Prelude.ARRAY_LENGTH, expression);
          if (length != null) {
            if (length instanceof IntegerExpression && !((IntegerExpression) length).isZero() || length instanceof ConCallExpression && ((ConCallExpression) length).getDefinition() == Prelude.SUC) {
              List<Expression> result = new ArrayList<>(4);
              if (getArrayLength() == null) result.add(length instanceof IntegerExpression intExpr ? intExpr.pred() : ((ConCallExpression) length).getDefCallArguments().get(0));
              Expression elementsType = FieldCallExpression.make(Prelude.ARRAY_ELEMENTS_TYPE, expression);
              if (getArrayElementsType() == null) result.add(elementsType);
              result.add(AppExpression.make(FieldCallExpression.make(Prelude.ARRAY_AT, expression), new SmallIntegerExpression(0), true));
              result.add(ArrayExpression.makeTail(length, elementsType, classCall, expression));
              return result;
            }
          }
        }
        return null;
      }
      if (function != Prelude.IDP) {
        return null;
      }
      if (expression instanceof FunCallExpression && ((FunCallExpression) expression).getDefinition() == Prelude.IDP) {
        return Collections.emptyList();
      }
      if (!(expression instanceof PathExpression)) {
        return null;
      }
      Expression arg = ((PathExpression) expression).getArgument();
      if (normalize) {
        arg = arg.normalize(NormalizationMode.WHNF);
      }
      LamExpression lamExpr = arg.cast(LamExpression.class);
      if (lamExpr == null) {
        return null;
      }
      Expression body = lamExpr.getParameters().getNext().hasNext() ? new LamExpression(lamExpr.getResultSort(), lamExpr.getParameters().getNext(), lamExpr.getBody()) : lamExpr.getBody();
      return NormalizingFindBindingVisitor.findBinding(body, lamExpr.getParameters()) ? null : Collections.emptyList();
    }

    if (dataExpr instanceof ConCallExpression || dataExpr instanceof SmallIntegerExpression) {
      ConCallExpression conCall = expression.cast(ConCallExpression.class);
      Definition myConstructor = getDefinition();
      if (conCall == null && (myConstructor == Prelude.ZERO || myConstructor == Prelude.SUC)) {
        IntegerExpression intExpr = expression.cast(IntegerExpression.class);
        if (intExpr != null) {
          return myConstructor == Prelude.ZERO && intExpr.isZero()
            ? Collections.emptyList()
            : myConstructor == Prelude.SUC && !intExpr.isZero()
              ? Collections.singletonList(intExpr.pred())
              : null;
        }
      }
      if (conCall == null || conCall.getDefinition() != myConstructor) {
        return null;
      }
      return conCall.getDefCallArguments();
    }

    NewExpression newExpr = expression.cast(NewExpression.class);
    if (newExpr == null) {
      return null;
    }
    List<Expression> arguments = new ArrayList<>();
    for (ClassField field : ((ClassCallExpression) dataExpr).getDefinition().getNotImplementedFields()) {
      if (!((ClassCallExpression) dataExpr).isImplementedHere(field)) {
        arguments.add(newExpr.getImplementation(field));
      }
    }
    return arguments;
  }