1 import Base 2 import ../types/internal_dlist.bend as E 3 4 # Doubly linked list with stable opaque handles, values of an erased type T. 5 # 6 # Representation: PARALLEL INDEXED ARENAS. Three `Base.Array` blocks of 7 # 2^depth slots share one index space: 8 # vals Maybe the element stored at an id (None: never used or removed) 9 # prevs U32 the LINK to the preceding element 10 # nexts U32 the LINK to the following element 11 # A link is id + 1, and `nil()` = 0 is the "no neighbour" link (as are the 12 # head and tail fields), so testing for a neighbour is a comparison with 0 13 # and following a link is one subtraction. Ids are slot indices below 2^31, 14 # so id + 1 never wraps. The element id IS its slot index; 15 # ids come from a monotone counter and are never reused, so a handle to a 16 # removed element is stale (its `vals` slot is None) and a handle whose tag 17 # differs from the list's is foreign. The blocks double when the counter 18 # reaches the capacity (the old block becomes the lower half, so every id 19 # keeps its slot), exactly as the dynamic array grows. 20 # 21 # The prev/next links are the doubly linked list's own links - what the 22 # structure is for - stored as arena indices. Keeping them in their own 23 # blocks makes relinking a neighbour ONE indexed write (no read-modify-write 24 # of a node record). Nothing is stored in a search tree or a cons list. 25 # 26 # Cost (n = number of elements ever inserted): every handle operation and 27 # push is O(1) indexed reads and writes; `length` is the cached count; 28 # `to_list` reads O(count) slots. A push that finds the blocks full doubles 29 # them (one `Base.Array` node and one fresh half per block), amortised O(1). 30 # Because ids are never reused the blocks grow with n, not with the live 31 # count - the same trade the reference C implementation makes. 32 # 33 # Errors: a foreign handle gives Fail{ForeignHandle}, a stale one 34 # Fail{StaleHandle}; every failure returns the list unchanged. 35 36 type DList<-T: Data> is Type: 37 DL{tag: U32, fresh: U32, free: U32, count: Nat, head: U32, tail: U32, depth: Nat, cap: U32, vals: Array>, prevs: Array, nexts: Array} 38 39 def nil() -> U32: 40 0 41 42 # The link to an element, and the element a (non-nil) link points to. 43 def link(+i: U32) -> U32: 44 U32.inc(i) 45 46 def slot(+l: U32) -> U32: 47 U32.sub(l, 1) 48 49 def new_vals(~T: Data, +depth: Nat) -> Array>: 50 Array.new(Maybe<&2, T>, depth, None{}) 51 52 def new_links(+depth: Nat) -> Array: 53 Array.new(U32, depth, nil()) 54 55 def new(~T: Data, tag: U32) -> DList: 56 DL{tag, 0, 0, 0n, nil(), nil(), 0n, 1, new_vals(~T, 0n), new_links(0n), new_links(0n)} 57 58 # A link as the Maybe the public API reports. 59 def pick_link(none: Bool, +l: U32) -> Maybe<&2, U32>: 60 match none: 61 case True{}: 62 None{} 63 case False{}: 64 Some{l} 65 66 # ---- relinking ---- 67 68 # Point the link stored at element a (if a is a link, not nil) at q. 69 def link_of(+l: U32) -> Maybe<&2, U32>: 70 pick_link(U32.is_eq(l, nil()), l) 71 72 def set_next_go(nexts: Array, +a: U32, +q: U32, none: Bool) -> Array: 73 match none: 74 case True{}: 75 nexts 76 case False{}: 77 Array.set(U32, nexts, slot(a), q) 78 79 # ---- insertion ---- 80 81 def set_next(nexts: Array, +a: U32, +q: U32) -> Array: 82 set_next_go(nexts, a, q, U32.is_eq(a, nil())) 83 84 def grown_vals(~T: Data, +depth: Nat, a: Array>) -> Array>: 85 ANode{a, new_vals(~T, depth)} 86 87 def grown_links(+depth: Nat, a: Array) -> Array: 88 ANode{a, new_links(depth)} 89 90 # The end pointer after linking n next to a (nil: n becomes that end). 91 def pick_end(none: Bool, +n: U32, +e: U32) -> U32: 92 match none: 93 case True{}: 94 n 95 case False{}: 96 e 97 98 # Store x at slot n between the links a and b (either may be nil) and relink them. 99 def link_in(~T: Data, +tag: U32, +n: U32, +nfresh: U32, +nfree: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +a: U32, +b: U32, x: T) -> DList & E.Handle: 100 (DL{tag, nfresh, nfree, 1n+count, pick_end(U32.is_eq(a, nil()), link(n), head), pick_end(U32.is_eq(b, nil()), link(n), tail), depth, cap, 101 Array.set(Maybe<&2, T>, vals, n, Some{x}), 102 set_next(Array.set(U32, prevs, n, a), b, link(n)), 103 set_next(Array.set(U32, nexts, n, b), a, link(n))}, E.H{tag, n}) 104 105 def insert_room(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +a: U32, +b: U32, x: T, room: Bool) -> DList & E.Handle: 106 match room: 107 case True{}: 108 link_in(~T, tag, fresh, U32.inc(fresh), free, count, head, tail, depth, cap, vals, prevs, nexts, a, b, x) 109 case False{}: 110 link_in(~T, tag, fresh, U32.inc(fresh), free, count, head, tail, 1n+depth, U32.shl(cap), grown_vals(~T, depth, vals), grown_links(depth, prevs), grown_links(depth, nexts), a, b, x) 111 112 def insert_between(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +a: U32, +b: U32, x: T) -> DList & E.Handle: 113 insert_room(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, a, b, x, U32.is_lt(fresh, cap)) 114 115 def length(~T: Data, s: DList) -> DList & Nat: 116 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 117 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, count) 118 119 def push_front(~T: Data, s: DList, x: T) -> DList & E.Handle: 120 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 121 insert_between(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, nil(), head, x) 122 123 def push_back(~T: Data, s: DList, x: T) -> DList & E.Handle: 124 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 125 insert_between(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, tail, nil(), x) 126 127 def done_handle(~T: Data, r: DList & E.Handle) -> DList & Result<&2, &2, E.Error, E.Handle>: 128 (s, h) = r 129 (s, Done{h}) 130 131 # ---- validating a handle ---- 132 # 133 # `live(i)` reads the value slot; every handle operation branches on it. 134 135 def fail_same(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, e: E.Error) -> DList & E.Error: 136 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, e) 137 138 # The neighbour link on one side of a live element. 139 def link_at(links: Array, +i: U32) -> Array & U32: 140 Array.get(U32, links, i) 141 142 def ins_side(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +i: U32, +p: U32, +n: U32, x: T) -> DList & Result<&2, &2, E.Error, E.Handle>: 143 match after: 144 case False{}: 145 done_handle(~T, insert_between(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, p, link(i), x)) 146 case True{}: 147 done_handle(~T, insert_between(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, link(i), n, x)) 148 149 def ins_live2(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, +i: U32, x: T, pr: Array & U32, nx: Array & U32) -> DList & Result<&2, &2, E.Error, E.Handle>: 150 (prevs, p) = pr 151 (nexts, n) = nx 152 ins_side(~T, after, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, p, n, x) 153 154 def ins_found(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array, nexts: Array, +i: U32, x: T, r: Array> & Maybe<&2, T>) -> DList & Result<&2, &2, E.Error, E.Handle>: 155 (vals, m) = r 156 match m: 157 case None{}: 158 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}}) 159 case Some{v}: 160 ins_live2(~T, after, tag, fresh, free, count, head, tail, depth, cap, vals, i, x, link_at(prevs, i), link_at(nexts, i)) 161 162 def insert_checked(~T: Data, after: Bool, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +i: U32, x: T, same: Bool) -> DList & Result<&2, &2, E.Error, E.Handle>: 163 match ok same: 164 case _ False{}: 165 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}}) 166 case False{} True{}: 167 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}}) 168 case True{} True{}: 169 ins_found(~T, after, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, i, x, Array.get(Maybe<&2, T>, vals, i)) 170 171 def insert_before(~T: Data, s: DList, h: E.Handle, x: T) -> DList & Result<&2, &2, E.Error, E.Handle>: 172 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 173 E.H{+l, +i} = h 174 insert_checked(~T, False{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, x, U32.is_eq(l, tag)) 175 176 def insert_after(~T: Data, s: DList, h: E.Handle, x: T) -> DList & Result<&2, &2, E.Error, E.Handle>: 177 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 178 E.H{+l, +i} = h 179 insert_checked(~T, True{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, x, U32.is_eq(l, tag)) 180 181 # ---- removal ---- 182 183 def rm_links(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, +v: T, pr: Array & U32, nx: Array & U32) -> DList & Result<&2, &2, E.Error, T>: 184 (prevs, +p) = pr 185 (nexts, +n) = nx 186 (DL{tag, fresh, free, Nat.sub(count, 1n), pick_end(U32.is_eq(p, nil()), n, head), pick_end(U32.is_eq(n, nil()), p, tail), depth, cap, 187 vals, set_next(prevs, n, p), set_next(nexts, p, n)}, Done{v}) 188 189 def rm_found(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array, nexts: Array, +i: U32, r: Array> & Maybe<&2, T>) -> DList & Result<&2, &2, E.Error, T>: 190 (vals, m) = r 191 match m: 192 case None{}: 193 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}}) 194 case Some{+v}: 195 rm_links(~T, tag, fresh, free, count, head, tail, depth, cap, Array.set(Maybe<&2, T>, vals, i, None{}), v, link_at(prevs, i), link_at(nexts, i)) 196 197 def remove_checked(~T: Data, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +i: U32, same: Bool) -> DList & Result<&2, &2, E.Error, T>: 198 match ok same: 199 case _ False{}: 200 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}}) 201 case False{} True{}: 202 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}}) 203 case True{} True{}: 204 rm_found(~T, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, i, Array.get(Maybe<&2, T>, vals, i)) 205 206 def remove(~T: Data, s: DList, h: E.Handle) -> DList & Result<&2, &2, E.Error, T>: 207 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 208 E.H{+l, +i} = h 209 remove_checked(~T, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, U32.is_eq(l, tag)) 210 211 # ---- reading and writing one element ---- 212 213 def value_of(~T: Data, m: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>: 214 match m: 215 case None{}: 216 Fail{E.StaleHandle{}} 217 case Some{v}: 218 Done{v} 219 220 def get_fin(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array, nexts: Array, r: Array> & Maybe<&2, T>) -> DList & Result<&2, &2, E.Error, T>: 221 (vals, m) = r 222 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, value_of(~T, m)) 223 224 def get_checked(~T: Data, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +i: U32, same: Bool) -> DList & Result<&2, &2, E.Error, T>: 225 match ok same: 226 case _ False{}: 227 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}}) 228 case False{} True{}: 229 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}}) 230 case True{} True{}: 231 get_fin(~T, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, Array.get(Maybe<&2, T>, vals, i)) 232 233 def get(~T: Data, s: DList, h: E.Handle) -> DList & Result<&2, &2, E.Error, T>: 234 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 235 E.H{+l, +i} = h 236 get_checked(~T, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, U32.is_eq(l, tag)) 237 238 def set_fin(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array, nexts: Array, +i: U32, x: T, r: Array> & Maybe<&2, T>) -> DList & Result<&2, &2, E.Error, Unit>: 239 (vals, m) = r 240 match m: 241 case None{}: 242 (DL{tag, fresh, free, count, head, tail, depth, cap, Array.set(Maybe<&2, T>, vals, i, None{}), prevs, nexts}, Fail{E.StaleHandle{}}) 243 case Some{v}: 244 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Done{Unit{}}) 245 246 # set swaps the new value in: one indexed access when the element is live; 247 # a stale slot is None and is written back as None. 248 def set_checked(~T: Data, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +i: U32, +x: T, same: Bool) -> DList & Result<&2, &2, E.Error, Unit>: 249 match ok same: 250 case _ False{}: 251 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}}) 252 case False{} True{}: 253 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}}) 254 case True{} True{}: 255 set_fin(~T, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, i, x, Array.swap(Maybe<&2, T>, vals, i, Some{x})) 256 257 def set(~T: Data, s: DList, h: E.Handle, x: T) -> DList & Result<&2, &2, E.Error, Unit>: 258 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 259 E.H{+l, +i} = h 260 set_checked(~T, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, x, U32.is_eq(l, tag)) 261 262 # ---- neighbours ---- 263 264 def handle_go(+tag: U32, +l: U32, none: Bool) -> Maybe<&2, E.Handle>: 265 match none: 266 case True{}: 267 None{} 268 case False{}: 269 Some{E.H{tag, slot(l)}} 270 271 def handle(+tag: U32, +l: U32) -> Maybe<&2, E.Handle>: 272 handle_go(tag, l, U32.is_eq(l, nil())) 273 274 def nbr_n(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, r: Array & U32) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 275 (nexts, +n) = r 276 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Done{handle(tag, n)}) 277 278 def nbr_p(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, nexts: Array, r: Array & U32) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 279 (prevs, +p) = r 280 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Done{handle(tag, p)}) 281 282 def nbr_fin(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +i: U32, m: Maybe<&2, T>) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 283 match after m: 284 case _ None{}: 285 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}}) 286 case True{} Some{v}: 287 nbr_n(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, link_at(nexts, i)) 288 case False{} Some{v}: 289 nbr_p(~T, tag, fresh, free, count, head, tail, depth, cap, vals, nexts, link_at(prevs, i)) 290 291 def nbr_read(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array, nexts: Array, +i: U32, r: Array> & Maybe<&2, T>) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 292 (vals, m) = r 293 nbr_fin(~T, after, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, m) 294 295 def nbr_checked(~T: Data, after: Bool, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +i: U32, same: Bool) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 296 match ok same: 297 case _ False{}: 298 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}}) 299 case False{} True{}: 300 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}}) 301 case True{} True{}: 302 nbr_read(~T, after, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, i, Array.get(Maybe<&2, T>, vals, i)) 303 304 def next(~T: Data, s: DList, h: E.Handle) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 305 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 306 E.H{+l, +i} = h 307 nbr_checked(~T, True{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, U32.is_eq(l, tag)) 308 309 def prev(~T: Data, s: DList, h: E.Handle) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 310 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 311 E.H{+l, +i} = h 312 nbr_checked(~T, False{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, U32.is_eq(l, tag)) 313 314 # ---- to_list ---- 315 # 316 # Walk BACKWARDS from the tail, consing onto an accumulator, so the list 317 # comes out in order and the walk is a tail call; the count bounds it. 318 319 # One loop, no mutual recursion: the state carries the next id to read. 320 type Cur<-T: Data> is Type: 321 C{vals: Array>, prevs: Array, acc: List<&2, T>, at: U32} 322 323 def step_p(~T: Data, vals: Array>, acc: List<&2, T>, r: Array & U32) -> Cur: 324 (prevs, p) = r 325 C{vals, prevs, acc, p} 326 327 def step_m(~T: Data, vals: Array>, prevs: Array, acc: List<&2, T>, +at: U32, m: Maybe<&2, T>) -> Cur: 328 match m: 329 case None{}: 330 C{vals, prevs, acc, nil()} 331 case Some{v}: 332 step_p(~T, vals, Con{v, acc}, Array.get(U32, prevs, slot(at))) 333 334 def step_v(~T: Data, prevs: Array, acc: List<&2, T>, +at: U32, r: Array> & Maybe<&2, T>) -> Cur: 335 (vals, m) = r 336 step_m(~T, vals, prevs, acc, at, m) 337 338 def step_back(~T: Data, c: Cur) -> Cur: 339 C{vals, prevs, acc, +at} = c 340 step_v(~T, prevs, acc, at, Array.get(Maybe<&2, T>, vals, slot(at))) 341 342 def walk(~T: Data, fuel: Nat, c: Cur) -> Cur: 343 match fuel: 344 case 0n: 345 c 346 case 1n+f: 347 walk(~T, f, step_back(~T, c)) 348 349 def tl_fin(~T: Data, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, nexts: Array, c: Cur) -> DList & List<&2, T>: 350 C{vals, prevs, acc, at} = c 351 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, acc) 352 353 def to_list(~T: Data, s: DList) -> DList & List<&2, T>: 354 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 355 tl_fin(~T, tag, fresh, free, count, head, tail, depth, cap, nexts, walk(~T, count, C{vals, prevs, Nil{}, tail})) 356 357 # ---- recycling end operations: the deque's storage API ---- 358 # 359 # `free` is a STACK of retired slots chained through `nexts`: the record's 360 # field is the link to the top (nil() = empty) and `nexts[s]` of a retired 361 # slot s is the link to the next retired one. A retired slot holds None in 362 # `vals` and is not in the list. 363 # 364 # The handle-stable API above NEVER touches this stack: its ids come from the 365 # monotone `fresh` counter and are never reused, so a handle to a removed 366 # element stays unambiguously stale (the objective's handle contract). The 367 # operations below DO recycle, and they are the storage operations 368 # src/deque.bend runs on: a deque exposes no handles at all, so reissuing an 369 # id is unobservable through it, and the arenas then grow with the PEAK 370 # number of live elements instead of with the number of pushes. They are not 371 # members of `Op`, so the list's trace laws are unaffected by them; they have 372 # component laws under proofs/dlist/reuse_*.bend and free_chain.bend. 373 # The general deque refinement is still being composed. 374 # 375 # Every one of them is O(1) indexed reads and writes. 376 377 # Allocate the top of the free stack: `nx` is the link it stored, which 378 # becomes the new top. `nexts[i]` is overwritten by `link_in`, after the read. 379 def ins_free_pop(~T: Data, +tag: U32, +fresh: U32, +f: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, +a: U32, +b: U32, x: T, r: Array & U32) -> DList & E.Handle: 380 (nexts, +nx) = r 381 link_in(~T, tag, slot(f), fresh, nx, count, head, tail, depth, cap, vals, prevs, nexts, a, b, x) 382 383 def ins_free_pick(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +a: U32, +b: U32, x: T, empty: Bool) -> DList & E.Handle: 384 match empty: 385 case True{}: 386 insert_between(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, a, b, x) 387 case False{}: 388 ins_free_pop(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, a, b, x, link_at(nexts, slot(free))) 389 390 def insert_between_free(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +a: U32, +b: U32, x: T) -> DList & E.Handle: 391 ins_free_pick(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, a, b, x, U32.is_eq(free, nil())) 392 393 def push_front_free(~T: Data, s: DList, x: T) -> DList & E.Handle: 394 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 395 insert_between_free(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, nil(), head, x) 396 397 def push_back_free(~T: Data, s: DList, x: T) -> DList & E.Handle: 398 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 399 insert_between_free(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, tail, nil(), x) 400 401 # Unlink the element at slot i and push i on the free stack. `set_next` writes 402 # at the NEIGHBOUR slots (both different from i), so the last write, which 403 # stores the old top in nexts[i], cannot be overwritten. 404 def rmf_links(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, +i: U32, v: T, pr: Array & U32, nx: Array & U32) -> DList & Maybe<&2, T>: 405 (prevs, +p) = pr 406 (nexts, +n) = nx 407 (DL{tag, fresh, link(i), Nat.sub(count, 1n), pick_end(U32.is_eq(p, nil()), n, head), pick_end(U32.is_eq(n, nil()), p, tail), depth, cap, 408 vals, set_next(prevs, n, p), Array.set(U32, set_next(nexts, p, n), i, free)}, Some{v}) 409 410 def rmf_found(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array, nexts: Array, +i: U32, r: Array> & Maybe<&2, T>) -> DList & Maybe<&2, T>: 411 (vals, m) = r 412 match m: 413 case None{}: 414 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, None{}) 415 case Some{v}: 416 rmf_links(~T, tag, fresh, free, count, head, tail, depth, cap, Array.set(Maybe<&2, T>, vals, i, None{}), i, v, link_at(prevs, i), link_at(nexts, i)) 417 418 def pop_end(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +l: U32, empty: Bool) -> DList & Maybe<&2, T>: 419 match empty: 420 case True{}: 421 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, None{}) 422 case False{}: 423 rmf_found(~T, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, slot(l), Array.get(Maybe<&2, T>, vals, slot(l))) 424 425 def pop_front_free(~T: Data, s: DList) -> DList & Maybe<&2, T>: 426 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 427 pop_end(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, head, U32.is_eq(head, nil())) 428 429 def pop_back_free(~T: Data, s: DList) -> DList & Maybe<&2, T>: 430 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 431 pop_end(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, tail, U32.is_eq(tail, nil())) 432 433 def peek_fin(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array, nexts: Array, r: Array> & Maybe<&2, T>) -> DList & Maybe<&2, T>: 434 (vals, m) = r 435 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, m) 436 437 def peek_end(~T: Data, +tag: U32, +fresh: U32, +free: U32, count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +l: U32, empty: Bool) -> DList & Maybe<&2, T>: 438 match empty: 439 case True{}: 440 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, None{}) 441 case False{}: 442 peek_fin(~T, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, Array.get(Maybe<&2, T>, vals, slot(l))) 443 444 def peek_front(~T: Data, s: DList) -> DList & Maybe<&2, T>: 445 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 446 peek_end(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, head, U32.is_eq(head, nil())) 447 448 def peek_back(~T: Data, s: DList) -> DList & Maybe<&2, T>: 449 DL{+tag, +fresh, +free, count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 450 peek_end(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, tail, U32.is_eq(tail, nil())) 451 452 # ---- trace runner ---- 453 454 def obs_nat(~T: Data, r: DList & Nat) -> DList & E.Obs: 455 (s, n) = r 456 (s, E.ONat{n}) 457 458 def obs_handle(~T: Data, r: DList & E.Handle) -> DList & E.Obs: 459 (s, h) = r 460 (s, E.OHandle{h}) 461 462 def obs_insert(~T: Data, r: DList & Result<&2, &2, E.Error, E.Handle>) -> DList & E.Obs: 463 (s, x) = r 464 (s, E.OInsert{x}) 465 466 def obs_val(~T: Data, r: DList & Result<&2, &2, E.Error, T>) -> DList & E.Obs: 467 (s, x) = r 468 (s, E.OVal{x}) 469 470 def obs_unit(~T: Data, r: DList & Result<&2, &2, E.Error, Unit>) -> DList & E.Obs: 471 (s, x) = r 472 (s, E.OUnit{x}) 473 474 def obs_nbr(~T: Data, r: DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>) -> DList & E.Obs: 475 (s, x) = r 476 (s, E.ONbr{x}) 477 478 def obs_list(~T: Data, r: DList & List<&2, T>) -> DList & E.Obs: 479 (s, xs) = r 480 (s, E.OList{xs}) 481 482 def step(~T: Data, s: DList, op: E.Op) -> DList & E.Obs: 483 match op: 484 case E.Length{}: 485 obs_nat(~T, length(~T, s)) 486 case E.PushFront{x}: 487 obs_handle(~T, push_front(~T, s, x)) 488 case E.PushBack{x}: 489 obs_handle(~T, push_back(~T, s, x)) 490 case E.InsertBefore{h, x}: 491 obs_insert(~T, insert_before(~T, s, h, x)) 492 case E.InsertAfter{h, x}: 493 obs_insert(~T, insert_after(~T, s, h, x)) 494 case E.Remove{h}: 495 obs_val(~T, remove(~T, s, h)) 496 case E.Get{h}: 497 obs_val(~T, get(~T, s, h)) 498 case E.Set{h, x}: 499 obs_unit(~T, set(~T, s, h, x)) 500 case E.Next{h}: 501 obs_nbr(~T, next(~T, s, h)) 502 case E.Prev{h}: 503 obs_nbr(~T, prev(~T, s, h)) 504 case E.ToList{}: 505 obs_list(~T, to_list(~T, s)) 506 507 def record(~T: Data, acc: List<&2, E.Obs>, r: DList & E.Obs) -> DList & List<&2, E.Obs>: 508 (s, o) = r 509 (s, Con{o, acc}) 510 511 def step_acc(~T: Data, op: E.Op, st: DList & List<&2, E.Obs>) -> DList & List<&2, E.Obs>: 512 (s, acc) = st 513 record(~T, acc, step(~T, s, op)) 514 515 def run_acc(~T: Data, ops: List<&2, E.Op>, st: DList & List<&2, E.Obs>) -> DList & List<&2, E.Obs>: 516 match ops: 517 case Nil{}: 518 st 519 case Con{op, rest}: 520 run_acc(~T, rest, step_acc(~T, op, st)) 521 522 def finish(~T: Data, st: DList & List<&2, E.Obs>) -> DList & List<&2, E.Obs>: 523 (s, acc) = st 524 (s, List.reverse(&2, E.Obs, acc)) 525 526 def run(~T: Data, ops: List<&2, E.Op>, s: DList) -> DList & List<&2, E.Obs>: 527 finish(~T, run_acc(~T, ops, (s, Nil{}))) 528 529 # Internal insertion variants for a generational public handle owner. 530 def ins_side_reuse(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +i: U32, +p: U32, +n: U32, x: T) -> DList & Result<&2, &2, E.Error, E.Handle>: 531 match after: 532 case False{}: 533 done_handle(~T, insert_between_free(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, p, link(i), x)) 534 case True{}: 535 done_handle(~T, insert_between_free(~T, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, link(i), n, x)) 536 537 def ins_live2_reuse(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, +i: U32, x: T, pr: Array & U32, nx: Array & U32) -> DList & Result<&2, &2, E.Error, E.Handle>: 538 (prevs, p) = pr 539 (nexts, n) = nx 540 ins_side_reuse(~T, after, tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, p, n, x) 541 542 def ins_found_reuse(~T: Data, after: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, prevs: Array, nexts: Array, +i: U32, x: T, r: Array> & Maybe<&2, T>) -> DList & Result<&2, &2, E.Error, E.Handle>: 543 (vals, m) = r 544 match m: 545 case None{}: 546 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}}) 547 case Some{v}: 548 ins_live2_reuse(~T, after, tag, fresh, free, count, head, tail, depth, cap, vals, i, x, link_at(prevs, i), link_at(nexts, i)) 549 550 def insert_checked_reuse(~T: Data, after: Bool, ok: Bool, +tag: U32, +fresh: U32, +free: U32, +count: Nat, +head: U32, +tail: U32, +depth: Nat, +cap: U32, vals: Array>, prevs: Array, nexts: Array, +i: U32, x: T, same: Bool) -> DList & Result<&2, &2, E.Error, E.Handle>: 551 match ok same: 552 case _ False{}: 553 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.ForeignHandle{}}) 554 case False{} True{}: 555 (DL{tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts}, Fail{E.StaleHandle{}}) 556 case True{} True{}: 557 ins_found_reuse(~T, after, tag, fresh, free, count, head, tail, depth, cap, prevs, nexts, i, x, Array.get(Maybe<&2, T>, vals, i)) 558 559 def insert_before_reuse(~T: Data, s: DList, h: E.Handle, x: T) -> DList & Result<&2, &2, E.Error, E.Handle>: 560 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 561 E.H{+l, +i} = h 562 insert_checked_reuse(~T, False{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, x, U32.is_eq(l, tag)) 563 564 def insert_after_reuse(~T: Data, s: DList, h: E.Handle, x: T) -> DList & Result<&2, &2, E.Error, E.Handle>: 565 DL{+tag, +fresh, +free, +count, +head, +tail, +depth, +cap, vals, prevs, nexts} = s 566 E.H{+l, +i} = h 567 insert_checked_reuse(~T, True{}, U32.is_lt(i, fresh), tag, fresh, free, count, head, tail, depth, cap, vals, prevs, nexts, i, x, U32.is_eq(l, tag)) 568 569 570 # Called only after a successful remove, by an owner that invalidated the 571 # removed handle's generation. The slot is already absent from the live list. 572 def recycle_slot(~T: Data, s: DList, +i: U32) -> DList: 573 DL{tag, fresh, +free, count, head, tail, depth, cap, vals, prevs, nexts} = s 574 DL{tag, fresh, link(i), count, head, tail, depth, cap, vals, prevs, Array.set(U32, nexts, i, free)}