0 | module Libraries.Data.SnocList.SizeOf
 1 |
 2 | import Data.SnocList
 3 | import Libraries.Data.SnocList.HasLength
 4 |
 5 | ---------------------------------------
 6 | -- horrible hack
 7 | import Libraries.Data.List.SizeOf as L
 8 |
 9 | public export
10 | 0 LSizeOf : {0 a : Type} -> List a -> Type
11 | LSizeOf xs = L.SizeOf xs
12 |
13 | %hide L.SizeOf
14 | ---------------------------------------
15 |
16 | %default total
17 |
18 | public export
19 | record SizeOf {a : Type} (sx : SnocList a) where
20 |   constructor MkSizeOf
21 |   size        : Nat
22 |   0 hasLength : HasLength size sx
23 |
24 | export
25 | 0 theList : SizeOf {a} sx -> SnocList a
26 | theList _ = sx
27 |
28 | public export
29 | Lin : SizeOf [<]
30 | Lin = MkSizeOf Z Z
31 |
32 | public export
33 | (:<) : SizeOf as -> (0 a : _) -> SizeOf (as :< a)
34 | MkSizeOf n p :< _ = MkSizeOf (S n) (S p)
35 |
36 | public export
37 | zero : SizeOf [<]
38 | zero = MkSizeOf Z Z
39 |
40 | public export
41 | suc : SizeOf as -> SizeOf (as :< a)
42 | suc (MkSizeOf n p) = MkSizeOf (S n) (S p)
43 |
44 | -- ||| suc but from the right
45 | export
46 | sucL : SizeOf as -> SizeOf ([<a] ++ as)
47 | sucL (MkSizeOf n p) = MkSizeOf (S n) (sucL p)
48 |
49 | public export
50 | (<><) : SizeOf {a} sx -> LSizeOf {a} ys -> SizeOf (sx <>< ys)
51 | MkSizeOf m p <>< MkSizeOf n q = MkSizeOf (n + m) (hlFish p q)
52 |
53 | public export
54 | (<>>) : SizeOf {a} sx -> LSizeOf {a} ys -> LSizeOf (sx <>> ys)
55 | MkSizeOf m p <>> MkSizeOf n q = MkSizeOf (m + n) (hlChips p q)
56 |
57 | export
58 | cast : LSizeOf {a} xs -> SizeOf {a} (cast xs)
59 | cast = ([<] <><)
60 |
61 | export
62 | (+) : SizeOf sx -> SizeOf sy -> SizeOf (sx ++ sy)
63 | MkSizeOf m p + MkSizeOf n q = MkSizeOf (n + m) (hlAppend p q)
64 |
65 | export
66 | mkSizeOf : (sx : SnocList a) -> SizeOf sx
67 | mkSizeOf sx = MkSizeOf (length sx) (mkHasLength sx)
68 |
69 | export
70 | reverse : SizeOf sx -> SizeOf (reverse sx)
71 | reverse (MkSizeOf n p) = MkSizeOf n (hlReverse p)
72 |
73 | export
74 | map : SizeOf sx -> SizeOf (map f sx)
75 | map (MkSizeOf n p) = MkSizeOf n (cast (sym $ lengthMap sx) p) where
76 |
77 |   lengthMap : (sx : _) -> SnocList.length (map f sx) === SnocList.length sx
78 |   lengthMap [<] = Refl
79 |   lengthMap (sx :< x) = cong S (lengthMap sx)
80 |
81 | {-
82 | public export
83 | take : {n : Nat} -> {0 sx : Stream a} -> SizeOf (take n sx)
84 | take = MkSizeOf n (take n sx)
85 | -}
86 |
87 | namespace SizedView
88 |
89 |   public export
90 |   data SizedView : SizeOf as -> Type where
91 |     Z : SizedView [<]
92 |     S : (n : SizeOf as) -> SizedView (n :< a)
93 |
94 | export
95 | sizedView : (p : SizeOf as) -> SizedView p
96 | sizedView (MkSizeOf Z Z)         = Z
97 | sizedView (MkSizeOf (S n) (S p)) = S (MkSizeOf n p)
98 |