comparison lib/ur/list.ur @ 1634:f4cb4eebf7ae

Some new List functions, based on code by Ron de Bruijn
author Adam Chlipala <adam@chlipala.net>
date Sun, 11 Dec 2011 15:02:55 -0500
parents 553a5cc3a4b5
children a613cae954ca
comparison
equal deleted inserted replaced
1633:deeeb036c8ed 1634:f4cb4eebf7ae
265 foldlMi' (i + 1) acc ls 265 foldlMi' (i + 1) acc ls
266 in 266 in
267 foldlMi' 0 267 foldlMi' 0
268 end 268 end
269 269
270 fun filterM [m] (_ : monad m) [a] (p : a -> m bool) =
271 let
272 fun filterM' (acc : list a) (xs : list a) : m (list a) =
273 case xs of
274 [] => return (rev acc)
275 | x :: xs =>
276 c <- p x;
277 filterM' (if c then x :: acc else acc) xs
278 in
279 filterM' []
280 end
281
270 fun all [m] f = 282 fun all [m] f =
271 let 283 let
272 fun all' ls = 284 fun all' ls =
273 case ls of 285 case ls of
274 [] => True 286 [] => True
391 | Some _ => ls 403 | Some _ => ls
392 404
393 fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r) 405 fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r)
394 = @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs => 406 = @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs =>
395 x :: xs) [] fl 407 x :: xs) [] fl
408
409 fun take [a] (n : int) (xs : list a) : list a =
410 if n <= 0 then
411 []
412 else
413 case xs of
414 [] => []
415 | x :: xs => x :: take (n-1) xs
416
417 fun drop [a] (n : int) (xs : list a) : list a =
418 if n <= 0 then
419 xs
420 else
421 case xs of
422 [] => []
423 | x :: xs => drop (n-1) xs
424
425 fun splitAt [a] (n : int) (xs : list a) : list a * list a =
426 (take n xs, drop n xs)