private record NegationData()

in meta/src/main/java/org/arend/lib/meta/ContradictionMeta.java [83:117]
34 lines of code
8 McCabe index (conditional complexity)

  private record NegationData(List<RType> types, Deque<Object> instructions) {
    private ConcreteExpression makeExpression(Deque<ConcreteExpression> arguments, CoreConstructor constructor, ConcreteFactory factory) {
        List<ConcreteArgument> args = new ArrayList<>();
        CoreParameter param = constructor.getParameters();
        if (param.hasNext() && !param.isExplicit()) {
          for (CoreParameter dataParam = constructor.getDataType().getParameters(); dataParam.hasNext(); dataParam = dataParam.getNext()) {
            args.add(factory.arg(factory.hole(), false));
          }
        }
        for (; param.hasNext(); param = param.getNext()) {
          Object con = instructions.removeFirst();
          if (con instanceof CoreConstructor) {
            args.add(factory.arg(makeExpression(arguments, (CoreConstructor) con, factory), param.isExplicit()));
          } else {
            args.add(factory.arg(arguments.removeFirst(), param.isExplicit()));
          }
        }
        return factory.app(factory.ref(constructor.getRef()), args);
      }

      Negation make(List<CoreParameter> parameters, CoreExpression codomain, ConcreteExpression proof, ConcreteFactory factory) {
        return new Negation(types, codomain, arguments -> {
          List<ConcreteArgument> args = new ArrayList<>();
          for (CoreParameter param : parameters) {
            Object con = instructions.removeFirst();
            if (con instanceof CoreConstructor) {
              args.add(factory.arg(makeExpression(arguments, (CoreConstructor) con, factory), param.isExplicit()));
            } else {
              args.add(factory.arg(arguments.removeFirst(), param.isExplicit()));
            }
          }
          return factory.app(proof, args);
        });
      }
    }