From e954ed12bc8ead2944da007cbe3227c6fa1ca67c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 May 2019 07:29:38 -0700
Subject: [PATCH] chore(tests/bench/rbmap_checkpoint): use `myLean`

---
 tests/bench/rbmap_checkpoint.lean |  7 ++++++-
 tests/bench/rbmap_checkpoint.sml  | 10 +++++++++-
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/tests/bench/rbmap_checkpoint.lean b/tests/bench/rbmap_checkpoint.lean
index c06e42a1e0..5365678e46 100644
--- a/tests/bench/rbmap_checkpoint.lean
+++ b/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
diff --git a/tests/bench/rbmap_checkpoint.sml b/tests/bench/rbmap_checkpoint.sml
index 7fe05e0833..050cd1fc02 100644
--- a/tests/bench/rbmap_checkpoint.sml
+++ b/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 ())