in meta/src/main/java/org/arend/lib/meta/CasesMeta.java [115:151]
private ConcreteExpression resolveArgument1(ExpressionResolver resolver, ConcreteExpression argument) {
ConcreteExpression type = argument instanceof ConcreteTypedExpression ? resolver.resolve(((ConcreteTypedExpression) argument).getType()) : null;
if (argument instanceof ConcreteTypedExpression) argument = ((ConcreteTypedExpression) argument).getExpression();
List<ConcreteArgument> sequence = argument.getArgumentsSequence();
if (sequence.size() >= 3 && sequence.get(sequence.size() - 1).isExplicit() && sequence.get(sequence.size() - 2).isExplicit()) {
ConcreteExpression opArg = resolveArgRef(resolver, sequence.get(sequence.size() - 2).getExpression());
if (opArg instanceof ConcreteReferenceExpression && ((ConcreteReferenceExpression) opArg).getReferent() == argRef) {
ConcreteExpression result = resolver.resolve(argument.getData(), sequence.subList(0, sequence.size() - 2));
ConcreteExpression params = parameter.resolve(resolver, sequence.get(sequence.size() - 1).getExpression(), false, true);
if (params == null && type == null) return result;
ConcreteFactory factory = ext.factory.withData(argument.getData());
ConcreteAppBuilder builder = factory.appBuilder(opArg).app(result).app(params != null ? params : factory.tuple());
if (type != null) builder.app(type);
return builder.build();
}
if (opArg != null) {
sequence.set(sequence.size() - 2, ext.factory.arg(opArg, true));
return addType(resolver.resolve(argument.getData(), sequence), type, null);
}
}
if (sequence.size() >= 2 && sequence.get(sequence.size() - 1).isExplicit()) {
ConcreteExpression lastArg = resolveArgRef(resolver, sequence.get(sequence.size() - 1).getExpression());
if (lastArg instanceof ConcreteReferenceExpression && ((ConcreteReferenceExpression) lastArg).getReferent() == argRef) {
resolver.getErrorReporter().report(new NameResolverError("Expected an argument after '" + argRef.getRefName() + "'", lastArg));
}
if (lastArg != null) {
sequence.set(sequence.size() - 1, ext.factory.arg(lastArg, true));
return addType(resolver.resolve(argument.getData(), sequence), type, lastArg);
}
}
return addType(resolver.resolve(argument), type, null);
}