public Result visitArray()

in meta/src/main/java/org/arend/lib/meta/cong/CongVisitor.java [387:427]


  public Result visitArray(@NotNull CoreArrayExpression expr, ParamType parameter) {
    CoreExpression other = parameter.other.getUnderlyingExpression();
    if (!(other instanceof CoreArrayExpression)) {
      return visit(expr, parameter);
    }
    CoreArrayExpression array2 = (CoreArrayExpression) other;
    if (!(expr.getElements().size() == array2.getElements().size() && (expr.getTail() == null) == (array2.getTail() == null) && typechecker.compare(expr.getElementsType(), array2.getElementsType(), CMP.EQ, marker, false, true, false))) {
      return visit(expr, parameter);
    }

    boolean abstracted = false;
    List<ConcreteExpression> elements = new ArrayList<>();
    for (int i = 0; i < expr.getElements().size(); i++) {
      Result argResult = expr.getElements().get(i).accept(this, new ParamType(() -> new Result(null), array2.getElements().get(i)));
      if (argResult == null) return null;
      if (argResult.expression != null) {
        abstracted = true;
      }
      elements.add(argResult.getExpression(expr.getElements().get(i), factory));
    }
    ConcreteExpression tail;
    if (expr.getTail() != null) {
      Result tailResult = expr.getTail().accept(this, new ParamType(() -> new Result(null), array2.getTail()));
      if (tailResult == null) return null;
      if (tailResult.expression != null) {
        abstracted = true;
      }
      tail = tailResult.getExpression(expr.getTail(), factory);
    } else {
      tail = null;
    }
    if (!abstracted) {
      return new Result(null);
    }

    ConcreteExpression result = tail != null ? tail : factory.ref(prelude.getEmptyArray().getRef());
    for (int i = elements.size() - 1; i >= 0; i--) {
      result = factory.app(factory.ref(prelude.getArrayCons().getRef()), true, Arrays.asList(elements.get(i), result));
    }
    return new Result(result);
  }