list_rev.lean

import data.stream
open list

def list_rev_bench (size : ℕ) : ℕ :=
head $ stream.iterate reverse (iota (10*size)) size

vm_eval let size := 1200 in
timeit ("list_rev_bench " ++ size^.to_string ++ ":") (list_rev_bench size)

lpo.lean

import tools.super
open super expr

meta def mk_term (base : name) : ℕ → expr
| 0 := const base []
| (n+1) := let fn := if n % 2 = 0 then `f else `g in
           app (const fn []) (mk_term n)

meta def lpo_bench (size : ℕ) : bool :=
mk_lpo [`f, `g, `c, `d] (mk_term `d size) (mk_term `c size)

vm_eval let size := 10000 in
        timeit ("lpo_bench " ++ size^.to_string ++ ":") (lpo_bench size)

struct_perm.lean

import data.stream

structure foo :=
(a b c d e : ℕ)

def perm (x : foo) : foo :=
{ a := x^.b, b := x^.c, c := x^.d, d := x^.e, e := x^.a }

def struct_perm_bench (size : ℕ) : foo :=
stream.iterate perm (foo.mk 1 2 3 4 5) size

vm_eval let size := 10000000 in
  timeit ("struct_perm_bench " ++ size^.to_string ++ ":") (struct_perm_bench size)

with_checks.txt

list_rev_bench 1200: 1.36714 secs
lpo_bench 10000: 1.11722 secs
struct_perm_bench 10000000: 2.11369 secs

without_checks.txt

list_rev_bench 1200: 1.40080 secs
lpo_bench 10000: 1.09606 secs
struct_perm_bench 10000000: 1.90311 secs