Reservoir

Lean 4 Itertools

This package provides an assortment of abstraction tools for performing iterations.

def foo :=
  generate 0 (· + 1)
  |> stopIf (· == 10)
  |> filter (· % 2 == 0)
  |> map (· * 2)
  |> array

#eval foo -- #[0, 4, 8, 12, 16]

It makes heavy use of type-level iterators and the @[inline] amd @[specialize] attributes to produce highly efficient code. This way, writing iterators using the tools provided is just as efficient as writing the loop manually.

def Itertools.MGenerate.forIn.loop._at.foo._spec_1 (x_1 : obj) (x_2 : obj) : obj :=
  let x_3 : obj := 10;
  let x_4 : u8 := Nat.beq x_1 x_3;
  case x_4 : u8 of
  Bool.false →
    let x_5 : obj := 2;
    let x_6 : obj := Nat.mod x_1 x_5;
    let x_7 : obj := 0;
    let x_8 : u8 := Nat.beq x_6 x_7;
    dec x_6;
    case x_8 : u8 of
    Bool.false →
      let x_9 : obj := 1;
      let x_10 : obj := Nat.add x_1 x_9;
      dec x_1;
      let x_11 : obj := Itertools.MGenerate.forIn.loop._at.foo._spec_1 x_10 x_2;
      ret x_11
    Bool.true →
      let x_12 : obj := Nat.mul x_1 x_5;
      let x_13 : obj := Array.push ◾ x_2 x_12;
      let x_14 : obj := 1;
      let x_15 : obj := Nat.add x_1 x_14;
      dec x_1;
      let x_16 : obj := Itertools.MGenerate.forIn.loop._at.foo._spec_1 x_15 x_13;
      ret x_16
  Bool.true →
    dec x_1;
    ret x_2
def foo._closed_1 : obj :=
  let x_1 : obj := 0;
  let x_2 : obj := Array.mkEmpty ◾ x_1;
  ret x_2
def foo : obj :=
  let x_1 : obj := 0;
  let x_2 : obj := foo._closed_1;
  let x_3 : obj := Itertools.MGenerate.forIn.loop._at.foo._spec_1 x_1 x_2;
  ret x_3

It is currently a work-in-progress, but isn't everything?