0 | module Data.SnocList.HasLength
 1 |
 2 | import Data.Nat
 3 | import Data.SnocList
 4 |
 5 | ---------------------------------------
 6 | -- horrible hack
 7 | import Data.List.HasLength as L
 8 |
 9 | public export
10 | LHasLength : Nat -> List a -> Type
11 | LHasLength = L.HasLength
12 | %hide L.HasLength
13 | ---------------------------------------
14 |
15 | public export
16 | data HasLength : Nat -> SnocList a -> Type where
17 |   Z : HasLength Z [<]
18 |   S : HasLength n sa -> HasLength (S n) (sa :< a)
19 |
20 | export
21 | hasLength : HasLength n sx -> length sx === n
22 | hasLength Z = Refl
23 | hasLength (S p) = cong S (hasLength p)
24 |
25 | export
26 | map : (f : a -> b) -> HasLength n xs -> HasLength n (map f xs)
27 | map f Z = Z
28 | map f (S hl) = S (map f hl)
29 |
30 | export
31 | sucL : HasLength n sx -> HasLength (S n) ([<x] ++ sx)
32 | sucL Z     = S Z
33 | sucL (S n) = S (sucL n)
34 |
35 | export
36 | sucR : HasLength n sx -> HasLength (S n) (sx ++ [<x])
37 | sucR = S
38 |
39 | export
40 | hlAppend : HasLength m sx -> HasLength n sy -> HasLength (n + m) (sx ++ sy)
41 | hlAppend sx Z = sx
42 | hlAppend sx (S sy) = S (hlAppend sx sy)
43 |
44 | export
45 | hlFish : HasLength m sx -> LHasLength n ys -> HasLength (n + m) (sx <>< ys)
46 | hlFish x Z = x
47 | hlFish {n = S n} x (S y) = rewrite plusSuccRightSucc n m in hlFish (S x) y
48 |
49 | export
50 | mkHasLength : (sx : SnocList a) -> HasLength (length sx) sx
51 | mkHasLength [<] = Z
52 | mkHasLength (sx :< _) = S (mkHasLength sx)
53 |
54 | export
55 | hlChips : HasLength m sx -> LHasLength n ys -> LHasLength (m + n) (sx <>> ys)
56 | hlChips Z y = y
57 | hlChips {m = S m} {n} (S x) y
58 |   = rewrite plusSuccRightSucc m n in
59 |     hlChips x (S y)
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 |