Mercurial > urweb

annotate lib/ur/list.ur @ 1591:20f898c29525

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweaks to choices of source positions to use in error messages, including for subSgn
author Adam Chlipala <adam@chlipala.net>
date Sat, 05 Nov 2011 13:12:07 -0400
parents 553a5cc3a4b5
children f4cb4eebf7ae
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@1519 219 fun find [a] f =
adam@1519 220 let
adam@1519 221 fun find' ls =
adam@1519 222 case ls of
adam@1519 223 [] => None
adam@1519 224 | x :: ls =>
adam@1519 225 if f x then
adam@1519 226 Some x
adam@1519 227 else
adam@1519 228 find' ls
adam@1519 229 in
adam@1519 230 find'
adam@1519 231 end
adam@1519 232
adamc@839 233 fun search [a] [b] f =
adamc@839 234 let
adamc@839 235 fun search' ls =
adamc@839 236 case ls of
adamc@839 237 [] => None
adamc@839 238 | x :: ls =>
adamc@839 239 case f x of
adamc@839 240 None => search' ls
adamc@839 241 | v => v
adamc@839 242 in
adamc@839 243 search'
adamc@839 244 end
adamc@839 245
adamc@840 246 fun foldlM [m] (_ : monad m) [a] [b] f =
adamc@840 247 let
adamc@840 248 fun foldlM' acc ls =
adamc@840 249 case ls of
adamc@840 250 [] => return acc
adamc@840 251 | x :: ls =>
adamc@840 252 acc <- f x acc;
adamc@840 253 foldlM' acc ls
adamc@840 254 in
adamc@840 255 foldlM'
adamc@840 256 end
adamc@843 257
adam@1547 258 fun foldlMi [m] (_ : monad m) [a] [b] f =
adam@1547 259 let
adam@1547 260 fun foldlMi' i acc ls =
adam@1547 261 case ls of
adam@1547 262 [] => return acc
adam@1547 263 | x :: ls =>
adam@1547 264 acc <- f i x acc;
adam@1547 265 foldlMi' (i + 1) acc ls
adam@1547 266 in
adam@1547 267 foldlMi' 0
adam@1547 268 end
adam@1547 269
adamc@843 270 fun all [m] f =
adamc@843 271 let
adamc@843 272 fun all' ls =
adamc@843 273 case ls of
adamc@843 274 [] => True
adamc@843 275 | x :: ls => f x && all' ls
adamc@843 276 in
adamc@843 277 all'
adamc@843 278 end
adamc@844 279
adamc@844 280 fun app [m] (_ : monad m) [a] f =
adamc@844 281 let
adamc@844 282 fun app' ls =
adamc@844 283 case ls of
adamc@844 284 [] => return ()
adamc@844 285 | x :: ls =>
adamc@844 286 f x;
adamc@844 287 app' ls
adamc@844 288 in
adamc@844 289 app'
adamc@844 290 end
adamc@845 291
adamc@908 292 fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adam@1394 293 [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@908 294 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) =
adamc@995 295 ls <- query q
adamc@995 296 (fn fs acc => return (f fs :: acc))
adamc@995 297 [];
adamc@995 298 return (rev ls)
adamc@908 299
adamc@1107 300 fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adam@1394 301 [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@1107 302 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) =
adamc@1107 303 ls <- query q
adamc@1107 304 (fn fs acc => v <- f fs; return (v :: acc))
adamc@1107 305 [];
adamc@1107 306 return (rev ls)
adamc@1107 307
adamc@1107 308 fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type]
adam@1394 309 [tables ~ exps] (q : sql_query [] [] tables exps)
adamc@1107 310 (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) =
adamc@1107 311 ls <- query q
adamc@1107 312 (fn fs acc => v <- f fs;
adamc@1107 313 return (case v of
adamc@1107 314 None => acc
adamc@1107 315 | Some v => v :: acc))
adamc@1107 316 [];
adamc@1107 317 return (rev ls)
adamc@1107 318
adam@1321 319 fun sort [a] (gt : a -> a -> bool) (ls : t a) : t a =
adam@1321 320 let
adam@1321 321 fun split ls acc1 acc2 =
adam@1321 322 case ls of
adam@1321 323 [] => (rev acc1, rev acc2)
adam@1321 324 | x :: [] => (rev (x :: acc1), rev acc2)
adam@1321 325 | x1 :: x2 :: ls' => split ls' (x1 :: acc1) (x2 :: acc2)
adam@1321 326
adam@1321 327 fun merge ls1 ls2 acc =
adam@1321 328 case (ls1, ls2) of
adam@1321 329 ([], _) => revAppend acc ls2
adam@1321 330 | (_, []) => revAppend acc ls1
adam@1321 331 | (x1 :: ls1', x2 :: ls2') => if gt x1 x2 then merge ls1 ls2' (x2 :: acc) else merge ls1' ls2 (x1 :: acc)
adam@1321 332
adam@1321 333 fun sort' ls =
adam@1321 334 case ls of
adam@1321 335 [] => ls
adam@1321 336 | _ :: [] => ls
adam@1321 337 | _ =>
adam@1321 338 let
adam@1321 339 val (ls1, ls2) = split ls [] []
adam@1321 340 in
adam@1321 341 merge (sort' ls1) (sort' ls2) []
adam@1321 342 end
adam@1321 343 in
adam@1321 344 sort' ls
adam@1321 345 end
adam@1321 346
adam@1322 347 val nth [a] =
adam@1322 348 let
adam@1322 349 fun nth (ls : list a) (n : int) : option a =
adam@1322 350 case ls of
adam@1322 351 [] => None
adam@1322 352 | x :: ls' =>
adam@1322 353 if n <= 0 then
adam@1322 354 Some x
adam@1322 355 else
adam@1322 356 nth ls' (n-1)
adam@1322 357 in
adam@1322 358 nth
adam@1322 359 end
adam@1322 360
adam@1345 361 fun replaceNth [a] (ls : list a) (n : int) (v : a) : list a =
adam@1345 362 let
adam@1345 363 fun repNth (ls : list a) (n : int) (acc : list a) =
adam@1345 364 case ls of
adam@1345 365 [] => rev acc
adam@1345 366 | x :: ls' => if n <= 0 then
adam@1345 367 revAppend acc (v :: ls')
adam@1345 368 else
adam@1345 369 repNth ls' (n-1) (x :: acc)
adam@1345 370 in
adam@1345 371 repNth ls n []
adam@1345 372 end
adam@1345 373
adamc@845 374 fun assoc [a] [b] (_ : eq a) (x : a) =
adamc@845 375 let
adamc@845 376 fun assoc' (ls : list (a * b)) =
adamc@845 377 case ls of
adamc@845 378 [] => None
adamc@845 379 | (y, z) :: ls =>
adamc@845 380 if x = y then
adamc@845 381 Some z
adamc@845 382 else
adamc@845 383 assoc' ls
adamc@845 384 in
adamc@845 385 assoc'
adamc@845 386 end
adamc@845 387
adamc@845 388 fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
adamc@845 389 case assoc x ls of
adamc@845 390 None => (x, y) :: ls
adamc@845 391 | Some _ => ls
greenrd@1481 392
greenrd@1481 393 fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r)
greenrd@1481 394 = @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs =>
greenrd@1481 395 x :: xs) [] fl