
   0 | module Data.AssocList.Indexed
   1 | 
   2 | import Data.Linear.List
   3 | import Data.Array
   4 | import Data.Array.Mutable
   5 | import Data.List
   6 | 
   7 | %default total
   8 | 
   9 | --------------------------------------------------------------------------------
  10 | --          Utilities
  11 | --------------------------------------------------------------------------------
  12 | 
  13 | weakenp : (Fin n, t) -> (Fin (S n), t)
  14 | weakenp (x,v) = (weaken x, v)
  15 | 
  16 | weakenpN : (0 m : Nat) -> (Fin n, t) -> (Fin (n + m), t)
  17 | weakenpN m (x,v) = (weakenN m x, v)
  18 | 
  19 | --------------------------------------------------------------------------------
  20 | --          Rep
  21 | --------------------------------------------------------------------------------
  22 | 
  23 | 0 Rep : Nat -> Type -> Type
  24 | Rep n t = List (Fin n, t)
  25 | 
  26 | heqRep : Eq e => Rep k e -> Rep m e -> Bool
  27 | heqRep [] []               = True
  28 | heqRep ((n1,e1) :: xs) ((n2,e2) :: ys) =
  29 |   case finToNat n1 == finToNat n2 && e1 == e2 of
  30 |     True  => heqRep xs ys
  31 |     False => False
  32 | heqRep _         _         = False
  33 | 
  34 | insertRep : Fin n -> e -> Rep n e -> Rep n e
  35 | insertRep k el []        = [(k,el)]
  36 | insertRep k el (x :: xs) = case compare k (fst x) of
  37 |   LT => (k,el) :: x :: xs
  38 |   EQ => (k,el) :: xs
  39 |   GT => x :: insertRep k el xs
  40 | 
  41 | insertWithRep : (e -> e -> e) -> Fin n -> e -> Rep n e -> Rep n e
  42 | insertWithRep f k el []        = [(k,el)]
  43 | insertWithRep f k el (x :: xs) = case compare k (fst x) of
  44 |   LT => (k,el) :: x :: xs
  45 |   EQ => (k,f el (snd x)) :: xs
  46 |   GT => x :: insertWithRep f k el xs
  47 | 
  48 | lookupRep : Fin n -> Rep n e -> Maybe e
  49 | lookupRep x []        = Nothing
  50 | lookupRep x (y :: xs) = case compare x (fst y) of
  51 |   GT => lookupRep x xs
  52 |   EQ => Just (snd y)
  53 |   LT => Nothing
  54 | 
  55 | unionRep : Rep k e -> Rep k e -> Rep k e
  56 | unionRep []      ys      = ys
  57 | unionRep xs      []      = xs
  58 | unionRep l@(x::xs) r@(y::ys) = case compare (fst x) (fst y) of
  59 |   LT => x :: unionRep xs r
  60 |   EQ => x :: unionRep xs ys
  61 |   GT => y :: unionRep l ys
  62 | 
  63 | unionMapRep : (e -> e -> b) -> (e -> b) -> Rep k e -> Rep k e -> Rep k b
  64 | unionMapRep f g []        ys                    = map (map g) ys
  65 | unionMapRep f g xs        []                    = map (map g) xs
  66 | unionMapRep f g l@((k1,l1)::xs) r@((k2,l2)::ys) = case compare k1 k2 of
  67 |   LT => (k1, g l1)    :: unionMapRep f g xs r
  68 |   EQ => (k1, f l1 l2) :: unionMapRep f g xs ys
  69 |   GT => (k2, g l2)    :: unionMapRep f g l  ys
  70 | 
  71 | intersectWithRep : (e -> e -> b) -> Rep k e -> Rep k e -> Rep k b
  72 | intersectWithRep f []        ys                    = []
  73 | intersectWithRep f xs        []                    = []
  74 | intersectWithRep f l@((k1,l1)::xs) r@((k2,l2)::ys) = case compare k1 k2 of
  75 |   LT => intersectWithRep f xs r
  76 |   EQ => (k1, f l1 l2) :: intersectWithRep f xs ys
  77 |   GT => intersectWithRep f l  ys
  78 | 
  79 | weakenRep : Rep k e -> Rep (S k) e
  80 | weakenRep []        = []
  81 | weakenRep (x :: xs) = weakenp x :: weakenRep xs
  82 | 
  83 | weakenRepN : (0 m : Nat) -> Rep k e -> Rep (k + m) e
  84 | weakenRepN m []        = []
  85 | weakenRepN m (x :: xs) = weakenpN m x :: weakenRepN m xs
  86 | 
  87 | --------------------------------------------------------------------------------
  88 | --          AssocList
  89 | --------------------------------------------------------------------------------
  90 | 
  91 | export
  92 | record AssocList (k : Nat) (e : Type) where
  93 |   constructor AL
  94 |   ps : Rep k e
  95 | 
  96 | --------------------------------------------------------------------------------
  97 | --          Interfaces
  98 | --------------------------------------------------------------------------------
  99 | 
 100 | export
 101 | Functor (AssocList k) where
 102 |   map f (AL ps) = AL $ map (map f) ps
 103 | 
 104 | export %inline
 105 | Foldable (AssocList k) where
 106 |   foldr c n (AL r) = foldr (c . snd) n r
 107 |   foldl c n (AL r) = foldl (\x => c x . snd) n r
 108 |   null (AL r)      = null r
 109 |   foldMap f (AL r) = foldMap (f . snd) r
 110 |   toList (AL r)    = map snd r
 111 | 
 112 | export %inline
 113 | Traversable (AssocList k) where
 114 |   traverse f (AL r) = AL <$> traverse (\(n,l) => (n,) <$> f l) r
 115 | 
 116 | export %inline
 117 | Eq e => Eq (AssocList k e) where
 118 |   AL r1 == AL r2 = heqRep r1 r2
 119 | 
 120 | export
 121 | Show e => Show (AssocList k e) where
 122 |   showPrec p (AL r) =
 123 |     showCon p "fromList" $ showArg (map (\(n,l) => (finToNat n, l)) r)
 124 | 
 125 | export
 126 | weakenAL : AssocList k e -> AssocList (S k) e
 127 | weakenAL (AL r) = AL $ weakenRep r
 128 | 
 129 | export
 130 | weakenALN : (0 m : Nat) -> AssocList k e -> AssocList (k + m) e
 131 | weakenALN m (AL g) = AL $ weakenRepN m g
 132 | 
 133 | --------------------------------------------------------------------------------
 134 | --          Utilities
 135 | --------------------------------------------------------------------------------
 136 | 
 137 | export %inline
 138 | empty : AssocList k e
 139 | empty = AL []
 140 | 
 141 | export %inline
 142 | singleton : Fin k -> e -> AssocList k e
 143 | singleton n v = AL [(n,v)]
 144 | 
 145 | export %inline
 146 | pairs : AssocList k e -> List (Fin k, e)
 147 | pairs = ps
 148 | 
 149 | export %inline
 150 | mapKV : (Fin k -> e -> b) -> AssocList k e -> AssocList k b
 151 | mapKV f (AL r) = AL $ map (\(x,v) => (x, f x v)) r
 152 | 
 153 | export %inline
 154 | foldlKV : (Fin k -> acc -> e -> acc) -> acc -> AssocList k e -> acc
 155 | foldlKV f ini (AL r) = foldl (\v,(x,l) => f x v l) ini r
 156 | 
 157 | public export
 158 | traverseKV :
 159 |      {auto _ : Applicative f}
 160 |   -> ((Fin k,e) -> f b)
 161 |   -> AssocList k e
 162 |   -> f (AssocList k b)
 163 | traverseKV f (AL r) = AL <$> traverse (\(n,l) => (n,) <$> f (n,l)) r
 164 | 
 165 | ||| Lookup a key in an assoc list.
 166 | export %inline
 167 | lookup : Fin k -> AssocList k e -> Maybe e
 168 | lookup k (AL r) = lookupRep k r
 169 | 
 170 | ||| Checks if an `AssocList` has an entry for the given key.
 171 | export %inline
 172 | hasKey : AssocList k e -> Fin k -> Bool
 173 | hasKey l k = isJust $ lookup k l
 174 | 
 175 | export %inline
 176 | nonEmpty : AssocList k e -> Bool
 177 | nonEmpty (AL []) = False
 178 | nonEmpty _       = True
 179 | 
 180 | export %inline
 181 | isEmpty : AssocList k e -> Bool
 182 | isEmpty (AL []) = True
 183 | isEmpty _       = False
 184 | 
 185 | ||| Extracts the keys from the assoc list.
 186 | export %inline
 187 | keys : AssocList k e -> List (Fin k)
 188 | keys = map fst . ps
 189 | 
 190 | ||| Extracts the values from the assoc list.
 191 | export %inline
 192 | values : AssocList k e -> List e
 193 | values = map snd . ps
 194 | 
 195 | export %inline
 196 | length : AssocList k e -> Nat
 197 | length = length . ps
 198 | 
 199 | ||| Inserts a new key / value pair into an assoc list.
 200 | |||
 201 | ||| Note: If the given key `k` is already present in the assoc list,
 202 | ||| its associated value will be replaced with the new value.
 203 | export %inline
 204 | insert : Fin k -> e -> AssocList k e -> AssocList k e
 205 | insert key lbl (AL r) = AL $ insertRep key lbl r
 206 | 
 207 | ||| Like `insert` but in case `k` is already present in the assoc
 208 | ||| list, the `v` will be cobine with the old value via function `f`.
 209 | export %inline
 210 | insertWith :
 211 |      (f : e -> e -> e)
 212 |   -> Fin k
 213 |   -> (v : e)
 214 |   -> AssocList k e
 215 |   -> AssocList k e
 216 | insertWith f x v (AL r) = AL $ insertWithRep f x v r
 217 | 
 218 | export
 219 | fromList : List (Fin k,e) -> AssocList k e
 220 | fromList = foldl (\al,(k,v) => insert k v al) empty
 221 | 
 222 | ||| Tries to remove the entry with the given key from the
 223 | ||| assoc list. The key index of the result will be equal to
 224 | ||| or greater than `m`.
 225 | export %inline
 226 | delete : Fin k -> AssocList k e -> AssocList k e
 227 | delete x (AL r) = AL $ filter ((/= x) . fst) r
 228 | 
 229 | ||| Applies the given function to all values, keeping only the
 230 | ||| `Just` results.
 231 | export %inline
 232 | mapMaybe : (e -> Maybe b) -> AssocList k e -> AssocList k b
 233 | mapMaybe f (AL r) = AL $ mapMaybe (\(x,l) => (x,) <$> f l) r
 234 | 
 235 | ||| Applies the given function to all key / value pairs, keeping only the
 236 | ||| `Just` results.
 237 | export %inline
 238 | mapMaybeK : (Fin k -> e -> Maybe b) -> AssocList k e -> AssocList k b
 239 | mapMaybeK f (AL r) = AL $ mapMaybe (\(x,l) => (x,) <$> f x l) r
 240 | 
 241 | ||| Updates the value at the given position by applying the given function.
 242 | export %inline
 243 | update : Fin k -> (e -> e) -> AssocList k e -> AssocList k e
 244 | update k f (AL r) =
 245 |   AL $ map (\(x,l) => if k == x then (x, f l) else (x,l)) r
 246 | 
 247 | ||| Updates the value at the given position by applying the given effectful
 248 | ||| computation.
 249 | export %inline
 250 | updateA : Applicative f => Fin k -> (e -> f e) -> AssocList k e -> f (AssocList k e)
 251 | updateA k g (AL r) =
 252 |   AL <$> traverse (\(x,l) => if k == x then (x,) <$> g l else pure (x,l)) r
 253 | 
 254 | ||| Computes the union of two assoc lists.
 255 | |||
 256 | ||| In case of identical keys, the value of the second list
 257 | ||| is dropped. Use `unionWith` for better control over handling
 258 | ||| duplicate entries.
 259 | export %inline
 260 | union : AssocList k e -> AssocList k e -> AssocList k e
 261 | union (AL r1) (AL r2) = AL $ unionRep r1 r2
 262 | 
 263 | ||| Like `union` but in case of identical keys appearing in
 264 | ||| both lists, the associated values are combined using
 265 | ||| function `f`. Otherwise, values are converted with `g`.
 266 | export %inline
 267 | unionMap :
 268 |      (f : e -> e -> b)
 269 |   -> (g : e -> b)
 270 |   -> AssocList k e
 271 |   -> AssocList k e
 272 |   -> AssocList k b
 273 | unionMap f g (AL r1) (AL r2) = AL $ unionMapRep f g r1 r2
 274 | 
 275 | ||| Like `union` but in case of identical keys appearing in
 276 | ||| both lists, the associated values are combined using
 277 | ||| function `f`.
 278 | export %inline
 279 | unionWith : (e -> e -> e) -> AssocList k e -> AssocList k e -> AssocList k e
 280 | unionWith f = unionMap f id
 281 | 
 282 | ||| Computes the intersection of two assoc lists, keeping
 283 | ||| only entries appearing in both lists. Values of the two
 284 | ||| lists are combine using function `f`.
 285 | export
 286 | intersectWith : (e -> e -> b) -> AssocList k e -> AssocList k e -> AssocList k b
 287 | intersectWith f (AL r1) (AL r2) = AL $ intersectWithRep f r1 r2
 288 | 
 289 | ||| Computes the intersection of two assoc lists, keeping
 290 | ||| only entries appearing in both lists. Only the values of
 291 | ||| the first list are being kept.
 292 | export %inline
 293 | intersect : AssocList k e -> AssocList k e -> AssocList k e
 294 | intersect = intersectWith const
 295 | 
 296 | ||| Filter an assoc list via a linear function.
 297 | export %inline
 298 | filterLin : (Fin k -> F1 s Bool) -> AssocList k e -> F1 s (AssocList k e)
 299 | filterLin f (AL ps) t1 =
 300 |   let ps2 # t2 := filter1 (\(x,_) => f x) ps t1
 301 |    in AL ps2 # t2
 302 | 
 303 | ||| Using a comparator, find the minimal value and its
 304 | ||| index in an assoc list.
 305 | export %inline
 306 | minBy : Ord b => (a -> b) -> AssocList k a -> Maybe (Fin k, a)
 307 | minBy _ (AL [])        = Nothing
 308 | minBy f (AL $ p :: ps) = Just $ go p (f $ snd p) ps
 309 |   where
 310 |     go : (Fin k, a) -> b -> List (Fin k, a) -> (Fin k, a)
 311 |     go p v [] = p
 312 |     go p v (h :: t) =
 313 |       let v2 := f (snd h)
 314 |        in if v2 < v then go h v2 t else go p v t
 315 |