private Hypothesis typeToEquation()

in meta/src/main/java/org/arend/lib/meta/linear/LinearSolver.java [68:150]
78 lines of code
30 McCabe index (conditional complexity)

  private Hypothesis<CoreExpression> typeToEquation(CoreExpression type, CoreBinding binding, boolean reportError) {
    ConcreteExpression expr = binding == null ? null : factory.ref(binding);
    if (expr != null && type instanceof CorePiExpression) {
      ConcreteExpression newExpr = expr;
      while (type instanceof CorePiExpression) {
        List<ConcreteArgument> args = new ArrayList<>();
        for (CoreParameter param = ((CorePiExpression) type).getParameters(); param.hasNext(); param = param.getNext()) {
          args.add(factory.arg(factory.hole(), param.isExplicit()));
        }
        newExpr = factory.app(newExpr, args);
        type = ((CorePiExpression) type).getCodomain().normalize(NormalizationMode.WHNF);
      }
      TypedExpression typedExpr = typechecker.typecheck(newExpr, null);
      if (typedExpr != null) {
        expr = factory.core(typedExpr);
        type = typedExpr.getType();
      }
    }

    CoreFunCallExpression eq = type.toEquality();
    if (eq != null) {
      CoreExpression instance = findInstance(eq.getDefCallArguments().get(0), reportError);
      if (instance == null) return null;
      return new Hypothesis<>(expr, instance, Equation.Operation.EQUALS, eq.getDefCallArguments().get(1), eq.getDefCallArguments().get(2), BigInteger.ONE);
    }

    RelationData relationData = RelationData.getRelationData(type.normalize(NormalizationMode.WHNF));
    if (relationData == null) {
      if (reportError) reportTypeError(type);
      return null;
    }
    if (relationData.defCall instanceof CoreFieldCallExpression fieldCall) {
      CoreClassField field = fieldCall.getDefinition();
      if (field == ext.equationMeta.less || field == ext.equationMeta.lessOrEquals) {
        CoreExpression arg = fieldCall.getArgument();
        CoreExpression argType = arg.computeType().normalize(NormalizationMode.WHNF);
        if (argType instanceof CoreClassCallExpression classCall && classCall.getDefinition().isSubClassOf(getInstanceClass())) {
          return new Hypothesis<>(expr, arg, field == ext.equationMeta.less ? Equation.Operation.LESS : Equation.Operation.LESS_OR_EQUALS, relationData.leftExpr, relationData.rightExpr, BigInteger.ONE);
        } else {
          if (reportError) errorReporter.report(new TypeError(typechecker.getExpressionPrettifier(), "", argType, marker) {
            @Override
            public LineDoc getShortHeaderDoc(PrettyPrinterConfig ppConfig) {
              return DocFactory.hList(DocFactory.text("The type of the equation should be "), DocFactory.refDoc(getInstanceClass().getRef()));
            }
          });
          return null;
        }
      }
      if (reportError) reportTypeError(type);
      return null;
    }

    if (relationData.defCall.getDefinition() == ext.equationMeta.linearOrederLeq) {
      return new Hypothesis<>(expr, relationData.defCall.getDefCallArguments().get(0), Equation.Operation.LESS_OR_EQUALS, relationData.leftExpr, relationData.rightExpr, BigInteger.ONE);
    }

    if (relationData.defCall.getDefinition() == ext.equationMeta.addGroupLess) {
      CoreExpression instance = relationData.defCall.getDefCallArguments().get(0);
      TypedExpression typedInstance = instance.computeTyped();
      CoreExpression instanceType = typedInstance.getType().normalize(NormalizationMode.WHNF);
      if (!(instanceType instanceof CoreClassCallExpression classCall && classCall.getDefinition().isSubClassOf(getInstanceClass()))) {
        instance = findInstance(instanceType instanceof CoreClassCallExpression classCall ? Utils.getClassifyingExpression(classCall, typedInstance) : null, reportError);
        if (instance == null) return null;
      }
      return new Hypothesis<>(expr, instance, Equation.Operation.LESS, relationData.leftExpr, relationData.rightExpr, BigInteger.ONE);
    }

    var pair = instanceCache.computeIfAbsent(relationData.defCall.getDefinition(), def -> {
      DefImplInstanceSearchParameters parameters = new DefImplInstanceSearchParameters(def) {
        @Override
        protected List<CoreClassField> getRelationFields(CoreClassDefinition classDef) {
          return classDef.isSubClassOf(getInstanceClass()) ? Arrays.asList(ext.equationMeta.less, ext.equationMeta.lessOrEquals) : Collections.emptyList();
        }
      };
      TypedExpression instance = typechecker.findInstance(parameters, null, null, marker);
      return instance == null ? null : new Pair<>(instance, parameters.getRelationField());
    });
    if (pair == null) {
      if (reportError) reportTypeError(type);
      return null;
    }
    return new Hypothesis<>(expr, pair.proj1.getExpression(), pair.proj2 == ext.equationMeta.less ? Equation.Operation.LESS : Equation.Operation.LESS_OR_EQUALS, relationData.leftExpr, relationData.rightExpr, BigInteger.ONE);
  }