private ConcreteExpression computeTerm()

in meta/src/main/java/org/arend/lib/meta/equation/MonoidSolver.java [801:871]
66 lines of code
22 McCabe index (conditional complexity)

  private ConcreteExpression computeTerm(CoreExpression expression, List<Integer> nf) {
    CoreExpression expr = expression.normalize(NormalizationMode.WHNF);
    int dom = -1, cod = -1;
    ConcreteExpression hdata = isCat ? factory.appBuilder(factory.ref(meta.HDataFunc.getRef())).app(factory.ref(dataRef), false).build() : null;
    ConcreteExpression vdata = isCat ? factory.appBuilder(factory.ref(meta.VDataFunc.getRef())).app(factory.ref(dataRef), false).build() : null;

    if (isCat) {
      CoreExpression type = expr.computeType().normalize(NormalizationMode.WHNF);
      if (type instanceof CoreAppExpression) {
        CoreExpression fun = ((CoreAppExpression) type).getFunction().normalize(NormalizationMode.WHNF);
        if (fun instanceof CoreAppExpression) {
          dom = obValues.addValue(((CoreAppExpression) fun).getArgument());
          cod = obValues.addValue(((CoreAppExpression) type).getArgument());
        }
      }
    }

    if (ideMatcher.match(expr) != null) {
      if (isCat) {
        if (dom != -1 && cod != -1) {
          return factory.appBuilder(factory.ref(meta.idCTerm.getRef()))
                  .app(vdata, false)
                  .app(factory.number(dom), false)
                  .app(factory.number(cod), false)
                  .app(hdata, false)
                  .app(factory.ref(meta.ext.prelude.getIdp().getRef()))
                  .build();
        }
      }
      return isCat ? factory.app(factory.ref(meta.idCTerm.getRef()), true, singletonList(factory.ref(meta.ext.prelude.getIdp().getRef()))) : factory.ref(meta.ideMTerm.getRef());
    }


    List<CoreExpression> args = mulMatcher.match(expr);
    if (args != null) {
      List<ConcreteExpression> cArgs = new ArrayList<>();
      List<ConcreteExpression> implArgs = new ArrayList<>();
      var left = computeTerm(args.get(args.size() - 2), nf);
      var right = computeTerm(args.get(args.size() - 1), nf);
      if (isCat) {
        if (dom != -1 && cod != -1) {
          implArgs.add(vdata);
          implArgs.add(factory.number(dom));
          implArgs.add(factory.number(cod));
          implArgs.add(hdata);
        }
        cArgs.add(factory.number(obValues.addValue(args.get(1))));
      }
      cArgs.add(left);
      cArgs.add(right);
      ConcreteExpression comp = factory.ref((isCat ? meta.compCTerm : meta.mulMTerm).getRef());
      if (!implArgs.isEmpty()) {
        comp = factory.app(comp, false, implArgs);
      }
      return factory.app(comp, true, cArgs);
    }

    int index = values.addValue(expr);
    nf.add(index);
    if (isCat) {
      if (dom != -1 && cod != -1) {
        domMap.put(index, dom);
        codomMap.put(index, cod);
        Map<Integer, Integer> list = homMap.computeIfAbsent(new Pair<>(dom, cod), k -> new HashMap<>());
        int newIndex = list.size();
        Integer prev = list.putIfAbsent(index, newIndex);
        index = prev != null ? prev : newIndex;
      }
    }
    return factory.app(factory.ref((isCat ? meta.varCTerm : meta.varMTerm).getRef()), true, singletonList(factory.number(index)));
  }