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);
}