Data.SnocList

A Reversed List

Definitions

asList : SnocList type -> List type

  Transform to a list but keeping the contents in the spine order (term depth).

Totality: total
Visibility: public export

isLin : SnocList a -> Bool

  True iff input is Lin

Totality: total
Visibility: public export

isSnoc : SnocList a -> Bool

  True iff input is (:<)

Totality: total
Visibility: public export

spanBy : (a -> Maybe b) -> SnocList a -> (SnocList a, SnocList b)

  Given a predicate and a snoclist, returns a tuple consisting of the longest
  prefix of the snoclist whose elements satisfy the predicate, and the rest of the
  snoclist.

Totality: total
Visibility: public export

mapImpl : (a -> b) -> SnocList a -> SnocList b

Totality: total
Visibility: public export

SnocBiinjective : Biinjective (:<)

Totality: total
Visibility: export

find : (a -> Bool) -> SnocList a -> Maybe a

  Find the rightmost element of the snoc-list that satisfies the predicate.

Totality: total
Visibility: public export

data InBounds : Nat -> SnocList a -> Type

  Satisfiable if `k` is a valid index into `xs`.
  
  @ k  the potential index
  @ xs the snoc-list into which k may be an index

Totality: total
Visibility: public export
Constructors:

InFirst : InBounds 0 (xs :< x)

  Z is a valid index into any cons cell

InLater : InBounds k xs -> InBounds (S k) (xs :< x)

  Valid indices can be extended

findIndex : (a -> Bool) -> (xs : SnocList a) -> Maybe (Fin (length xs))

  Find the index (counting from right) of the rightmost element (if exists) of a
  snoc-list that satisfies the given test, else `Nothing`.

Totality: total
Visibility: public export

appendAssociative : (l : SnocList a) -> (c : SnocList a) -> (r : SnocList a) -> l ++ (c ++ r) = (l ++ c) ++ r

Totality: total
Visibility: export

appendLinLeftNeutral : (sx : SnocList a) -> [<] ++ sx = sx

Totality: total
Visibility: export

fishAsSnocAppend : (xs : SnocList a) -> (ys : List a) -> xs <>< ys = xs ++ cast ys

Totality: total
Visibility: export

chipsAsListAppend : (xs : SnocList a) -> (ys : List a) -> xs <>> ys = cast xs ++ ys

Totality: total
Visibility: export

toListAppend : (sx : SnocList a) -> (sy : SnocList a) -> toList (sx ++ sy) = toList sx ++ toList sy

Totality: total
Visibility: export

castListAppend : (xs : List a) -> (ys : List a) -> cast (xs ++ ys) = cast xs ++ cast ys

Totality: total
Visibility: export

castToList : (sx : SnocList a) -> cast (toList sx) = sx

Totality: total
Visibility: export

toListCast : (xs : List a) -> toList (cast xs) = xs

Totality: total
Visibility: export

cons : a -> SnocList a -> SnocList a

  Append an element to the head of a snoc-list.
  Note: Traverses the snoc-list, linear time complexity

Totality: total
Visibility: public export

foldAppend : (f : (acc -> a -> acc)) -> (init : acc) -> (sx : SnocList a) -> (sy : SnocList a) -> foldl f init (sx ++ sy) = foldl f (foldl f init sx) sy

Totality: total
Visibility: export

snocFoldlAsListFoldl : (f : (acc -> a -> acc)) -> (init : acc) -> (xs : SnocList a) -> foldl f init xs = foldl f init (toList xs)

Totality: total
Visibility: export

filterAppend : (f : (a -> Bool)) -> (sx : SnocList a) -> (sy : SnocList a) -> filter f (sx ++ sy) = filter f sx ++ filter f sy

Totality: total
Visibility: export

toListFilter : (f : (a -> Bool)) -> (sx : SnocList a) -> toList (filter f sx) = filter f (toList sx)

Totality: total
Visibility: export

filterCast : (f : (a -> Bool)) -> (xs : List a) -> filter f (cast xs) = cast (filter f xs)

Totality: total
Visibility: export

mapFusion : (g : (b -> c)) -> (f : (a -> b)) -> (sx : SnocList a) -> map g (map f sx) = map (g . f) sx

Totality: total
Visibility: export

mapAppend : (f : (a -> b)) -> (sx : SnocList a) -> (sy : SnocList a) -> map f (sx ++ sy) = map f sx ++ map f sy

Totality: total
Visibility: export

toListMap : (f : (a -> b)) -> (sx : SnocList a) -> toList (map f sx) = map f (toList sx)

Totality: total
Visibility: export

mapCast : (f : (a -> b)) -> (xs : List a) -> map f (cast xs) = cast (map f xs)

Totality: total
Visibility: export

mapMaybeFusion : (g : (b -> Maybe c)) -> (f : (a -> Maybe b)) -> (sx : SnocList a) -> mapMaybe g (mapMaybe f sx) = mapMaybe (f >=> g) sx

Totality: total
Visibility: export

mapMaybeAppend : (f : (a -> Maybe b)) -> (sx : SnocList a) -> (sy : SnocList a) -> mapMaybe f (sx ++ sy) = mapMaybe f sx ++ mapMaybe f sy

Totality: total
Visibility: export

toListMapMaybe : (f : (a -> Maybe b)) -> (sx : SnocList a) -> toList (mapMaybe f sx) = mapMaybe f (toList sx)

Totality: total
Visibility: export

mapMaybeCast : (f : (a -> Maybe b)) -> (xs : List a) -> mapMaybe f (cast xs) = cast (mapMaybe f xs)

Totality: total
Visibility: export

reverseInvolutive : (sx : SnocList a) -> reverse (reverse sx) = sx

  SnocList `reverse` applied twice yields the identity function.

Totality: total
Visibility: export

revOnto : (xs : SnocList a) -> (vs : SnocList a) -> reverseOnto xs vs = xs ++ reverse vs

  `reverseOnto` reverses the snoc list and prepends it to the "onto" argument

Totality: total
Visibility: export