public static ConcreteExpression chainOfTransports()

in meta/src/main/java/org/arend/lib/meta/RewriteMeta.java [205:241]
34 lines of code
7 McCabe index (conditional complexity)

  public static ConcreteExpression chainOfTransports(ConcreteExpression transport, CoreExpression type, List<EqProofConcrete> eqProofs, ConcreteExpression term, ConcreteFactory factory, StdExtension ext) {
    var result = term;
    var curType = type; //typechecker.typecheck(type, null);
    List<CoreBinding> paramList = new ArrayList<>();
    boolean isInverse = ((ConcreteReferenceExpression)transport).getReferent() == ext.transportInv.getRef();

    for (int i = 0; i < eqProofs.size(); ++i) {
      if (!(curType instanceof CoreLamExpression)) return null;
      var body = ((CoreLamExpression)(curType)).getBody();
      var param = ((CoreLamExpression)(curType)).getParameters();
      int finalI = i;
      paramList.add(param.getBinding());
      var absNewBody = SubstitutionMeta.makeLambda(body, paramList, factory, expression -> {
        var newBody = factory.core(expression.computeTyped());
        for (int j = finalI + 1; j < eqProofs.size(); ++j) {
          var left = !isInverse ? eqProofs.get(j).left : eqProofs.get(j).right;
          newBody = factory.appBuilder(newBody).app(left).build();
        }
        return newBody;
      });  //factory.lam(paramList, newBody);
      for (int j = 0; j < i; ++j) {
        var right = !isInverse ? eqProofs.get(j).right : eqProofs.get(j).left;
        absNewBody = factory.appBuilder(absNewBody).app(right).build();
      }
      var left = eqProofs.get(i).left; //isInverse ? eqProofs.get(i).left : eqProofs.get(i).right;//eqProofs.get(i).left; //
      var right = eqProofs.get(i).right; //isInverse ? eqProofs.get(i).right : eqProofs.get(i).left;//eqProofs.get(i).right; //
      result = factory.appBuilder(transport)//.app(factory.hole(), false)
              //.app(factory.core(transportType))
              .app(absNewBody) //.app(left, false).app(right, false)
              .app(eqProofs.get(i).proof)
              .app(result)
              .build();
      curType = body;
    }

    return result;
  }