Data.SnocList


   0 | ||| A Reversed List
   1 | module Data.SnocList
   2 | 
   3 | import Data.List
   4 | import Data.Fin
   5 | 
   6 | %default total
   7 | 
   8 | public export
   9 | Cast (SnocList a) (List a) where
  10 |   cast sx = sx <>> []
  11 | 
  12 | public export
  13 | Cast (List a) (SnocList a) where
  14 |   cast xs = Lin <>< xs
  15 | 
  16 | %transform "fastConcat" concat {t = SnocList} {a = String} = fastConcat . cast
  17 | 
  18 | ||| Transform to a list but keeping the contents in the spine order (term depth).
  19 | public export
  20 | asList : SnocList type -> List type
  21 | asList = (reverse . cast)
  22 | 
  23 | export
  24 | Uninhabited (Lin = x :< xs) where
  25 |   uninhabited Refl impossible
  26 | 
  27 | export
  28 | Uninhabited (x :< xs = Lin) where
  29 |   uninhabited Refl impossible
  30 | 
  31 | ||| True iff input is Lin
  32 | public export
  33 | isLin : SnocList a -> Bool
  34 | isLin Lin = True
  35 | isLin (sx :< x) = False
  36 | 
  37 | ||| True iff input is (:<)
  38 | public export
  39 | isSnoc : SnocList a -> Bool
  40 | isSnoc Lin     = False
  41 | isSnoc (sx :< x) = True
  42 | 
  43 | ||| Given a predicate and a snoclist, returns a tuple consisting of the longest
  44 | ||| prefix of the snoclist whose elements satisfy the predicate, and the rest of the
  45 | ||| snoclist.
  46 | public export
  47 | spanBy : (a -> Maybe b) -> SnocList a -> (SnocList a, SnocList b)
  48 | spanBy p [<] = ([<], [<])
  49 | spanBy p (xs :< x) = case p x of
  50 |   Just b =>
  51 |     let (as, bs) = spanBy p xs in
  52 |     (as, bs :< b)
  53 |   Nothing => (xs :< x, [<])
  54 | 
  55 | export
  56 | Show a => Show (SnocList a) where
  57 |   show xs = concat ("[< " :: intersperse ", " (show' [] xs) ++ ["]"])
  58 |     where
  59 |       show' : List String -> SnocList a -> List String
  60 |       show' acc Lin       = acc
  61 |       show' acc (xs :< x) = show' (show x :: acc) xs
  62 | 
  63 | public export
  64 | mapImpl : (a -> b) -> SnocList a -> SnocList b
  65 | mapImpl f Lin = Lin
  66 | mapImpl f (sx :< x) = (mapImpl f sx) :< (f x)
  67 | 
  68 | -- Utility for implementing `mapTR`
  69 | mapTR' : List b -> (a -> b) -> SnocList a -> SnocList b
  70 | mapTR' xs f (sx :< x) = mapTR' (f x :: xs) f sx
  71 | mapTR' xs f Lin       = Lin <>< xs
  72 | 
  73 | -- Tail recursive version of `map`. This is automatically used
  74 | -- at runtime due to a `transform` rule.
  75 | mapTR : (a -> b) -> SnocList a -> SnocList b
  76 | mapTR = mapTR' []
  77 | 
  78 | -- mapTRIsMap proves these are equivalent.
  79 | %transform "tailRecMapSnocList" SnocList.mapImpl = SnocList.mapTR
  80 | 
  81 | public export %inline
  82 | Functor SnocList where
  83 |   map = mapImpl
  84 | 
  85 | public export
  86 | Semigroup (SnocList a) where
  87 |   (<+>) = (++)
  88 | 
  89 | public export
  90 | Monoid (SnocList a) where
  91 |   neutral = Lin
  92 | 
  93 | public export
  94 | Foldable SnocList where
  95 |   foldr f z [<]       = z
  96 |   foldr f z (sx :< x) = foldr f (f x z) sx
  97 | 
  98 |   foldl f z Lin = z
  99 |   foldl f z (xs :< x) = f (foldl f z xs) x
 100 | 
 101 |   null Lin      = True
 102 |   null (_ :< _) = False
 103 | 
 104 |   toList = (<>> [])
 105 | 
 106 |   foldMap f = foldr (\v,acc => f v <+> acc) neutral
 107 | 
 108 | public export
 109 | Applicative SnocList where
 110 |   pure = (:<) Lin
 111 |   fs <*> xs = concatMap (flip map xs) fs
 112 | 
 113 | public export
 114 | Monad SnocList where
 115 |   xs >>= k = concatMap k xs
 116 | 
 117 | public export
 118 | Traversable SnocList where
 119 |   traverse _ Lin = pure Lin
 120 |   traverse f (xs :< x) = [| traverse f xs :< f x |]
 121 | 
 122 | public export
 123 | Alternative SnocList where
 124 |   empty = Lin
 125 |   xs <|> ys = xs ++ ys
 126 | 
 127 | -- Why can't we just use an implementation here?!
 128 | export %hint
 129 | SnocBiinjective : Biinjective (:<)
 130 | SnocBiinjective = MkBiinjective $ \case Refl => (Refl, Refl)
 131 | 
 132 | ||| Find the rightmost element of the snoc-list that satisfies the predicate.
 133 | public export
 134 | find : (a -> Bool) -> SnocList a -> Maybe a
 135 | find p Lin = Nothing
 136 | find p (xs :< x) = if p x then Just x else find p xs
 137 | 
 138 | ||| Satisfiable if `k` is a valid index into `xs`.
 139 | |||
 140 | ||| @ k  the potential index
 141 | ||| @ xs the snoc-list into which k may be an index
 142 | public export
 143 | data InBounds : (k : Nat) -> (xs : SnocList a) -> Type where
 144 |     ||| Z is a valid index into any cons cell
 145 |     InFirst : InBounds Z (xs :< x)
 146 |     ||| Valid indices can be extended
 147 |     InLater : InBounds k xs -> InBounds (S k) (xs :< x)
 148 | 
 149 | ||| Find the index (counting from right) of the rightmost element (if exists) of a
 150 | ||| snoc-list that satisfies the given test, else `Nothing`.
 151 | public export
 152 | findIndex : (a -> Bool) -> (xs : SnocList a) -> Maybe $ Fin (length xs)
 153 | findIndex _ Lin = Nothing
 154 | findIndex p (xs :< x) = if p x
 155 |   then Just FZ
 156 |   else FS <$> findIndex p xs
 157 | 
 158 | ---------------------------
 159 | -- Zippable --
 160 | ---------------------------
 161 | 
 162 | public export
 163 | Zippable SnocList where
 164 |   zipWith _ [<] _ = [<]
 165 |   zipWith _ _ [<] = [<]
 166 |   zipWith f (xs :< x) (ys :< y) = zipWith f xs ys :< f x y
 167 | 
 168 |   zipWith3 _ [<] _ _ = [<]
 169 |   zipWith3 _ _ [<] _ = [<]
 170 |   zipWith3 _ _ _ [<] = [<]
 171 |   zipWith3 f (xs :< x) (ys :< y) (zs :< z) = zipWith3 f xs ys zs :< f x y z
 172 | 
 173 |   unzipWith f [<] = ([<], [<])
 174 |   unzipWith f (xs :< x) = let (bs, cs) = unzipWith f xs
 175 |                               (b, c) = f x
 176 |                           in (bs :< b, cs :< c)
 177 | 
 178 |   unzipWith3 f [<] = ([<], [<], [<])
 179 |   unzipWith3 f (xs :< x) = let (bs, cs, ds) = unzipWith3 f xs
 180 |                                (b, c, d) = f x
 181 |                            in  (bs :< b, cs :< c, ds :< d)
 182 | 
 183 | ------------------
 184 | --- Properties ---
 185 | ------------------
 186 | 
 187 | --- Usual snoc-list append (++) ---
 188 | 
 189 | export
 190 | appendAssociative : (l, c, r : SnocList a) -> l ++ (c ++ r) = (l ++ c) ++ r
 191 | appendAssociative l c [<]       = Refl
 192 | appendAssociative l c (sx :< _) = rewrite appendAssociative l c sx in Refl
 193 | 
 194 | export
 195 | appendLinLeftNeutral : (sx : SnocList a) -> [<] ++ sx = sx
 196 | appendLinLeftNeutral [<]       = Refl
 197 | appendLinLeftNeutral (sx :< _) = rewrite appendLinLeftNeutral sx in Refl
 198 | 
 199 | --- Fish (<><) and chips (<>>) appends ---
 200 | 
 201 | export
 202 | fishAsSnocAppend : (xs : SnocList a) -> (ys : List a) -> xs <>< ys = xs ++ cast ys
 203 | fishAsSnocAppend xs []        = Refl
 204 | fishAsSnocAppend xs (y :: ys) = do
 205 |   rewrite fishAsSnocAppend (xs :< y) ys
 206 |   rewrite fishAsSnocAppend [<y] ys
 207 |   rewrite appendAssociative xs [<y] (cast ys)
 208 |   Refl
 209 | 
 210 | export
 211 | chipsAsListAppend : (xs : SnocList a) -> (ys : List a) -> xs <>> ys = cast xs ++ ys
 212 | chipsAsListAppend [<]       ys = Refl
 213 | chipsAsListAppend (sx :< x) ys = do
 214 |   rewrite chipsAsListAppend sx (x :: ys)
 215 |   rewrite chipsAsListAppend sx [x]
 216 |   rewrite sym $ appendAssociative (cast sx) [x] ys
 217 |   Refl
 218 | 
 219 | --- More on append ---
 220 | 
 221 | export
 222 | toListAppend : (sx, sy : SnocList a) -> toList (sx ++ sy) = toList sx ++ toList sy
 223 | toListAppend sx [<] = rewrite appendNilRightNeutral $ toList sx in Refl
 224 | toListAppend sx (sy :< y) = do
 225 |   rewrite chipsAsListAppend sy [y]
 226 |   rewrite appendAssociative (cast sx) (cast sy) [y]
 227 |   rewrite chipsAsListAppend (sx ++ sy) [y]
 228 |   rewrite toListAppend sx sy
 229 |   Refl
 230 | 
 231 | export
 232 | castListAppend : (xs, ys : List a) -> cast {to=SnocList a} (xs ++ ys) === cast xs ++ cast ys
 233 | castListAppend []      ys = rewrite appendLinLeftNeutral $ [<] <>< ys in Refl
 234 | castListAppend (x::xs) ys = do
 235 |   rewrite fishAsSnocAppend [<x] (xs ++ ys)
 236 |   rewrite castListAppend xs ys
 237 |   rewrite appendAssociative [<x] (cast xs) (cast ys)
 238 |   rewrite sym $ fishAsSnocAppend [<x] xs
 239 |   Refl
 240 | 
 241 | --- Pure casts (including `toList`)
 242 | 
 243 | export
 244 | castToList : (sx : SnocList a) -> cast (toList sx) === sx
 245 | castToList [<]       = Refl
 246 | castToList (sx :< x) = do
 247 |   rewrite chipsAsListAppend sx [x]
 248 |   rewrite castListAppend (cast sx) [x]
 249 |   rewrite castToList sx
 250 |   Refl
 251 | 
 252 | export
 253 | toListCast : (xs : List a) -> toList (cast {to=SnocList a} xs) === xs
 254 | toListCast []      = Refl
 255 | toListCast (x::xs) = do
 256 |   rewrite fishAsSnocAppend [<x] xs
 257 |   rewrite toListAppend [<x] (cast xs)
 258 |   rewrite toListCast xs
 259 |   Refl
 260 | 
 261 | ||| Append an element to the head of a snoc-list.
 262 | ||| Note: Traverses the snoc-list, linear time complexity
 263 | public export
 264 | cons : a -> SnocList a -> SnocList a
 265 | cons x sx = [< x] ++ sx
 266 | 
 267 | --- Folds ---
 268 | 
 269 | export
 270 | foldAppend : (f : acc -> a -> acc) -> (init : acc) -> (sx, sy : SnocList a) -> foldl f init (sx ++ sy) = foldl f (foldl f init sx) sy
 271 | foldAppend f init sx [<]       = Refl
 272 | foldAppend f init sx (sy :< x) = rewrite foldAppend f init sx sy in Refl
 273 | 
 274 | export
 275 | snocFoldlAsListFoldl : (f : acc -> a -> acc) -> (init : acc) -> (xs : SnocList a) -> foldl f init xs = foldl f init (toList xs)
 276 | snocFoldlAsListFoldl f init [<]       = Refl
 277 | snocFoldlAsListFoldl f init (sx :< x) = do
 278 |   rewrite chipsAsListAppend sx [x]
 279 |   rewrite snocFoldlAsListFoldl f init sx
 280 |   rewrite foldlAppend f init (cast sx) [x]
 281 |   Refl
 282 | 
 283 | --- Filtering ---
 284 | 
 285 | export
 286 | filterAppend : (f : a -> Bool) -> (sx, sy : SnocList a) -> filter f (sx ++ sy) = filter f sx ++ filter f sy
 287 | filterAppend f sx [<]       = Refl
 288 | filterAppend f sx (sy :< x) with (f x)
 289 |   _ | False = filterAppend f sx sy
 290 |   _ | True  = rewrite filterAppend f sx sy in Refl
 291 | 
 292 | export
 293 | toListFilter : (f : a -> Bool) -> (sx : SnocList a) -> toList (filter f sx) = filter f (toList sx)
 294 | toListFilter f [<]       = Refl
 295 | toListFilter f (sx :< x) = do
 296 |   rewrite chipsAsListAppend sx [x]
 297 |   rewrite filterAppend f (cast sx) [x]
 298 |   rewrite filterStepLemma
 299 |   rewrite toListFilter f sx
 300 |   Refl
 301 |   where
 302 |     filterStepLemma : toList (filter f (sx :< x)) = toList (filter f sx) ++ filter f [x]
 303 |     filterStepLemma with (f x)
 304 |       _ | False = rewrite appendNilRightNeutral $ toList $ filter f sx in Refl
 305 |       _ | True  = rewrite chipsAsListAppend (filter f sx) [x] in Refl
 306 | 
 307 | export
 308 | filterCast : (f : a -> Bool) -> (xs : List a) -> filter f (cast {to=SnocList a} xs) = cast (filter f xs)
 309 | filterCast f []      = Refl
 310 | filterCast f (x::xs) = do
 311 |   rewrite fishAsSnocAppend [<x] xs
 312 |   rewrite filterAppend f [<x] (cast xs)
 313 |   rewrite filterStepLemma
 314 |   rewrite filterCast f xs
 315 |   Refl
 316 |   where
 317 |     filterStepLemma : cast (filter f (x::xs)) = filter f [<x] ++ cast (filter f xs)
 318 |     filterStepLemma with (f x)
 319 |       _ | False = rewrite appendLinLeftNeutral $ [<] <>< filter f xs in Refl
 320 |       _ | True  = rewrite fishAsSnocAppend [<x] (filter f xs) in Refl
 321 | 
 322 | --- Functor map ---
 323 | 
 324 | export
 325 | mapFusion : (g : b -> c) -> (f : a -> b) -> (sx : SnocList a) -> map g (map f sx) = map (g . f) sx
 326 | mapFusion g f [<]       = Refl
 327 | mapFusion g f (sx :< x) = rewrite mapFusion g f sx in Refl
 328 | 
 329 | export
 330 | mapAppend : (f : a -> b) -> (sx, sy : SnocList a) -> map f (sx ++ sy) = map f sx ++ map f sy
 331 | mapAppend f sx [<]       = Refl
 332 | mapAppend f sx (sy :< x) = rewrite mapAppend f sx sy in Refl
 333 | 
 334 | export
 335 | toListMap : (f : a -> b) -> (sx : SnocList a) -> toList (map f sx) = map f (toList sx)
 336 | toListMap f [<]       = Refl
 337 | toListMap f (sx :< x) = do
 338 |   rewrite chipsAsListAppend (map f sx) [f x]
 339 |   rewrite chipsAsListAppend sx [x]
 340 |   rewrite mapAppend f (toList sx) [x]
 341 |   rewrite toListMap f sx
 342 |   Refl
 343 | 
 344 | export
 345 | mapCast : (f : a -> b) -> (xs : List a) -> map f (cast {to=SnocList a} xs) = cast (map f xs)
 346 | mapCast f []      = Refl
 347 | mapCast f (x::xs) = do
 348 |   rewrite fishAsSnocAppend [<f x] (map f xs)
 349 |   rewrite fishAsSnocAppend [<x] xs
 350 |   rewrite mapAppend f [<x] (cast xs)
 351 |   rewrite mapCast f xs
 352 |   Refl
 353 | 
 354 | --- mapMaybe ---
 355 | 
 356 | export
 357 | mapMaybeFusion : (g : b -> Maybe c) -> (f : a -> Maybe b) -> (sx : SnocList a) -> mapMaybe g (mapMaybe f sx) = mapMaybe (f >=> g) sx
 358 | mapMaybeFusion g f [<]       = Refl
 359 | mapMaybeFusion g f (sx :< x) with (f x)
 360 |   _ | Nothing = mapMaybeFusion g f sx
 361 |   _ | (Just y) with (g y)
 362 |     _ | Nothing = mapMaybeFusion g f sx
 363 |     _ | (Just z) = rewrite mapMaybeFusion g f sx in Refl
 364 | 
 365 | export
 366 | mapMaybeAppend : (f : a -> Maybe b) -> (sx, sy : SnocList a) -> mapMaybe f (sx ++ sy) = mapMaybe f sx ++ mapMaybe f sy
 367 | mapMaybeAppend f sx [<]       = Refl
 368 | mapMaybeAppend f sx (sy :< x) with (f x)
 369 |   _ | Nothing = mapMaybeAppend f sx sy
 370 |   _ | (Just y) = rewrite mapMaybeAppend f sx sy in Refl
 371 | 
 372 | export
 373 | toListMapMaybe : (f : a -> Maybe b) -> (sx : SnocList a) -> toList (mapMaybe f sx) = mapMaybe f (toList sx)
 374 | toListMapMaybe f [<]       = Refl
 375 | toListMapMaybe f (sx :< x) = do
 376 |   rewrite chipsAsListAppend sx [x]
 377 |   rewrite mapMaybeAppend f (toList sx) [x]
 378 |   rewrite mapMaybeStepLemma
 379 |   rewrite toListMapMaybe f sx
 380 |   Refl
 381 |   where
 382 |     mapMaybeStepLemma : toList (mapMaybe f (sx :< x)) = toList (mapMaybe f sx) ++ mapMaybe f [x]
 383 |     mapMaybeStepLemma with (f x)
 384 |       _ | Nothing  = rewrite appendNilRightNeutral $ toList $ mapMaybe f sx in Refl
 385 |       _ | (Just y) = rewrite chipsAsListAppend (mapMaybe f sx) [y] in Refl
 386 | 
 387 | export
 388 | mapMaybeCast : (f : a -> Maybe b) -> (xs : List a) -> mapMaybe f (cast {to=SnocList a} xs) = cast (mapMaybe f xs)
 389 | mapMaybeCast f []      = Refl
 390 | mapMaybeCast f (x::xs) = do
 391 |   rewrite fishAsSnocAppend [<x] xs
 392 |   rewrite mapMaybeAppend f [<x] (cast xs)
 393 |   rewrite mapMaybeStepLemma
 394 |   rewrite mapMaybeCast f xs
 395 |   Refl
 396 |   where
 397 |     mapMaybeStepLemma : cast (mapMaybe f (x::xs)) = mapMaybe f [<x] ++ cast (mapMaybe f xs)
 398 |     mapMaybeStepLemma with (f x)
 399 |       _ | Nothing  = rewrite appendLinLeftNeutral $ [<] <>< mapMaybe f xs in Refl
 400 |       _ | (Just y) = rewrite fishAsSnocAppend [<y] (mapMaybe f xs) in Refl
 401 | 
 402 | 0 mapTRIsMap :  (f : a -> b) -> (sa : SnocList a) -> mapTR f sa === map f sa
 403 | mapTRIsMap f = lemma []
 404 |   where lemma :  (bs : List b)
 405 |               -> (sa : SnocList a)
 406 |               -> mapTR' bs f sa === (map f sa <>< bs)
 407 |         lemma bs Lin       = Refl
 408 |         lemma bs (sx :< x) = lemma (f x :: bs) sx
 409 | 
 410 | 
 411 | 0 mapMaybeTRIsMapMaybe :  (f : a -> Maybe b)
 412 |                        -> (sa : SnocList a)
 413 |                        -> mapMaybeTR f sa === mapMaybe f sa
 414 | mapMaybeTRIsMapMaybe f = lemma []
 415 |   where lemma :  (bs : List b)
 416 |               -> (sa : SnocList a)
 417 |               -> mapMaybeAppend bs f sa === (mapMaybe f sa <>< bs)
 418 |         lemma bs Lin = Refl
 419 |         lemma bs (sx :< x) with (f x)
 420 |           lemma bs (sx :< x) | Nothing = lemma bs sx
 421 |           lemma bs (sx :< x) | Just v  = lemma (v :: bs) sx
 422 | 
 423 | 0 filterTRIsFilter :  (f : a -> Bool)
 424 |                    -> (sa : SnocList a)
 425 |                    -> filterTR f sa === filter f sa
 426 | filterTRIsFilter f = lemma []
 427 |   where lemma :  (as : List a)
 428 |               -> (sa : SnocList a)
 429 |               -> filterAppend as f sa === (filter f sa <>< as)
 430 |         lemma as Lin = Refl
 431 |         lemma as (sx :< x) with (f x)
 432 |           lemma as (sx :< x) | False = lemma as sx
 433 |           lemma as (sx :< x) | True  = lemma (x :: as) sx
 434 | 
 435 | -- SnocList `reverse` applied to `reverseOnto` is equivalent to swapping the
 436 | -- arguments of `reverseOnto`.
 437 | reverseReverseOnto : (l, r : SnocList a) ->
 438 |                      reverse (reverseOnto l r) = reverseOnto r l
 439 | reverseReverseOnto _ Lin = Refl
 440 | reverseReverseOnto l (sx :< x) = reverseReverseOnto (l :< x) sx
 441 | 
 442 | ||| SnocList `reverse` applied twice yields the identity function.
 443 | export
 444 | reverseInvolutive : (sx : SnocList a) -> reverse (reverse sx) = sx
 445 | reverseInvolutive = reverseReverseOnto Lin
 446 | 
 447 | -- Appending `x` to `l` and then reversing the result onto `r` is the same as
 448 | -- using (::) with `x` and the result of reversing `l` onto `r`.
 449 | snocReverse : (x : a) -> (l, r : SnocList a) ->
 450 |               reverseOnto r l :< x = reverseOnto r (reverseOnto [<x] (reverse l))
 451 | snocReverse _ Lin _ = Refl
 452 | snocReverse x (sy :< y) r
 453 |   = rewrite snocReverse x sy (r :< y) in
 454 |       rewrite cong (reverseOnto r . reverse) $ snocReverse x sy [<y] in
 455 |         rewrite reverseInvolutive (reverseOnto [<x] (reverse sy) :< y) in
 456 |           Refl
 457 | 
 458 | -- Proof that it is safe to lift a (::) out of the first `tailRecAppend`
 459 | -- argument.
 460 | snocTailRecAppend : (x : a) -> (l, r : SnocList a) ->
 461 |                     tailRecAppend l (r :< x) = (tailRecAppend l r) :< x
 462 | snocTailRecAppend x l r =
 463 |   rewrite snocReverse x (reverse r) l in
 464 |     rewrite reverseInvolutive r in
 465 |        Refl
 466 | 
 467 | -- Proof that `(++)` and `tailRecAppend` do the same thing, so the %transform
 468 | -- directive is safe.
 469 | tailRecAppendIsAppend : (sx, sy : SnocList a) -> tailRecAppend sx sy = sx ++ sy
 470 | tailRecAppendIsAppend sx Lin = Refl
 471 | tailRecAppendIsAppend sx (sy :< y) =
 472 |   trans (snocTailRecAppend y sx sy) (cong (:< y) $ tailRecAppendIsAppend sx sy)
 473 | 
 474 | ||| `reverseOnto` reverses the snoc list and prepends it to the "onto" argument
 475 | export
 476 | revOnto : (xs, vs : SnocList a) -> reverseOnto xs vs = xs ++ reverse vs
 477 | revOnto _ [<] = Refl
 478 | revOnto xs (vs :< v) =
 479 |   do rewrite revOnto (xs :< v) vs
 480 |      rewrite sym $ appendAssociative xs [<v] (reverse vs)
 481 |      rewrite revOnto [<v] vs
 482 |      Refl
 483 |