1 (* -------------------------------------------------------------------------- *) 2 3 (* The standard definition of immutable lists. *) 4 5 data list a = 6 | Nil 7 | Cons { head: a; tail: list a } 8 9 (* -------------------------------------------------------------------------- *) 10 11 (* A definition for a list cell whose [tail] field has not yet been 12 initialized. Such a cell is mutable, and can be frozen (turned 13 into an immutable list cell) via a tag update instruction. *) 14 15 mutable data cell a = 16 | Cell { head: a; tail: () } 17 18 (* The following function writes [xs] into [c.tail] and declares 19 that [c] is now immutable. *) 20 21 (* Note: in order to ensure that the tag update instruction does 22 nothing at runtime and can be erased, we need [Cons] and [Cell] 23 to translate to the same tag number. This could be achieved by 24 adding a new tag to the definition of the type [cell]. However 25 that would force us to change the type [cell a] to the more 26 verbose type [Cell { head: a; tail: () }] in several function 27 headers. Maybe we will do that when we have type abbreviations. 28 TEMPORARY *) 29 30 val freeze [a] (consumes c: cell a, xs: unknown) : (| c @ Cons { head: a; tail = xs }) = 31 c.tail <- xs; 32 tag of c <- Cons 33 34 (* The type assigned to [freeze] faithfully reflects its behavior. 35 We could think of a more readable type: 36 val freeze [a] (consumes c: cell a, xs: list a) : (| c @ list a) 37 This type is also valid, but is strictly less general, and it turns 38 out that the extra generality is needed: when [xs] is written into 39 [c.tail], [xs] is usually not yet a list. *) 40 41 (* -------------------------------------------------------------------------- *) 42 43 (* Short-hands for constructing lists. *) 44 45 val nil = 46 Nil 47 48 val cons [a] (consumes x: a, consumes xs: list a) : list a = 49 Cons { head = x; tail = xs } 50 51 val two [a] (consumes x1: a, consumes x2: a) : list a = 52 Cons { head = x1; tail = Cons { head = x2; tail = Nil }} 53 54 val three [a] (consumes x1: a, consumes x2: a, consumes x3: a) : list a = 55 Cons { head = x1; tail = Cons { head = x2; tail = Cons { head = x3; tail = Nil }}} 56 57 val init [a, p : perm] (n : int, f : (int | p) -> a | p) : list a = 58 let rec loop (i : int | p) : list a = 59 if i = n then 60 Nil 61 else 62 Cons { head = f i; tail = loop (i + 1) } 63 in 64 loop 0 65 66 (* -------------------------------------------------------------------------- *) 67 68 (* List length. *) 69 70 (* I am sure that not everybody will like this use of [if xs then ...]. I find 71 it cute. Note that the access to [xs.tail] is safe! *) 72 73 val rec length_aux [a] (accu: int, xs: list a) : int = 74 if xs then length_aux (accu + 1, xs.tail) else accu 75 76 val length [a] (xs: list a) : int = 77 length_aux (0, xs) 78 79 (* -------------------------------------------------------------------------- *) 80 81 (* List head and tail. *) 82 83 (* These functions are likely to be of little use, but at least they are safe, 84 unlike their ocaml counterparts. *) 85 86 val hd [a] (consumes xs: Cons { head: a; tail: unknown }) : a = 87 xs.head 88 89 val tl [a] (consumes xs: Cons { head: unknown; tail: list a }) : list a = 90 xs.tail 91 92 (* -------------------------------------------------------------------------- *) 93 94 (* Indexing operations. *) 95 96 val rec nth_aux [a] (consumes xs: list a, n: int) : a = 97 if xs then 98 if n = 0 then xs.head else nth_aux (xs.tail, n - 1) 99 else 100 fail 101 102 val nth [a] (consumes xs: list a, n: int) : a = 103 if n < 0 then fail else nth_aux (xs, n) 104 105 val rec chop [a] (k: int, consumes xs: list a) : list a = 106 if k = 0 then xs 107 else if xs then chop (k - 1, xs.tail) 108 else fail 109 110 (* This conventional, non-tail-recursive version of splitAt is here as a 111 test of the type-checker. *) 112 113 val rec splitAt [a] (k: int, consumes xs: list a) : (list a, list a) = 114 if k = 0 then 115 Nil, xs 116 else if xs then begin 117 let prefix, suffix = splitAt (k - 1, xs.tail) in 118 Cons { head = xs.head; tail = prefix }, suffix 119 end 120 else fail 121 122 (* This is a tail-recursive, destination-passing-style version of splitAt. *) 123 124 val rec splitAtAux [a] (k: int, consumes xs: list a, consumes c: cell a) : (list a | c @ list a) = 125 if k = 0 then begin 126 freeze (c, Nil); 127 xs 128 end 129 else if xs then begin 130 let d = Cell { head = xs.head; tail = () } in 131 freeze (c, d); 132 splitAtAux (k - 1, xs.tail, d) 133 end 134 else fail 135 136 val splitAt [a] (k: int, consumes xs: list a) : (list a, list a) = 137 if k = 0 then 138 Nil, xs 139 else if xs then begin 140 let ys = Cell { head = xs.head; tail = () } in 141 let zs = splitAtAux (k - 1, xs.tail, ys) in 142 ys, zs 143 end 144 else fail 145 (* TEMPORARY maybe it would be nice to also offer a version of splitAt 146 that does not fail when [length xs] is smaller than [k] *) 147 148 (* -------------------------------------------------------------------------- *) 149 150 (* List concatenation and reversal. *) 151 152 (* A non-tail-recursive version of [append]. *) 153 154 val rec append [a] (consumes xs: list a, consumes ys: list a) : list a = 155 if xs then 156 Cons { head = xs.head; tail = append (xs.tail, ys) } 157 else 158 ys 159 160 (* A tail-recursive version of [append], which uses auxiliary storage. *) 161 162 val rec rev_append [a] (consumes xs: list a, consumes ys: list a) : list a = 163 if xs then 164 rev_append (xs.tail, Cons { head = xs.head; tail = ys }) 165 else 166 ys 167 168 val rev [a] (consumes xs: list a) : list a = 169 rev_append (xs, Nil) 170 171 val append [a] (consumes xs: list a, consumes ys: list a) : list a = 172 rev_append (rev xs, ys) 173 174 (* A tail-recursive version of [append], using no auxiliary storage, in 175 destination-passing-style. *) 176 177 val rec appendAux [a] ( 178 consumes dst: cell a, 179 consumes xs: list a, 180 consumes ys: list a) 181 : (| dst @ list a) 182 = 183 if xs then begin 184 let dst' = Cell { head = xs.head; tail = () } in 185 freeze (dst, dst'); 186 appendAux (dst', xs.tail, ys) 187 end 188 else 189 freeze (dst, ys) 190 191 val append [a] (consumes xs: list a, consumes ys: list a) : list a = 192 if xs then begin 193 let dst = Cell { head = xs.head; tail = () } in 194 appendAux (dst, xs.tail, ys); 195 dst 196 end 197 else 198 ys 199 200 (* -------------------------------------------------------------------------- *) 201 202 (* Flattening a list of lists. *) 203 204 val rec flatten [a] (consumes xss : list (list a)) : list a = 205 if xss then 206 append (xss.head, flatten xss.tail) 207 else 208 Nil 209 210 (* -------------------------------------------------------------------------- *) 211 212 (* Map. *) 213 214 (* The following type does allow the function [f] to perform a strong update 215 on the argument list, whose type changes from [list a1] to [list a2]. A 216 new list of type [list b] is produced. *) 217 218 val rec map [a1, a2, b, p : perm] ( 219 consumes xs: list a1, 220 f: (consumes x: a1 | p) -> ( b | x @ a2) 221 | p) : (list b | xs @ list a2) 222 = 223 if xs then 224 Cons { head = f xs.head; tail = map (xs.tail, f) } 225 else 226 Nil 227 228 val rev_map [a1, a2, b, p : perm] ( 229 consumes xs: list a1, 230 f: (consumes x: a1 | p) -> ( b | x @ a2) 231 | p) : (list b | xs @ list a2) 232 = 233 let rec rev_map_aux (consumes accu: list b, consumes xs: list a1 | p) : (list b | xs @ list a2) = 234 if xs then 235 rev_map_aux (Cons { head = f xs.head; tail = accu }, xs.tail) 236 else 237 accu 238 in 239 rev_map_aux (Nil, xs) 240 241 (* -------------------------------------------------------------------------- *) 242 243 (* Iteration. *) 244 245 (* The following type allows the function [f] to perform a strong update 246 on the argument list, whose type changes from [list a1] to [list a2]. 247 It also allows [f] to have a side effect at [p]. *) 248 249 val rec iter [a1, a2, p : perm] ( 250 consumes xs: list a1, 251 f: (consumes x: a1 | p) 252 -> (| x @ a2) 253 | p 254 ) : (| xs @ list a2) 255 = 256 if xs then begin 257 f xs.head; 258 iter (xs.tail, f) 259 end 260 261 (* The following function should not be useful to the client, who can just 262 use [iter], but it is a good test of the type-checker. *) 263 264 val simpler_iter [a] (xs: list a, f: a -> ()) : () = 265 iter (xs, f) 266 267 (* -------------------------------------------------------------------------- *) 268 269 (* Fold. *) 270 271 (* The following type allows the function [f] to perform a strong update 272 on the argument list, whose type changes from [list a1] to [list a2]. An 273 accumulator of type [b] is maintained. *) 274 275 (* It is not necessary to explicitly thread a permission [p], because the 276 type [b] already serves this purpose. *) 277 278 val rec fold_left [a1, a2, b] ( 279 f: (consumes b, consumes x: a1) -> (b | x @ a2), 280 consumes accu: b, consumes xs: list a1) : (b | xs @ list a2) 281 = 282 if xs then 283 fold_left (f, f (accu, xs.head), xs.tail) 284 else 285 accu 286 287 val rec fold_right [a1, a2, b] ( 288 f: (consumes x: a1, consumes b) -> (b | x @ a2), 289 consumes xs: list a1, consumes accu: b) : (b | xs @ list a2) 290 = 291 if xs then 292 f (xs.head, fold_right (f, xs.tail, accu)) 293 else 294 accu 295 296 (* -------------------------------------------------------------------------- *) 297 298 (* Various flavors of list search. *) 299 300 (* Note that these are not instances of [fold], because we need to bail out 301 early when the search is successful. *) 302 303 val rec for_all [a, p : perm] (ok: (a | p) -> bool, xs: list a | p) : bool = 304 if xs then 305 if ok xs.head then for_all (ok, xs.tail) else False 306 else 307 True 308 309 val rec rich_for_all 310 [a, p : perm, q : perm] (ok: (a | p) -> rich_bool q empty, xs: list a | p) : rich_bool q empty = 311 match xs with 312 | Nil -> 313 RichTrue 314 | Cons { head; tail } -> 315 conjunction ( 316 ok head, 317 fun (| p * tail @ list a) : rich_bool q empty = 318 rich_for_all (ok, tail) 319 ) 320 end 321 322 val rec rich_for_all_with_inlined_conjunction 323 [a, p : perm, q : perm] (ok: (a | p) -> rich_bool q empty, xs: list a | p) : rich_bool q empty = 324 match xs with 325 | Nil -> 326 RichTrue 327 | Cons { head; tail } -> 328 ok head && rich_for_all_with_inlined_conjunction (ok, tail) 329 end 330 331 val rec exists [a, p : perm] (ok: (a | p) -> bool, xs: list a | p) : bool = 332 if xs then 333 if ok xs.head then True else exists (ok, xs.tail) 334 else 335 False 336 337 val rec rich_exists_with_inlined_disjunction 338 [a, p : perm, q : perm] (ok: (a | p) -> rich_bool empty q, xs: list a | p) : rich_bool empty q = 339 match xs with 340 | Nil -> 341 RichFalse 342 | Cons { head; tail } -> 343 ok head || rich_exists_with_inlined_disjunction (ok, tail) 344 end 345 346 (* The function [find] cannot raise an exception, as it does in OCaml. 347 Instead, it returns a sub-list, which either is empty or begins with 348 the desired element. This is more general than returning an option, 349 since it allows repeated searches, and is more efficient, since it 350 does not require memory allocation! *) 351 352 val rec find [a, p : perm] (ok: (a | p) -> bool, consumes xs: list a | p) : list a = 353 if xs then 354 if ok xs.head then xs else find (ok, xs.tail) 355 else 356 xs 357 358 (* The call [remove (ok, xs)] produces the list [xs], deprived of the first 359 element that satisfies the predicate [ok], if there is one. *) 360 361 val rec remove [a, p : perm] (ok : (a | p) -> bool, consumes xs: list a | p) : list a = 362 if xs then 363 if ok xs.head then xs.tail else Cons { head = xs.head; tail = remove (ok, xs.tail) } 364 else 365 xs 366 367 (* The function [mem] is parameterized with a notion of equality. It is just a 368 variant of [find] that does not require the function [equal] to be 369 partially applied to [x] ahead of time. *) 370 371 val mem [a, p : perm] (equal: (a, a | p) -> bool, x: a, consumes xs: list a | p) : list a = 372 let ok (y : a | x @ a * p) : bool = 373 equal (x, y) 374 in 375 find (ok, xs) 376 377 val rec mem [a, p : perm] (equal: (a, a | p) -> bool, x: a, consumes xs: list a | p) : list a = 378 if xs then 379 if equal (x, xs.head) then xs else mem (equal, x, xs.tail) 380 else 381 Nil 382 383 (* [assoc] is a version of [find]. It is specialized with a notion of equality 384 of key-value pairs as equality of keys. *) 385 386 val assoc [a, b, p : perm] (equal: (a, a | p) -> bool, x: a, consumes xs: list (a, b) | p) : list (a, b) = 387 let ok (y: a, _: b | x @ a * p) : bool = 388 equal (x, y) 389 in 390 find [(a, b), (x @ a * p)] (ok, xs) 391 392 (* TEMPORARY 393 mem should be called find_equal 394 assoc should be called find_equal_key 395 remove could be specialized in the same ways as find *) 396 397 (* -------------------------------------------------------------------------- *) 398 399 (* Filtering. *) 400 401 val filter [a, p : perm] (consumes xs: list a, ok: (a | p) -> bool | p) : list a = 402 let f (consumes accu: list a, consumes x: a | p) : list a = 403 if ok x then Cons { head = x; tail = accu } else accu 404 in 405 rev (fold_left [a, unknown, (list a | p)] (f, Nil, xs)) 406 407 val partition [a] (p: a -> bool, consumes xs: list a) : (list a, list a) = 408 let f (consumes (yes: list a, no: list a), consumes x: a) : (list a, list a) = 409 if p x then 410 Cons { head = x; tail = yes }, no 411 else 412 yes, Cons { head = x; tail = no } 413 in 414 let (yes, no) = fold_left [a, unknown, (list a, list a)] (f, (Nil, Nil), xs) in 415 rev yes, rev no 416 417 (* -------------------------------------------------------------------------- *) 418 419 (* Lists of pairs. *) 420 421 val rec split [a, b] (consumes xys : list (a, b)) : (list a, list b) = 422 if xys then begin 423 let x, y = xys.head in 424 let xs, ys = split xys.tail in 425 Cons { head = x; tail = xs }, 426 Cons { head = y; tail = ys } 427 end 428 else 429 Nil, 430 Nil 431 432 val rec combine [a, b] (consumes xs: list a, consumes ys: list b) : list (a, b) = 433 match xs, ys with 434 | Cons, Cons -> 435 Cons { head = (xs.head, ys.head); tail = combine (xs.tail, ys.tail) } 436 | Nil, Nil -> 437 Nil 438 | Nil, Cons -> 439 Nil 440 | Cons, Nil -> 441 Nil 442 end 443 444 (* -------------------------------------------------------------------------- *) 445 446 (* This auxiliary function is used by [sort]. It peforms a dynamic test 447 of duplicability in order to choose between two ways of splitting a 448 list, one of which causes the list elements to apparently become 449 shared. *) 450 451 (* While porting [sort] from OCaml's standard library, we encountered an 452 ownership problem. OCaml's code uses a trick, which is to *not* truncate 453 the list in the first recursive call. In other words, the first recursive 454 instance of [sort] is passed the entire list, but has permission to use 455 only the [n1] first elements of it. Mezzo's type system cannot express this 456 subtlety. As a result, it seems that we have to either restrict the code to 457 the case where the type [a] is duplicable, or truncate the list that is 458 passed to the first recursive call (at a cost). In fact, we can encapsulate 459 both versions of the code into a single [sort] function, which takes an 460 argument of [duplicability a], and performs the choice at runtime, 461 depending on the type [a]. This is perhaps not great, but it shows that we 462 do have a few tricks up our sleeve. *) 463 464 val splitAtOrShareAndChop [a] ( 465 dupa: reflection::duplicability a, 466 k: int, 467 consumes xs: list a 468 ) : (list a, list a) = 469 if dupa then 470 (* If the list elements are duplicable, then we can follow the OCaml 471 version of the code, and keep the first list unchanged. It is too 472 long, but the extra elements will never be accessed. *) 473 xs, chop (k, xs) 474 else 475 (* Otherwise, we have to use [splitAt], which is less efficient (the 476 first part of the list spine is copied) but obviously does not 477 cause the list elements to become shared. Our type system is not 478 expressive enough to understand that ``we own only the first [k] 479 elements of this list''. *) 480 splitAt (k, xs) 481 482 (* -------------------------------------------------------------------------- *) 483 484 (* Merging and sorting. *) 485 486 (* Note: [merge] is not tail-recursive, and is not used by [sort], 487 which has its own [rev_merge]. *) 488 489 val rec merge [a] ( 490 cmp: (a, a) -> int, 491 consumes xs: list a, 492 consumes ys: list a 493 ) : list a = 494 match xs, ys with 495 | Nil, _ -> 496 ys 497 | _, Nil -> 498 xs 499 | Cons { head = x }, Cons { head = y } -> 500 if cmp (x, y) <= 0 501 then Cons { head = x; tail = merge (cmp, xs.tail, ys) } 502 else Cons { head = y; tail = merge (cmp, xs, ys.tail) } 503 end 504 505 val sort [a] ( 506 dupa: reflection::duplicability a, 507 cmp: (a, a) -> int, 508 consumes xs: list a 509 ) : list a = 510 (* Wrap the comparison function [cmp] so as to take an extra 511 argument, [sense], which takes the value -1 or 1 and allows 512 reversing the ordering if desired. *) 513 let cmp (sense: int, x: a, y: a) : int = 514 sense * cmp (x, y) 515 in 516 (* [rev_merge (sense, xs, ys, accu)] merges the lists [xs] and [ys] 517 and concatenates the reverse of the resulting list in front of 518 [accu]. The ordering is dictated by [sense]. *) 519 let rec rev_merge (sense: int, consumes xs: list a, consumes ys: list a, consumes accu: list a) : list a = 520 if xs then 521 if ys then begin 522 let x = xs.head 523 and y = ys.head in 524 if cmp (sense, x, y) <= 0 525 then rev_merge (sense, xs.tail, ys, Cons { head = x; tail = accu }) 526 else rev_merge (sense, xs, ys.tail, Cons { head = y; tail = accu }) 527 end 528 else 529 rev_append (xs, accu) 530 else 531 rev_append (ys, accu) 532 in 533 (* This is the main sorting function. The integer [n] is always at 534 least [2], and is less than or equal to the length of [xs]. Again, 535 the ordering is dictated by [sense]. *) 536 let rec sort (sense: int, n: int, consumes xs: list a) : list a = 537 (* Leaf cases. *) 538 if n = 2 then 539 match xs with 540 | Cons { head = x1; tail = Cons { head = x2; tail = any }} -> 541 if cmp (sense, x1, x2) <= 0 then two (x1, x2) else two (x2, x1) 542 | _ -> 543 fail (* impossible *) 544 end 545 else if n = 3 then 546 match xs with 547 | Cons { head = x1; tail = Cons { head = x2; tail = Cons { head = x3; tail = any }}} -> 548 if cmp (sense, x1, x2) <= 0 then begin 549 if cmp (sense, x2, x3) <= 0 then three (x1, x2, x3) 550 else if cmp (sense, x1, x3) <= 0 then three (x1, x3, x2) 551 else three (x3, x1, x2) 552 end else begin 553 if cmp (sense, x1, x3) <= 0 then three (x2, x1, x3) 554 else if cmp (sense, x2, x3) <= 0 then three (x2, x3, x1) 555 else three (x3, x2, x1) 556 end 557 | _ -> 558 fail (* impossible *) 559 end 560 (* The general case. *) 561 else begin 562 let n1 = n / 2 in 563 let n2 = n - n1 in 564 let xs1, xs2 = splitAtOrShareAndChop (dupa, n1, xs) in 565 let xs1 = sort (-sense, n1, xs1) in 566 let xs2 = sort (-sense, n2, xs2) in 567 rev_merge (-sense, xs1, xs2, Nil) 568 end 569 in 570 let n = length xs in 571 if n < 2 then xs else sort (1, n, xs) 572 573 (* -------------------------------------------------------------------------- *) 574 575 (* Comparison. *) 576 577 val rec equal [a, b] (eq: (a, b) -> bool, xs: list a, ys: list b) : bool = 578 if xs then 579 if ys then 580 if eq (xs.head, ys.head) then 581 equal (eq, xs.tail, ys.tail) 582 else 583 False 584 else 585 False 586 else 587 if ys then 588 False 589 else 590 True 591 592 val rec compare [a, b] (cmp: (a, b) -> int, xs: list a, ys: list b) : int = 593 if xs then 594 if ys then begin 595 let c = cmp (xs.head, ys.head) in 596 if c = 0 then 597 compare (cmp, xs.tail, ys.tail) 598 else 599 c 600 end 601 else 602 1 603 else 604 if ys then 605 -1 606 else 607 0 608 609 (* -------------------------------------------------------------------------- *) 610 611 (* Conversions between arrays and lists. *) 612 613 (* Converting an array (segment) to a list. *) 614 615 val rec segment2list [a] duplicable a => (x: array a, i: int, j: int, consumes accu: list a) : list a = 616 if i < j then 617 segment2list (x, i, j - 1, Cons { head = array::get (x, j - 1); tail = accu }) 618 else 619 accu 620 621 val array2list [a] duplicable a => (x: array a) : list a = 622 segment2list (x, 0, array::length x, Nil) 623 624 (* TEMPORARY using [array::transform], we could offer a variant of [array2list] 625 where the ownership of the elements is transferred from the array to the list *) 626 627 (* Converting a list to an array. *) 628 629 val list2array [a] (consumes xs: list a) : array a = 630 let n = length xs in 631 let r = newref xs in 632 array::init (Up, n, fun (i: int | r @ ref (list a)) : a = 633 match !r with 634 | Cons { head; tail } -> 635 r := tail; 636 head 637 | Nil -> 638 fail (* impossible *) 639 end 640 ) 641 642 (* 643 Local Variables: 644 compile-command: "../mezzo list.mz" 645 End: 646 *)