ConcreteExpression make()

in meta/src/main/java/org/arend/lib/meta/SimpCoeMeta.java [255:291]
35 lines of code
7 McCabe index (conditional complexity)

    ConcreteExpression make(ConcreteFactory factory, CoreExpression transportTypeArg, ConcreteExpression transportLeftArg, ConcreteExpression transportRightArg, ConcreteExpression transportPathArg, CoreExpression transportValueArg, CoreExpression eqRight) {
      ArendRef jLamRef1 = factory.local("a''");
      ArendRef jLamRef2 = factory.local("q");
      ArendRef jPiRef = factory.local("s'");
      ArendRef typeRef = factory.local("T");
      ConcreteExpression leftExpr = makeConcreteValueArg(transportValueArg, factory);
      ConcreteExpression concreteTransportLam = factory.core(transportLam.computeTyped());
      List<ConcreteParameter> sigmaParams = new ArrayList<>();
      for (int i = 0; i < sigmaParamTypes.size(); i++) {
        sigmaParams.add(factory.param(List.of(), factory.app(factory.ref(ext.prelude.getEquality().getRef()), true, Arrays.asList(factory.app(factory.ref(ext.transport.getRef()), true, Arrays.asList(SubstitutionMeta.makeLambda(sigmaParamTypes.get(i), transportLam.getParameters().getBinding(), factory), factory.ref(jLamRef2), proj(leftExpr, i, factory))), proj(factory.ref(jPiRef), i, factory)))));
      }
      ConcreteExpression jDom = factory.sigma(sigmaParams);
      ConcreteExpression jCod = factory.appBuilder(factory.ref(ext.prelude.getEquality().getRef()))
        .app(factory.ref(typeRef), false)
        .app(factory.app(factory.ref(ext.transport.getRef()), true, Arrays.asList(concreteTransportLam, factory.ref(jLamRef2), leftExpr)))
        .app(factory.ref(jPiRef))
        .build();
      ConcreteLetClause letClause = factory.letClause(typeRef, Collections.emptyList(), null, factory.app(concreteTransportLam, true, Collections.singletonList(factory.ref(jLamRef1))));
      ConcreteExpression jLam = factory.lam(Arrays.asList(factory.param(jLamRef1), factory.param(jLamRef2)), factory.letExpr(false, false, Collections.singletonList(letClause), factory.pi(Collections.singletonList(factory.param(true, Collections.singletonList(jPiRef), factory.ref(typeRef))), factory.arr(isForward ? jCod : jDom, isForward ? jDom : jCod))));

      ArendRef jArgRef = factory.local("h");
      ConcreteExpression jArgArg;
      if (isForward) {
        List<ConcreteExpression> fields = new ArrayList<>(sigmaParams.size());
        for (int i = 0; i < sigmaParams.size(); i++) {
          ArendRef iRef = factory.local("i");
          fields.add(factory.path(factory.lam(Collections.singletonList(factory.param(iRef)), proj(factory.app(factory.ref(jArgRef), true, factory.ref(iRef)), i, factory))));
        }
        jArgArg = factory.tuple(fields);
      } else {
        jArgArg = factory.app(factory.meta("ext", ext.extMeta), true, factory.ref(jArgRef));
      }
      ConcreteExpression jArg = factory.lam(Arrays.asList(factory.param(null), factory.param(jArgRef)), jArgArg);

      ConcreteExpression result = factory.app(factory.ref(ext.Jl.getRef()), true, Arrays.asList(jLam, jArg, transportPathArg, factory.core(eqRight.computeTyped()), argument));
      return letClauses.isEmpty() ? result : factory.letExpr(false, false, letClauses, result);
    }