0 | module Data.SortedMap.Dependent
  1 |
  2 | import Data.DPair
  3 |
  4 | import Decidable.Equality
  5 |
  6 | -- TODO: write split
  7 |
  8 | -------------------------------
  9 | --- Internal representation ---
 10 | -------------------------------
 11 |
 12 | private
 13 | data Tree : Nat -> (k : Type) -> (v : k -> Type) -> Ord k -> Type where
 14 |   Leaf : (x : k) -> v x -> Tree Z k v o
 15 |   Branch2 : Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o
 16 |   Branch3 : Tree n k v o -> k -> Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o
 17 |
 18 | branch4 :
 19 |   Tree n k v o -> k ->
 20 |   Tree n k v o -> k ->
 21 |   Tree n k v o -> k ->
 22 |   Tree n k v o ->
 23 |   Tree (S (S n)) k v o
 24 | branch4 a b c d e f g =
 25 |   Branch2 (Branch2 a b c) d (Branch2 e f g)
 26 |
 27 | branch5 :
 28 |   Tree n k v o -> k ->
 29 |   Tree n k v o -> k ->
 30 |   Tree n k v o -> k ->
 31 |   Tree n k v o -> k ->
 32 |   Tree n k v o ->
 33 |   Tree (S (S n)) k v o
 34 | branch5 a b c d e f g h i =
 35 |   Branch2 (Branch2 a b c) d (Branch3 e f g h i)
 36 |
 37 | branch6 :
 38 |   Tree n k v o -> k ->
 39 |   Tree n k v o -> k ->
 40 |   Tree n k v o -> k ->
 41 |   Tree n k v o -> k ->
 42 |   Tree n k v o -> k ->
 43 |   Tree n k v o ->
 44 |   Tree (S (S n)) k v o
 45 | branch6 a b c d e f g h i j k =
 46 |   Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)
 47 |
 48 | branch7 :
 49 |   Tree n k v o -> k ->
 50 |   Tree n k v o -> k ->
 51 |   Tree n k v o -> k ->
 52 |   Tree n k v o -> k ->
 53 |   Tree n k v o -> k ->
 54 |   Tree n k v o -> k ->
 55 |   Tree n k v o ->
 56 |   Tree (S (S n)) k v o
 57 | branch7 a b c d e f g h i j k l m =
 58 |   Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)
 59 |
 60 | merge1 : Tree n k v o -> k -> Tree (S n) k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v o
 61 | merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
 62 | merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
 63 | merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k
 64 | merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m
 65 |
 66 | merge2 : Tree (S n) k v o -> k -> Tree n k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v o
 67 | merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
 68 | merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
 69 | merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k
 70 | merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m
 71 |
 72 | merge3 : Tree (S n) k v o -> k -> Tree (S n) k v o -> k -> Tree n k v o -> Tree (S (S n)) k v o
 73 | merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
 74 | merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k
 75 | merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k
 76 | merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m
 77 |
 78 | treeLookup : Ord k => (x : k) -> Tree n k v o -> Maybe (y : k ** v y) -- may also return an erased `So (x == y)`
 79 | treeLookup k (Leaf k' v) =
 80 |   if k == k' then
 81 |     Just (k' ** v)
 82 |   else
 83 |     Nothing
 84 | treeLookup k (Branch2 t1 k' t2) =
 85 |   if k <= k' then
 86 |     treeLookup k t1
 87 |   else
 88 |     treeLookup k t2
 89 | treeLookup k (Branch3 t1 k1 t2 k2 t3) =
 90 |   if k <= k1 then
 91 |     treeLookup k t1
 92 |   else if k <= k2 then
 93 |     treeLookup k t2
 94 |   else
 95 |     treeLookup k t3
 96 |
 97 | treeInsert' : Ord k => (x : k) -> v x -> Tree n k v o -> Either (Tree n k v o) (Tree n k v o, k, Tree n k v o)
 98 | treeInsert' k v (Leaf k' v') =
 99 |   case compare k k' of
100 |     LT => Right (Leaf k v, k, Leaf k' v')
101 |     EQ => Left (Leaf k v)
102 |     GT => Right (Leaf k' v', k', Leaf k v)
103 | treeInsert' k v (Branch2 t1 k' t2) =
104 |   if k <= k' then
105 |     case treeInsert' k v t1 of
106 |       Left t1' => Left (Branch2 t1' k' t2)
107 |       Right (a, b, c) => Left (Branch3 a b c k' t2)
108 |   else
109 |     case treeInsert' k v t2 of
110 |       Left t2' => Left (Branch2 t1 k' t2')
111 |       Right (a, b, c) => Left (Branch3 t1 k' a b c)
112 | treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
113 |   if k <= k1 then
114 |     case treeInsert' k v t1 of
115 |       Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
116 |       Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3)
117 |   else
118 |     if k <= k2 then
119 |       case treeInsert' k v t2 of
120 |         Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
121 |         Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3)
122 |     else
123 |       case treeInsert' k v t3 of
124 |         Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
125 |         Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)
126 |
127 | treeInsert : Ord k => (x : k) -> v x -> Tree n k v o -> Either (Tree n k v o) (Tree (S n) k v o)
128 | treeInsert k v t =
129 |   case treeInsert' k v t of
130 |     Left t' => Left t'
131 |     Right (a, b, c) => Right (Branch2 a b c)
132 |
133 | delType : Nat -> (k : Type) -> (v : k -> Type) -> Ord k -> Type
134 | delType Z k v o = ()
135 | delType (S n) k v o = Tree n k v o
136 |
137 | treeDelete : Ord k => (n : Nat) -> k -> Tree n k v o -> Either (Tree n k v o) (delType n k v o)
138 | treeDelete _ k (Leaf k' v) =
139 |   if k == k' then
140 |     Right ()
141 |   else
142 |     Left (Leaf k' v)
143 | treeDelete (S Z) k (Branch2 t1 k' t2) =
144 |   if k <= k' then
145 |     case treeDelete Z k t1 of
146 |       Left t1' => Left (Branch2 t1' k' t2)
147 |       Right () => Right t2
148 |   else
149 |     case treeDelete Z k t2 of
150 |       Left t2' => Left (Branch2 t1 k' t2')
151 |       Right () => Right t1
152 | treeDelete (S Z) k (Branch3 t1 k1 t2 k2 t3) =
153 |   if k <= k1 then
154 |     case treeDelete Z k t1 of
155 |       Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
156 |       Right () => Left (Branch2 t2 k2 t3)
157 |   else if k <= k2 then
158 |     case treeDelete Z k t2 of
159 |       Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
160 |       Right () => Left (Branch2 t1 k1 t3)
161 |   else
162 |     case treeDelete Z k t3 of
163 |       Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
164 |       Right () => Left (Branch2 t1 k1 t2)
165 | treeDelete (S (S n)) k (Branch2 t1 k' t2) =
166 |   if k <= k' then
167 |     case treeDelete (S n) k t1 of
168 |       Left t1' => Left (Branch2 t1' k' t2)
169 |       Right t1' =>
170 |         case t2 of
171 |           Branch2 a b c => Right (Branch3 t1' k' a b c)
172 |           Branch3 a b c d e => Left (branch4 t1' k' a b c d e)
173 |   else
174 |     case treeDelete (S n) k t2 of
175 |       Left t2' => Left (Branch2 t1 k' t2')
176 |       Right t2' =>
177 |         case t1 of
178 |           Branch2 a b c => Right (Branch3 a b c k' t2')
179 |           Branch3 a b c d e => Left (branch4 a b c d e k' t2')
180 | treeDelete (S (S n)) k (Branch3 t1 k1 t2 k2 t3) =
181 |   if k <= k1 then
182 |     case treeDelete (S n) k t1 of
183 |       Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
184 |       Right t1' => Left (merge1 t1' k1 t2 k2 t3)
185 |   else if k <= k2 then
186 |     case treeDelete (S n) k t2 of
187 |       Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
188 |       Right t2' => Left (merge2 t1 k1 t2' k2 t3)
189 |   else
190 |     case treeDelete (S n) k t3 of
191 |       Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
192 |       Right t3' => Left (merge3 t1 k1 t2 k2 t3')
193 |
194 | treeToList : Tree n k v o -> List (x : k ** v x)
195 | treeToList = treeToList' (:: [])
196 |   where
197 |     -- explicit quantification to avoid conflation with {n} from treeToList
198 |     treeToList' : {0 n : Nat} -> ((x : k ** v x) -> List (x : k ** v x)) -> Tree n k v o -> List (x : k ** v x)
199 |     treeToList' cont (Leaf k v) = cont (k ** v)
200 |     treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
201 |     treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
202 |
203 | ----------------------
204 | --- User interface ---
205 | ----------------------
206 |
207 | export
208 | data SortedDMap : (k : Type) -> (v : k -> Type) -> Type where
209 |   Empty : Ord k => SortedDMap k v
210 |   M : (o : Ord k) => (n : Nat) -> Tree n k v o -> SortedDMap k v
211 |
212 | export
213 | empty : Ord k => SortedDMap k v
214 | empty = Empty
215 |
216 | export
217 | lookup : (x : k) -> SortedDMap k v -> Maybe (y : k ** v y) -- could return also `So (x == y)`
218 | lookup _ Empty = Nothing
219 | lookup k (M _ t) = treeLookup k t
220 |
221 | public export %inline
222 | lookup' : SortedDMap k v -> (x : k) -> Maybe (y : k ** v y)
223 | lookup' = flip lookup
224 |
225 | export
226 | lookupPrecise : DecEq k => (x : k) -> SortedDMap k v -> Maybe (v x)
227 | lookupPrecise x = lookup x >=> \(y ** v) =>
228 |   case decEq x y of
229 |     Yes Refl => Just v
230 |     No _     => Nothing
231 |
232 | public export %inline
233 | lookupPrecise' : DecEq k => SortedDMap k v -> (x : k) -> Maybe (v x)
234 | lookupPrecise' m x = lookupPrecise x m
235 |
236 | export
237 | insert : (x : k) -> v x -> SortedDMap k v -> SortedDMap k v
238 | insert k v Empty = M Z (Leaf k v)
239 | insert k v (M _ t) =
240 |   case treeInsert k v t of
241 |     Left t' => (M _ t')
242 |     Right t' => (M _ t')
243 |
244 | public export %inline
245 | insert' : SortedDMap k v -> (x : k ** v x) -> SortedDMap k v
246 | insert' m (x ** v) = insert x v m
247 |
248 | export
249 | singleton : Ord k => (x : k) -> v x -> SortedDMap k v
250 | singleton k v = insert k v empty
251 |
252 | export
253 | insertFrom : Foldable f => f (x : k ** v x) -> SortedDMap k v -> SortedDMap k v
254 | insertFrom = flip $ foldl insert'
255 |
256 | public export %inline
257 | insertFrom' : Foldable f => SortedDMap k v -> f (x : k ** v x) -> SortedDMap k v
258 | insertFrom' = flip insertFrom
259 |
260 | export
261 | delete : k -> SortedDMap k v -> SortedDMap k v
262 | delete _ Empty = Empty
263 | delete k (M Z t) =
264 |   case treeDelete Z k t of
265 |     Left t' => (M _ t')
266 |     Right () => Empty
267 | delete k (M (S n) t) =
268 |   case treeDelete (S n) k t of
269 |     Left t' => (M _ t')
270 |     Right t' => (M _ t')
271 |
272 | public export %inline
273 | delete' : SortedDMap k v -> k -> SortedDMap k v
274 | delete' = flip delete
275 |
276 | ||| Updates or deletes a value based on the decision function
277 | |||
278 | ||| The decision function takes information about the presence of the value,
279 | ||| and the value itself, if it is present.
280 | ||| It returns a new value or the fact that there should be no value as the result.
281 | |||
282 | ||| The current implementation performs up to two traversals of the original map
283 | export
284 | update : DecEq k => (x : k) -> (Maybe (v x) -> Maybe (v x)) -> SortedDMap k v -> SortedDMap k v
285 | update k f m = case f $ lookupPrecise k m of
286 |   Just v  => insert k v m
287 |   Nothing => delete k m
288 |
289 | public export %inline
290 | update' : DecEq k => SortedDMap k v -> (x : k ** Maybe (v x) -> Maybe (v x)) -> SortedDMap k v
291 | update' m (x ** f) = update x f m
292 |
293 | ||| Updates existing value, if it is present, and does nothing otherwise
294 | |||
295 | ||| The current implementation performs up to two traversals of the original map
296 | export
297 | updateExisting : DecEq k => (x : k) -> (v x -> v x) -> SortedDMap k v -> SortedDMap k v
298 | updateExisting k f m = case lookupPrecise k m of
299 |   Just v  => insert k (f v) m
300 |   Nothing => m
301 |
302 | public export %inline
303 | updateExisting' : DecEq k => SortedDMap k v -> (x : k ** v x -> v x) -> SortedDMap k v
304 | updateExisting' m (x ** f) = updateExisting x f m
305 |
306 | export
307 | fromList : Ord k => List (x : k ** v x) -> SortedDMap k v
308 | fromList = foldl insert' empty
309 |
310 | export
311 | toList : SortedDMap k v -> List (x : k ** v x)
312 | toList Empty = []
313 | toList (M _ t) = treeToList t
314 |
315 | ||| Returns a list of key-value pairs stored in this map
316 | public export %inline
317 | kvList : SortedDMap k v -> List (x : k ** v x)
318 | kvList = toList
319 |
320 | ||| Gets the keys of the map.
321 | export
322 | keys : SortedDMap k v -> List k
323 | keys = map fst . kvList
324 |
325 | export
326 | values : SortedDMap k v -> List (x : k ** v x)
327 | values = kvList
328 |
329 | treeMap : ({x : k} -> a x -> b x) -> Tree n k a o -> Tree n k b o
330 | treeMap f (Leaf k v) = Leaf k (f v)
331 | treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
332 | treeMap f (Branch3 t1 k1 t2 k2 t3)
333 |     = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)
334 |
335 | treeTraverse : Applicative f => ({x : k} -> a x -> f (b x)) -> Tree n k a o -> f (Tree n k b o)
336 | treeTraverse f (Leaf k v) = Leaf k <$> f v
337 | treeTraverse f (Branch2 t1 k t2) =
338 |   Branch2
339 |     <$> treeTraverse f t1
340 |     <*> pure k
341 |     <*> treeTraverse f t2
342 | treeTraverse f (Branch3 t1 k1 t2 k2 t3) =
343 |   Branch3
344 |     <$> treeTraverse f t1
345 |     <*> pure k1
346 |     <*> treeTraverse f t2
347 |     <*> pure k2
348 |     <*> treeTraverse f t3
349 |
350 | export
351 | map : ({x : k} -> v x -> w x) -> SortedDMap k v -> SortedDMap k w
352 | map _ Empty = Empty
353 | map f (M _ t) = M _ $ treeMap f t
354 |
355 | export
356 | foldl : (acc -> (x : k ** v x) -> acc) -> acc -> SortedDMap k v -> acc
357 | foldl f i = foldl f i . values
358 |
359 | export
360 | foldr : ((x : k ** v x) -> acc -> acc) -> acc -> SortedDMap k v -> acc
361 | foldr f i = foldr f i . values
362 |
363 | export
364 | foldlM : Monad m => (acc -> (x : k ** v x) -> m acc) -> acc -> SortedDMap k v -> m acc
365 | foldlM f i = foldl (\ma, b => ma >>= flip f b) (pure i)
366 |
367 | export
368 | foldMap : Monoid m => (f : (x : k) -> v x -> m) -> SortedDMap k v -> m
369 | foldMap f = foldr ((<+>) . uncurry f) neutral
370 |
371 | export
372 | null : SortedDMap k v -> Bool
373 | null Empty   = True
374 | null (M _ _) = False
375 |
376 | export
377 | traverse : Applicative f => ({x : k} -> v x -> f (w x)) -> SortedDMap k v -> f (SortedDMap k w)
378 | traverse _ Empty = pure Empty
379 | traverse f (M _ t) = M _ <$> treeTraverse f t
380 |
381 | public export %inline
382 | for : Applicative f => SortedDMap k v -> ({x : k} -> v x -> f (w x)) -> f (SortedDMap k w)
383 | for = flip traverse
384 |
385 | ||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
386 | ||| Uses the ordering of the first map given.
387 | export
388 | mergeWith : DecEq k => ({x : k} -> v x -> v x -> v x) -> SortedDMap k v -> SortedDMap k v -> SortedDMap k v
389 | mergeWith f x y = insertFrom inserted x where
390 |   inserted : List (x : k ** v x)
391 |   inserted = do
392 |     (k ** v) <- kvList y
393 |     let v' = (maybe id f $ lookupPrecise k x) v
394 |     pure (k ** v')
395 |
396 | ||| Merge two maps using the Semigroup (and by extension, Monoid) operation.
397 | ||| Uses mergeWith internally, so the ordering of the left map is kept.
398 | export
399 | merge : DecEq k => ({x : k} -> Semigroup (v x)) => SortedDMap k v -> SortedDMap k v -> SortedDMap k v
400 | merge = mergeWith (<+>)
401 |
402 | ||| Left-biased merge, also keeps the ordering specified  by the left map.
403 | export
404 | mergeLeft : DecEq k => SortedDMap k v -> SortedDMap k v -> SortedDMap k v
405 | mergeLeft = mergeWith const
406 |
407 | treeLeftMost : Tree n k v o -> (x : k ** v x)
408 | treeLeftMost (Leaf x y) = (x ** y)
409 | treeLeftMost (Branch2 x _ _) = treeLeftMost x
410 | treeLeftMost (Branch3 x _ _ _ _) = treeLeftMost x
411 |
412 | treeRightMost : Tree n k v o -> (x : k ** v x)
413 | treeRightMost (Leaf x y) = (x ** y)
414 | treeRightMost (Branch2 _ _ x) = treeRightMost x
415 | treeRightMost (Branch3 _ _ _ _ x) = treeRightMost x
416 |
417 | treeLookupBetween : Ord k => k -> Tree n k v o -> (Maybe (x : k ** v x), Maybe (x : k ** v x))
418 | treeLookupBetween k (Leaf k' v) with (k < k')
419 |   treeLookupBetween k (Leaf k' v) | True = (Nothing, Just (k' ** v))
420 |   treeLookupBetween k (Leaf k' v) | False = (Just (k' ** v), Nothing)
421 | treeLookupBetween k (Branch2 t1 k' t2) with (k < k')
422 |   treeLookupBetween k (Branch2 t1 k' t2) | True = -- k < k'
423 |     let (lower, upper) = treeLookupBetween k t1 in
424 |     (lower, upper <|> pure (treeLeftMost t2))
425 |   treeLookupBetween k (Branch2 t1 k' t2) | False = -- k >= k'
426 |     let (lower, upper) = treeLookupBetween k t2 in
427 |     (lower <|> pure (treeRightMost t1), upper)
428 | treeLookupBetween k (Branch3 t1 k1 t2 k2 t3) with (k < k1)
429 |   treeLookupBetween k (Branch3 t1 k1 t2 k2 t3) | True = treeLookupBetween k (Branch2 t1 k1 t2)
430 |   treeLookupBetween k (Branch3 t1 k1 t2 k2 t3) | False with (k < k2)
431 |     treeLookupBetween k (Branch3 t1 k1 t2 k2 t3) | False | False = treeLookupBetween k (Branch2 t2 k2 t3)
432 |     treeLookupBetween k (Branch3 t1 k1 t2 k2 t3) | False | True = --k1 <= k < k2
433 |       let (lower, upper) = treeLookupBetween k (Branch2 t1 k1 t2) in
434 |       (lower, upper <|> pure (treeLeftMost t3))
435 |
436 | ||| looks up a key in map, returning the left and right closest values, so that
437 | |||  k1 <= k < k2. If at the end of the beginning and/or end of the sorted map, returns
438 | ||| nothing appropriately
439 | export
440 | lookupBetween : k -> SortedDMap k v -> (Maybe (x : k ** v x), Maybe (x : k ** v x))
441 | lookupBetween k Empty = (Nothing, Nothing)
442 | lookupBetween k (M _ t) = treeLookupBetween k t
443 |
444 |
445 | ||| Returns the leftmost (least) key and value
446 | export
447 | leftMost : SortedDMap k v -> Maybe (x : k ** v x)
448 | leftMost Empty = Nothing
449 | leftMost (M _ t) = Just $ treeLeftMost t
450 |
451 |
452 | ||| Returns the rightmost (greatest) key and value
453 | export
454 | rightMost : SortedDMap k v -> Maybe (x : k ** v x)
455 | rightMost Empty = Nothing
456 | rightMost (M _ t) = Just $ treeRightMost t
457 |
458 | ||| Pops the leftmost key and corresponding value from the map
459 | export
460 | pop : SortedDMap k v -> Maybe ((x : k ** v x), SortedDMap k v)
461 | pop m = do
462 |   kv@(k ** _) <- leftMost m
463 |   pure (kv, delete k m)
464 |
465 | export
466 | (Show k, {x : k} -> Show (v x)) => Show (SortedDMap k v) where
467 |    show m = "fromList " ++ (show $ kvList m)
468 |
469 | export
470 | (DecEq k, {x : k} -> Eq (v x)) => Eq (SortedDMap k v) where
471 |   (==) = (==) `on` kvList
472 |
473 | export
474 | strictSubmap : DecEq k => ({x : k} -> Eq (v x)) => (sub : SortedDMap k v) -> (sup : SortedDMap k v) -> Bool
475 | strictSubmap sub sup = all (\(k ** v) => Just v == lookupPrecise k sup) $ kvList sub
476 |
477 | -- TODO: is this the right variant of merge to use for this? I think it is, but
478 | -- I could also see the advantages of using `mergeLeft`. The current approach is
479 | -- strictly more powerful I believe, because `mergeLeft` can be emulated with
480 | -- the `First` monoid. However, this does require more code to do the same
481 | -- thing.
482 | export
483 | DecEq k => ({x : k} -> Semigroup (v x)) => Semigroup (SortedDMap k v) where
484 |   (<+>) = merge
485 |
486 | ||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.
487 | ||| However, semantically, it should be equal.
488 | export
489 | DecEq k => Ord k => ({x : k} -> Semigroup (v x)) => Monoid (SortedDMap k v) where
490 |   neutral = empty
491 |