chore(tests/bench/rbmap_checkpoint): use myLean

tests/bench/rbmap_checkpoint.lean

@@ -74,6 +74,11 @@ def mkMapAux (freq : Nat) : Nat → Tree → List Tree → List Tree
 def mkMap (n : Nat) (freq : Nat) : List Tree :=
 mkMapAux freq n Leaf []
 
+def myLen : List Tree → Nat → Nat
+| (Node _ _ _ _ _ :: xs) r := myLen xs (r + 1)
+| (_ :: xs) r := myLen xs r
+| [] r := r
+
 def main (xs : List String) : IO UInt32 :=
 do
 [n, freq] ← pure xs | throw "invalid input",
@@ -82,5 +87,5 @@ let freq  := freq.toNat,
 let freq  := if freq == 0 then 1 else freq,
 let mList := mkMap n freq,
 let v     := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0,
-IO.println (toString mList.length ++ " " ++ toString v) *>
+IO.println (toString (myLen mList 0) ++ " " ++ toString v) *>
 pure 0

tests/bench/rbmap_checkpoint.sml

@@ -64,11 +64,19 @@ else let val n = n-1
 
 fun mk_map n freq = mk_map_aux freq n Leaf [];;
 
+fun mylen m r =
+case m of
+  [] => r
+| (x::xs) =>
+  case x of
+    Node _ => mylen xs (r + 1)
+  | _ => mylen xs r;;
+
 fun main n freq =
 let
   val m = mk_map n freq
   val v = fold (fn k => fn v => fn r => if v then r + 1 else r) (List.hd m) 0 in
-print (Int.toString (List.length m) ^ " " ^ Int.toString v)
+print (Int.toString (mylen m 0) ^ " " ^ Int.toString v)
 end
 
 val l = List.map (valOf o Int.fromString) (CommandLine.arguments ())