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 (* Short-hands for constructing lists. *)
 12 
 13 val nil   : Nil
 14 val cons  : [a] (consumes a, consumes list a) -> list a
 15 val two   : [a] (consumes (a, a)) -> list a
 16 val three : [a] (consumes (a, a, a)) -> list a
 17 val init  : [a, p : perm] (n : int, f : (int | p) -> a | p) -> list a
 18 
 19 (* -------------------------------------------------------------------------- *)
 20 
 21 (* List length. *)
 22 
 23 val length : [a] list a -> int
 24 
 25 (* -------------------------------------------------------------------------- *)
 26 
 27 (* List head and tail. *)
 28 
 29 val hd : [a] (consumes Cons { head: a; tail: unknown }) -> a
 30 val tl : [a] (consumes Cons { head: unknown; tail: list a }) -> list a
 31 
 32 (* -------------------------------------------------------------------------- *)
 33 
 34 (* Indexing operations. *)
 35 
 36 val nth     : [a] (consumes list a, int) -> a
 37 val chop    : [a] (int, consumes list a) -> list a
 38 val splitAt : [a] (int, consumes list a) -> (list a, list a)
 39 
 40 (* -------------------------------------------------------------------------- *)
 41 
 42 (* List concatenation and reversal. *)
 43 
 44 val append     : [a] (consumes list a, consumes list a) -> list a
 45 val rev_append : [a] (consumes list a, consumes list a) -> list a
 46 val rev        : [a] (consumes list a) -> list a
 47 
 48 (* -------------------------------------------------------------------------- *)
 49 
 50 (* Flattening a list of lists. *)
 51 
 52 val flatten : [a] (consumes list (list a)) -> list a
 53 
 54 (* -------------------------------------------------------------------------- *)
 55 
 56 (* Map. *)
 57 
 58 val map : [a1, a2, b, p : perm] (
 59       consumes xs: list a1,
 60   f: (consumes  x:      a1 | p) -> (     b |  x @      a2)
 61                            | p) -> (list b | xs @ list a2)
 62 
 63 val rev_map : [a1, a2, b, p : perm] (
 64       consumes xs: list a1,
 65   f: (consumes  x:      a1 | p) -> (     b |  x @      a2)
 66                            | p) -> (list b | xs @ list a2)
 67 
 68 (* -------------------------------------------------------------------------- *)
 69 
 70 (* Iteration. *)
 71 
 72 val iter : [a1, a2, p : perm] (
 73   consumes xs: list a1,
 74   f: (consumes x:  a1 | p)
 75          -> (| x @ a2)
 76 | p
 77 )   -> (| xs @ list a2)
 78 
 79 (* -------------------------------------------------------------------------- *)
 80 
 81 (* Fold. *)
 82 
 83 val fold_left : [a1, a2, b] (
 84   f: (consumes       b, consumes  x:      a1) -> (b |  x @      a2),
 85       consumes accu: b, consumes xs: list a1) -> (b | xs @ list a2)
 86 
 87 val fold_right : [a1, a2, b] (
 88   f: (consumes  x:      a1, consumes       b) -> (b |  x @      a2),
 89       consumes xs: list a1, consumes accu: b) -> (b | xs @ list a2)
 90 
 91 (* -------------------------------------------------------------------------- *)
 92 
 93 (* Various flavors of list search. *)
 94 
 95 val for_all : [a, p : perm] ((a | p) -> bool, list a | p) -> bool
 96 val exists  : [a, p : perm] ((a | p) -> bool, list a | p) -> bool
 97 val find    : [a, p : perm] ((a | p) -> bool, consumes list a | p) -> list a
 98 val remove  : [a, p : perm] ((a | p) -> bool, consumes list a | p) -> list a
 99 
100 val mem     : [a, p : perm] (equal: (a, a | p) -> bool, x: a, consumes xs: list a | p) -> list a
101 
102 val assoc   : [a, b, p : perm] (
103   equal: (a, a | p) -> bool,
104   x: a,
105   consumes xs: list (a, b)
106 | p) -> list (a, b)
107 
108 (* -------------------------------------------------------------------------- *)
109 
110 (* Filtering. *)
111 
112 val filter    : [a, p : perm] (consumes xs: list a, ok: (a | p) -> bool | p) -> list a
113 val partition : [a] (p: a -> bool, consumes xs: list a) -> (list a, list a)
114 
115 (* -------------------------------------------------------------------------- *)
116 
117 (* Lists of pairs. *)
118 
119 val split   : [a, b] (consumes xys: list (a, b)) -> (list a, list b)
120 val combine : [a, b] (consumes list a, consumes list b) -> list (a, b)
121 
122 (* -------------------------------------------------------------------------- *)
123 
124 (* Merging and sorting. *)
125 
126 val merge : [a] (
127   cmp: (a, a) -> int,
128   consumes list a,
129   consumes list a
130 ) -> list a
131 
132 val sort  : [a] (
133   reflection::duplicability a,
134   cmp: (a, a) -> int,
135   consumes list a
136 ) -> list a
137 
138 (* -------------------------------------------------------------------------- *)
139 
140 (* Comparison. *)
141 
142 val equal   : [a, b] (eq: (a, b) -> bool, xs: list a, ys: list b) -> bool
143 val compare : [a, b] (cmp: (a, b) -> int, xs: list a, ys: list b) -> int
144 
145 (* -------------------------------------------------------------------------- *)
146 
147 (* Conversions between arrays and lists. *)
148 
149 val array2list : [a] duplicable a => array a -> list a
150 val list2array : [a] (consumes list a) -> array a
151