protected Pair simplifySubexpression()

in meta/src/main/java/org/arend/lib/meta/simplify/MulOfNegativesRule.java [27:57]

30 lines of code
9 McCabe index (conditional complexity)


  protected Pair<CoreExpression, ConcreteExpression> simplifySubexpression(CoreExpression subexpr) {
    List<CoreExpression> args = mulMatcher.match(subexpr);
    if (args != null) {
      var left = args.get(args.size() - 2);
      var right = args.get(args.size() - 1);
      args = negativeMatcher.match(left);
      boolean isNegOnTheLeft = args != null;
      if (args == null) {
        args = negativeMatcher.match(right);
        if (args == null) {
          return null;
        }
      }
      var firstValue = isNegOnTheLeft ? args.get(0) : left;
      var secondValue = isNegOnTheLeft ? right : args.get(0);
      ConcreteExpression negPath = isNegOnTheLeft ? factory.ref(ext.equationMeta.negMulLeft.getRef()) : factory.ref(ext.equationMeta.negMulRight.getRef());

      if (firstValue != null) {
        var subexprPath = factory.appBuilder(negPath)
                .app(factory.hole(), false)
                .app(factory.core(firstValue.computeTyped()), false)
                .app(factory.core(secondValue.computeTyped()), false).build();
        var newExpr = factory.appBuilder(factory.ref(ext.equationMeta.negative.getRef())).
                app(factory.appBuilder(factory.ref(ext.equationMeta.mul.getRef())).app(factory.core(firstValue.computeTyped())).app(factory.core(secondValue.computeTyped())).build()).build();
        var checkedNewExpr = typechecker.typecheck(newExpr, subexpr.computeType());
        if (checkedNewExpr == null) return null;
        return new Pair<>(checkedNewExpr.getExpression(), subexprPath);
      }
    }
    return null;
  }