Why it's not optimized

Stream: lean4

[lean_user]

leanprover/lean4:v4.20.1

set_option trace.compiler.ir.result true in
def f_optimized (xs : List Nat) : List Nat :=
  (xs.map (· + 1)).map (· * 2) -- expected xs.map ((· + 1)  *  2)

#eval Lean.Compiler.compile #[``f_optimized]
#eval Lean.Compiler.LCNF.showDecl .base ``f_optimized

[lean_user]

set_option trace.compiler.ir.result true in
...
[result]
def List.mapTR.loop._at.f_optimized._spec_1 (x_1 : obj) (x_2 : obj) : obj :=
  case x_1 : obj of
  List.nil →
    let x_3 : obj := List.reverse._rarg x_2;
    ret x_3
  List.cons →
    let x_4 : u8 := isShared x_1;
    case x_4 : u8 of
    Bool.false →
      let x_5 : obj := proj[0] x_1;
      let x_6 : obj := proj[1] x_1;
      let x_7 : obj := 1;
      let x_8 : obj := Nat.add x_5 x_7;
      dec x_5;
      set x_1[1] := x_2;
      set x_1[0] := x_8;
      let x_9 : obj := List.mapTR.loop._at.f_optimized._spec_1 x_6 x_1;
      ret x_9
    Bool.true →
      let x_10 : obj := proj[0] x_1;
      let x_11 : obj := proj[1] x_1;
      inc x_11;
      inc x_10;
      dec x_1;
      let x_12 : obj := 1;
      let x_13 : obj := Nat.add x_10 x_12;
      dec x_10;
      let x_14 : obj := ctor_1[List.cons] x_13 x_2;
      let x_15 : obj := List.mapTR.loop._at.f_optimized._spec_1 x_11 x_14;
      ret x_15
def List.mapTR.loop._at.f_optimized._spec_2 (x_1 : obj) (x_2 : obj) : obj :=
  case x_1 : obj of
  List.nil →
    let x_3 : obj := List.reverse._rarg x_2;
    ret x_3
  List.cons →
    let x_4 : u8 := isShared x_1;
    case x_4 : u8 of
    Bool.false →
      let x_5 : obj := proj[0] x_1;
      let x_6 : obj := proj[1] x_1;
      let x_7 : obj := 2;
      let x_8 : obj := Nat.mul x_5 x_7;
      dec x_5;
      set x_1[1] := x_2;
      set x_1[0] := x_8;
      let x_9 : obj := List.mapTR.loop._at.f_optimized._spec_2 x_6 x_1;
      ret x_9
    Bool.true →
      let x_10 : obj := proj[0] x_1;
      let x_11 : obj := proj[1] x_1;
      inc x_11;
      inc x_10;
      dec x_1;
      let x_12 : obj := 2;
      let x_13 : obj := Nat.mul x_10 x_12;
      dec x_10;
      let x_14 : obj := ctor_1[List.cons] x_13 x_2;
      let x_15 : obj := List.mapTR.loop._at.f_optimized._spec_2 x_11 x_14;
      ret x_15
def f_optimized (x_1 : obj) : obj :=
  let x_2 : obj := ctor_0[List.nil];
  let x_3 : obj := List.mapTR.loop._at.f_optimized._spec_1 x_1 x_2;
  let x_4 : obj := List.mapTR.loop._at.f_optimized._spec_2 x_3 x_2;
  ret x_4

#eval Lean.Compiler.LCNF.showDecl .base ``f_optimized
def f_optimized xs : List Nat :=
  let _x.1 := instMulNat;
  let _x.2 := @instHMul _ _x.1;
  fun _f.3 x.4 : Nat :=
    let _x.5 := _x.2 # 0;
    let _x.6 := 2;
    let _x.7 := instOfNatNat _x.6;
    let _x.8 := _x.7 # 0;
    let _x.9 := _x.5 x.4 _x.8;
    return _x.9;
  let _x.10 := instAddNat;
  let _x.11 := @instHAdd _ _x.10;
  fun _f.12 x.13 : Nat :=
    let _x.14 := _x.11 # 0;
    let _x.15 := 1;
    let _x.16 := instOfNatNat _x.15;
    let _x.17 := _x.16 # 0;
    let _x.18 := _x.14 x.13 _x.17;
    return _x.18;
  let _x.19 := @List.mapTR _ _ _f.12 xs;
  let _x.20 := @List.mapTR _ _ _f.3 _x.19;
  return _x.20

[Henrik Böving]

Because the compile has no support for fusion right now.