private ConcreteExpression processParameters()

in meta/src/main/java/org/arend/lib/meta/ExistsMeta.java [141:276]
128 lines of code
39 McCabe index (conditional complexity)

    private ConcreteExpression processParameters(List<? extends ConcreteParameter> parameters, int abstracted, ExpressionTypechecker typechecker) {
      if (parameters.isEmpty()) {
        return getResult();
      }

      ConcreteParameter param = parameters.get(0);
      ConcreteExpression cType = Objects.requireNonNull(param.getType());
      ConcreteExpression aType;
      List<ConcreteParameter> varParams;
      TypedExpression typedType;
      CoreExpression type = null;
      if (cType instanceof ConcreteHoleExpression) {
        typedType = typechecker.typecheckType(cType);
        if (typedType == null) return null;
        aType = factory.core(typedType);
      } else {
        CoreExpression[] types = new CoreExpression[] { null };
        Pair<AbstractedExpression, TypedExpression> pair = typechecker.typecheckAbstracted(cType, null, abstracted, typed -> {
          typed = typed.normalizeType();
          types[0] = typed.getType();
          if (!(types[0] instanceof CoreUniverseExpression || types[0] instanceof CorePiExpression || types[0] instanceof CoreClassCallExpression && ((CoreClassCallExpression) types[0]).getDefinition() == ext.prelude.getDArray())) {
            typed = typechecker.coerceToType(typed, cType);
            if (typed == null) {
              if (!types[0].reportIfError(typechecker.getErrorReporter(), cType)) {
                typechecker.getErrorReporter().report(new TypeMismatchError(DocFactory.text("\\Type"), types[0], cType));
              }
              return null;
            }
          }
          return typed;
        });
        if (pair == null) return null;
        aType = factory.withData(cType.getData()).abstracted(pair.proj1, new ArrayList<>(arguments));
        typedType = pair.proj2;
        type = types[0];
      }

      List<ArendRef> refs;
      if (type instanceof CorePiExpression) {
        List<CoreParameter> piParams = new ArrayList<>();
        CoreExpression cod = type.getPiParameters(piParams);
        if (!(cod instanceof CoreUniverseExpression)) {
          typechecker.getErrorReporter().report(new TypeMismatchError(DocFactory.text("_ -> \\Type"), type, cType));
          return null;
        }
        refs = null;
        List<ArendRef> sigmaRefs = new ArrayList<>(param.getRefList().size());
        List<? extends ArendRef> paramRefList = param.getRefList();
        if (param.getRefList().isEmpty() || param.getRefList().size() == 1 && param.getRefList().get(0) == null) {
          paramRefList = new ArrayList<>(piParams.size());
          for (CoreParameter ignored : piParams) {
            paramRefList.add(null);
          }
        }
        int i = 0;
        for (ArendRef ref : paramRefList) {
          sigmaRefs.add(ref != null ? ref : factory.local(ext.renamerFactory.getNameFromType(piParams.get(i % piParams.size()).getTypeExpr(), null)));
          i++;
        }
        if (sigmaRefs.size() % piParams.size() != 0) {
          typechecker.getErrorReporter().report(new TypecheckingError("Expected (" + piParams.size() + " * n) parameters", param));
          return null;
        }

        varParams = new ArrayList<>(piParams.size());
        int j = 0;
        for (CoreParameter piParam : piParams) {
          List<ArendRef> curRef = new ArrayList<>();
          for (i = j; i < sigmaRefs.size(); i += piParams.size()) {
            curRef.add(sigmaRefs.get(i));
          }
          ConcreteParameter varParam = produceParam(param.isExplicit(), curRef, factory.withData(cType.getData()).core(piParam.getTypedType()), null);
          sigmaParams.add(varParam);
          varParams.add(varParam);
          j++;
        }
        i = 0;
        while (i < sigmaRefs.size()) {
          List<ConcreteArgument> args = new ArrayList<>(piParams.size());
          for (CoreParameter piParam : piParams) {
            args.add(factory.arg(factory.ref(sigmaRefs.get(i++)), piParam.isExplicit()));
          }
          sigmaParams.add(produceParam(true, null, factory.app(aType, args), null));
        }

        j = 0;
        for (CoreParameter ignored : piParams) {
          for (i = j; i < paramRefList.size(); i += piParams.size()) {
            ArendRef ref = paramRefList.get(i);
            arguments.add(ref == null ? null : factory.ref(ref));
          }
          j++;
        }
      } else if (type instanceof CoreClassCallExpression && ((CoreClassCallExpression) type).getDefinition() == ext.prelude.getDArray()) {
        refs = new ArrayList<>(param.getRefList().size());
        for (ArendRef ignored : param.getRefList()) {
          refs.add(factory.local("j" + (arrayIndex == 0 ? "" : arrayIndex)));
          arrayIndex++;
        }
        ConcreteParameter varParam = produceParam(param.isExplicit(), refs, factory.app(factory.ref(ext.prelude.getFin().getRef()), true, Collections.singletonList(factory.app(factory.ref(ext.prelude.getArrayLength().getRef()), false, Collections.singletonList(aType)))), param.getData());
        varParams = Collections.singletonList(varParam);
        sigmaParams.add(varParam);

        for (ArendRef ref : refs) {
          arguments.add(factory.ref(ref));
        }
      } else {
        refs = null;
        varParams = Collections.singletonList(factory.withData(param.getData()).param(param.isExplicit(), param.getRefList(), factory.withData(cType.getData()).core(typedType)));
        sigmaParams.add(produceParam(param.isExplicit(), param.getRefList(), aType, null));

        for (ArendRef ref : param.getRefList()) {
          arguments.add(ref == null ? null : factory.ref(ref));
        }
      }

      if (parameters.size() == 1) {
        return getResult();
      }

      return typechecker.withFreeBindings(new FreeBindingsModifier().addParams(varParams), tc -> {
        List<? extends ConcreteParameter> newParams = parameters.subList(1, parameters.size());
        int newAbstracted = abstracted + param.getNumberOfParameters();
        if (refs == null) {
          return processParameters(newParams, newAbstracted, tc);
        }
        List<Pair<ArendRef, CoreBinding>> list = new ArrayList<>(refs.size());
        for (int i = 0; i < refs.size(); i++) {
          TypedExpression result = tc.typecheck(factory.app(factory.ref(ext.prelude.getArrayIndex().getRef()), true, Arrays.asList(factory.withData(cType.getData()).core(typedType), factory.ref(refs.get(i)))), null);
          if (result == null) return null;
          ArendRef ref = param.getRefList().get(i);
          list.add(new Pair<>(ref, result.makeEvaluatingBinding(ref != null ? ref.getRefName() : ext.renamerFactory.getNameFromType(result.getType(), null))));
        }
        return tc.withFreeBindings(new FreeBindingsModifier().addRef(list), tc2 -> processParameters(newParams, newAbstracted, tc2));
      });
    }