0 | module Libraries.Data.SnocList.HasLength
 1 |
 2 | import Data.Nat
 3 | ---------------------------------------
 4 | -- horrible hack
 5 | import Data.List.HasLength as L
 6 |
 7 | public export
 8 | LHasLength : Nat -> List a -> Type
 9 | LHasLength = L.HasLength
10 | %hide L.HasLength
11 | ---------------------------------------
12 |
13 | public export
14 | data HasLength : Nat -> SnocList a -> Type where
15 |   Z : HasLength Z [<]
16 |   S : HasLength n sa -> HasLength (S n) (sa :< a)
17 |
18 | export
19 | hasLength : HasLength n sx -> length sx === n
20 | hasLength Z = Refl
21 | hasLength (S p) = cong S (hasLength p)
22 |
23 | export
24 | sucR : HasLength n sx -> HasLength (S n) (sx ++ [<x])
25 | sucR = S
26 |
27 | export
28 | sucL : HasLength n sx -> HasLength (S n) ([<x] ++ sx)
29 | sucL Z     = S Z
30 | sucL (S n) = S (sucL n)
31 |
32 | export
33 | hlAppend : HasLength m sx -> HasLength n sy -> HasLength (n + m) (sx ++ sy)
34 | hlAppend sx Z = sx
35 | hlAppend sx (S sy) = S (hlAppend sx sy)
36 |
37 | export
38 | hlFish : HasLength m sx -> LHasLength n ys -> HasLength (n + m) (sx <>< ys)
39 | hlFish x Z = x
40 | hlFish {n = S n} x (S y) = rewrite plusSuccRightSucc n m in hlFish (S x) y
41 |
42 | export
43 | mkHasLength : (sx : SnocList a) -> HasLength (length sx) sx
44 | mkHasLength [<] = Z
45 | mkHasLength (sx :< _) = S (mkHasLength sx)
46 |
47 | export
48 | hlChips : HasLength m sx -> LHasLength n ys -> LHasLength (m + n) (sx <>> ys)
49 | hlChips Z y = y
50 | hlChips {m = S m} {n} (S x) y
51 |   = rewrite plusSuccRightSucc m n in
52 |     hlChips x (S y)
53 |
54 | {-
55 | export
56 | take : (n : Nat) -> (xs : Stream a) -> HasLength n (take n xs)
57 | take Z _ = Z
58 | take (S n) (x :: xs) = S (take n xs)
59 | -}
60 |
61 | export
62 | cast : {sy : _} -> (0 _ : SnocList.length sx = SnocList.length sy) ->
63 |        HasLength m sx -> HasLength m sy
64 | cast {sy = [<]} eq Z = Z
65 | cast {sy = sy :< _} eq (S p) = S (cast (injective eq) p)
66 |
67 | hlReverseOnto : HasLength m acc -> HasLength n sx -> HasLength (m + n) (reverseOnto acc sx)
68 | hlReverseOnto p Z = rewrite plusZeroRightNeutral m in p
69 | hlReverseOnto {n = S n} p (S q) = rewrite sym (plusSuccRightSucc m n) in hlReverseOnto (S p) q
70 |
71 | export
72 | hlReverse : HasLength m acc -> HasLength m (reverse acc)
73 | hlReverse = hlReverseOnto Z
74 |