public boolean isApplicable()

in meta/src/main/java/org/arend/lib/meta/equation/TransitivitySolver.java [77:147]
65 lines of code
17 McCabe index (conditional complexity)

  public boolean isApplicable(CoreExpression type) {
    RelationData relationData = RelationData.getRelationData(type);
    if (relationData == null || instanceDefinition != null && relationData.defCall.getDefinition() != instanceDefinition) {
      return false;
    }

    leftValue = relationData.leftExpr;
    rightValue = relationData.rightExpr;
    if (relationData.defCall instanceof CoreFieldCallExpression fieldCall) {
      transFieldData = fieldCall.getDefinition().getUserData(meta.ext.transitivityKey);
      if (transFieldData == null) {
        return false;
      }

      reflFieldData = fieldCall.getDefinition().getUserData(meta.ext.reflexivityKey);
      relation = new Lazy<>(() -> factory.core(fieldCall.computeTyped()));
      valuesType = new Lazy<>(() -> {
        TypedExpression instance = fieldCall.getArgument().computeTyped();
        if (instance.getType() instanceof CoreClassCallExpression) {
          CoreExpression result = ((CoreClassCallExpression) instance.getType()).getImplementation(meta.ext.carrier, instance);
          if (result != null) {
            return result;
          }
        }
        return Objects.requireNonNull(typechecker.typecheck(factory.app(factory.ref(meta.ext.carrier.getRef()), false, Collections.singletonList(factory.core(instance))), null)).getExpression();
      });
      instanceDefinition = fieldCall.getDefinition();
    } else {
      CoreDefCallExpression defCall = relationData.defCall;
      EquationMeta.TransitivityInstanceCache cache = meta.transitivityInstanceCache.get(defCall.getDefinition());
      CoreClassField relationField;
      TypedExpression instance;
      if (cache != null) {
        List<ConcreteExpression> args = new ArrayList<>();
        for (CoreParameter param = cache.instance.getParameters(); param.hasNext(); param = param.getNext()) {
          if (param.isExplicit()) {
            args.add(factory.hole());
          }
        }
        instance = typechecker.typecheck(factory.app(factory.ref(cache.instance.getRef()), true, args), null);
        relationField = cache.relationField;
      } else {
        MyInstanceSearchParameters parameters = new MyInstanceSearchParameters(defCall.getDefinition());
        instance = typechecker.findInstance(parameters, null, null, refExpr);
        if (instance != null && instance.getExpression() instanceof CoreFunCallExpression) {
          meta.transitivityInstanceCache.put(defCall.getDefinition(), new EquationMeta.TransitivityInstanceCache(((CoreFunCallExpression) instance.getExpression()).getDefinition(), parameters.getRelationField()));
        }
        relationField = parameters.getRelationField();
      }

      if (instance == null || !(instance.getType() instanceof CoreClassCallExpression)) {
        return false;
      }

      transFieldData = relationField.getUserData(meta.ext.transitivityKey);
      reflFieldData = relationField.getUserData(meta.ext.reflexivityKey);
      relation = new Lazy<>(() -> factory.core(Objects.requireNonNull(((CoreClassCallExpression) instance.getType()).getImplementation(relationField, instance)).computeTyped()));
      valuesType = new Lazy<>(() -> ((CoreClassCallExpression) instance.getType()).getImplementation(meta.ext.carrier, instance));
      instanceDefinition = defCall.getDefinition();
    }

    List<ConcreteArgument> args = new ArrayList<>(3);
    for (int i = 0; i < 3; i++) {
      if (transFieldData.parametersExplicitness.get(i)) {
        args.add(factory.arg(factory.hole(), true));
      }
    }
    trans = factory.app(factory.ref(transFieldData.field.getRef()), args);

    return true;
  }