5db219aae5
@kha The Lean rbmap is 3x slower than the C++ rb_map. I tried two different implementations: rbmap2 (Appel's Coq implementation), and rbmap3 (tries to simulate the C++ version). I believe rbmap3 is broken since it is too slow. I have also identified missing reset/reuse opportunities. The actual implementation misses a case the simple code at reuse.txt gets :( rbmap3 also exposes the "TODO(Leo): improve this" at library/compiler/reduce_arity.cpp
14 lines
414 B
Text
14 lines
414 B
Text
@[reducible] def map : Type := rbmap nat bool (<)
|
|
|
|
def mk_map_aux : nat → map → map
|
|
| 0 m := m
|
|
| (n+1) m := mk_map_aux n (m.insert n (n % 10 = 0))
|
|
|
|
def mk_map (n : nat) :=
|
|
mk_map_aux n (mk_rbmap nat bool (<))
|
|
|
|
def main (xs : list string) : io uint32 :=
|
|
let m := mk_map xs.head.to_nat in
|
|
let v := rbmap.fold (λ (k : nat) (v : bool) (r : nat), if v then r + k else r) m 0 in
|
|
io.println' (to_string v) *>
|
|
pure 0
|