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 *)