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 (S k) x = x ::: replicate k x
60 | cycle : List1 a -> Colist1 a
61 | cycle (x ::: xs) = x ::: cycle (xs ++ [x])
65 | iterate : (f : a -> a) -> a -> Colist1 a
66 | iterate f a = a ::: iterate f (f a)
71 | iterateMaybe : (f : a -> Maybe a) -> a -> Colist1 a
72 | iterateMaybe f a = a ::: iterateMaybe f (f a)
78 | unfold : (f : s -> Maybe (s,a)) -> s -> a -> Colist1 a
79 | unfold f s a = a ::: unfold f s
87 | forget : Colist1 a -> Colist a
88 | forget (h ::: t) = h :: t
92 | forgetInf : Inf (Colist1 a) -> Inf (Colist a)
93 | forgetInf (h ::: t) = h :: t
97 | cons : (x : a) -> (xs : Colist1 a) -> Colist1 a
98 | cons x xs = x ::: forget xs
102 | append : Colist1 a -> Colist1 a -> Colist1 a
103 | append (h ::: t) ys = h ::: append t (forget ys)
107 | lappend : List a -> Colist1 a -> Colist1 a
108 | lappend Nil ys = ys
109 | lappend (x :: xs) ys = x ::: lappend xs (forget ys)
113 | appendl : Colist1 a -> List a -> Colist1 a
114 | appendl (x ::: xs) ys = x ::: appendl xs ys
118 | uncons : Colist1 a -> (a, Colist a)
119 | uncons (h ::: tl) = (h, tl)
123 | head : Colist1 a -> a
128 | tail : Colist1 a -> Colist a
133 | take : (n : Nat) -> {auto 0 prf : IsSucc n} -> Colist1 a -> List1 a
134 | take (S k) (x ::: xs) = x ::: take k xs
139 | takeUntil : (p : a -> Bool) -> Colist1 a -> Colist1 a
140 | takeUntil p (x ::: xs) = if p x then singleton x else x ::: takeUntil p xs
145 | takeBefore : (p : a -> Bool) -> Colist1 a -> Colist a
146 | takeBefore p = takeBefore p . forget
151 | takeWhile : (p : a -> Bool) -> Colist1 a -> Colist a
152 | takeWhile p = takeWhile p . forget
157 | takeWhileJust : Colist1 (Maybe a) -> Colist a
158 | takeWhileJust = takeWhileJust . forget
162 | drop : (n : Nat) -> Colist1 a -> Colist a
163 | drop n = drop n . forget
167 | index : (n : Nat) -> Colist1 a -> Maybe a
168 | index n = index n . forget
175 | scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Colist1 b) -> Colist1 a
176 | scanl f acc (x ::: xs) = acc ::: scanl f (f acc x) xs
183 | Semigroup (Colist1 a) where
187 | Functor Colist1 where
188 | map f (x ::: xs) = f x ::: map f xs
191 | Applicative Colist1 where
194 | (f ::: fs) <*> (a ::: as) = f a ::: (fs <*> as)
196 | public export %hint %inline
197 | ZippableColist1 : Zippable Colist1
198 | ZippableColist1 = FromApplicative
209 | zig : List1 (Colist1 a) -> Colist (Colist1 a) -> Colist a
212 | zag : List1 a -> List (Colist1 a) -> Colist (Colist1 a) -> Colist a
214 | zig xs = zag (head <$> xs) (mapMaybe (fromColist . tail) $
forget xs)
216 | zag (x ::: []) [] [] = x :: []
217 | zag (x ::: []) (z :: zs) [] = x :: zig (z ::: zs) []
218 | zag (x ::: []) zs (l :: ls) = x :: zig (l ::: zs) ls
219 | zag (x ::: (y :: xs)) zs ls = x :: zag (y ::: xs) zs ls
222 | cantor : Colist1 (Colist1 a) -> Colist1 a
223 | cantor (xxs ::: []) = xxs
224 | cantor ((x ::: xs) ::: (yys :: zzss))
225 | = x ::: zig (yys ::: mapMaybe fromColist [xs]) zzss
230 | cantor : List (Colist a) -> Colist a
232 | let Just (l ::: ls) = List.toList1' $
mapMaybe fromColist xs
234 | in zig (l ::: []) (fromList ls)
239 | let nats : Colist Nat;
nats = fromStream Stream.nats in
240 | take 10 (Colist.cantor [ map (0,) nats
246 | , (2, 0), (1, 1), (0, 2)
247 | , (3, 0), (2, 1), (1, 2), (0, 3)
256 | planeWith : {0 p : a -> Type} ->
257 | ((x : a) -> p x -> c) ->
258 | Colist1 a -> ((x : a) -> Colist1 (p x)) ->
260 | planeWith k as f = cantor (map (\ x => map (k x) (f x)) as)
265 | plane : {0 p : a -> Type} ->
266 | Colist1 a -> ((x : a) -> Colist1 (p x)) ->
267 | Colist1 (x : a ** p x)
268 | plane = planeWith (\ x, prf => (
x ** prf)
)
275 | planeWith : (a -> b -> c) ->
276 | Colist1 a -> (a -> Colist1 b) ->
278 | planeWith k as f = cantor (map (\ x => map (k x) (f x)) as)
283 | plane : Colist1 a -> (a -> Colist1 b) -> Colist1 (a, b)
284 | plane = Pair.planeWith (,)
293 | let nats1 = fromStream Stream.nats in
294 | Colist1.take 10 (Pair.plane nats1 (const nats1))
297 | , (2, 0), (1, 1), (0, 2)
298 | , (3, 0), (2, 1), (1, 2), (0, 3)