private ConcreteExpression resolveArgument1()

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