private boolean makeNegation()

in meta/src/main/java/org/arend/lib/meta/ContradictionMeta.java [181:243]
60 lines of code
17 McCabe index (conditional complexity)

  private boolean makeNegation(CoreExpression type, ConcreteExpression proof, ConcreteFactory factory, List<Negation> negations, Values<UncheckedExpression> values, Map<CoreClassField, Map<Integer, List<Edge<Integer>>>> transGraphs) {
    List<CoreParameter> parameters;
    if (type instanceof CorePiExpression) {
      parameters = new ArrayList<>();
      type = type.getPiParameters(parameters);
    } else {
      parameters = Collections.emptyList();
    }

    if (isEmpty(type)) {
      if (parameters.size() == 1) {
        Triple triple = Triple.make(Utils.unfoldType(parameters.get(0).getTypeExpr().normalize(NormalizationMode.WHNF)));
        if (triple != null) {
          if (triple.fun.getDefinition() == ext.equationMeta.less) {
            CoreExpression argType = triple.fun.getArgument().computeType().normalize(NormalizationMode.WHNF);
            if (argType instanceof CoreClassCallExpression && ((CoreClassCallExpression) argType).getDefinition().isSubClassOf(ext.equationMeta.LinearOrder)) {
              Integer index1 = values.addValue(triple.arg2);
              transGraphs.computeIfAbsent(ext.equationMeta.less, k -> new HashMap<>()).computeIfAbsent(index1, k -> new ArrayList<>())
                .add(new Edge<>(index1, values.addValue(triple.arg1), proof, EdgeKind.LESS_OR_EQ, null));
            }
          }
        }
      }

      List<NegationData> negationDataList = new ArrayList<>();
      makeNegationData(new ArrayDeque<>(parameters), type, new NegationData(new ArrayList<>(), new ArrayDeque<>()), negationDataList);
      for (NegationData negationData : negationDataList) {
        negations.add(negationData.make(parameters, type, proof, factory));
      }
      return true;
    } else if (parameters.isEmpty() && type instanceof CoreAppExpression app2) {
      if (app2.getFunction() instanceof CoreAppExpression app1) {
        CoreExpression fun = app1.getFunction();
        if (fun instanceof CoreFieldCallExpression) {
          CoreClassField field = ((CoreFieldCallExpression) fun).getDefinition();
          if (field.getUserData(ext.transitivityKey) != null) {
            Integer index1 = values.addValue(app1.getArgument());
            transGraphs.computeIfAbsent(field, f -> new HashMap<>()).computeIfAbsent(index1, i -> new ArrayList<>()).add(new Edge<>(index1, values.addValue(app2.getArgument()), proof, EdgeKind.LESS, factory.core(app1.computeTyped())));
            return true;
          }
          FieldKey.Data irreflexivityData = field.getUserData(ext.irreflexivityKey);
          if (irreflexivityData != null) {
            List<CoreParameter> irrParams = new ArrayList<>(2);
            CoreExpression irrCodomain = irreflexivityData.field.getResultType().getPiParameters(irrParams);
            if (irrParams.size() != 2) { // This shouldn't happen
              return false;
            }
            negations.add(new Negation(Collections.singletonList(new EqType(null, null, app1.getArgument(), app2.getArgument())), irrCodomain, args -> {
              List<ConcreteArgument> irrArgs = new ArrayList<>(2);
              if (irrParams.get(0).isExplicit()) {
                irrArgs.add(factory.arg(factory.hole(), true));
              }
              irrArgs.add(factory.arg(factory.app(factory.ref(ext.transportInv.getRef()), true, Arrays.asList(factory.core(app1.computeTyped()), args.getFirst(), proof)), irrParams.get(1).isExplicit()));
              return factory.app(factory.ref(irreflexivityData.field.getRef()), irrArgs);
            }));
            return true;
          }
        }
      }
    }

    return false;
  }