0 | ||| Operations on `SnocList`s, analogous to the `List` ones.
  1 | ||| Depending on your style of programming, these might cause
  2 | ||| ambiguities, so import with care
  3 | module Data.SnocList.Operations
  4 |
  5 | import Data.SnocList
  6 | import Data.List
  7 | import Data.Nat
  8 | import Syntax.PreorderReasoning
  9 | import Syntax.PreorderReasoning.Generic
 10 |
 11 | %default total
 12 |
 13 | ||| Take `n` last elements from `sx`, returning the whole list if
 14 | ||| `n` >= length `sx`.
 15 | |||
 16 | ||| @ n  the number of elements to take
 17 | ||| @ sx the snoc-list to take the elements from
 18 | public export
 19 | takeTail : (n : Nat) -> (sx : SnocList a) -> SnocList a
 20 | takeTail (S n) (sx :< x) = takeTail n sx :< x
 21 | takeTail _ _ = [<]
 22 |
 23 | ||| Remove `n` last elements from `xs`, returning the empty list if
 24 | ||| `n >= length xs`
 25 | |||
 26 | ||| @ n  the number of elements to remove
 27 | ||| @ xs the list to drop the elements from
 28 | public export
 29 | dropTail : (n : Nat) -> (sx : SnocList a) -> SnocList a
 30 | dropTail  0    sx        = sx
 31 | dropTail (S n) [<]       = [<]
 32 | dropTail (S n) (sx :< x) = dropTail n sx
 33 |
 34 | public export
 35 | concatDropTailTakeTail : (n : Nat) -> (sx : SnocList a) ->
 36 |   dropTail n sx ++ takeTail n sx === sx
 37 | concatDropTailTakeTail 0 (sx :< x) = Refl
 38 | concatDropTailTakeTail (S n) (sx :< x) = cong (:< x) $ concatDropTailTakeTail n sx
 39 | concatDropTailTakeTail 0 [<] = Refl
 40 | concatDropTailTakeTail (S k) [<] = Refl
 41 |
 42 |
 43 | {- We can traverse a list while retaining both sides by decomposing it
 44 |    into a snoc-list and a cons-list
 45 | -}
 46 |
 47 | ||| Shift `n` elements from the beginning of `xs` to the end of `sx`,
 48 | ||| returning the same lists if `n` >= length `xs`.
 49 | |||
 50 | ||| @ n  the number of elements to take
 51 | ||| @ sx the snoc-list to append onto
 52 | ||| @ xs the list to take the elements from
 53 | public export
 54 | splitOntoLeft : (n : Nat) -> (sx : SnocList a) -> (xs : List a) -> (SnocList a, List a)
 55 | splitOntoLeft (S n) sx (x :: xs) = splitOntoLeft n (sx :< x) xs
 56 | splitOntoLeft _ sx xs = (sx, xs)
 57 |
 58 | ||| Shift `n` elements from the end of `sx` to the beginning of `xs`,
 59 | ||| returning the same lists if `n` >= length `sx`.
 60 | |||
 61 | ||| @ n  the number of elements to take
 62 | ||| @ sx the snoc-list to take the elements from
 63 | ||| @ xs the list to append onto
 64 | public export
 65 | splitOntoRight : (n : Nat) -> (sx : SnocList a) -> (xs : List a) -> (SnocList a, List a)
 66 | splitOntoRight (S n) (sx :< x) xs = splitOntoRight n sx (x :: xs)
 67 | splitOntoRight _ sx xs = (sx, xs)
 68 |
 69 | export
 70 | splitOntoRightInvariant : (n : Nat) -> (sx : SnocList a) -> (xs : List a) ->
 71 |   fst (splitOntoRight n sx xs) <>< snd (splitOntoRight n sx xs) === sx <>< xs
 72 | splitOntoRightInvariant (S n) (sx :< x) xs = splitOntoRightInvariant n sx (x :: xs)
 73 | splitOntoRightInvariant  0    sx  xs = Refl
 74 | splitOntoRightInvariant (S k) [<] xs = Refl
 75 |
 76 | export
 77 | splitOntoRightSpec : (n : Nat) -> (sx : SnocList a) -> (xs : List a) ->
 78 |   (fst (splitOntoRight n sx xs) === dropTail n sx, snd (splitOntoRight n sx xs) = takeTail n sx <>> xs)
 79 | splitOntoRightSpec (S k) (sx :< x) xs = splitOntoRightSpec k sx (x :: xs)
 80 | splitOntoRightSpec  0    sx        xs = (Refl, Refl)
 81 | splitOntoRightSpec (S k) [<]       xs = (Refl, Refl)
 82 |
 83 | export
 84 | splitOntoLeftSpec : (n : Nat) -> (sx : SnocList a) -> (xs : List a) ->
 85 |   (fst (splitOntoLeft n sx xs) === sx <>< take n xs, snd (splitOntoLeft n sx xs) = drop n xs)
 86 | splitOntoLeftSpec (S k) sx (x :: xs) = splitOntoLeftSpec k (sx :< x) xs
 87 | splitOntoLeftSpec  0    sx        xs = (Refl, Refl)
 88 | splitOntoLeftSpec (S k) sx [] = (Refl, Refl)
 89 |
 90 | export
 91 | lengthHomomorphism : (sx,sy : SnocList a) -> length (sx ++ sy) === length sx + length sy
 92 | lengthHomomorphism sx [<] = sym $ plusZeroRightNeutral _
 93 | lengthHomomorphism sx (sy :< x) = Calc $
 94 |   |~ 1 + (length (sx ++ sy))
 95 |   ~~ 1 + (length sx + length sy) ...(cong (1+) $ lengthHomomorphism _ _)
 96 |   ~~ length sx + (1 + length sy) ...(plusSuccRightSucc _ _)
 97 |
 98 | export
 99 | lengthDistributesOverFish : (sx : SnocList a) -> (ys : List a) ->
100 |                             length (sx <>< ys) === length sx + length ys
101 | lengthDistributesOverFish sx [] = sym $ plusZeroRightNeutral _
102 | lengthDistributesOverFish sx (y :: ys) = Calc $
103 |   |~ length ((sx :< y) <>< ys)
104 |   ~~ length (sx :< y) + length ys ...( lengthDistributesOverFish (sx :< y) ys)
105 |   ~~ S (length sx) + length ys    ...( Refl )
106 |   ~~ length sx + S (length ys)    ...( plusSuccRightSucc _ _ )
107 |   ~~ length sx + length (y :: ys) ...( Refl )
108 |
109 | -- cons-list operations on snoc-lists
110 |
111 | ||| Take `n` first elements from `sx`, returning the whole list if
112 | ||| `n` >= length `sx`.
113 | |||
114 | ||| @ n  the number of elements to take
115 | ||| @ sx the snoc-list to take the elements from
116 | |||
117 | ||| Note: traverses the whole the input list, so linear in `n` and
118 | ||| `length sx`
119 | public export
120 | take : (n : Nat) -> (sx : SnocList a) -> SnocList a
121 | take n sx = dropTail (length sx `minus` n) sx
122 |
123 | ||| Drop `n` first elements from `sx`, returning an empty list if
124 | ||| `n` >= length `sx`.
125 | |||
126 | ||| @ n  the number of elements to drop
127 | ||| @ sx the snoc-list to drop the elements from
128 | |||
129 | ||| Note: traverses the whole the input list, so linear in `n` and
130 | ||| `length sx`
131 | public export
132 | drop : (n : Nat) -> (sx : SnocList a) -> SnocList a
133 | drop n sx = takeTail (length sx `minus` n) sx
134 |
135 | public export
136 | data NonEmpty : SnocList a -> Type where
137 |   IsSnoc : NonEmpty (sx :< x)
138 |
139 | public export
140 | last : (sx : SnocList a) -> {auto 0 nonEmpty : NonEmpty sx} -> a
141 | last (sx :< x) {nonEmpty = IsSnoc} = x
142 |
143 | public export
144 | intersectBy : (a -> a -> Bool) -> SnocList a -> SnocList a -> SnocList a
145 | intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]
146 |
147 | public export
148 | intersect : Eq a => SnocList a -> SnocList a -> SnocList a
149 | intersect = intersectBy (==)
150 |