
   0 | module Data.AssocList
   1 | 
   2 | import Data.DPair
   3 | import Data.Prim.Bits32
   4 | import Data.Maybe.Upper
   5 | 
   6 | %default total
   7 | 
   8 | public export
   9 | 0 Key : Type
  10 | Key = Bits32
  11 | 
  12 | public export
  13 | 0 (<): Maybe Key -> Maybe Key -> Type
  14 | (<) = Upper (<)
  15 | 
  16 | public export
  17 | 0 (<=): Maybe Key -> Maybe Key -> Type
  18 | (<=) = ReflexiveClosure (<)
  19 | 
  20 | ||| A provably sorted assoc list with `Bits64` as the key type.
  21 | |||
  22 | ||| This is mainly useful for short sequences of key / value pairs.
  23 | ||| It comes with O(n) runtime complexity for `insert`, `update`,
  24 | ||| `lookup` and `delete`, but also with fast O(n) complexity for
  25 | ||| `union` and `intersection`.
  26 | public export
  27 | data AL : (ix : Maybe Key) -> Type -> Type where
  28 |   Nil : AL Nothing a
  29 |   (::) :  {0 ix : _}
  30 |        -> (p     : (Key,a))
  31 |        -> (ps    : AL ix a)
  32 |        -> (0 prf : Just (fst p) < ix)
  33 |        => AL (Just $ fst p) a
  34 | 
  35 | public export
  36 | Functor (AL ix) where
  37 |   map f []       = []
  38 |   map f ((k,v) :: t) = (k,f v) :: map f t
  39 | 
  40 | public export
  41 | foldlKV_ : (acc -> (Key,el) -> acc) -> acc -> AL m el -> acc
  42 | foldlKV_ f x (p :: ps) = foldlKV_ f (f x p) ps
  43 | foldlKV_ _ x []        = x
  44 | 
  45 | public export
  46 | traverseKV_ : Applicative f => ((Key,a) -> f b) -> AL m a -> f (AL m b)
  47 | traverseKV_ g []             = pure []
  48 | traverseKV_ g (p :: ps) =
  49 |   [| (\vb,ps' => (fst p,vb) :: ps') (g p) (traverseKV_ g ps) |]
  50 | 
  51 | 
  52 | public export
  53 | Foldable (AL ix) where
  54 |   foldr c n [] = n
  55 |   foldr c n (x::xs) = c (snd x) (foldr c n xs)
  56 | 
  57 |   foldl f q [] = q
  58 |   foldl f q (x::xs) = foldl f (f q $ snd x) xs
  59 | 
  60 |   null [] = True
  61 |   null (_::_) = False
  62 | 
  63 |   foldMap f = foldl (\acc, elem => acc <+> f elem) neutral
  64 | 
  65 | public export
  66 | Traversable (AL ix) where
  67 |   traverse f [] = pure []
  68 |   traverse f (p :: ps) =
  69 |     (\v,qs => (fst p,v) :: qs) <$> f (snd p) <*> traverse f ps
  70 | 
  71 | ||| Lookup a key in an assoc list.
  72 | public export
  73 | lookup_ : (k : Key) -> AL ix a -> Maybe a
  74 | lookup_ k (p :: ps) = case comp k (fst p) of
  75 |   LT _ _ _ => Nothing
  76 |   EQ _ _ _ => Just $ snd p
  77 |   GT _ _ _ => lookup_ k ps
  78 | lookup_ _ []        = Nothing
  79 | 
  80 | public export
  81 | nonEmpty_ : AL m a -> Bool
  82 | nonEmpty_ (p :: ps) = True
  83 | nonEmpty_ []        = False
  84 | 
  85 | public export
  86 | isEmpty_ : AL m a -> Bool
  87 | isEmpty_ (p :: ps) = False
  88 | isEmpty_ []        = True
  89 | 
  90 | ||| Extracts the key / value pairs from the assoc list.
  91 | public export
  92 | pairs_ : AL ix a -> List (Key,a)
  93 | pairs_ (p :: ps) = p :: pairs_ ps
  94 | pairs_ []        = []
  95 | 
  96 | ||| Extracts the keys from the assoc list.
  97 | public export
  98 | keys_ : AL ix a -> List Key
  99 | keys_ (p :: ps) = fst p :: keys_ ps
 100 | keys_ []        = []
 101 | 
 102 | ||| Extracts the values from the assoc list.
 103 | public export
 104 | values_ : AL ix a -> List a
 105 | values_ (p :: ps) = snd p :: values_ ps
 106 | values_ []        = []
 107 | 
 108 | public export
 109 | length_ : AL ix a -> Nat
 110 | length_ (p :: ps) = S $ length_ ps
 111 | length_ []        = 0
 112 | 
 113 | ||| Heterogeneous equality check.
 114 | public export
 115 | heq : Eq a => AL m a -> AL n a -> Bool
 116 | heq (p :: ps) (q :: qs) = p == q && heq ps qs
 117 | heq [] [] = True
 118 | heq _ _   = False
 119 | 
 120 | public export %inline
 121 | Eq a => Eq (AL m a) where
 122 |   (==) = heq
 123 | 
 124 | export %inline
 125 | Show a => Show (AL m a) where
 126 |   showPrec p m = showPrec p (pairs_ m)
 127 | 
 128 | --------------------------------------------------------------------------------
 129 | --          Insert
 130 | --------------------------------------------------------------------------------
 131 | 
 132 | ||| Inserting a new key / value pair leads to a new assoc list where the
 133 | ||| key at the head is either equal to the new key or the one previously
 134 | ||| at the head.
 135 | |||
 136 | ||| @ k  New key that was inserted
 137 | ||| @ mk Key index of the original assoc list
 138 | public export
 139 | record InsertRes (k : Key) (mk : Maybe Key) (a : Type) where
 140 |   constructor IR
 141 |   {0 firstKey : Key}
 142 |   pairs : AL (Just firstKey) a
 143 |   0 prf : Either (firstKey === k) (Just firstKey === mk)
 144 | 
 145 | 0 prependLemma :
 146 |      {x,y,k : Key}
 147 |   -> {mk : Maybe Key}
 148 |   -> Either (x === k) (Just x === mk)
 149 |   -> {auto 0 ltyk : Just y < Just k}
 150 |   -> {auto 0 ltym : Just y < mk}
 151 |   -> Just y < Just x
 152 | prependLemma (Left Refl) = ltyk
 153 | prependLemma (Right z)   = rewrite z in ltym
 154 | 
 155 | %inline
 156 | prepend :
 157 |      (p : (Key,a))
 158 |   -> InsertRes k mk a
 159 |   -> {auto 0 lt : Just (fst p) < Just k}
 160 |   -> {auto 0 sm : Just (fst p) < mk}
 161 |   -> InsertRes k (Just $ fst p) a
 162 | prepend p (IR ps prf1) =
 163 |   let 0 prf := prependLemma prf1
 164 |    in IR (p :: ps) (Right Refl)
 165 | 
 166 | ||| Inserts a new key / value pair into an assoc list.
 167 | ||| The result type reflects the possibilities with regard
 168 | ||| to the head pair of the new assoc list.
 169 | |||
 170 | ||| Note: If the given key `k` is already present in the assoc list,
 171 | ||| its associated value will be replaced with `v`.
 172 | public export
 173 | insert_ : (k : Key) -> (v : a) -> AL ix a -> InsertRes k ix a
 174 | insert_ k v (p :: ps) = case comp k (fst p) of
 175 |   LT prf _ _ => IR ((k,v) :: p :: ps) (Left Refl)
 176 |   EQ _ prf _ => IR ((fst p, v) :: ps) (Right Refl)
 177 |   GT _ _ prf => prepend p $ insert_  k v ps
 178 | insert_ k v []        = IR [(k,v)] (Left Refl)
 179 | 
 180 | ||| Like `insert` but in case `k` is already present in the assoc
 181 | ||| list, the `v` will be cobine with the old value via function `f`.
 182 | public export
 183 | insertWith_ :
 184 |      (f : a -> a -> a)
 185 |   -> (k : Key)
 186 |   -> (v : a)
 187 |   -> AL ix a
 188 |   -> InsertRes k ix a
 189 | insertWith_ f k v (p :: ps) = case comp k (fst p) of
 190 |   LT prf _ _ => IR ((k,v) :: p :: ps) (Left Refl)
 191 |   EQ _ prf _ => IR ((fst p, f v $ snd p) :: ps) (Right Refl)
 192 |   GT _ _ prf => prepend p $ insertWith_ f k v ps
 193 | insertWith_ _ k v []        = IR [(k,v)] (Left Refl)
 194 | 
 195 | --------------------------------------------------------------------------------
 196 | --          Delete
 197 | --------------------------------------------------------------------------------
 198 | 
 199 | ||| Deleting an entry from an assoc list results in a new assoc list
 200 | ||| the index of which is equal to or smaller than the one from
 201 | ||| the original list.
 202 | |||
 203 | ||| @ m1 : Key index of the original assoc list.
 204 | public export
 205 | record DeleteRes (m1 : Maybe Key) (a : Type) where
 206 |   constructor DR
 207 |   {0 mx : Maybe Key}
 208 |   pairs : AL mx a
 209 |   0 prf : m1 <= mx
 210 | 
 211 | export %inline
 212 | prependDR :
 213 |      (p : (Key,a))
 214 |   -> DeleteRes m a
 215 |   -> {auto 0 lt : Just (fst p) < m}
 216 |   -> DeleteRes (Just $ fst p) a
 217 | prependDR p (DR ps lte) =
 218 |   let 0 lt = strictLeft lt lte
 219 |    in DR (p :: ps) Refl
 220 | 
 221 | ||| Tries to remove the entry with the given key from the
 222 | ||| assoc list. The key index of the result will be equal to
 223 | ||| or greater than `m`.
 224 | export
 225 | delete_ : (k : Key) -> AL m a -> DeleteRes m a
 226 | delete_ k (p :: ps) = case comp k (fst p) of
 227 |   LT _ _ _ => DR (p :: ps) %search
 228 |   EQ _ _ _ => DR ps %search
 229 |   GT _ _ _ => prependDR p $ delete_ k ps
 230 | delete_ k []        = DR [] %search
 231 | 
 232 | ||| Applies the given function to all values, keeping only the
 233 | ||| `Just` results.
 234 | export
 235 | mapMaybe_ : (a -> Maybe b) -> AL m a -> DeleteRes m b
 236 | mapMaybe_ f (p :: ps) = case f (snd p) of
 237 |   Just v  => prependDR (fst p, v) $ mapMaybe_ f ps
 238 |   Nothing =>
 239 |     let DR qs prf := mapMaybe_ f ps
 240 |      in DR qs (transitive %search prf)
 241 | mapMaybe_ f []        = DR [] %search
 242 | 
 243 | ||| Applies the given function to all key / value pairs, keeping only the
 244 | ||| `Just` results.
 245 | export
 246 | mapMaybeK_ : (Key -> a -> Maybe b) -> AL m a -> DeleteRes m b
 247 | mapMaybeK_ f ((n,va) :: ps) = case f n va of
 248 |   Just vb => prependDR (n,vb) $ mapMaybeK_ f ps
 249 |   Nothing =>
 250 |     let DR qs prf := mapMaybeK_ f ps
 251 |      in DR qs (transitive %search prf)
 252 | mapMaybeK_ f []        = DR [] %search
 253 | 
 254 | --------------------------------------------------------------------------------
 255 | --          Update
 256 | --------------------------------------------------------------------------------
 257 | 
 258 | ||| Updates the value at the given position by applying the given function.
 259 | export
 260 | update_ : (k : Key) -> (a -> a) -> AL m a -> AL m a
 261 | update_ k f (p :: ps) = case comp k (fst p) of
 262 |   LT _ _ _ => p :: ps
 263 |   EQ _ _ _ => (fst p, f $ snd p) :: ps
 264 |   GT _ _ _ => p :: update_ k f ps
 265 | update_ k f []        = []
 266 | 
 267 | ||| Updates the value at the given position by applying the given effectful
 268 | ||| computation.
 269 | export
 270 | updateA_ : Applicative f => (k : Key) -> (a -> f a) -> AL m a -> f (AL m a)
 271 | updateA_ k g (p :: ps) = case comp k (fst p) of
 272 |   LT _ _ _ => pure $ p :: ps
 273 |   EQ _ _ _ => map (\v => (fst p, v) :: ps) (g $ snd p)
 274 |   GT _ _ _ => (p ::) <$>  updateA_ k g ps
 275 | updateA_ k g []        = pure []
 276 | 
 277 | --------------------------------------------------------------------------------
 278 | --          Union
 279 | --------------------------------------------------------------------------------
 280 | 
 281 | ||| Result of computing the union of two assoc lists with
 282 | ||| key indices `m1` and `m2`. The result's key index is equal to either
 283 | ||| `m1` or `m2`
 284 | public export
 285 | record UnionRes (m1,m2 : Maybe Key) (a : Type) where
 286 |   constructor UR
 287 |   {0 mx : Maybe Key}
 288 |   pairs : AL mx a
 289 |   0 prf : Either (m1 === mx) (m2 === mx)
 290 | 
 291 | 0 trans_LT_EQ : {0 lt : _} -> Transitive a lt => lt x y -> y === z -> lt x z
 292 | trans_LT_EQ w Refl = w
 293 | 
 294 | public export %inline
 295 | prepLT :
 296 |      (p : (Key,a))
 297 |   -> UnionRes m1 (Just k2) a
 298 |   -> {auto 0 prf1 : Just (fst p) < m1}
 299 |   -> {auto 0 prf2 : Just (fst p) < Just k2}
 300 |   -> UnionRes (Just $ fst p) (Just k2) a
 301 | prepLT p (UR ps prf) =
 302 |   let 0 lt := either (trans_LT_EQ prf1) (trans_LT_EQ prf2) prf
 303 |    in UR (p :: ps) (Left Refl)
 304 | 
 305 | public export %inline
 306 | prepGT :
 307 |     (p : (Key,a))
 308 |   -> UnionRes (Just k1) m2 a
 309 |   -> {auto 0 prf1 : Just (fst p) < m2}
 310 |   -> {auto 0 prf2 : Just (fst p) < Just k1}
 311 |   -> UnionRes (Just k1) (Just $ fst p) a
 312 | prepGT p (UR ps prf) =
 313 |   let 0 lt := either (trans_LT_EQ prf2) (trans_LT_EQ prf1) prf
 314 |    in UR (p :: ps) (Right Refl)
 315 | 
 316 | public export %inline
 317 | prepEQ :
 318 |      {0 x : Maybe Key}
 319 |   -> (p : (Key,a))
 320 |   -> (0 eq  : fst p === k)
 321 |   -> UnionRes m1 m2 a
 322 |   -> {auto 0 prf1 : Just (fst p) < m1}
 323 |   -> {auto 0 prf2 : Just k < m2}
 324 |   -> UnionRes (Just $ fst p) x a
 325 | prepEQ p eq (UR ps prf) =
 326 |   let 0 fstp_lt_m2 := rewrite eq in prf2
 327 |       0 lt = either (trans_LT_EQ prf1) (trans_LT_EQ fstp_lt_m2) prf
 328 |    in UR (p :: ps) (Left Refl)
 329 | 
 330 | ||| Computes the union of two assoc lists.
 331 | |||
 332 | ||| In case of identical keys, the value of the second list
 333 | ||| is dropped. Use `unionWith` for better control over handling
 334 | ||| duplicate entries.
 335 | public export
 336 | union_ : AL m1 a -> AL m2 a -> UnionRes m1 m2 a
 337 | union_ xs@(p :: ps) ys@(q :: qs) =
 338 |   case comp (fst p) (fst q) of
 339 |     LT prf _   _   => prepLT p $ union_ ps ys
 340 |     EQ _   prf _   => prepEQ p prf $ union_ ps qs
 341 |     GT _   _   prf => prepGT q $ union_ xs qs
 342 | union_ y [] = UR y (Left Refl)
 343 | union_ [] y = UR y (Right Refl)
 344 | 
 345 | ||| Like `union` but in case of identical keys appearing in
 346 | ||| both lists, the associated values are combined using
 347 | ||| function `f`. Otherwise, values are converted with `g`.
 348 | public export
 349 | unionMap_ :
 350 |      (f : a -> a -> b)
 351 |   -> (g : a -> b)
 352 |   -> AL m1 a
 353 |   -> AL m2 a
 354 |   -> UnionRes m1 m2 b
 355 | unionMap_ f g xs@(p :: ps) ys@(q :: qs) =
 356 |   case comp (fst p) (fst q) of
 357 |     LT prf _   _   => prepLT (fst p, g $ snd p) $ unionMap_ f g ps ys
 358 |     EQ _   prf _   => prepEQ (fst p, f (snd p) (snd q)) prf $ unionMap_ f g ps qs
 359 |     GT _   _   prf => prepGT (fst q, g $ snd q) $ unionMap_ f g xs qs
 360 | unionMap_ _ g y [] = UR (map g y) (Left Refl)
 361 | unionMap_ _ g [] y = UR (map g y) (Right Refl)
 362 | 
 363 | ||| Like `union` but in case of identical keys appearing in
 364 | ||| both lists, the associated values are combined using
 365 | ||| function `f`.
 366 | public export
 367 | unionWith_ : (a -> a -> a) -> AL m1 a -> AL m2 a -> UnionRes m1 m2 a
 368 | unionWith_ f = unionMap_ f id
 369 | 
 370 | --------------------------------------------------------------------------------
 371 | --          Intersection
 372 | --------------------------------------------------------------------------------
 373 | 
 374 | ||| The result of building the intersection of two assoc lists may
 375 | ||| contain an arbitrary new key index, which is not smaller than
 376 | ||| the head indices of the original lists.
 377 | public export
 378 | record IntersectRes (m1,m2 : Maybe Key) (a : Type) where
 379 |   constructor IS
 380 |   {0 mx : Maybe Key}
 381 |   pairs  : AL mx a
 382 |   0 prf1 : m1 <= mx
 383 |   0 prf2 : m2 <= mx
 384 | 
 385 | 0 lteNothing : {m : Maybe Key} -> m <= Nothing
 386 | lteNothing {m = Nothing} = Refl
 387 | lteNothing {m = Just _}  = Rel %search
 388 | 
 389 | public export %inline
 390 | prependIS :
 391 |      {0 m1,m2 : Maybe Key}
 392 |   -> (p : (Key, a))
 393 |   -> (0 prf : fst p === k)
 394 |   -> IntersectRes m1 m2 a
 395 |   -> {auto 0 lt  : Just (fst p) < m1}
 396 |   -> IntersectRes (Just $ fst p) (Just k) a
 397 | prependIS p prf (IS ps prf1 prf2) =
 398 |   let 0 ltp := strictLeft lt prf1
 399 |    in IS (p :: ps) Refl (fromEq $ cong Just (sym prf))
 400 | 
 401 | ||| Computes the intersection of two assoc lists, keeping
 402 | ||| only entries appearing in both lists. Only the values of
 403 | ||| the first list are being kept.
 404 | public export
 405 | intersect_ : AL m1 a -> AL m2 a -> IntersectRes m1 m2 a
 406 | intersect_ xs@(p :: ps) ys@(q :: qs) =
 407 |   case comp (fst p) (fst q) of
 408 |     LT _ _ _   =>
 409 |       let IS res p1 p2 := intersect_ ps ys
 410 |        in IS res (transitive %search p1) p2
 411 |     EQ _ y _ => prependIS p y $ intersect_ ps qs
 412 |     GT _ _ _ =>
 413 |       let IS res p1 p2 := intersect_ xs qs
 414 |        in IS res p1 (transitive %search p2)
 415 | intersect_ y [] = IS [] lteNothing %search
 416 | intersect_ [] y = IS [] %search lteNothing
 417 | 
 418 | ||| Computes the intersection of two assoc lists, keeping
 419 | ||| only entries appearing in both lists. Values of the two
 420 | ||| lists are combine using function `f`.
 421 | public export
 422 | intersectWith_ : (a -> a -> b) -> AL m1 a -> AL m2 a -> IntersectRes m1 m2 b
 423 | intersectWith_ f xs@(p :: ps) ys@(q :: qs) =
 424 |   case comp (fst p) (fst q) of
 425 |     LT _ _ _ =>
 426 |       let IS res p1 p2 := intersectWith_ f ps ys
 427 |        in IS res (transitive %search p1) p2
 428 |     EQ _ y _ => prependIS (fst p, f (snd p) (snd q)) y $ intersectWith_ f ps qs
 429 |     GT _ _ _ =>
 430 |       let IS res p1 p2 := intersectWith_ f xs qs
 431 |        in IS res p1 (transitive %search p2)
 432 | intersectWith_ _ y [] = IS [] lteNothing %search
 433 | intersectWith_ _ [] y = IS [] %search lteNothing
 434 | 
 435 | --------------------------------------------------------------------------------
 436 | --          AssocList
 437 | --------------------------------------------------------------------------------
 438 | 
 439 | public export
 440 | record AssocList a where
 441 |   constructor MkAL
 442 |   {0 firstKey : Maybe Key}
 443 |   repr : AL firstKey a
 444 | 
 445 | public export %inline
 446 | Functor AssocList where
 447 |   map f (MkAL r) = MkAL $ map f r
 448 | 
 449 | public export %inline
 450 | foldlKV : (acc -> (Key,el) -> acc) -> acc -> AssocList el -> acc
 451 | foldlKV f ini (MkAL r) = foldlKV_ f ini r
 452 | 
 453 | public export
 454 | traverseKV : Applicative f => ((Key,a) -> f b) -> AssocList a -> f (AssocList b)
 455 | traverseKV f (MkAL r) = MkAL <$> traverseKV_ f r
 456 | 
 457 | public export %inline
 458 | Foldable AssocList where
 459 |   foldr c n (MkAL r) = foldr c n r
 460 |   foldl c n (MkAL r) = foldl c n r
 461 |   null (MkAL r) = null r
 462 |   foldMap f (MkAL r) = foldMap f r
 463 | 
 464 | public export %inline
 465 | Traversable AssocList where
 466 |   traverse f (MkAL r) = MkAL <$> traverse f r
 467 | 
 468 | ||| Lookup a key in an assoc list.
 469 | public export %inline
 470 | lookup : (k : Key) -> AssocList a -> Maybe a
 471 | lookup k (MkAL r) = lookup_ k r
 472 | 
 473 | public export %inline
 474 | nonEmpty : AssocList a -> Bool
 475 | nonEmpty (MkAL r) = nonEmpty_ r
 476 | 
 477 | public export %inline
 478 | isEmpty : AssocList a -> Bool
 479 | isEmpty (MkAL r) = isEmpty_ r
 480 | 
 481 | ||| Extracts the key / value pairs from the assoc list.
 482 | public export %inline
 483 | pairs : AssocList a -> List (Key,a)
 484 | pairs (MkAL r) = pairs_ r
 485 | 
 486 | ||| Extracts the keys from the assoc list.
 487 | public export %inline
 488 | keys : AssocList a -> List Key
 489 | keys (MkAL r) = keys_ r
 490 | 
 491 | ||| Extracts the values from the assoc list.
 492 | public export %inline
 493 | values : AssocList a -> List a
 494 | values (MkAL r) = values_ r
 495 | 
 496 | public export %inline
 497 | length : AssocList a -> Nat
 498 | length (MkAL r) = length_ r
 499 | 
 500 | public export %inline
 501 | Eq a => Eq (AssocList a) where
 502 |   MkAL r1 == MkAL r2 = heq r1 r2
 503 | 
 504 | export
 505 | Show a => Show (AssocList a) where
 506 |   showPrec p (MkAL r) = showCon p "MkAL" $ showArg r
 507 | 
 508 | ||| Inserts a new key / value pair into an assoc list.
 509 | ||| The result type reflects the possibilities with regard
 510 | ||| to the head pair of the new assoc list.
 511 | |||
 512 | ||| Note: If the given key `k` is already present in the assoc list,
 513 | ||| its associated value will be replaced with `v`.
 514 | public export %inline
 515 | insert : (k : Key) -> (v : a) -> AssocList a -> AssocList a
 516 | insert k v (MkAL r) = MkAL $ pairs $ insert_ k v r
 517 | 
 518 | ||| Like `insert` but in case `k` is already present in the assoc
 519 | ||| list, the `v` will be cobine with the old value via function `f`.
 520 | public export %inline
 521 | insertWith :
 522 |      (f : a -> a -> a)
 523 |   -> (k : Key)
 524 |   -> (v : a)
 525 |   -> AssocList a
 526 |   -> AssocList a
 527 | insertWith f k v (MkAL r) = MkAL $ pairs $ insertWith_ f k v r
 528 | 
 529 | public export
 530 | fromList : List (Key,a) -> AssocList a
 531 | fromList = foldl (\al,(k,v) => insert k v al) (MkAL [])
 532 | 
 533 | ||| Tries to remove the entry with the given key from the
 534 | ||| assoc list. The key index of the result will be equal to
 535 | ||| or greater than `m`.
 536 | public export %inline
 537 | delete : (k : Key) -> AssocList a -> AssocList a
 538 | delete k (MkAL r) = MkAL $ pairs $ delete_ k r
 539 | 
 540 | ||| Applies the given function to all values, keeping only the
 541 | ||| `Just` results.
 542 | public export %inline
 543 | mapMaybe : (a -> Maybe b) -> AssocList a -> AssocList b
 544 | mapMaybe f (MkAL r) = MkAL $ pairs $ mapMaybe_ f r
 545 | 
 546 | ||| Applies the given function to all key / value pairs, keeping only the
 547 | ||| `Just` results.
 548 | public export %inline
 549 | mapMaybeK : (Key -> a -> Maybe b) -> AssocList a -> AssocList b
 550 | mapMaybeK f (MkAL r) = MkAL $ pairs $ mapMaybeK_ f r
 551 | 
 552 | ||| Updates the value at the given position by applying the given function.
 553 | public export %inline
 554 | update : (k : Key) -> (a -> a) -> AssocList a -> AssocList a
 555 | update k f (MkAL r) = MkAL $ update_ k f r
 556 | 
 557 | ||| Updates the value at the given position by applying the given effectful
 558 | ||| computation.
 559 | public export %inline
 560 | updateA : Applicative f => Key -> (a -> f a) -> AssocList a -> f (AssocList a)
 561 | updateA k g (MkAL r) = MkAL <$> updateA_ k g r
 562 | 
 563 | ||| Computes the union of two assoc lists.
 564 | |||
 565 | ||| In case of identical keys, the value of the second list
 566 | ||| is dropped. Use `unionWith` for better control over handling
 567 | ||| duplicate entries.
 568 | public export %inline
 569 | union : AssocList a -> AssocList a -> AssocList a
 570 | union (MkAL r1) (MkAL r2) = MkAL $ pairs $ union_ r1 r2
 571 | 
 572 | ||| Like `union` but in case of identical keys appearing in
 573 | ||| both lists, the associated values are combined using
 574 | ||| function `f`. Otherwise, values are converted with `g`.
 575 | public export %inline
 576 | unionMap :
 577 |      (f : a -> a -> b)
 578 |   -> (g : a -> b)
 579 |   -> AssocList a
 580 |   -> AssocList a
 581 |   -> AssocList b
 582 | unionMap f g (MkAL r1) (MkAL r2) = MkAL $ pairs $ unionMap_ f g r1 r2
 583 | 
 584 | ||| Like `union` but in case of identical keys appearing in
 585 | ||| both lists, the associated values are combined using
 586 | ||| function `f`.
 587 | public export %inline
 588 | unionWith : (a -> a -> a) -> AssocList a -> AssocList a -> AssocList a
 589 | unionWith f = unionMap f id
 590 | 
 591 | ||| Computes the intersection of two assoc lists, keeping
 592 | ||| only entries appearing in both lists. Only the values of
 593 | ||| the first list are being kept.
 594 | public export %inline
 595 | intersect : AssocList a -> AssocList a -> AssocList a
 596 | intersect (MkAL r1) (MkAL r2) = MkAL $ pairs $ intersect_ r1 r2
 597 | 
 598 | ||| Computes the intersection of two assoc lists, keeping
 599 | ||| only entries appearing in both lists. Values of the two
 600 | ||| lists are combine using function `f`.
 601 | public export
 602 | intersectWith : (a -> a -> b) -> AssocList a -> AssocList a -> AssocList b
 603 | intersectWith f (MkAL r1) (MkAL r2) = MkAL $ pairs $ intersectWith_ f r1 r2
 604 |