Mercurial > urweb

annotate lib/ur/list.ur @ 2117:f1c4edf0a655

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New release
author Adam Chlipala <adam@chlipala.net>
date Sat, 14 Feb 2015 08:17:36 -0500
parents d9f918b79b5a
children
rev   line source
adamc@794 1 datatype t = datatype Basis.list
adamc@794 2
adamc@826 3 val show = fn [a] (_ : show a) =>
adamc@826 4 let
adamc@826 5 fun show' (ls : list a) =
adamc@826 6 case ls of
adamc@826 7 [] => "[]"
adamc@826 8 | x :: ls => show x ^ " :: " ^ show' ls
adamc@826 9 in
adamc@826 10 mkShow show'
adamc@826 11 end
adamc@794 12
adamc@846 13 val eq = fn [a] (_ : eq a) =>
adamc@846 14 let
adamc@846 15 fun eq' (ls1 : list a) ls2 =
adamc@846 16 case (ls1, ls2) of
adamc@846 17 ([], []) => True
adamc@846 18 | (x1 :: ls1, x2 :: ls2) => x1 = x2 && eq' ls1 ls2
adamc@846 19 | _ => False
adamc@846 20 in
adamc@846 21 mkEq eq'
adamc@846 22 end
adamc@846 23
adamc@1057 24 fun foldl [a] [b] (f : a -> b -> b) =
adamc@845 25 let
adamc@845 26 fun foldl' acc ls =
adamc@845 27 case ls of
adamc@845 28 [] => acc
adamc@845 29 | x :: ls => foldl' (f x acc) ls
adamc@845 30 in
adamc@845 31 foldl'
adamc@845 32 end
adamc@845 33
adamc@1057 34 val rev = fn [a] =>
adamc@1057 35 let
adamc@1057 36 fun rev' acc (ls : list a) =
adamc@1057 37 case ls of
adamc@1057 38 [] => acc
adamc@1057 39 | x :: ls => rev' (x :: acc) ls
adamc@1057 40 in
adamc@1057 41 rev' []
adamc@1057 42 end
adamc@1057 43
adamc@1057 44 fun foldr [a] [b] f (acc : b) (ls : list a) = foldl f acc (rev ls)
adamc@1057 45
adamc@850 46 fun foldlAbort [a] [b] f =
adamc@846 47 let
adamc@850 48 fun foldlAbort' acc ls =
adamc@846 49 case ls of
adamc@846 50 [] => Some acc
adamc@846 51 | x :: ls =>
adamc@846 52 case f x acc of
adamc@846 53 None => None
adamc@850 54 | Some acc' => foldlAbort' acc' ls
adamc@846 55 in
adamc@850 56 foldlAbort'
adamc@846 57 end
adamc@846 58
adamc@916 59 val length = fn [a] =>
adamc@916 60 let
adamc@916 61 fun length' acc (ls : list a) =
adamc@916 62 case ls of
adamc@916 63 [] => acc
adamc@916 64 | _ :: ls => length' (acc + 1) ls
adamc@916 65 in
adamc@916 66 length' 0
adamc@916 67 end
adamc@916 68
adamc@850 69 fun foldlMapAbort [a] [b] [c] f =
adamc@850 70 let
adamc@850 71 fun foldlMapAbort' ls' acc ls =
adamc@850 72 case ls of
adamc@850 73 [] => Some (rev ls', acc)
adamc@850 74 | x :: ls =>
adamc@850 75 case f x acc of
adamc@850 76 None => None
adamc@850 77 | Some (x', acc') => foldlMapAbort' (x' :: ls') acc' ls
adamc@850 78 in
adamc@850 79 foldlMapAbort' []
adamc@850 80 end
adamc@850 81
adamc@826 82 val revAppend = fn [a] =>
adamc@826 83 let
adamc@826 84 fun ra (ls : list a) acc =
adamc@826 85 case ls of
adamc@826 86 [] => acc
adamc@826 87 | x :: ls => ra ls (x :: acc)
adamc@826 88 in
adamc@826 89 ra
adamc@826 90 end
adamc@821 91
adamc@826 92 fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
adamc@821 93
adamc@826 94 fun mp [a] [b] f =
adamc@794 95 let
adamc@794 96 fun mp' acc ls =
adamc@794 97 case ls of
adamc@794 98 [] => rev acc
adamc@794 99 | x :: ls => mp' (f x :: acc) ls
adamc@794 100 in
adamc@794 101 mp' []
adamc@794 102 end
adamc@796 103
adamc@1279 104 fun mapi [a] [b] f =
adamc@1279 105 let
adamc@1279 106 fun mp' n acc ls =
adamc@1279 107 case ls of
adamc@1279 108 [] => rev acc
adamc@1279 109 | x :: ls => mp' (n + 1) (f n x :: acc) ls
adamc@1279 110 in
adamc@1279 111 mp' 0 []
adamc@1279 112 end
adamc@1279 113
adamc@826 114 fun mapPartial [a] [b] f =
adamc@821 115 let
adamc@821 116 fun mp' acc ls =
adamc@821 117 case ls of
adamc@821 118 [] => rev acc
adamc@821 119 | x :: ls => mp' (case f x of
adamc@821 120 None => acc
adamc@821 121 | Some y => y :: acc) ls
adamc@821 122 in
adamc@821 123 mp' []
adamc@821 124 end
adamc@821 125
adamc@826 126 fun mapX [a] [ctx ::: {Unit}] f =
adamc@796 127 let
adamc@796 128 fun mapX' ls =
adamc@796 129 case ls of
adamc@796 130 [] => <xml/>
adamc@796 131 | x :: ls => <xml>{f x}{mapX' ls}</xml>
adamc@796 132 in
adamc@796 133 mapX'
adamc@796 134 end
adamc@800 135
adam@1539 136 fun mapXi [a] [ctx ::: {Unit}] f =
adam@1539 137 let
adam@1539 138 fun mapX' i ls =
adam@1539 139 case ls of
adam@1539 140 [] => <xml/>
adam@1539 141 | x :: ls => <xml>{f i x}{mapX' (i + 1) ls}</xml>
adam@1539 142 in
adam@1539 143 mapX' 0
adam@1539 144 end
adam@1539 145
adamc@826 146 fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@800 147 let
adamc@800 148 fun mapM' acc ls =
adamc@800 149 case ls of
adamc@818 150 [] => return (rev acc)
adamc@818 151 | x :: ls => x' <- f x; mapM' (x' :: acc) ls
adamc@800 152 in
adamc@818 153 mapM' []
adamc@800 154 end
adamc@821 155
adamc@1107 156 fun mapPartialM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
adamc@1107 157 let
adamc@1107 158 fun mapPartialM' acc ls =
adamc@1107 159 case ls of
adamc@1107 160 [] => return (rev acc)
adamc@1107 161 | x :: ls =>
adamc@1107 162 v <- f x;
adamc@1107 163 mapPartialM' (case v of
adamc@1107 164 None => acc
adamc@1107 165 | Some x' => x' :: acc) ls
adamc@1107 166 in
adamc@1107 167 mapPartialM' []
adamc@1107 168 end
adamc@1107 169
adamc@830 170 fun mapXM [m ::: (Type -> Type)] (_ : monad m) [a] [ctx ::: {Unit}] f =
adamc@830 171 let
adamc@830 172 fun mapXM' ls =
adamc@830 173 case ls of
adamc@830 174 [] => return <xml/>
adamc@830 175 | x :: ls =>
adamc@830 176 this <- f x;
adamc@830 177 rest <- mapXM' ls;
adamc@830 178 return <xml>{this}{rest}</xml>
adamc@830 179 in
adamc@830 180 mapXM'
adamc@830 181 end
adamc@830 182
adamc@826 183 fun filter [a] f =
adamc@821 184 let
adamc@821 185 fun fil acc ls =
adamc@821 186 case ls of
adamc@821 187 [] => rev acc
adamc@821 188 | x :: ls => fil (if f x then x :: acc else acc) ls
adamc@821 189 in
adamc@821 190 fil []
adamc@821 191 end
adamc@822 192
adamc@826 193 fun exists [a] f =
adamc@822 194 let
adamc@822 195 fun ex ls =
adamc@822 196 case ls of
adamc@822 197 [] => False
adamc@822 198 | x :: ls =>
adamc@822 199 if f x then
adamc@822 200 True
adamc@822 201 else
adamc@822 202 ex ls
adamc@822 203 in
adamc@822 204 ex
adamc@822 205 end
adamc@822 206
adamc@826 207 fun foldlMap [a] [b] [c] f =
adamc@822 208 let
adamc@822 209 fun fold ls' st ls =
adamc@822 210 case ls of
adamc@822 211 [] => (rev ls', st)
adamc@822 212 | x :: ls =>
adamc@822 213 case f x st of
adamc@822 214 (y, st) => fold (y :: ls') st ls
adamc@822 215 in
adamc@822 216 fold []
adamc@822 217 end
adamc@839 218
adam@2095 219 fun mem [a] (_ : eq a) (x : a) =
adam@2095 220 let
adam@2095 221 fun mm ls =
adam@2095 222 case ls of
adam@2095 223 [] => False
adam@2095 224 | y :: ls => y = x || mm ls
adam@2095 225 in
adam@2095 226 mm
adam@2095 227 end
adam@2095 228
adam@1519 229 fun find [a] f =
adam@1519 230 let
adam@1519 231 fun find' ls =
adam@1519 232 case ls of
adam@1519 233 [] => None
adam@1519 234 | x :: ls =>
adam@1519 235 if f x then
adam@1519 236 Some x
adam@1519 237 else
adam@1519 238 find' ls
adam@1519 239 in
adam@1519 240 find'
adam@1519 241 end
adam@1519 242
adamc@839 243 fun search [a] [b] f =
adamc@839 244 let
adamc@839 245 fun search' ls =
adamc@839 246 case ls of
adamc@839 247 [] => None
adamc@839 248 | x :: ls =>
adamc@839 249 case f x of
adamc@839 250 None => search' ls
adamc@839 251 | v => v
adamc@839 252 in
adamc@839 253 search'
adamc@839 254 end
adamc@839 255
adamc@840 256 fun foldlM [m] (_ : monad m) [a] [b] f =
adamc@840 257 let
adamc@840 258 fun foldlM' acc ls =
adamc@840 259 case ls of
adamc@840 260 [] => return acc
adamc@840 261 | x :: ls =>
adamc@840 262 acc <- f x acc;
adamc@840 263 foldlM' acc ls
adamc@840 264 in
adamc@840 265 foldlM'
adamc@840 266 end
adamc@843 267
adam@1547 268 fun foldlMi [m] (_ : monad m) [a] [b] f =
adam@1547 269 let
adam@1547 270 fun foldlMi' i acc ls =
adam@1547 271 case ls of
adam@1547 272 [] => return acc
adam@1547 273 | x :: ls =>
adam@1547 274 acc <- f i x acc;
adam@1547 275 foldlMi' (i + 1) acc ls
adam@1547 276 in
adam@1547 277 foldlMi' 0
adam@1547 278 end
adam@1547 279
adam@1634 280 fun filterM [m] (_ : monad m) [a] (p : a -> m bool) =
adam@1634 281 let
adam@1634 282 fun filterM' (acc : list a) (xs : list a) : m (list a) =
adam@1634 283 case xs of
adam@1634 284 [] => return (rev acc)
adam@1634 285 | x :: xs =>
adam@1634 286 c <- p x;
adam@1634 287 filterM' (if c then x :: acc else acc) xs
adam@1634 288 in
adam@1634 289 filterM' []
adam@1634 290 end
adam@1634 291
adamc@843 292 fun all [m] f =
adamc@843 293 let
adamc@843 294 fun all' ls =
adamc@843 295 case ls of
adamc@843 296 [] => True
adamc@843 297 | x :: ls => f x && all' ls
adamc@843 298 in
adamc@843 299 all'
adamc@843 300 end
adamc@844 301
adamc@844 302 fun app [m] (_ : monad m) [a] f =
adamc@844 303 let
adamc@844 304 fun app' ls =
adamc@844 305 case ls of
adamc@844 306 [] => return ()
adamc@844 307 | x :: ls =>
adamc@844 308 f x;
adamc@844 309 app' ls
adamc@844 310 in
adamc@844 311 app'
adamc@844 312 end
adamc@845 313
adamc@908 314 fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adam@1394 315 [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@908 316 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
adamc@995 317 ls <- query q
adamc@995 318 (fn fs acc => return (f fs :: acc))
adamc@995 319 [];
adamc@995 320 return (rev ls)
adamc@908 321
adamc@1107 322 fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adam@1394 323 [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@1107 324 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) =
adamc@1107 325 ls <- query q
adamc@1107 326 (fn fs acc => v <- f fs; return (v :: acc))
adamc@1107 327 [];
adamc@1107 328 return (rev ls)
adamc@1107 329
adamc@1107 330 fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adam@1394 331 [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@1107 332 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) =
adamc@1107 333 ls <- query q
adamc@1107 334 (fn fs acc => v <- f fs;
adamc@1107 335 return (case v of
adamc@1107 336 None => acc
adamc@1107 337 | Some v => v :: acc))
adamc@1107 338 [];
adamc@1107 339 return (rev ls)
adamc@1107 340
adam@1321 341 fun sort [a] (gt : a -> a -> bool) (ls : t a) : t a =
adam@1321 342 let
adam@1321 343 fun split ls acc1 acc2 =
adam@1321 344 case ls of
adam@1321 345 [] => (rev acc1, rev acc2)
adam@1321 346 | x :: [] => (rev (x :: acc1), rev acc2)
adam@1321 347 | x1 :: x2 :: ls' => split ls' (x1 :: acc1) (x2 :: acc2)
adam@1321 348
adam@1321 349 fun merge ls1 ls2 acc =
adam@1321 350 case (ls1, ls2) of
adam@1321 351 ([], _) => revAppend acc ls2
adam@1321 352 | (_, []) => revAppend acc ls1
adam@1321 353 | (x1 :: ls1', x2 :: ls2') => if gt x1 x2 then merge ls1 ls2' (x2 :: acc) else merge ls1' ls2 (x1 :: acc)
adam@1321 354
adam@1321 355 fun sort' ls =
adam@1321 356 case ls of
adam@1321 357 [] => ls
adam@1321 358 | _ :: [] => ls
adam@1321 359 | _ =>
adam@1321 360 let
adam@1321 361 val (ls1, ls2) = split ls [] []
adam@1321 362 in
adam@1321 363 merge (sort' ls1) (sort' ls2) []
adam@1321 364 end
adam@1321 365 in
adam@1321 366 sort' ls
adam@1321 367 end
adam@1321 368
adam@1322 369 val nth [a] =
adam@1322 370 let
adam@1322 371 fun nth (ls : list a) (n : int) : option a =
adam@1322 372 case ls of
adam@1322 373 [] => None
adam@1322 374 | x :: ls' =>
adam@1322 375 if n <= 0 then
adam@1322 376 Some x
adam@1322 377 else
adam@1322 378 nth ls' (n-1)
adam@1322 379 in
adam@1322 380 nth
adam@1322 381 end
adam@1322 382
adam@1345 383 fun replaceNth [a] (ls : list a) (n : int) (v : a) : list a =
adam@1345 384 let
adam@1345 385 fun repNth (ls : list a) (n : int) (acc : list a) =
adam@1345 386 case ls of
adam@1345 387 [] => rev acc
adam@1345 388 | x :: ls' => if n <= 0 then
adam@1345 389 revAppend acc (v :: ls')
adam@1345 390 else
adam@1345 391 repNth ls' (n-1) (x :: acc)
adam@1345 392 in
adam@1345 393 repNth ls n []
adam@1345 394 end
adam@1345 395
adamc@845 396 fun assoc [a] [b] (_ : eq a) (x : a) =
adamc@845 397 let
adamc@845 398 fun assoc' (ls : list (a * b)) =
adamc@845 399 case ls of
adamc@845 400 [] => None
adamc@845 401 | (y, z) :: ls =>
adamc@845 402 if x = y then
adamc@845 403 Some z
adamc@845 404 else
adamc@845 405 assoc' ls
adamc@845 406 in
adamc@845 407 assoc'
adamc@845 408 end
adamc@845 409
adamc@845 410 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
adamc@845 411 case assoc x ls of
adamc@845 412 None => (x, y) :: ls
adamc@845 413 | Some _ => ls
greenrd@1481 414
greenrd@1481 415 fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r)
greenrd@1481 416 = @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs =>
greenrd@1481 417 x :: xs) [] fl
adam@1634 418
adam@1634 419 fun take [a] (n : int) (xs : list a) : list a =
adam@1634 420 if n <= 0 then
adam@1634 421 []
adam@1634 422 else
adam@1634 423 case xs of
adam@1634 424 [] => []
adam@1634 425 | x :: xs => x :: take (n-1) xs
adam@1634 426
adam@1634 427 fun drop [a] (n : int) (xs : list a) : list a =
adam@1634 428 if n <= 0 then
adam@1634 429 xs
adam@1634 430 else
adam@1634 431 case xs of
adam@1634 432 [] => []
adam@1634 433 | x :: xs => drop (n-1) xs
adam@1634 434
adam@1634 435 fun splitAt [a] (n : int) (xs : list a) : list a * list a =
adam@1634 436 (take n xs, drop n xs)
adam@1768 437
adam@1768 438 fun mapXiM [m ::: Type -> Type] (_ : monad m) [a] [ctx ::: {Unit}] (f : int -> a -> m (xml ctx [] [])) : t a -> m (xml ctx [] []) =
adam@1768 439 let
adam@1768 440 fun mapXiM' i ls =
adam@1768 441 case ls of
adam@1768 442 [] => return <xml/>
adam@1768 443 | x :: ls =>
adam@1768 444 this <- f i x;
adam@1768 445 rest <- mapXiM' (i+1) ls;
adam@1768 446 return <xml>{this}{rest}</xml>
adam@1768 447 in
adam@1768 448 mapXiM' 0
adam@1768 449 end
adam@1840 450
adam@1840 451 fun tabulateM [m] (_ : monad m) [a] (f : int -> m a) n =
adam@1840 452 let
adam@1840 453 fun tabulate' n acc =
adam@1840 454 if n <= 0 then
adam@1840 455 return acc
adam@1840 456 else
adam@1840 457 (v <- f (n-1);
adam@1840 458 tabulate' (n-1) (v :: acc))
adam@1840 459 in
adam@1840 460 tabulate' n []
adam@1840 461 end