public static List addArguments()

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