@@ -183,11 +183,13 @@ treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =
183183 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
184184 Right t3' => Left (merge3 t1 k1 t2 k2 t3')
185185
186−-- FIXME: this is very inefficient
187186treeToList : Ord k => Tree n k v -> List (k, v)
188−treeToList (Leaf k v) = [(k, v)]
189−treeToList (Branch2 t1 _ t2) = treeToList t1 ++ treeToList t2
190−treeToList (Branch3 t1 _ t2 _ t3) = treeToList t1 ++ treeToList t2 ++ treeToList t3
187+treeToList = treeToList' (:: [])
188+ where
189+ treeToList' : Ord k => ((k, v) -> List (k, v)) -> Tree n k v -> List (k, v)
190+ treeToList' cont (Leaf k v) = cont (k, v)
191+ treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
192+ treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
191193
192194data SortedMap : Type -> Type -> Type where
193195 Empty : SortedMap k v