in meta/src/main/java/org/arend/lib/util/Utils.java [115:170]
public static List<ConcreteExpression> addArguments(ConcreteExpression expr, StdExtension ext, int expectedParameters, boolean addGoals) {
ConcreteReferenceExpression refExpr = null;
if (expr instanceof ConcreteReferenceExpression) {
refExpr = (ConcreteReferenceExpression) expr;
} else if (expr instanceof ConcreteAppExpression) {
ConcreteExpression fun = ((ConcreteAppExpression) expr).getFunction();
if (fun instanceof ConcreteReferenceExpression) {
refExpr = (ConcreteReferenceExpression) fun;
}
}
if (refExpr == null) {
return Collections.emptyList();
}
int numberOfArgs = 0;
ArendRef ref = refExpr.getReferent();
if (ref instanceof MetaRef) {
MetaDefinition meta = ((MetaRef) ref).getDefinition();
if (meta instanceof BaseMetaDefinition) {
boolean[] explicitness = ((BaseMetaDefinition) meta).argumentExplicitness();
if (explicitness != null) {
for (boolean explicit : explicitness) {
if (explicit) {
numberOfArgs++;
}
}
}
}
} else {
CoreDefinition argDef = ext.definitionProvider.getCoreDefinition(ref);
if (argDef == null) {
return Collections.emptyList();
}
numberOfArgs = numberOfExplicitParameters(argDef) - expectedParameters;
}
if (expr instanceof ConcreteAppExpression && numberOfArgs > 0) {
for (ConcreteArgument argument : ((ConcreteAppExpression) expr).getArguments()) {
if (argument.isExplicit()) {
numberOfArgs--;
}
}
}
if (numberOfArgs <= 0) {
return Collections.emptyList();
}
ConcreteFactory factory = ext.factory.withData(expr.getData());
List<ConcreteExpression> args = new ArrayList<>(numberOfArgs);
for (int i = 0; i < numberOfArgs; i++) {
args.add(addGoals ? factory.goal() : factory.hole());
}
return args;
}