in base/src/main/java/org/arend/term/prettyprint/PrettyPrintVisitor.java [53:154]
public Void visitApp(Concrete.AppExpression expr, Precedence prec) {
List<String> tail = null;
Concrete.Expression it = expr;
do {
expr = (Concrete.AppExpression) it;
TCDefReferable tcRef = expr.getFunction() instanceof Concrete.ReferenceExpression && ((ReferenceExpression) expr.getFunction()).getReferent() instanceof TCDefReferable ? (TCDefReferable) ((ReferenceExpression) expr.getFunction()).getReferent() : null;
Constructor constructor = tcRef == null ? null : tcRef.getTypechecked() instanceof Constructor ? (Constructor) tcRef.getTypechecked() : null;
if (constructor == null || constructor.getRecursiveParameter() < 0) {
break;
}
List<Concrete.Argument> args = expr.getArguments();
if (tcRef.getRepresentablePrecedence().isInfix && isInfix(args)) {
int explicitIndex = -1;
int i = 0;
for (DependentLink link = constructor.getParameters(); link.hasNext(); link = link.getNext(), i++) {
if (link.isExplicit()) {
if (link.getNext().hasNext() && link.getNext().isExplicit()) {
explicitIndex = i;
}
break;
}
}
if (explicitIndex == -1 || explicitIndex != constructor.getRecursiveParameter() && explicitIndex + 1 != constructor.getRecursiveParameter()) {
break;
}
StringBuilder tailBuilder = new StringBuilder();
boolean leftParamIsRecursive = explicitIndex == constructor.getRecursiveParameter();
prec = visitBinOp(leftParamIsRecursive ? null : args.get(args.size() - 2).getExpression(), (Concrete.ReferenceExpression) expr.getFunction(), args.subList(0, args.size() - 2), leftParamIsRecursive ? args.get(args.size() - 1).getExpression() : null, prec, tailBuilder);
if (!tailBuilder.isEmpty()) {
if (tail == null) {
tail = new ArrayList<>();
}
tail.add(tailBuilder.toString());
}
it = args.get(args.size() - (leftParamIsRecursive ? 2 : 1)).getExpression();
} else {
int recursiveArg = 0;
int recursiveParam = 0;
for (DependentLink link = constructor.getParameters(); link.hasNext() && recursiveArg < args.size(); link = link.getNext(), recursiveArg++, recursiveParam++) {
while (link.hasNext() && recursiveArg < args.size() && link.isExplicit() != args.get(recursiveArg).isExplicit()) {
if (link.isExplicit()) {
recursiveArg++;
} else {
link = link.getNext();
recursiveParam++;
}
}
if (recursiveParam == constructor.getRecursiveParameter()) {
break;
}
}
if (recursiveArg == args.size()) {
break;
}
if (prec.priority > Concrete.AppExpression.PREC) myBuilder.append('(');
printExpr(expr.getFunction(), new Precedence(Concrete.AppExpression.PREC));
for (int i = 0; i < recursiveArg; i++) {
myBuilder.append(' ');
printArgument(args.get(i));
}
myBuilder.append(' ');
if (!args.get(recursiveArg).isExplicit()) {
myBuilder.append('{');
}
if (!args.get(recursiveArg).isExplicit() || recursiveArg < args.size() - 1 || prec.priority > Concrete.AppExpression.PREC) {
if (tail == null) {
tail = new ArrayList<>();
}
PrettyPrintVisitor ppVisitor = copy(new StringBuilder(), myIndent, !noIndent);
if (!args.get(recursiveArg).isExplicit()) {
ppVisitor.printClosingBrace();
}
for (int i = recursiveArg + 1; i < args.size(); i++) {
ppVisitor.myBuilder.append(' ');
ppVisitor.printArgument(args.get(i));
}
if (prec.priority > Concrete.AppExpression.PREC) ppVisitor.myBuilder.append(')');
tail.add(ppVisitor.myBuilder.toString());
}
it = args.get(recursiveArg).getExpression();
prec = args.get(recursiveArg).isExplicit() ? new Precedence((byte) (Concrete.AppExpression.PREC + 1)) : new Precedence(Concrete.Expression.PREC);
}
} while (it instanceof Concrete.AppExpression);
if (it instanceof Concrete.AppExpression) {
visitAppImpl((Concrete.AppExpression) it, prec);
} else {
printExpr(it, prec);
}
if (tail != null) {
for (int i = tail.size() - 1; i >= 0; i--) {
myBuilder.append(tail.get(i));
}
}
return null;
}