0 | module Libraries.Data.SnocList.Extra
 1 |
 2 | import Data.Nat
 3 | import Data.SnocList
 4 | import Syntax.PreorderReasoning
 5 |
 6 | -- TODO left-to-right reversal of the stream
 7 | --      is this what we want?
 8 | {-
 9 | public export
10 | take : (n : Nat) -> (xs : Stream a) -> SnocList a
11 | take Z xs = [<]
12 | take (S k) (x :: xs) = take k xs :< x
13 | -}
14 |
15 | public export
16 | snocAppendFishAssociative :
17 |   (sx, sy : SnocList a) -> (zs : List a) ->
18 |   (sx ++ sy) <>< zs === sx ++ (sy <>< zs)
19 | snocAppendFishAssociative sx sy [] = Refl
20 | snocAppendFishAssociative sx sy (z :: zs)
21 |   = snocAppendFishAssociative sx (sy :< z) zs
22 |
23 | export
24 | snocAppendAsFish : (sx, sy : SnocList a) -> sx ++ sy === sx <>< (cast sy)
25 | snocAppendAsFish sx sy = sym
26 |   $ trans (fishAsSnocAppend sx (sy <>> []))
27 |           (cong (sx ++) (castToList sy))
28 |
29 | export
30 | lookup : Eq a => a -> SnocList (a, b) -> Maybe b
31 | lookup n [<] = Nothing
32 | lookup n (ns :< (x, n')) = if x == n then Just n' else lookup n ns
33 |
34 | lengthDistributesOverAppend
35 |   : (xs, ys : SnocList a)
36 |   -> length (ys ++ xs) = length xs + length ys
37 | lengthDistributesOverAppend [<] ys = Refl
38 | lengthDistributesOverAppend (xs :< x) ys =
39 |   cong S $ lengthDistributesOverAppend xs ys
40 |
41 | export
42 | lengthDistributesOverFish : (sx : SnocList a) -> (ys : List a) ->
43 |                             length (sx <>< ys) === length sx + length ys
44 | lengthDistributesOverFish sx [] = sym $ plusZeroRightNeutral _
45 | lengthDistributesOverFish sx (y :: ys) = Calc $
46 |   |~ length ((sx :< y) <>< ys)
47 |   ~~ length (sx :< y) + length ys ...( lengthDistributesOverFish (sx :< y) ys )
48 |   ~~ S (length sx) + length ys    ...( Refl )
49 |   ~~ length sx + S (length ys)    ...( plusSuccRightSucc _ _ )
50 |   ~~ length sx + length (y :: ys) ...( Refl )
51 |