1 import Base 2 import ./internal/dlist_storage.bend as R 3 import ./types/internal_dlist.bend as I 4 import ./types/doubly_linked_list.bend as E 5 6 # Public generational handles over the shared indexed DLL storage. 7 # Removed slots are reused. A generation at UINT32_MAX is retired forever 8 # instead of wrapping; capacity therefore follows peak live + exhausted slots. 9 # Values are released by remove, but the pool keeps capacity for later use. 10 type DList<-T: Data> is Type: 11 DL{tag: U32, depth: Nat, cap: U32, storage: R.DList, generations: Array} 12 13 def new(~T: Data, +tag: U32) -> DList: 14 DL{tag, 0n, 1, R.new(~T, tag), Array.new(U32, 0n, 0)} 15 16 def error(e: I.Error) -> E.Error: 17 match e: 18 case I.ForeignHandle{}: 19 E.ForeignHandle{} 20 case I.StaleHandle{}: 21 E.StaleHandle{} 22 23 def old_handle(h: E.Handle) -> I.Handle: 24 E.H{tag, id, generation} = h 25 I.H{tag, id} 26 27 def inserted_gen(~T: Data, +tag: U32, depth: Nat, cap: U32, raw: R.DList, id: U32, r: Array & U32) -> DList & E.Handle: 28 (gens, generation) = r 29 (DL{tag, depth, cap, raw, gens}, E.H{tag, id, generation}) 30 31 def inserted_room(~T: Data, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList, gens: Array, +id: U32, grow: Bool) -> DList & E.Handle: 32 match grow: 33 case False{}: 34 inserted_gen(~T, tag, depth, cap, raw, id, Array.get(U32, gens, id)) 35 case True{}: 36 inserted_gen(~T, tag, 1n+depth, U32.shl(cap), raw, id, Array.get(U32, ANode{gens, Array.new(U32, depth, 0)}, id)) 37 38 def inserted(~T: Data, +tag: U32, depth: Nat, +cap: U32, gens: Array, r: R.DList & I.Handle) -> DList & E.Handle: 39 (raw, I.H{rtag, +id}) = r 40 inserted_room(~T, tag, depth, cap, raw, gens, id, U32.is_eq(id, cap)) 41 42 def push_front(~T: Data, s: DList, x: T) -> DList & E.Handle: 43 DL{+tag, depth, +cap, raw, gens} = s 44 inserted(~T, tag, depth, cap, gens, R.push_front_free(~T, raw, x)) 45 46 def push_back(~T: Data, s: DList, x: T) -> DList & E.Handle: 47 DL{+tag, depth, +cap, raw, gens} = s 48 inserted(~T, tag, depth, cap, gens, R.push_back_free(~T, raw, x)) 49 50 def generation_error(same: Bool) -> Maybe<&2, E.Error>: 51 match same: 52 case True{}: 53 None{} 54 case False{}: 55 Some{E.StaleHandle{}} 56 57 def valid_gen(~T: Data, tag: U32, depth: Nat, cap: U32, raw: R.DList, expected: U32, r: Array & U32) -> DList & Maybe<&2, E.Error>: 58 (gens, actual) = r 59 (DL{tag, depth, cap, raw, gens}, generation_error(U32.is_eq(actual, expected))) 60 61 def valid_bounds(~T: Data, tag: U32, depth: Nat, cap: U32, raw: R.DList, gens: Array, id: U32, expected: U32, same: Bool, inside: Bool) -> DList & Maybe<&2, E.Error>: 62 match same inside: 63 case False{} _: 64 (DL{tag, depth, cap, raw, gens}, Some{E.ForeignHandle{}}) 65 case True{} False{}: 66 (DL{tag, depth, cap, raw, gens}, Some{E.StaleHandle{}}) 67 case True{} True{}: 68 valid_gen(~T, tag, depth, cap, raw, expected, Array.get(U32, gens, id)) 69 70 def validate(~T: Data, s: DList, h: E.Handle) -> DList & Maybe<&2, E.Error>: 71 DL{+tag, depth, +cap, raw, gens} = s 72 E.H{owner, +id, expected} = h 73 valid_bounds(~T, tag, depth, cap, raw, gens, id, expected, U32.is_eq(tag, owner), U32.is_lt(id, cap)) 74 75 def item_result(~T: Data, r: Result<&2, &2, I.Error, T>) -> Result<&2, &2, E.Error, T>: 76 match r: 77 case Done{x}: 78 Done{x} 79 case Fail{e}: 80 Fail{error(e)} 81 82 def value_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array, r: R.DList & Result<&2, &2, I.Error, T>) -> DList & E.Obs: 83 (raw, result) = r 84 (DL{tag, depth, cap, raw, gens}, E.OVal{item_result(~T, result)}) 85 86 def unit_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array, r: R.DList & Result<&2, &2, I.Error, Unit>) -> DList & E.Obs: 87 (raw, result) = r 88 (DL{tag, depth, cap, raw, gens}, E.OUnit{item_result(~Unit, result)}) 89 90 def retire(~T: Data, tag: U32, depth: Nat, cap: U32, raw: R.DList, gens: Array, +id: U32, +generation: U32, v: T, exhausted: Bool) -> DList & E.Obs: 91 match exhausted: 92 case True{}: 93 (DL{tag, depth, cap, raw, gens}, E.OVal{Done{v}}) 94 case False{}: 95 (DL{tag, depth, cap, R.recycle_slot(~T, raw, id), Array.set(U32, gens, id, U32.inc(generation))}, E.OVal{Done{v}}) 96 97 def removed(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array, id: U32, +generation: U32, r: R.DList & Result<&2, &2, I.Error, T>) -> DList & E.Obs: 98 match r: 99 case Tuple{raw, Fail{e}}: 100 (DL{tag, depth, cap, raw, gens}, E.OVal{Fail{error(e)}}) 101 case Tuple{raw, Done{v}}: 102 retire(~T, tag, depth, cap, raw, gens, id, generation, v, U32.is_eq(generation, 4294967295)) 103 104 def relative_done(~T: Data, r: DList & E.Handle) -> DList & E.Obs: 105 (s, h) = r 106 (s, E.OInsert{Done{h}}) 107 108 def relative_result(~T: Data, +tag: U32, depth: Nat, +cap: U32, gens: Array, r: R.DList & Result<&2, &2, I.Error, I.Handle>) -> DList & E.Obs: 109 match r: 110 case Tuple{raw, Fail{e}}: 111 (DL{tag, depth, cap, raw, gens}, E.OInsert{Fail{error(e)}}) 112 case Tuple{raw, Done{I.H{owner, +id}}}: 113 relative_done(~T, inserted_room(~T, tag, depth, cap, raw, gens, id, U32.is_eq(id, cap))) 114 115 def neighbour_gen(~T: Data, tag: U32, depth: Nat, cap: U32, raw: R.DList, owner: U32, id: U32, r: Array & U32) -> DList & E.Obs: 116 (gens, generation) = r 117 (DL{tag, depth, cap, raw, gens}, E.ONbr{Done{Some{E.H{owner, id, generation}}}}) 118 119 def neighbour_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array, r: R.DList & Result<&2, &2, I.Error, Maybe<&2, I.Handle>>) -> DList & E.Obs: 120 match r: 121 case Tuple{raw, Fail{e}}: 122 (DL{tag, depth, cap, raw, gens}, E.ONbr{Fail{error(e)}}) 123 case Tuple{raw, Done{None{}}}: 124 (DL{tag, depth, cap, raw, gens}, E.ONbr{Done{None{}}}) 125 case Tuple{raw, Done{Some{I.H{owner, +id}}}}: 126 neighbour_gen(~T, tag, depth, cap, raw, owner, id, Array.get(U32, gens, id)) 127 128 def length_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array, r: R.DList & Nat) -> DList & E.Obs: 129 (raw, n) = r 130 (DL{tag, depth, cap, raw, gens}, E.ONat{n}) 131 132 def list_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array, r: R.DList & List<&2, T>) -> DList & E.Obs: 133 (raw, xs) = r 134 (DL{tag, depth, cap, raw, gens}, E.OList{xs}) 135 136 def pushed_obs(~T: Data, r: DList & E.Handle) -> DList & E.Obs: 137 (s, h) = r 138 (s, E.OHandle{h}) 139 140 def dispatch(~T: Data, s: DList, op: E.Op) -> DList & E.Obs: 141 DL{+tag, +depth, +cap, raw, gens} = s 142 match op: 143 case E.Length{}: 144 length_result(~T, tag, depth, cap, gens, R.length(~T, raw)) 145 case E.ToList{}: 146 list_result(~T, tag, depth, cap, gens, R.to_list(~T, raw)) 147 case E.PushFront{x}: 148 pushed_obs(~T, inserted(~T, tag, depth, cap, gens, R.push_front_free(~T, raw, x))) 149 case E.PushBack{x}: 150 pushed_obs(~T, inserted(~T, tag, depth, cap, gens, R.push_back_free(~T, raw, x))) 151 case E.Get{h}: 152 value_result(~T, tag, depth, cap, gens, R.get(~T, raw, old_handle(h))) 153 case E.Set{h, x}: 154 unit_result(~T, tag, depth, cap, gens, R.set(~T, raw, old_handle(h), x)) 155 case E.Remove{E.H{+owner, +id, generation}}: 156 removed(~T, tag, depth, cap, gens, id, generation, R.remove(~T, raw, I.H{owner, id})) 157 case E.Next{h}: 158 neighbour_result(~T, tag, depth, cap, gens, R.next(~T, raw, old_handle(h))) 159 case E.Prev{h}: 160 neighbour_result(~T, tag, depth, cap, gens, R.prev(~T, raw, old_handle(h))) 161 case E.InsertBefore{h, x}: 162 relative_result(~T, tag, depth, cap, gens, R.insert_before_reuse(~T, raw, old_handle(h), x)) 163 case E.InsertAfter{h, x}: 164 relative_result(~T, tag, depth, cap, gens, R.insert_after_reuse(~T, raw, old_handle(h), x)) 165 166 def op_handle(~T: Data, op: E.Op) -> Maybe<&2, E.Handle>: 167 match op: 168 case E.Get{h}: 169 Some{h} 170 case E.Set{h, x}: 171 Some{h} 172 case E.Remove{h}: 173 Some{h} 174 case E.Next{h}: 175 Some{h} 176 case E.Prev{h}: 177 Some{h} 178 case E.InsertBefore{h, x}: 179 Some{h} 180 case E.InsertAfter{h, x}: 181 Some{h} 182 case _: 183 None{} 184 185 def failed(~T: Data, op: E.Op, e: E.Error) -> E.Obs: 186 match op: 187 case E.Set{h, x}: 188 E.OUnit{Fail{e}} 189 case E.Next{h}: 190 E.ONbr{Fail{e}} 191 case E.Prev{h}: 192 E.ONbr{Fail{e}} 193 case E.InsertBefore{h, x}: 194 E.OInsert{Fail{e}} 195 case E.InsertAfter{h, x}: 196 E.OInsert{Fail{e}} 197 case _: 198 E.OVal{Fail{e}} 199 200 def checked(~T: Data, op: E.Op, r: DList & Maybe<&2, E.Error>) -> DList & E.Obs: 201 match r: 202 case Tuple{s, None{}}: 203 dispatch(~T, s, op) 204 case Tuple{s, Some{e}}: 205 (s, failed(~T, op, e)) 206 207 def step_handle(~T: Data, s: DList, op: E.Op, h: Maybe<&2, E.Handle>) -> DList & E.Obs: 208 match h: 209 case None{}: 210 dispatch(~T, s, op) 211 case Some{handle}: 212 checked(~T, op, validate(~T, s, handle)) 213 214 def step(~T: Data, s: DList, +op: E.Op) -> DList & E.Obs: 215 step_handle(~T, s, op, op_handle(~T, op)) 216 217 def project_value(~T: Data, r: DList & E.Obs) -> DList & Result<&2, &2, E.Error, T>: 218 match r: 219 case Tuple{s, E.OVal{x}}: 220 (s, x) 221 case Tuple{s, other}: 222 (s, Fail{E.StaleHandle{}}) 223 224 def project_unit(~T: Data, r: DList & E.Obs) -> DList & Result<&2, &2, E.Error, Unit>: 225 match r: 226 case Tuple{s, E.OUnit{x}}: 227 (s, x) 228 case Tuple{s, other}: 229 (s, Fail{E.StaleHandle{}}) 230 231 def project_insert(~T: Data, r: DList & E.Obs) -> DList & Result<&2, &2, E.Error, E.Handle>: 232 match r: 233 case Tuple{s, E.OInsert{x}}: 234 (s, x) 235 case Tuple{s, other}: 236 (s, Fail{E.StaleHandle{}}) 237 238 def project_neighbour(~T: Data, r: DList & E.Obs) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 239 match r: 240 case Tuple{s, E.ONbr{x}}: 241 (s, x) 242 case Tuple{s, other}: 243 (s, Fail{E.StaleHandle{}}) 244 245 def project_length(~T: Data, r: DList & E.Obs) -> DList & Nat: 246 match r: 247 case Tuple{s, E.ONat{x}}: 248 (s, x) 249 case Tuple{s, other}: 250 (s, 0n) 251 252 def project_list(~T: Data, r: DList & E.Obs) -> DList & List<&2, T>: 253 match r: 254 case Tuple{s, E.OList{x}}: 255 (s, x) 256 case Tuple{s, other}: 257 (s, Nil{}) 258 259 def length_direct_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array, r: R.DList & Nat) -> DList & Nat: 260 (raw, n) = r 261 (DL{tag, depth, cap, raw, gens}, n) 262 263 def length(~T: Data, s: DList) -> DList & Nat: 264 DL{tag, depth, cap, raw, gens} = s 265 length_direct_result(~T, tag, depth, cap, gens, R.length(~T, raw)) 266 267 def to_list_direct_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array, r: R.DList & List<&2, T>) -> DList & List<&2, T>: 268 (raw, xs) = r 269 (DL{tag, depth, cap, raw, gens}, xs) 270 271 def to_list(~T: Data, s: DList) -> DList & List<&2, T>: 272 DL{tag, depth, cap, raw, gens} = s 273 to_list_direct_result(~T, tag, depth, cap, gens, R.to_list(~T, raw)) 274 275 # Direct public read path. Keep generation validation, but avoid allocating an 276 # Op/Obs envelope and executing the general trace dispatcher for one get. 277 def get_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array, r: R.DList & Result<&2, &2, I.Error, T>) -> DList & Result<&2, &2, E.Error, T>: 278 (raw, result) = r 279 (DL{tag, depth, cap, raw, gens}, item_result(~T, result)) 280 281 def get_ready(~T: Data, h: E.Handle, r: DList & Maybe<&2, E.Error>) -> DList & Result<&2, &2, E.Error, T>: 282 match r: 283 case Tuple{s, Some{e}}: 284 (s, Fail{e}) 285 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}: 286 get_result(~T, tag, depth, cap, gens, R.get(~T, raw, old_handle(h))) 287 288 def get(~T: Data, s: DList, +h: E.Handle) -> DList & Result<&2, &2, E.Error, T>: 289 get_ready(~T, h, validate(~T, s, h)) 290 291 def remove_ready(~T: Data, h: E.Handle, r: DList & Maybe<&2, E.Error>) -> DList & Result<&2, &2, E.Error, T>: 292 match h r: 293 case E.H{owner, id, generation} Tuple{s, Some{e}}: 294 (s, Fail{e}) 295 case E.H{+owner, +id, generation} Tuple{DL{tag, depth, cap, raw, gens}, None{}}: 296 project_value(~T, removed(~T, tag, depth, cap, gens, id, generation, R.remove(~T, raw, I.H{owner, id}))) 297 298 def remove(~T: Data, s: DList, +h: E.Handle) -> DList & Result<&2, &2, E.Error, T>: 299 remove_ready(~T, h, validate(~T, s, h)) 300 301 def set_result(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array, r: R.DList & Result<&2, &2, I.Error, Unit>) -> DList & Result<&2, &2, E.Error, Unit>: 302 (raw, result) = r 303 (DL{tag, depth, cap, raw, gens}, item_result(~Unit, result)) 304 305 def set_ready(~T: Data, +h: E.Handle, x: T, r: DList & Maybe<&2, E.Error>) -> DList & Result<&2, &2, E.Error, Unit>: 306 match r: 307 case Tuple{s, Some{e}}: 308 (s, Fail{e}) 309 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}: 310 set_result(~T, tag, depth, cap, gens, R.set(~T, raw, old_handle(h), x)) 311 312 def set(~T: Data, s: DList, +h: E.Handle, x: T) -> DList & Result<&2, &2, E.Error, Unit>: 313 set_ready(~T, h, x, validate(~T, s, h)) 314 315 def next_ready(~T: Data, +h: E.Handle, r: DList & Maybe<&2, E.Error>) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 316 match r: 317 case Tuple{s, Some{e}}: 318 (s, Fail{e}) 319 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}: 320 project_neighbour(~T, neighbour_result(~T, tag, depth, cap, gens, R.next(~T, raw, old_handle(h)))) 321 322 def next(~T: Data, s: DList, +h: E.Handle) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 323 next_ready(~T, h, validate(~T, s, h)) 324 325 def prev_ready(~T: Data, +h: E.Handle, r: DList & Maybe<&2, E.Error>) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 326 match r: 327 case Tuple{s, Some{e}}: 328 (s, Fail{e}) 329 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}: 330 project_neighbour(~T, neighbour_result(~T, tag, depth, cap, gens, R.prev(~T, raw, old_handle(h)))) 331 332 def prev(~T: Data, s: DList, +h: E.Handle) -> DList & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>: 333 prev_ready(~T, h, validate(~T, s, h)) 334 335 def insert_before_ready(~T: Data, +h: E.Handle, +x: T, r: DList & Maybe<&2, E.Error>) -> DList & Result<&2, &2, E.Error, E.Handle>: 336 match r: 337 case Tuple{s, Some{e}}: 338 (s, Fail{e}) 339 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}: 340 project_insert(~T, relative_result(~T, tag, depth, cap, gens, R.insert_before_reuse(~T, raw, old_handle(h), x))) 341 342 def insert_before(~T: Data, s: DList, +h: E.Handle, x: T) -> DList & Result<&2, &2, E.Error, E.Handle>: 343 insert_before_ready(~T, h, x, validate(~T, s, h)) 344 345 def insert_after_ready(~T: Data, +h: E.Handle, +x: T, r: DList & Maybe<&2, E.Error>) -> DList & Result<&2, &2, E.Error, E.Handle>: 346 match r: 347 case Tuple{s, Some{e}}: 348 (s, Fail{e}) 349 case Tuple{DL{tag, depth, cap, raw, gens}, None{}}: 350 project_insert(~T, relative_result(~T, tag, depth, cap, gens, R.insert_after_reuse(~T, raw, old_handle(h), x))) 351 352 def insert_after(~T: Data, s: DList, +h: E.Handle, x: T) -> DList & Result<&2, &2, E.Error, E.Handle>: 353 insert_after_ready(~T, h, x, validate(~T, s, h)) 354 355 def record(~T: Data, acc: List<&2, E.Obs>, r: DList & E.Obs) -> DList & List<&2, E.Obs>: 356 (s, o) = r 357 (s, Con{o, acc}) 358 359 def step_acc(~T: Data, op: E.Op, st: DList & List<&2, E.Obs>) -> DList & List<&2, E.Obs>: 360 (s, acc) = st 361 record(~T, acc, step(~T, s, op)) 362 363 def run_acc(~T: Data, ops: List<&2, E.Op>, st: DList & List<&2, E.Obs>) -> DList & List<&2, E.Obs>: 364 match ops: 365 case Nil{}: 366 st 367 case Con{op, rest}: 368 run_acc(~T, rest, step_acc(~T, op, st)) 369 370 def finish(~T: Data, st: DList & List<&2, E.Obs>) -> DList & List<&2, E.Obs>: 371 (s, acc) = st 372 (s, List.reverse(&2, E.Obs, acc)) 373 374 def run(~T: Data, ops: List<&2, E.Op>, s: DList) -> DList & List<&2, E.Obs>: 375 finish(~T, run_acc(~T, ops, (s, Nil{})))