0 | module Data.Colist
  1 |
  2 | import Data.List
  3 | import Data.List1
  4 | import public Data.Zippable
  5 |
  6 | %default total
  7 |
  8 | ||| A possibly finite Stream.
  9 | public export
 10 | data Colist : (a : Type) -> Type where
 11 |   Nil : Colist a
 12 |   (::) : a -> Inf (Colist a) -> Colist a
 13 |
 14 | --------------------------------------------------------------------------------
 15 | --          Creating Colists
 16 | --------------------------------------------------------------------------------
 17 |
 18 | ||| Convert a list to a `Colist`.
 19 | public export
 20 | fromList : List a -> Colist a
 21 | fromList []        = Nil
 22 | fromList (x :: xs) = x :: fromList xs
 23 |
 24 | ||| Convert a stream to a `Colist`.
 25 | public export
 26 | fromStream : Stream a -> Colist a
 27 | fromStream (x :: xs) = x :: fromStream xs
 28 |
 29 | ||| Create a `Colist` of only a single element.
 30 | public export
 31 | singleton : a -> Colist a
 32 | singleton a = a :: Nil
 33 |
 34 | ||| An infinite `Colist` of repetitions of the same element.
 35 | public export
 36 | repeat : a -> Colist a
 37 | repeat v = v :: repeat v
 38 |
 39 | ||| Create a `Colist` of `n` replications of the given element.
 40 | public export
 41 | replicate : Nat -> a -> Colist a
 42 | replicate 0     _ = Nil
 43 | replicate (S k) x = x :: replicate k x
 44 |
 45 | ||| Produce a `Colist` by repeating a sequence.
 46 | public export
 47 | cycle : List a -> Colist a
 48 | cycle Nil       = Nil
 49 | cycle (x :: xs) = run x xs
 50 |   where run : a -> List a -> Colist a
 51 |         run v []        = v :: run x xs
 52 |         run v (y :: ys) = v :: run y ys
 53 |
 54 | ||| Generate an infinite `Colist` by repeatedly applying a function.
 55 | public export
 56 | iterate : (a -> a) -> a -> Colist a
 57 | iterate f a = a :: iterate f (f a)
 58 |
 59 | ||| Generate a `Colist` by repeatedly applying a function.
 60 | ||| This stops once the function returns `Nothing`.
 61 | public export
 62 | iterateMaybe : (f : a -> Maybe a) -> Maybe a -> Colist a
 63 | iterateMaybe _ Nothing  = Nil
 64 | iterateMaybe f (Just x) = x :: iterateMaybe f (f x)
 65 |
 66 | ||| Generate an `Colist` by repeatedly applying a function
 67 | ||| to a seed value.
 68 | ||| This stops once the function returns `Nothing`.
 69 | public export
 70 | unfold : (f : s -> Maybe (s,a)) -> s -> Colist a
 71 | unfold f s = case f s of
 72 |                   Just (s2,a) => a :: unfold f s2
 73 |                   Nothing     => Nil
 74 |
 75 | --------------------------------------------------------------------------------
 76 | --          Basic Functions
 77 | --------------------------------------------------------------------------------
 78 |
 79 | ||| True, if this is the empty `Colist`.
 80 | public export
 81 | isNil : Colist a -> Bool
 82 | isNil [] = True
 83 | isNil _  = False
 84 |
 85 | ||| True, if the given `Colist` is non-empty.
 86 | public export
 87 | isCons : Colist a -> Bool
 88 | isCons [] = False
 89 | isCons _  = True
 90 |
 91 | ||| Concatenate two `Colist`s.
 92 | public export
 93 | append : Colist a -> Colist a -> Colist a
 94 | append []        ys = ys
 95 | append (x :: xs) ys = x :: append xs ys
 96 |
 97 | ||| Append a `Colist` to a `List`.
 98 | public export
 99 | lappend : List a -> Colist a -> Colist a
100 | lappend xs = append (fromList xs)
101 |
102 | ||| Append a `List` to a `Colist`.
103 | public export
104 | appendl : Colist a -> List a -> Colist a
105 | appendl xs = append xs . fromList
106 |
107 | ||| Try to extract the head and tail of a `Colist`.
108 | public export
109 | uncons : Colist a -> Maybe (a, Colist a)
110 | uncons [] = Nothing
111 | uncons (x :: xs) = Just (x, xs)
112 |
113 | ||| Try to extract the first element from a `Colist`.
114 | public export
115 | head : Colist a -> Maybe a
116 | head []       = Nothing
117 | head (x :: _) = Just x
118 |
119 | ||| Try to drop the first element from a `Colist`.
120 | ||| This returns `Nothing` if the given `Colist` is
121 | ||| empty.
122 | public export
123 | tail : Colist a -> Maybe (Colist a)
124 | tail []        = Nothing
125 | tail (_ :: xs) = Just xs
126 |
127 | ||| Take up to `n` elements from a `Colist`.
128 | public export
129 | take : (n : Nat) -> Colist a -> List a
130 | take 0     _         = Nil
131 | take (S k) []        = Nil
132 | take (S k) (x :: xs) = x :: take k xs
133 |
134 | ||| Take elements from a `Colist` up to and including the
135 | ||| first element, for which `p` returns `True`.
136 | public export
137 | takeUntil : (p : a -> Bool) -> Colist a -> Colist a
138 | takeUntil _ []        = Nil
139 | takeUntil p (x :: xs) = if p x then [x] else x :: takeUntil p xs
140 |
141 | ||| Take elements from a `Colist` up to (but not including) the
142 | ||| first element, for which `p` returns `True`.
143 | public export
144 | takeBefore : (a -> Bool) -> Colist a -> Colist a
145 | takeBefore _ []        = Nil
146 | takeBefore p (x :: xs) = if p x then [] else x :: takeBefore p xs
147 |
148 | ||| Take elements from a `Colist` while the given predicate
149 | ||| returns `True`.
150 | public export
151 | takeWhile : (a -> Bool) -> Colist a -> Colist a
152 | takeWhile p = takeBefore (not . p)
153 |
154 | ||| Extract all values wrapped in `Just` from the beginning
155 | ||| of a `Colist`. This stops, once the first `Nothing` is encountered.
156 | public export
157 | takeWhileJust : Colist (Maybe a) -> Colist a
158 | takeWhileJust []              = []
159 | takeWhileJust (Nothing :: _)  = []
160 | takeWhileJust (Just x  :: xs) = x :: takeWhileJust xs
161 |
162 | ||| Drop up to `n` elements from the beginning of the `Colist`.
163 | public export
164 | drop : (n : Nat) -> Colist a -> Colist a
165 | drop _ []            = Nil
166 | drop 0           xs  = xs
167 | drop (S k) (x :: xs) = drop k xs
168 |
169 | ||| Try to extract the `n`-th element from a `Colist`.
170 | public export
171 | index : (n : Nat) -> Colist a -> Maybe a
172 | index _     []        = Nothing
173 | index 0     (x :: _)  = Just x
174 | index (S k) (_ :: xs) = index k xs
175 |
176 | ||| Produce a `Colist` of left folds of prefixes of the given `Colist`.
177 | ||| @ f the combining function
178 | ||| @ acc the initial value
179 | ||| @ xs the `Colist` to process
180 | public export
181 | scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Colist b) -> Colist a
182 | scanl _ acc Nil       = [acc]
183 | scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
184 |
185 | --------------------------------------------------------------------------------
186 | -- InBounds and inBounds for Colists
187 | --------------------------------------------------------------------------------
188 |
189 | ||| Satisfiable if `k` is a valid index into `xs`
190 | |||
191 | ||| @ k the potential index
192 | ||| @ xs the Colist into which k may be an index
193 | public export
194 | data InBounds : (k : Nat) -> (xs : Colist a) -> Type where
195 |     ||| Z is a valid index into any cons cell
196 |     InFirst : {0 xs : Inf (Colist a)} -> InBounds Z (x :: xs)
197 |     ||| Valid indices can be extended
198 |     InLater : {0 xs : Inf (Colist a)} -> InBounds k xs -> InBounds (S k) (x :: xs)
199 |
200 | public export
201 | Uninhabited (Data.Colist.InBounds k []) where
202 |   uninhabited InFirst impossible
203 |   uninhabited (InLater _) impossible
204 |
205 | export
206 | Uninhabited (Colist.InBounds k xs) => Uninhabited (Colist.InBounds (S k) (x::xs)) where
207 |   uninhabited (InLater y) = uninhabited y
208 |
209 | ||| Decide whether `k` is a valid index into Colist `xs`
210 | public export
211 | inBounds : (k : Nat) -> (xs : Colist a) -> Dec (InBounds k xs)
212 | inBounds k [] = No uninhabited
213 | inBounds Z (x::xs) = Yes InFirst
214 | inBounds (S k) (x::xs) = case inBounds k xs of
215 |   Yes p => Yes $ InLater p
216 |   No up => No $ \(InLater p) => up p
217 |
218 | ||| Find a particular element of a Colist using InBounds
219 | |||
220 | ||| @ ok a proof that the index is within bounds
221 | public export
222 | index' : (k : Nat) -> (xs : Colist a) -> {auto 0 ok : InBounds k xs} -> a
223 | index' Z (x::_) {ok = InFirst} = x
224 | index' (S k) (_::xs) {ok = InLater _} = index' k xs
225 |
226 | --------------------------------------------------------------------------------
227 | --          Implementations
228 | --------------------------------------------------------------------------------
229 |
230 | public export
231 | Semigroup (Colist a) where
232 |   (<+>) = append
233 |
234 | public export
235 | Monoid (Colist a) where
236 |   neutral = Nil
237 |
238 | public export
239 | Functor Colist where
240 |   map f []        = []
241 |   map f (x :: xs) = f x :: map f xs
242 |
243 | public export
244 | Applicative Colist where
245 |   pure = repeat
246 |
247 |   [] <*> _  = []
248 |   _  <*> [] = []
249 |   f :: fs <*> a :: as = f a :: (fs <*> as)
250 |
251 | public export %hint %inline
252 | ZippableColist : Zippable Colist
253 | ZippableColist = FromApplicative
254 |