Mercurial > urweb
comparison lib/ur/list.ur @ 1321:4172863d049d
queryL1 and List.sort
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 20 Nov 2010 10:45:22 -0500 |
| parents | 4c367c8f5b2d |
| children | 80bff6449f41 |
comparison
equal
deleted
inserted
replaced
| 1320:add5ae41969e | 1321:4172863d049d |
|---|---|
| 278 None => acc | 278 None => acc |
| 279 | Some v => v :: acc)) | 279 | Some v => v :: acc)) |
| 280 []; | 280 []; |
| 281 return (rev ls) | 281 return (rev ls) |
| 282 | 282 |
| 283 fun sort [a] (gt : a -> a -> bool) (ls : t a) : t a = | |
| 284 let | |
| 285 fun split ls acc1 acc2 = | |
| 286 case ls of | |
| 287 [] => (rev acc1, rev acc2) | |
| 288 | x :: [] => (rev (x :: acc1), rev acc2) | |
| 289 | x1 :: x2 :: ls' => split ls' (x1 :: acc1) (x2 :: acc2) | |
| 290 | |
| 291 fun merge ls1 ls2 acc = | |
| 292 case (ls1, ls2) of | |
| 293 ([], _) => revAppend acc ls2 | |
| 294 | (_, []) => revAppend acc ls1 | |
| 295 | (x1 :: ls1', x2 :: ls2') => if gt x1 x2 then merge ls1 ls2' (x2 :: acc) else merge ls1' ls2 (x1 :: acc) | |
| 296 | |
| 297 fun sort' ls = | |
| 298 case ls of | |
| 299 [] => ls | |
| 300 | _ :: [] => ls | |
| 301 | _ => | |
| 302 let | |
| 303 val (ls1, ls2) = split ls [] [] | |
| 304 in | |
| 305 merge (sort' ls1) (sort' ls2) [] | |
| 306 end | |
| 307 in | |
| 308 sort' ls | |
| 309 end | |
| 310 | |
| 283 fun assoc [a] [b] (_ : eq a) (x : a) = | 311 fun assoc [a] [b] (_ : eq a) (x : a) = |
| 284 let | 312 let |
| 285 fun assoc' (ls : list (a * b)) = | 313 fun assoc' (ls : list (a * b)) = |
| 286 case ls of | 314 case ls of |
| 287 [] => None | 315 [] => None |