public ConcreteExpression simplifyTypeOfExpression()

in meta/src/main/java/org/arend/lib/meta/simplify/Simplifier.java [227:307]
44 lines of code
11 McCabe index (conditional complexity)

    public ConcreteExpression simplifyTypeOfExpression(ConcreteExpression expression, CoreExpression type, boolean isForward) {
        CoreExpression normType = type.normalize(NormalizationMode.WHNF);
        var processor = new SimplifyExpressionProcessor();
        typechecker.withCurrentState(tc -> normType.processSubexpression(processor));

        var occurrences = processor.getSimplificationOccurrences().stream().map(x -> x.proj1).collect(Collectors.toList());
        var lamParams = new ArrayList<ConcreteParameter>();

        if (occurrences.isEmpty()) {
            errorReporter.report(new TypecheckingError("Nothing to simplify", refExpr));
            return expression;
        }

        for (int i = 0; i < occurrences.size(); ++i) {
            var var = factory.local("y" + i);
            var typeParam = factory.core(occurrences.get(i).computeType().computeTyped());
            lamParams.add(factory.param(true, Collections.singletonList(var), typeParam));
        }

        ConcreteExpression lam = factory.lam(lamParams, factory.meta("\\lam y_v => {!}", new MetaDefinition() {
            @Override
            public TypedExpression invokeMeta(@NotNull ExpressionTypechecker typechecker, @NotNull ContextData contextData) {
                List<TypedExpression> checkedVars = new ArrayList<>();

                for (var param : lamParams) {
                    var checkedVar =  typechecker.typecheck(factory.ref(param.getRefList().get(0)), null);
                    assert checkedVar != null;
                    checkedVars.add(checkedVar);
                }

                Map<Wrapper<CoreExpression>, Integer> indexOfSubExpr = new HashMap<>();

                for (int i = 0; i < occurrences.size(); ++i) {
                    indexOfSubExpr.put(new Wrapper<>(occurrences.get(i)), i);
                }

                UncheckedExpression typeWithOccur = replaceSubexpr(normType, checkedVars, indexOfSubExpr, processor.getExprsToNormalize(), occurrences);

        /*final boolean[] subexprNormalized = {true};

        while (subexprNormalized[0]) {
          subexprNormalized[0] = false;
          typeWithOccur = typeWithOccur.replaceSubexpressions(expression -> {
            var newSubexpr = expression;
            if (processor.getExprsToNormalize().containsKey(expression)) {
              subexprNormalized[0] = true;
              newSubexpr = processor.getExprsToNormalize().get(expression);
            }
            Integer occurInd = indexOfSubExpr.get(new Wrapper<>(newSubexpr));
            if (occurInd != null) {
              return newSubexpr;
            }
            return newSubexpr == expression ? null : newSubexpr;
          }, true);
          if (typeWithOccur == null) break;
        }

        typeWithOccur = typeWithOccur == null ? null : typeWithOccur.replaceSubexpressions(expression -> {
          Integer occurInd = indexOfSubExpr.get(new Wrapper<>(expression));
          if (occurInd == null) return null;
          return checkedVars.get(occurInd).getExpression();
        }, false); /**/

                TypedExpression result = typeWithOccur != null ? Utils.tryTypecheck(typechecker, tc -> tc.check(typeWithOccur, refExpr)) : null;
                if (result == null) {
                    errorReporter.report(typeWithOccur == null ? new SimplifyError(typechecker.getExpressionPrettifier(), occurrences, normType, refExpr) : new TypeError(typechecker.getExpressionPrettifier(), "Cannot substitute a variable. The resulting type is invalid", typeWithOccur, refExpr));
                }/**/
                return result;
                // return typeWithOccur;
            }
        }));

        var checkedLam = typechecker.typecheck(lam, null);

        if (checkedLam == null || checkedLam instanceof CoreErrorExpression) {
            return null;
        }
        var proofs = processor.simplificationOccurrences.stream().map(x -> isForward ? x.proj2 : x.proj2.inverse(factory, ext)).collect(Collectors.toList());
        return RewriteMeta.chainOfTransports(factory.ref(ext.transport.getRef(), refExpr.getPLevels(), refExpr.getHLevels()),
                checkedLam.getExpression(), proofs, expression, factory, ext);
    }