private void makeNegationData()

in meta/src/main/java/org/arend/lib/meta/ContradictionMeta.java [127:163]
36 lines of code
12 McCabe index (conditional complexity)

  private void makeNegationData(Deque<CoreParameter> parameters, CoreExpression codomain, NegationData negationData, List<NegationData> result) {
    while (!parameters.isEmpty()) {
      CoreParameter parameter = parameters.removeFirst();
      CoreExpression type = Utils.unfoldType(parameter.getTypeExpr().normalize(NormalizationMode.WHNF));
      List<CoreDataCallExpression.ConstructorWithDataArguments> constructors = isAppropriateDataCall(type) ? type.computeMatchedConstructorsWithDataArguments() : null;
      if (constructors != null) {
        boolean ok = codomain == null || !codomain.findFreeBinding(parameter.getBinding());
        if (ok) {
          for (CoreParameter param : parameters) {
            if (param.getTypeExpr().findFreeBinding(parameter.getBinding())) {
              ok = false;
              break;
            }
          }
        }
        if (ok) {
          for (CoreDataCallExpression.ConstructorWithDataArguments constructor : constructors) {
            NegationData conData = new NegationData(new ArrayList<>(negationData.types), new ArrayDeque<>(negationData.instructions));
            conData.instructions.addLast(constructor.getConstructor());
            List<CoreParameter> conParams = new ArrayList<>();
            for (CoreParameter conParam = constructor.getParameters(); conParam.hasNext(); conParam = conParam.getNext()) {
              conParams.add(conParam);
            }
            for (int i = conParams.size() - 1; i >= 0; i--) {
              parameters.addFirst(conParams.get(i));
            }
            makeNegationData(parameters, null, conData, result);
          }
          return;
        }
      }

      negationData.types.add(makeRType(parameter.getBinding(), type));
      negationData.instructions.addLast(Boolean.TRUE); // it doesn't matter what we add here
    }
    result.add(negationData);
  }