private BasePiTree make()

in meta/src/main/java/org/arend/lib/meta/pi_tree/PiTreeMaker.java [46:133]
81 lines of code
18 McCabe index (conditional complexity)

  private BasePiTree make(boolean isRoot, CoreParameter parameter, CoreExpression expr) {
    List<CoreParameter> params = new ArrayList<>();
    expr = expr.normalize(NormalizationMode.WHNF);
    CoreExpression codomain = expr;
    int k = lamParams.size();
    List<Integer> indices1 = new ArrayList<>();
    loop:
    while (codomain instanceof CorePiExpression) {
      CorePiExpression piExpr = (CorePiExpression) codomain;
      Set<? extends CoreBinding> codomainFreeVars = piExpr.getCodomain().findFreeBindings();
      for (CoreParameter param = piExpr.getParameters(); param.hasNext(); param = param.getNext(), k++) {
        ArendRef lamRef = factory.local("x" + (k + 1));
        lamParams.add(factory.param(lamRef));
        substitution.add(new SubstitutionPair(param.getBinding(), factory.ref(lamRef)));

        if (codomainFreeVars.contains(param.getBinding())) {
          if (isRoot && param.getTypeExpr().findFreeBindings(substBindings) == null) {
            indices1.add(k);
          } else {
            break loop;
          }
        }
      }

      for (CoreParameter param = piExpr.getParameters(); param.hasNext(); param = param.getNext()) {
        params.add(param);
      }
      codomain = piExpr.getCodomain();
    }

    Set<? extends CoreBinding> freeVars = expr.findFreeBindings();
    List<Integer> indices = new ArrayList<>(freeVars.size());
    for (int i = 0; i < substitution.size(); i++) {
      if (freeVars.contains(substitution.get(i).binding)) {
        indices.add(i);
      }
    }
    indices.addAll(indices1);

    ConcreteExpression concrete;
    boolean useLet;
    if (indices.isEmpty()) {
      if (!isRoot) {
        params.clear();
        codomain = expr;
      }
      concrete = factory.core(codomain.computeTyped());
      useLet = !(expr instanceof CoreReferenceExpression);
    } else {
      List<ConcreteParameter> redLamParams;
      List<SubstitutionPair> redSubstitution;
      if (indices.size() == substitution.size()) {
        redLamParams = lamParams;
        redSubstitution = substitution;
      } else {
        redLamParams = new ArrayList<>(indices.size());
        redSubstitution = new ArrayList<>(indices.size());
        for (Integer index : indices) {
          redLamParams.add(lamParams.get(index));
          redSubstitution.add(substitution.get(index));
        }
      }

      TypedExpression result = typechecker.typecheck(factory.lam(redLamParams, factory.meta("ext_sigma_pi_param", new SubstitutionMeta(codomain, redSubstitution))), null);
      if (result == null) return null;
      concrete = factory.core(result);
      useLet = !(result.getExpression() instanceof CoreReferenceExpression);
    }

    ConcreteExpression altHead;
    if (useLet) {
      ArendRef letRef = factory.local("T" + index++);
      ConcreteLetClause clause = factory.letClause(letRef, Collections.emptyList(), null, concrete);
      clauses.add(clause);
      clauseMap.put(letRef, clause);
      altHead = factory.ref(letRef);
    } else {
      altHead = concrete;
    }

    List<PiTreeNode> subtrees = new ArrayList<>(params.size());
    for (CoreParameter param : params) {
      PiTreeNode subtree = (PiTreeNode) make(false, param, param.getTypeExpr());
      if (subtree == null) return null;
      subtrees.add(subtree);
    }
    return isRoot ? new PiTreeRoot(concrete, altHead, indices, subtrees, indices.size() == indices1.size()) : new PiTreeNode(parameter, concrete, altHead, indices, subtrees);
  }