chore: add rbmap.library benchmark to bench suite

This commit is contained in:
Sebastian Ullrich 2022-09-24 12:35:08 +02:00
parent 2a6697e077
commit 9f29967fb0
2 changed files with 21 additions and 10 deletions

View file

@ -1,14 +1,17 @@
@[reducible] def Map : Type := RBMap Nat Bool (fun a b => a < b)
import Lean.Data.RBMap
def mkMapAux : Nat → Map → Map
| 0, m => m
| n+1, m => mkMapAux n (m.insert n (n % 10 = 0))
open Std
abbrev Tree : Type := RBMap Nat Bool compare
def mkMapAux : Nat → Tree → Tree
| 0, m => m
| n+1, m => mkMapAux n (m.insert n (n % 10 = 0))
def mkMap (n : Nat) :=
mkMapAux n {}
mkMapAux n {}
def main (xs : List String) : IO UInt32 :=
let m := mkMap xs.head.toNat;
let v := m.fold (fun (r : Nat) (k : Nat) (v : Bool) => if v then r + 1 else r) 0;
IO.println (toString v) *>
pure 0
def main (xs : List String) : IO Unit :=
let m := mkMap xs.head!.toNat!
let v := m.fold (fun _ r v => if v then r + 1 else r) 0
IO.println (toString v)

View file

@ -136,6 +136,14 @@
cmd: ./rbmap_checkpoint.lean.out 2000000 10
build_config:
cmd: ./compile.sh rbmap_checkpoint.lean
- attributes:
description: rbmap_library
tags: [fast, suite]
run_config:
<<: *time
cmd: ./rbmap.library.lean.out 2000000
build_config:
cmd: ./compile.sh rbmap.library.lean
- attributes:
description: unionfind
tags: [fast, suite]