@@ -110,7 +110,110 @@ data Tree a = Balanced (Array (Tree a))
110110 | Unbalanced (Array (Tree a)) (Array Nat )
111111 | Leaf (Array a)
112112
113- %runElab derive " Tree" [Eq ,Ord ,Show ]
113+ -- ------------------------------------------------------------------------------
114+ -- Query (Tree)
115+ -- ------------------------------------------------------------------------------
116+
117+ ||| Is the tree empty? O(1)
118+ private
119+ null : Tree a
120+ -> Bool
121+ null (Balanced arr) =
122+ null arr
123+ null (Unbalanced arr _ ) =
124+ null arr
125+ null (Leaf arr) =
126+ null arr
127+
128+ -- ------------------------------------------------------------------------------
129+ -- Folds (Tree)
130+ -- ------------------------------------------------------------------------------
131+
132+ private
133+ foldl : (b -> a -> b)
134+ -> b
135+ -> Tree a
136+ -> b
137+ foldl f acc tree =
138+ foldlTree acc tree
139+ where
140+ foldlTree : b
141+ -> Tree a
142+ -> b
143+ foldlTree acc' (Balanced arr) =
144+ assert_total $ foldl foldlTree acc' arr
145+ foldlTree acc' (Unbalanced arr _ ) =
146+ assert_total $ foldl foldlTree acc' arr
147+ foldlTree acc' (Leaf arr) =
148+ assert_total $ foldl f acc' arr
149+
150+ private
151+ foldr : (a -> b -> b)
152+ -> b
153+ -> Tree a
154+ -> b
155+ foldr f acc tree =
156+ foldrTree tree acc
157+ where
158+ foldrTree : Tree a
159+ -> b
160+ -> b
161+ foldrTree (Balanced arr) acc' =
162+ assert_total $ foldr foldrTree acc' arr
163+ foldrTree (Unbalanced arr _ ) acc' =
164+ assert_total $ foldr foldrTree acc' arr
165+ foldrTree (Leaf arr) acc' =
166+ assert_total $ foldr f acc' arr
167+
168+ -- ------------------------------------------------------------------------------
169+ -- Creating Lists from Trees
170+ -- ------------------------------------------------------------------------------
171+
172+ export
173+ toList : Tree a
174+ -> List a
175+ toList (Balanced arr) =
176+ assert_total $ concat (map toList (toList arr))
177+ toList (Unbalanced arr _ ) =
178+ assert_total $ concat (map toList (toList arr))
179+ toList (Leaf arr) =
180+ toList arr
181+
182+ -- ------------------------------------------------------------------------------
183+ -- Interfaces (Tree)
184+ -- ------------------------------------------------------------------------------
185+
186+ public export
187+ Show a => Show (Tree a) where
188+ show (Balanced arr) =
189+ assert_total $ " Balanced " ++ show arr
190+ show (Unbalanced arr _ ) =
191+ assert_total $ " Unbalanced " ++ show arr
192+ show (Leaf arr) =
193+ " Leaf " ++ show arr
194+
195+ public export
196+ Foldable Tree where
197+ foldl f z = Data . RRBVector . Unsized . Internal . foldl f z
198+ foldr f z = Data . RRBVector . Unsized . Internal . foldr f z
199+ toList = Data . RRBVector . Unsized . Internal . toList
200+ null = Data . RRBVector . Unsized . Internal . null
201+
202+ public export
203+ Eq a => Eq (Tree a) where
204+ (Balanced arr1) == (Balanced arr2) =
205+ assert_total $ arr1 == arr2
206+ (Unbalanced arr1 _ ) == (Unbalanced arr2 _ ) =
207+ assert_total $ arr1 == arr2
208+ (Leaf arr1) == (Leaf arr2) =
209+ arr1 == arr2
210+ _ == _ =
211+ False
212+
213+ public export
214+ Ord a => Ord (Tree a) where
215+ compare tree1 tree2 =
216+ compare (Data . RRBVector . Unsized . Internal . toList tree1) (Data . RRBVector . Unsized . Internal . toList tree2)
114217
115218-- ------------------------------------------------------------------------------
116219-- Show Utilities (Tree)
0 commit comments