0 | module Libraries.Data.List.SizeOf
 1 |
 2 | import Data.List
 3 | import Data.List.HasLength
 4 | import Libraries.Data.List.HasLength
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | record SizeOf {a : Type} (xs : List a) where
10 |   constructor MkSizeOf
11 |   size        : Nat
12 |   0 hasLength : HasLength size xs
13 |
14 | export
15 | 0 theList : SizeOf {a} xs -> List a
16 | theList _ = xs
17 |
18 | public export
19 | zero : SizeOf []
20 | zero = MkSizeOf Z Z
21 |
22 | public export
23 | suc : SizeOf as -> SizeOf (a :: as)
24 | suc (MkSizeOf n p) = MkSizeOf (S n) (S p)
25 |
26 | -- ||| suc but from the right
27 | export
28 | sucR : SizeOf as -> SizeOf (as ++ [a])
29 | sucR (MkSizeOf n p) = MkSizeOf (S n) (sucR p)
30 |
31 | export
32 | (+) : SizeOf xs -> SizeOf ys -> SizeOf (xs ++ ys)
33 | MkSizeOf m p + MkSizeOf n q = MkSizeOf (m + n) (hasLengthAppend p q)
34 |
35 | export
36 | mkSizeOf : (xs : List a) -> SizeOf xs
37 | mkSizeOf xs = MkSizeOf (length xs) (hasLength xs)
38 |
39 | export
40 | reverse : SizeOf xs -> SizeOf (reverse xs)
41 | reverse (MkSizeOf n p) = MkSizeOf n (hasLengthReverse p)
42 |
43 | export
44 | map : SizeOf xs -> SizeOf (map f xs)
45 | map (MkSizeOf n p) = MkSizeOf n (cast (sym $ lengthMap xs) p)
46 |
47 | export
48 | take : {n : Nat} -> {0 xs : Stream a} -> SizeOf (take n xs)
49 | take = MkSizeOf n (take n xs)
50 |
51 | namespace SizedView
52 |
53 |   public export
54 |   data SizedView : SizeOf as -> Type where
55 |     Z : SizedView (MkSizeOf Z Z)
56 |     S : (n : SizeOf as) -> SizedView (suc {a} n)
57 |
58 | export
59 | sizedView : (p : SizeOf as) -> SizedView p
60 | sizedView (MkSizeOf Z Z)         = Z
61 | sizedView (MkSizeOf (S n) (S p)) = S (MkSizeOf n p)
62 |