private boolean initializeAlgebraSolver()

in meta/src/main/java/org/arend/lib/meta/equation/EqualitySolver.java [118:160]
40 lines of code
14 McCabe index (conditional complexity)

  private boolean initializeAlgebraSolver(CoreExpression type) {
    if (!useSolver) {
      return false;
    }

    type = type == null ? null : type.normalize(NormalizationMode.WHNF);

    if (type instanceof CoreAppExpression) {
      CoreExpression typeFun = ((CoreAppExpression) type).getFunction().normalize(NormalizationMode.WHNF);
      if (typeFun instanceof CoreAppExpression) {
        CoreExpression fun = ((CoreAppExpression) typeFun).getFunction().normalize(NormalizationMode.WHNF);
        if (fun instanceof CoreFieldCallExpression) {
          if (((CoreFieldCallExpression) fun).getDefinition() == meta.ext.sipMeta.catHom) {
            algebraSolver = new MonoidSolver(meta, typechecker, factory, refExpr, equality, ((CoreFieldCallExpression) fun).getArgument().computeTyped(), null, null, false);
            return true;
          }
          return false;
        }
      }
    }

    var possibleClasses = new HashSet<>(Arrays.asList(meta.Monoid, meta.AddMonoid, meta.MSemilattice));
    Pair<TypedExpression, CoreClassCallExpression> pair = Utils.findInstanceWithClassCall(new InstanceSearchParameters() {
        @Override
        public boolean testClass(@NotNull CoreClassDefinition classDefinition) {
          if (forcedClass != null && !classDefinition.isSubClassOf(forcedClass)) {
            return false;
          }
          for (var clazz : possibleClasses) {
            if (classDefinition.isSubClassOf(clazz) && (forcedClass == null || forcedClass.isSubClassOf(clazz))) {
              return true;
            }
          }
          return false;
        }
      }, meta.ext.carrier, type, typechecker, refExpr, forcedClass);
    if (pair != null) {
      initializeAlgebraSolver(pair.proj1, pair.proj2);
      return true;
    } else {
      return false;
    }
  }