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 | ||| Find the leftmost element of the snoc-list (the element added first).
 159 | |||
 160 | ||| This corresponds to the head of the list if the snoc-list were converted
 161 | ||| to a standard list.
 162 | |||
 163 | ||| Examples:
 164 | |||
 165 | ||| ```idris
 166 | ||| leftMost [<]
 167 | ||| -- Nothing
 168 | |||
 169 | ||| leftMost [< 1]
 170 | ||| -- Just 1
 171 | |||
 172 | ||| leftMost [< 1, 2, 3]
 173 | ||| -- Just 1
 174 | ||| ```
 175 | export
 176 | leftMost : SnocList a -> Maybe a
 177 | leftMost [<]       = Nothing
 178 | leftMost [<x]      = Just x
 179 | leftMost (xs :< _) = leftMost xs
 180 | 
 181 | ---------------------------
 182 | -- Zippable --
 183 | ---------------------------
 184 | 
 185 | public export
 186 | Zippable SnocList where
 187 |   zipWith _ [<] _ = [<]
 188 |   zipWith _ _ [<] = [<]
 189 |   zipWith f (xs :< x) (ys :< y) = zipWith f xs ys :< f x y
 190 | 
 191 |   zipWith3 _ [<] _ _ = [<]
 192 |   zipWith3 _ _ [<] _ = [<]
 193 |   zipWith3 _ _ _ [<] = [<]
 194 |   zipWith3 f (xs :< x) (ys :< y) (zs :< z) = zipWith3 f xs ys zs :< f x y z
 195 | 
 196 |   unzipWith f [<] = ([<], [<])
 197 |   unzipWith f (xs :< x) = let (bs, cs) = unzipWith f xs
 198 |                               (b, c) = f x
 199 |                           in (bs :< b, cs :< c)
 200 | 
 201 |   unzipWith3 f [<] = ([<], [<], [<])
 202 |   unzipWith3 f (xs :< x) = let (bs, cs, ds) = unzipWith3 f xs
 203 |                                (b, c, d) = f x
 204 |                            in  (bs :< b, cs :< c, ds :< d)
 205 | 
 206 | ------------------
 207 | --- Properties ---
 208 | ------------------
 209 | 
 210 | --- Usual snoc-list append (++) ---
 211 | 
 212 | export
 213 | appendAssociative : (l, c, r : SnocList a) -> l ++ (c ++ r) = (l ++ c) ++ r
 214 | appendAssociative l c [<]       = Refl
 215 | appendAssociative l c (sx :< _) = rewrite appendAssociative l c sx in Refl
 216 | 
 217 | export
 218 | appendLinLeftNeutral : (sx : SnocList a) -> [<] ++ sx = sx
 219 | appendLinLeftNeutral [<]       = Refl
 220 | appendLinLeftNeutral (sx :< _) = rewrite appendLinLeftNeutral sx in Refl
 221 | 
 222 | --- Fish (<><) and chips (<>>) appends ---
 223 | 
 224 | export
 225 | fishAsSnocAppend : (xs : SnocList a) -> (ys : List a) -> xs <>< ys = xs ++ cast ys
 226 | fishAsSnocAppend xs []        = Refl
 227 | fishAsSnocAppend xs (y :: ys) = do
 228 |   rewrite fishAsSnocAppend (xs :< y) ys
 229 |   rewrite fishAsSnocAppend [<y] ys
 230 |   rewrite appendAssociative xs [<y] (cast ys)
 231 |   Refl
 232 | 
 233 | export
 234 | chipsAsListAppend : (xs : SnocList a) -> (ys : List a) -> xs <>> ys = cast xs ++ ys
 235 | chipsAsListAppend [<]       ys = Refl
 236 | chipsAsListAppend (sx :< x) ys = do
 237 |   rewrite chipsAsListAppend sx (x :: ys)
 238 |   rewrite chipsAsListAppend sx [x]
 239 |   rewrite sym $ appendAssociative (cast sx) [x] ys
 240 |   Refl
 241 | 
 242 | --- More on append ---
 243 | 
 244 | export
 245 | toListAppend : (sx, sy : SnocList a) -> toList (sx ++ sy) = toList sx ++ toList sy
 246 | toListAppend sx [<] = rewrite appendNilRightNeutral $ toList sx in Refl
 247 | toListAppend sx (sy :< y) = do
 248 |   rewrite chipsAsListAppend sy [y]
 249 |   rewrite appendAssociative (cast sx) (cast sy) [y]
 250 |   rewrite chipsAsListAppend (sx ++ sy) [y]
 251 |   rewrite toListAppend sx sy
 252 |   Refl
 253 | 
 254 | export
 255 | castListAppend : (xs, ys : List a) -> cast {to=SnocList a} (xs ++ ys) === cast xs ++ cast ys
 256 | castListAppend []      ys = rewrite appendLinLeftNeutral $ [<] <>< ys in Refl
 257 | castListAppend (x::xs) ys = do
 258 |   rewrite fishAsSnocAppend [<x] (xs ++ ys)
 259 |   rewrite castListAppend xs ys
 260 |   rewrite appendAssociative [<x] (cast xs) (cast ys)
 261 |   rewrite sym $ fishAsSnocAppend [<x] xs
 262 |   Refl
 263 | 
 264 | --- Pure casts (including `toList`)
 265 | 
 266 | export
 267 | castToList : (sx : SnocList a) -> cast (toList sx) === sx
 268 | castToList [<]       = Refl
 269 | castToList (sx :< x) = do
 270 |   rewrite chipsAsListAppend sx [x]
 271 |   rewrite castListAppend (cast sx) [x]
 272 |   rewrite castToList sx
 273 |   Refl
 274 | 
 275 | export
 276 | toListCast : (xs : List a) -> toList (cast {to=SnocList a} xs) === xs
 277 | toListCast []      = Refl
 278 | toListCast (x::xs) = do
 279 |   rewrite fishAsSnocAppend [<x] xs
 280 |   rewrite toListAppend [<x] (cast xs)
 281 |   rewrite toListCast xs
 282 |   Refl
 283 | 
 284 | ||| Append an element to the head of a snoc-list.
 285 | ||| Note: Traverses the snoc-list, linear time complexity
 286 | public export
 287 | cons : a -> SnocList a -> SnocList a
 288 | cons x sx = [< x] ++ sx
 289 | 
 290 | --- Folds ---
 291 | 
 292 | export
 293 | foldAppend : (f : acc -> a -> acc) -> (init : acc) -> (sx, sy : SnocList a) -> foldl f init (sx ++ sy) = foldl f (foldl f init sx) sy
 294 | foldAppend f init sx [<]       = Refl
 295 | foldAppend f init sx (sy :< x) = rewrite foldAppend f init sx sy in Refl
 296 | 
 297 | export
 298 | snocFoldlAsListFoldl : (f : acc -> a -> acc) -> (init : acc) -> (xs : SnocList a) -> foldl f init xs = foldl f init (toList xs)
 299 | snocFoldlAsListFoldl f init [<]       = Refl
 300 | snocFoldlAsListFoldl f init (sx :< x) = do
 301 |   rewrite chipsAsListAppend sx [x]
 302 |   rewrite snocFoldlAsListFoldl f init sx
 303 |   rewrite foldlAppend f init (cast sx) [x]
 304 |   Refl
 305 | 
 306 | --- Filtering ---
 307 | 
 308 | export
 309 | filterAppend : (f : a -> Bool) -> (sx, sy : SnocList a) -> filter f (sx ++ sy) = filter f sx ++ filter f sy
 310 | filterAppend f sx [<]       = Refl
 311 | filterAppend f sx (sy :< x) with (f x)
 312 |   _ | False = filterAppend f sx sy
 313 |   _ | True  = rewrite filterAppend f sx sy in Refl
 314 | 
 315 | export
 316 | toListFilter : (f : a -> Bool) -> (sx : SnocList a) -> toList (filter f sx) = filter f (toList sx)
 317 | toListFilter f [<]       = Refl
 318 | toListFilter f (sx :< x) = do
 319 |   rewrite chipsAsListAppend sx [x]
 320 |   rewrite filterAppend f (cast sx) [x]
 321 |   rewrite filterStepLemma
 322 |   rewrite toListFilter f sx
 323 |   Refl
 324 |   where
 325 |     filterStepLemma : toList (filter f (sx :< x)) = toList (filter f sx) ++ filter f [x]
 326 |     filterStepLemma with (f x)
 327 |       _ | False = rewrite appendNilRightNeutral $ toList $ filter f sx in Refl
 328 |       _ | True  = rewrite chipsAsListAppend (filter f sx) [x] in Refl
 329 | 
 330 | export
 331 | filterCast : (f : a -> Bool) -> (xs : List a) -> filter f (cast {to=SnocList a} xs) = cast (filter f xs)
 332 | filterCast f []      = Refl
 333 | filterCast f (x::xs) = do
 334 |   rewrite fishAsSnocAppend [<x] xs
 335 |   rewrite filterAppend f [<x] (cast xs)
 336 |   rewrite filterStepLemma
 337 |   rewrite filterCast f xs
 338 |   Refl
 339 |   where
 340 |     filterStepLemma : cast (filter f (x::xs)) = filter f [<x] ++ cast (filter f xs)
 341 |     filterStepLemma with (f x)
 342 |       _ | False = rewrite appendLinLeftNeutral $ [<] <>< filter f xs in Refl
 343 |       _ | True  = rewrite fishAsSnocAppend [<x] (filter f xs) in Refl
 344 | 
 345 | --- Functor map ---
 346 | 
 347 | export
 348 | mapFusion : (g : b -> c) -> (f : a -> b) -> (sx : SnocList a) -> map g (map f sx) = map (g . f) sx
 349 | mapFusion g f [<]       = Refl
 350 | mapFusion g f (sx :< x) = rewrite mapFusion g f sx in Refl
 351 | 
 352 | export
 353 | mapAppend : (f : a -> b) -> (sx, sy : SnocList a) -> map f (sx ++ sy) = map f sx ++ map f sy
 354 | mapAppend f sx [<]       = Refl
 355 | mapAppend f sx (sy :< x) = rewrite mapAppend f sx sy in Refl
 356 | 
 357 | export
 358 | toListMap : (f : a -> b) -> (sx : SnocList a) -> toList (map f sx) = map f (toList sx)
 359 | toListMap f [<]       = Refl
 360 | toListMap f (sx :< x) = do
 361 |   rewrite chipsAsListAppend (map f sx) [f x]
 362 |   rewrite chipsAsListAppend sx [x]
 363 |   rewrite mapAppend f (toList sx) [x]
 364 |   rewrite toListMap f sx
 365 |   Refl
 366 | 
 367 | export
 368 | mapCast : (f : a -> b) -> (xs : List a) -> map f (cast {to=SnocList a} xs) = cast (map f xs)
 369 | mapCast f []      = Refl
 370 | mapCast f (x::xs) = do
 371 |   rewrite fishAsSnocAppend [<f x] (map f xs)
 372 |   rewrite fishAsSnocAppend [<x] xs
 373 |   rewrite mapAppend f [<x] (cast xs)
 374 |   rewrite mapCast f xs
 375 |   Refl
 376 | 
 377 | --- mapMaybe ---
 378 | 
 379 | export
 380 | mapMaybeFusion : (g : b -> Maybe c) -> (f : a -> Maybe b) -> (sx : SnocList a) -> mapMaybe g (mapMaybe f sx) = mapMaybe (f >=> g) sx
 381 | mapMaybeFusion g f [<]       = Refl
 382 | mapMaybeFusion g f (sx :< x) with (f x)
 383 |   _ | Nothing = mapMaybeFusion g f sx
 384 |   _ | (Just y) with (g y)
 385 |     _ | Nothing = mapMaybeFusion g f sx
 386 |     _ | (Just z) = rewrite mapMaybeFusion g f sx in Refl
 387 | 
 388 | export
 389 | mapMaybeAppend : (f : a -> Maybe b) -> (sx, sy : SnocList a) -> mapMaybe f (sx ++ sy) = mapMaybe f sx ++ mapMaybe f sy
 390 | mapMaybeAppend f sx [<]       = Refl
 391 | mapMaybeAppend f sx (sy :< x) with (f x)
 392 |   _ | Nothing = mapMaybeAppend f sx sy
 393 |   _ | (Just y) = rewrite mapMaybeAppend f sx sy in Refl
 394 | 
 395 | export
 396 | toListMapMaybe : (f : a -> Maybe b) -> (sx : SnocList a) -> toList (mapMaybe f sx) = mapMaybe f (toList sx)
 397 | toListMapMaybe f [<]       = Refl
 398 | toListMapMaybe f (sx :< x) = do
 399 |   rewrite chipsAsListAppend sx [x]
 400 |   rewrite mapMaybeAppend f (toList sx) [x]
 401 |   rewrite mapMaybeStepLemma
 402 |   rewrite toListMapMaybe f sx
 403 |   Refl
 404 |   where
 405 |     mapMaybeStepLemma : toList (mapMaybe f (sx :< x)) = toList (mapMaybe f sx) ++ mapMaybe f [x]
 406 |     mapMaybeStepLemma with (f x)
 407 |       _ | Nothing  = rewrite appendNilRightNeutral $ toList $ mapMaybe f sx in Refl
 408 |       _ | (Just y) = rewrite chipsAsListAppend (mapMaybe f sx) [y] in Refl
 409 | 
 410 | export
 411 | mapMaybeCast : (f : a -> Maybe b) -> (xs : List a) -> mapMaybe f (cast {to=SnocList a} xs) = cast (mapMaybe f xs)
 412 | mapMaybeCast f []      = Refl
 413 | mapMaybeCast f (x::xs) = do
 414 |   rewrite fishAsSnocAppend [<x] xs
 415 |   rewrite mapMaybeAppend f [<x] (cast xs)
 416 |   rewrite mapMaybeStepLemma
 417 |   rewrite mapMaybeCast f xs
 418 |   Refl
 419 |   where
 420 |     mapMaybeStepLemma : cast (mapMaybe f (x::xs)) = mapMaybe f [<x] ++ cast (mapMaybe f xs)
 421 |     mapMaybeStepLemma with (f x)
 422 |       _ | Nothing  = rewrite appendLinLeftNeutral $ [<] <>< mapMaybe f xs in Refl
 423 |       _ | (Just y) = rewrite fishAsSnocAppend [<y] (mapMaybe f xs) in Refl
 424 | 
 425 | 0 mapTRIsMap :  (f : a -> b) -> (sa : SnocList a) -> mapTR f sa === map f sa
 426 | mapTRIsMap f = lemma []
 427 |   where lemma :  (bs : List b)
 428 |               -> (sa : SnocList a)
 429 |               -> mapTR' bs f sa === (map f sa <>< bs)
 430 |         lemma bs Lin       = Refl
 431 |         lemma bs (sx :< x) = lemma (f x :: bs) sx
 432 | 
 433 | 
 434 | 0 mapMaybeTRIsMapMaybe :  (f : a -> Maybe b)
 435 |                        -> (sa : SnocList a)
 436 |                        -> mapMaybeTR f sa === mapMaybe f sa
 437 | mapMaybeTRIsMapMaybe f = lemma []
 438 |   where lemma :  (bs : List b)
 439 |               -> (sa : SnocList a)
 440 |               -> mapMaybeAppend bs f sa === (mapMaybe f sa <>< bs)
 441 |         lemma bs Lin = Refl
 442 |         lemma bs (sx :< x) with (f x)
 443 |           lemma bs (sx :< x) | Nothing = lemma bs sx
 444 |           lemma bs (sx :< x) | Just v  = lemma (v :: bs) sx
 445 | 
 446 | 0 filterTRIsFilter :  (f : a -> Bool)
 447 |                    -> (sa : SnocList a)
 448 |                    -> filterTR f sa === filter f sa
 449 | filterTRIsFilter f = lemma []
 450 |   where lemma :  (as : List a)
 451 |               -> (sa : SnocList a)
 452 |               -> filterAppend as f sa === (filter f sa <>< as)
 453 |         lemma as Lin = Refl
 454 |         lemma as (sx :< x) with (f x)
 455 |           lemma as (sx :< x) | False = lemma as sx
 456 |           lemma as (sx :< x) | True  = lemma (x :: as) sx
 457 | 
 458 | -- SnocList `reverse` applied to `reverseOnto` is equivalent to swapping the
 459 | -- arguments of `reverseOnto`.
 460 | reverseReverseOnto : (l, r : SnocList a) ->
 461 |                      reverse (reverseOnto l r) = reverseOnto r l
 462 | reverseReverseOnto _ Lin = Refl
 463 | reverseReverseOnto l (sx :< x) = reverseReverseOnto (l :< x) sx
 464 | 
 465 | ||| SnocList `reverse` applied twice yields the identity function.
 466 | export
 467 | reverseInvolutive : (sx : SnocList a) -> reverse (reverse sx) = sx
 468 | reverseInvolutive = reverseReverseOnto Lin
 469 | 
 470 | -- Appending `x` to `l` and then reversing the result onto `r` is the same as
 471 | -- using (::) with `x` and the result of reversing `l` onto `r`.
 472 | snocReverse : (x : a) -> (l, r : SnocList a) ->
 473 |               reverseOnto r l :< x = reverseOnto r (reverseOnto [<x] (reverse l))
 474 | snocReverse _ Lin _ = Refl
 475 | snocReverse x (sy :< y) r
 476 |   = rewrite snocReverse x sy (r :< y) in
 477 |       rewrite cong (reverseOnto r . reverse) $ snocReverse x sy [<y] in
 478 |         rewrite reverseInvolutive (reverseOnto [<x] (reverse sy) :< y) in
 479 |           Refl
 480 | 
 481 | -- Proof that it is safe to lift a (::) out of the first `tailRecAppend`
 482 | -- argument.
 483 | snocTailRecAppend : (x : a) -> (l, r : SnocList a) ->
 484 |                     tailRecAppend l (r :< x) = (tailRecAppend l r) :< x
 485 | snocTailRecAppend x l r =
 486 |   rewrite snocReverse x (reverse r) l in
 487 |     rewrite reverseInvolutive r in
 488 |        Refl
 489 | 
 490 | -- Proof that `(++)` and `tailRecAppend` do the same thing, so the %transform
 491 | -- directive is safe.
 492 | tailRecAppendIsAppend : (sx, sy : SnocList a) -> tailRecAppend sx sy = sx ++ sy
 493 | tailRecAppendIsAppend sx Lin = Refl
 494 | tailRecAppendIsAppend sx (sy :< y) =
 495 |   trans (snocTailRecAppend y sx sy) (cong (:< y) $ tailRecAppendIsAppend sx sy)
 496 | 
 497 | ||| `reverseOnto` reverses the snoc list and prepends it to the "onto" argument
 498 | export
 499 | revOnto : (xs, vs : SnocList a) -> reverseOnto xs vs = xs ++ reverse vs
 500 | revOnto _ [<] = Refl
 501 | revOnto xs (vs :< v) =
 502 |   do rewrite revOnto (xs :< v) vs
 503 |      rewrite sym $ appendAssociative xs [<v] (reverse vs)
 504 |      rewrite revOnto [<v] vs
 505 |      Refl
 506 |