public List normalizeArguments()

in base/src/main/java/org/arend/core/elimtree/BranchElimTree.java [218:332]


  public List<Expression> normalizeArguments(List<? extends Expression> arguments) {
    List<Expression> result = new ArrayList<>(arguments.size());
    int index = getSkip();
    result.addAll(arguments.subList(0, index));
    Expression argument = arguments.get(index).normalize(NormalizationMode.WHNF);

    SingleConstructor singleConstructor = getSingleConstructorKey();
    if (singleConstructor instanceof IdpConstructor) {
      if (singleConstructor.getMatchedArguments(argument, true) != null) {
        result.add(argument);
        result.addAll(getSingleConstructorChild().normalizeArguments(arguments.subList(index + 1, arguments.size())));
        return result;
      }
    } else if (singleConstructor instanceof TupleConstructor) {
      if (argument instanceof TupleExpression tuple) {
        List<Expression> args = new ArrayList<>();
        args.addAll(tuple.getFields());
        args.addAll(arguments.subList(index + 1, arguments.size()));
        List<Expression> newArgs = getSingleConstructorChild().normalizeArguments(args);
        result.add(new TupleExpression(newArgs.subList(0, tuple.getFields().size()), tuple.getSigmaType()));
        result.addAll(newArgs.subList(tuple.getFields().size(), newArgs.size()));
        return result;
      }
    } else if (singleConstructor instanceof ClassConstructor) {
      if (argument instanceof NewExpression) {
        ClassConstructor classCon = (ClassConstructor) singleConstructor;
        ClassCallExpression classCall = ((NewExpression) argument).getType();
        List<Expression> args = new ArrayList<>();
        for (ClassField field : classCon.getClassDefinition().getNotImplementedFields()) {
          if (!classCon.getImplementedFields().contains(field)) {
            if (field.isProperty()) {
              args.add(FieldCallExpression.make(field, argument));
            } else {
              args.add(classCall.getAbsImplementationHere(field));
            }
          }
        }
        args.addAll(arguments.subList(index + 1, arguments.size()));
        List<Expression> newArgs = getSingleConstructorChild().normalizeArguments(args);
        Map<ClassField, Expression> implementations = new LinkedHashMap<>();
        int i = 0;
        for (ClassField field : classCon.getClassDefinition().getNotImplementedFields()) {
          if (classCon.getImplementedFields().contains(field)) {
            implementations.put(field, classCall.getAbsImplementationHere(field));
          } else {
            implementations.put(field, newArgs.get(i++));
          }
        }
        result.add(new NewExpression(null, new ClassCallExpression(classCall.getDefinition(), classCall.getLevels(), implementations, classCall.getSort(), classCall.getUniverseKind())));
        result.addAll(newArgs.subList(i, newArgs.size()));
        return result;
      }
    } else if (argument instanceof ConCallExpression conCall) {
      ElimTree elimTree = myChildren.get(conCall.getDefinition());
      if (elimTree != null) {
        List<Expression> args = new ArrayList<>();
        args.addAll(conCall.getDefCallArguments());
        args.addAll(arguments.subList(index + 1, arguments.size()));
        List<Expression> newArgs = elimTree.normalizeArguments(args);
        result.add(ConCallExpression.make(conCall.getDefinition(), conCall.getLevels(), conCall.getDataTypeArguments(), newArgs.subList(0, conCall.getDefCallArguments().size())));
        result.addAll(newArgs.subList(conCall.getDefCallArguments().size(), newArgs.size()));
        return result;
      }
    } else if (argument instanceof IntegerExpression intExpr) {
      boolean isZero = intExpr.isZero();
      ElimTree elimTree = myChildren.get(isZero ? Prelude.ZERO : Prelude.SUC);
      if (elimTree != null) {
        List<Expression> args = new ArrayList<>();
        if (!isZero) args.add(intExpr.pred());
        args.addAll(arguments.subList(index + 1, arguments.size()));
        List<Expression> newArgs = elimTree.normalizeArguments(args);
        result.add(isZero ? intExpr : Suc(newArgs.get(0)));
        result.addAll(isZero ? newArgs : newArgs.subList(1, newArgs.size()));
        return result;
      }
    } else if (argument instanceof ArrayExpression array) {
      ElimTree elimTree = myChildren.get(new ArrayConstructor(array.getElements().isEmpty(), true, true));
      if (elimTree != null) {
        List<Expression> args = new ArrayList<>();
        boolean withElementsType = withArrayElementsType();
        boolean withLength = withArrayLength();
        if (!withLength) {
          args.add(array.getLength());
        }
        if (!withElementsType) {
          args.add(array.getElementsType());
        }
        if (!array.getElements().isEmpty()) {
          args.add(array.getElements().get(0));
          args.add(array.drop(1));
        }
        args.addAll(arguments.subList(index + 1, arguments.size()));
        List<Expression> newArgs = elimTree.normalizeArguments(args);
        if (array.getElements().isEmpty()) {
          result.add(array);
        } else {
          List<Expression> consArgs = new ArrayList<>(4);
          if (withLength) {
            consArgs.add(array.getLength());
          }
          if (withElementsType) {
            consArgs.add(array.getElementsType());
          }
          consArgs.addAll(newArgs.subList(0, 2 + (withLength ? 0 : 1) + (withElementsType ? 0 : 1)));
          result.add(FunCallExpression.make(Prelude.ARRAY_CONS, array.getLevels(), consArgs));
        }
        result.addAll(newArgs.subList((array.getElements().isEmpty() ? 0 : 2) + (withElementsType ? 0 : 1) + (withLength ? 0 : 1), newArgs.size()));
        return result;
      }
    }

    result.add(argument);
    result.addAll(arguments.subList(index + 1, arguments.size()));
    return result;
  }