1 # Deque: a double-ended queue, as a front list and a reversed back list. 2 # 3 # Pushing and popping on either end is amortized O(1), in any mix of ends 4 # (the refill below says why). Like List, the queries consume the deque: a 5 # Data deque is shared with +. 6 # 7 # The laws at the bottom are checked every time this file is imported. 8 import Base 9 10 type Deque is Kind(a): 11 Deq{front: List, back: List} 12 13 def Deque.new(a, -A: Kind(a)) -> Deque: 14 Deq{Nil{}, Nil{}} 15 16 # the list's first element is the deque's front 17 def Deque.from_list(a, -A: Kind(a), xs: List) -> Deque: 18 Deq{xs, Nil{}} 19 20 def Deque.push_front(a, -A: Kind(a), x: A, d: Deque) -> Deque: 21 match d: 22 case Deq{f, b}: 23 Deq{x <> f, b} 24 25 def Deque.push_back(a, -A: Kind(a), x: A, d: Deque) -> Deque: 26 match d: 27 case Deq{f, b}: 28 Deq{f, x <> b} 29 30 def Deque.count.put( 31 a, -A: Kind(a), h: A, rn: List & Nat 32 ) -> List & Nat: 33 (rest, n) = rn 34 (h <> rest, 1n+n) 35 36 # a list and its length, in one pass that hands the list back 37 def Deque.count(a, -A: Kind(a), xs: List) -> List & Nat: 38 match xs: 39 case Nil{}: 40 (Nil{}, 0n) 41 case h <> t: 42 Deque.count.put(a, A, h, Deque.count(a, A, t)) 43 44 def Deque.half(n: Nat) -> Nat: 45 match n: 46 case 0n: 47 0n 48 case 1n+p: 49 match p: 50 case 0n: 51 0n 52 case 1n+q: 53 1n+Deque.half(q) 54 55 def Deque.split.put( 56 a, -A: Kind(a), h: A, lr: List & List 57 ) -> List & List: 58 (l, r) = lr 59 (h <> l, r) 60 61 # the first n elements, and the rest 62 def Deque.split(a, -A: Kind(a), n: Nat, xs: List) -> 63 List & List: 64 match n: 65 case 0n: 66 (Nil{}, xs) 67 case 1n+p: 68 match xs: 69 case Nil{}: 70 (Nil{}, Nil{}) 71 case h <> t: 72 Deque.split.put(a, A, h, Deque.split(a, A, p, t)) 73 74 # When one end runs out, the other list is split in half and only the half 75 # nearest the empty end is reversed over. Moving everything would let pops 76 # that alternate ends reverse the whole deque each time; halving keeps the 77 # lists balanced, so every operation stays amortized O(1). 78 79 def Deque.pop_front.go( 80 a, -A: Kind(a), xs: List, b: List 81 ) -> Maybe<&1, A & Deque>: 82 match xs: 83 case Nil{}: 84 None{} 85 case h <> t: 86 Some{(h, Deq{t, b})} 87 88 def Deque.pop_front.halves( 89 a, -A: Kind(a), sm: List & List 90 ) -> Maybe<&1, A & Deque>: 91 (stay, move) = sm 92 Deque.pop_front.go(a, A, List.reverse(a, A, move), stay) 93 94 def Deque.pop_front.refill( 95 a, -A: Kind(a), bn: List & Nat 96 ) -> Maybe<&1, A & Deque>: 97 (b, n) = bn 98 Deque.pop_front.halves(a, A, Deque.split(a, A, Deque.half(n), b)) 99 100 def Deque.pop_front( 101 a, -A: Kind(a), d: Deque 102 ) -> Maybe<&1, A & Deque>: 103 match d: 104 case Deq{f, b}: 105 match f: 106 case h <> t: 107 Some{(h, Deq{t, b})} 108 case Nil{}: 109 Deque.pop_front.refill(a, A, Deque.count(a, A, b)) 110 111 def Deque.pop_back.go( 112 a, -A: Kind(a), xs: List, f: List 113 ) -> Maybe<&1, A & Deque>: 114 match xs: 115 case Nil{}: 116 None{} 117 case h <> t: 118 Some{(h, Deq{f, t})} 119 120 def Deque.pop_back.halves( 121 a, -A: Kind(a), sm: List & List 122 ) -> Maybe<&1, A & Deque>: 123 (stay, move) = sm 124 Deque.pop_back.go(a, A, List.reverse(a, A, move), stay) 125 126 def Deque.pop_back.refill( 127 a, -A: Kind(a), fn: List & Nat 128 ) -> Maybe<&1, A & Deque>: 129 (f, n) = fn 130 Deque.pop_back.halves(a, A, Deque.split(a, A, Deque.half(n), f)) 131 132 def Deque.pop_back( 133 a, -A: Kind(a), d: Deque 134 ) -> Maybe<&1, A & Deque>: 135 match d: 136 case Deq{f, b}: 137 match b: 138 case h <> t: 139 Some{(h, Deq{f, t})} 140 case Nil{}: 141 Deque.pop_back.refill(a, A, Deque.count(a, A, f)) 142 143 # the elements, front to back 144 def Deque.to_list(a, -A: Kind(a), d: Deque) -> List: 145 match d: 146 case Deq{f, b}: 147 List.append(a, A, f, List.reverse(a, A, b)) 148 149 def Deque.length(a, -A: Kind(a), d: Deque) -> Nat: 150 match d: 151 case Deq{f, b}: 152 Nat.add(List.length(a, A, f), List.length(a, A, b)) 153 154 def Deque.is_empty(a, -A: Kind(a), d: Deque) -> Bool: 155 match d: 156 case Deq{f, b}: 157 Bool.and(List.is_empty(a, A, f), List.is_empty(a, A, b)) 158 159 # Laws 160 # ---- 161 # Each law reads a deque through to_list, the only view a user has of it. 162 163 # LAW: a new deque reads as the empty list 164 law Deque.to_list.new: 165 for -A: Data 166 {Deque.to_list(&2, A, Deque.new(&2, A)) == Nil{} : List<&2, A>} 167 168 def Deque.to_list.new(A): 169 {==} 170 171 # LAW: push_front puts the element at the head of the list 172 law Deque.to_list.push_front: 173 for -A: Data 174 for -x: A 175 for d: Deque<&2, A> 176 {Deque.to_list(&2, A, Deque.push_front(&2, A, x, d)) 177 == x <> Deque.to_list(&2, A, d) : List<&2, A>} 178 179 def Deque.to_list.push_front(A, x, d): 180 match d: 181 case Deq{f, b}: 182 {==} 183 184 # LAW: pop_front undoes push_front 185 law Deque.pop_front.push_front: 186 for -A: Data 187 for -x: A 188 for d: Deque<&2, A> 189 {Deque.pop_front(&2, A, Deque.push_front(&2, A, x, d)) 190 == Some{(x, d)} : Maybe<&1, A & Deque<&2, A>>} 191 192 def Deque.pop_front.push_front(A, x, d): 193 match d: 194 case Deq{f, b}: 195 {==} 196 197 # LAW: pop_back undoes push_back 198 law Deque.pop_back.push_back: 199 for -A: Data 200 for -x: A 201 for d: Deque<&2, A> 202 {Deque.pop_back(&2, A, Deque.push_back(&2, A, x, d)) 203 == Some{(x, d)} : Maybe<&1, A & Deque<&2, A>>} 204 205 def Deque.pop_back.push_back(A, x, d): 206 match d: 207 case Deq{f, b}: 208 {==} 209 210 # Lemmas over Base's List, by induction on the first list 211 212 law Deque.lemma.append_nil: 213 for -A: Data 214 for xs: List<&2, A> 215 {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>} 216 217 def Deque.lemma.append_nil(A, xs): 218 match xs: 219 case Nil{}: 220 {==} 221 case h <> t: 222 %Deque.lemma.append_nil(A, t) : {h <> List.append(&2, A, t, Nil{}) 223 == h <> _ : List<&2, A>} 224 {==} 225 226 law Deque.lemma.append_assoc: 227 for -A: Data 228 for xs: List<&2, A> 229 for -ys: List<&2, A> 230 for -zs: List<&2, A> 231 {List.append(&2, A, List.append(&2, A, xs, ys), zs) 232 == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>} 233 234 def Deque.lemma.append_assoc(A, xs, ys, zs): 235 match xs: 236 case Nil{}: 237 {==} 238 case h <> t: 239 %Deque.lemma.append_assoc(A, t, ys, zs) : {h <> List.append(&2, A, 240 List.append(&2, A, t, ys), zs) == h <> _ : List<&2, A>} 241 {==} 242 243 # LAW: a list read into a deque reads back as itself 244 law Deque.to_list.from_list: 245 for -A: Data 246 for xs: List<&2, A> 247 {Deque.to_list(&2, A, Deque.from_list(&2, A, xs)) == xs : List<&2, A>} 248 249 def Deque.to_list.from_list(A, xs): 250 Deque.lemma.append_nil(A, xs) 251 252 # reversing onto an accumulator is reversing, then appending it 253 law Deque.lemma.reverse_go: 254 for -A: Data 255 for xs: List<&2, A> 256 for -acc: List<&2, A> 257 {List.append(&2, A, List.reverse.go(&2, A, xs, Nil{}), acc) 258 == List.reverse.go(&2, A, xs, acc) : List<&2, A>} 259 260 def Deque.lemma.reverse_go(A, xs, acc): 261 match xs: 262 case Nil{}: 263 {==} 264 case +h <> +t: 265 %Deque.lemma.reverse_go(A, t, [h]) : {List.append(&2, A, _, acc) 266 == List.reverse.go(&2, A, t, h <> acc) : List<&2, A>} 267 %Deque.lemma.reverse_go(A, t, h <> acc) : {List.append(&2, A, 268 List.append(&2, A, List.reverse.go(&2, A, t, Nil{}), [h]), acc) 269 == _ : List<&2, A>} 270 Deque.lemma.append_assoc(A, List.reverse.go(&2, A, t, Nil{}), [h], acc) 271 272 # LAW: push_back puts the element at the end of the list 273 law Deque.to_list.push_back: 274 for -A: Data 275 for -x: A 276 for d: Deque<&2, A> 277 {Deque.to_list(&2, A, Deque.push_back(&2, A, x, d)) 278 == List.append(&2, A, Deque.to_list(&2, A, d), [x]) : List<&2, A>} 279 280 def Deque.to_list.push_back(A, x, d): 281 match d: 282 case Deq{+f, +b}: 283 %Deque.lemma.reverse_go(A, b, [x]) : {List.append(&2, A, f, _) 284 == List.append(&2, A, List.append(&2, A, f, List.reverse(&2, A, b)), 285 [x]) : List<&2, A>} 286 %Deque.lemma.append_assoc(A, f, List.reverse(&2, A, b), [x]) : {_ 287 == List.append(&2, A, List.append(&2, A, f, List.reverse(&2, A, b)), 288 [x]) : List<&2, A>} 289 {==}