7 | import public Data.Zippable
13 | data Colist1 : (a : Type) -> Type where
14 | (:::) : a -> Colist a -> Colist1 a
22 | fromList1 : List1 a -> Colist1 a
23 | fromList1 (h ::: t) = h ::: fromList t
27 | fromStream : Stream a -> Colist1 a
28 | fromStream (x :: xs) = x ::: fromStream xs
33 | fromColist : Colist a -> Maybe (Colist1 a)
34 | fromColist Nil = Nothing
35 | fromColist (x :: xs) = Just (x ::: xs)
40 | fromList : List a -> Maybe (Colist1 a)
41 | fromList = fromColist . fromList
45 | singleton : a -> Colist1 a
46 | singleton a = a ::: Nil
50 | repeat : a -> Colist1 a
51 | repeat v = v ::: repeat v
55 | replicate : (n : Nat) -> {auto 0 prf : IsSucc n} -> a -> Colist1 a
56 | replicate 0 _ impossible
57 | replicate (S k) x = x ::: replicate k x
61 | cycle : List1 a -> Colist1 a
62 | cycle (x ::: xs) = x ::: cycle (xs ++ [x])
66 | iterate : (f : a -> a) -> a -> Colist1 a
67 | iterate f a = a ::: iterate f (f a)
72 | iterateMaybe : (f : a -> Maybe a) -> a -> Colist1 a
73 | iterateMaybe f a = a ::: iterateMaybe f (f a)
79 | unfold : (f : s -> Maybe (s,a)) -> s -> a -> Colist1 a
80 | unfold f s a = a ::: unfold f s
88 | forget : Colist1 a -> Colist a
89 | forget (h ::: t) = h :: t
93 | forgetInf : Inf (Colist1 a) -> Inf (Colist a)
94 | forgetInf (h ::: t) = h :: t
98 | cons : (x : a) -> (xs : Colist1 a) -> Colist1 a
99 | cons x xs = x ::: forget xs
103 | append : Colist1 a -> Colist1 a -> Colist1 a
104 | append (h ::: t) ys = h ::: append t (forget ys)
108 | lappend : List a -> Colist1 a -> Colist1 a
109 | lappend Nil ys = ys
110 | lappend (x :: xs) ys = x ::: lappend xs (forget ys)
114 | appendl : Colist1 a -> List a -> Colist1 a
115 | appendl (x ::: xs) ys = x ::: appendl xs ys
119 | uncons : Colist1 a -> (a, Colist a)
120 | uncons (h ::: tl) = (h, tl)
124 | head : Colist1 a -> a
129 | tail : Colist1 a -> Colist a
134 | take : (n : Nat) -> {auto 0 prf : IsSucc n} -> Colist1 a -> List1 a
135 | take 0 _ impossible
136 | take (S k) (x ::: xs) = x ::: take k xs
141 | takeUntil : (p : a -> Bool) -> Colist1 a -> Colist1 a
142 | takeUntil p (x ::: xs) = if p x then singleton x else x ::: takeUntil p xs
147 | takeBefore : (p : a -> Bool) -> Colist1 a -> Colist a
148 | takeBefore p = takeBefore p . forget
153 | takeWhile : (p : a -> Bool) -> Colist1 a -> Colist a
154 | takeWhile p = takeWhile p . forget
159 | takeWhileJust : Colist1 (Maybe a) -> Colist a
160 | takeWhileJust = takeWhileJust . forget
164 | drop : (n : Nat) -> Colist1 a -> Colist a
165 | drop n = drop n . forget
169 | index : (n : Nat) -> Colist1 a -> Maybe a
170 | index n = index n . forget
177 | scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Colist1 b) -> Colist1 a
178 | scanl f acc (x ::: xs) = acc ::: scanl f (f acc x) xs
185 | Semigroup (Colist1 a) where
189 | Functor Colist1 where
190 | map f (x ::: xs) = f x ::: map f xs
193 | Applicative Colist1 where
196 | (f ::: fs) <*> (a ::: as) = f a ::: (fs <*> as)
198 | public export %hint %inline
199 | ZippableColist1 : Zippable Colist1
200 | ZippableColist1 = FromApplicative
211 | zig : List1 (Colist1 a) -> Colist (Colist1 a) -> Colist a
214 | zag : List1 a -> List (Colist1 a) -> Colist (Colist1 a) -> Colist a
216 | zig xs = zag (head <$> xs) (mapMaybe (fromColist . tail) $
forget xs)
218 | zag (x ::: []) [] [] = x :: []
219 | zag (x ::: []) (z :: zs) [] = x :: zig (z ::: zs) []
220 | zag (x ::: []) zs (l :: ls) = x :: zig (l ::: zs) ls
221 | zag (x ::: (y :: xs)) zs ls = x :: zag (y ::: xs) zs ls
224 | cantor : Colist1 (Colist1 a) -> Colist1 a
225 | cantor (xxs ::: []) = xxs
226 | cantor ((x ::: xs) ::: (yys :: zzss))
227 | = x ::: zig (yys ::: mapMaybe fromColist [xs]) zzss
232 | cantor : List (Colist a) -> Colist a
234 | let Just (l ::: ls) = List.toList1' $
mapMaybe fromColist xs
236 | in zig (l ::: []) (fromList ls)
241 | let nats : Colist Nat;
nats = fromStream Stream.nats in
242 | take 10 (Colist.cantor [ map (0,) nats
248 | , (2, 0), (1, 1), (0, 2)
249 | , (3, 0), (2, 1), (1, 2), (0, 3)
258 | planeWith : {0 p : a -> Type} ->
259 | ((x : a) -> p x -> c) ->
260 | Colist1 a -> ((x : a) -> Colist1 (p x)) ->
262 | planeWith k as f = cantor (map (\ x => map (k x) (f x)) as)
267 | plane : {0 p : a -> Type} ->
268 | Colist1 a -> ((x : a) -> Colist1 (p x)) ->
269 | Colist1 (x : a ** p x)
270 | plane = planeWith (\ x, prf => (
x ** prf)
)
277 | planeWith : (a -> b -> c) ->
278 | Colist1 a -> (a -> Colist1 b) ->
280 | planeWith k as f = cantor (map (\ x => map (k x) (f x)) as)
285 | plane : Colist1 a -> (a -> Colist1 b) -> Colist1 (a, b)
286 | plane = Pair.planeWith (,)
295 | let nats1 = fromStream Stream.nats in
296 | Colist1.take 10 (Pair.plane nats1 (const nats1))
299 | , (2, 0), (1, 1), (0, 2)
300 | , (3, 0), (2, 1), (1, 2), (0, 3)