Lean benchmarks

lean_forin.lean

def countPairs (xm ym:Nat) : IO Nat := do
  let mut count := 0
  for x in [0:xm+1] do
    for y in [0:ym+1] do
      count := if x == y then count + 1 else count
  return count

def main (args : List String) : IO UInt32 :=
do
  let xmax := 10000
  let ymax := 10000
  let c <- countPairs xmax ymax
  IO.println c
  return 0

matrix_slow.lean

partial def makePairs (ymax x y:Nat) : List (Nat × Nat) :=
(x, y) :: match (x, y) with
| (0, 0) => []
| (x, 0) => makePairs ymax (x-1) ymax
| (x, y) => makePairs ymax x (y-1)



def main (args : List String) : IO UInt32 :=
do
  let xmax := 10000
  let ymax := 10000
  let ps := makePairs ymax xmax ymax
  let fn := ps.filter (λ(x, y)=> x == y)
  IO.println fn.length
  return 0

matrix_tailrec.lean

partial def makePairs (ymax x y:Nat) (l:List (Nat × Nat)) : List (Nat × Nat) :=
match (x, y) with
| (0, 0) => (x, y) :: l
| (x, 0) => makePairs ymax (x-1) ymax ((x, y)::l)
| (x, y) => makePairs ymax x (y-1) ((x, y)::l)



def main (args : List String) : IO UInt32 :=
do
  let xmax := 10000
  let ymax := 10000
  let ps := makePairs ymax xmax ymax []
  let fn := ps.filter (λ(x, y)=> x == y)
  IO.println fn.length
  return 0

time.txt

Real time using UNIX time on a 2016 Macbook Pro with 2,9 GHz Dual-Core Intel Core i5

matrix_slow.lean    Stack Overflow
matrix_tailrec.lean 58.35s
matrix_forin.lean   53.22s