src/containers/intrusive_links.bend source

src/containers/intrusive_links.bend on the hub · documented module

import Baseimport ./intrusive_doubly_linked_list.bend as IL# A ready-made link table for the intrusive list: entity ids are U32 values# 1 .. 2^node_depth - 1 (0 means "no entity"), roots are 0 .. 2^root_depth - 1.# One U32 per link, so a membership edit is a few indexed array writes. The# accessors below are the ones proved to meet the adapter laws for every size# (proofs/containers/intrusive_doubly_linked_list/links.bend); an application# that keeps its own entity array can copy this layout.type Links is Type:  Links{nexts: Array<U32>, prevs: Array<U32>, heads: Array<U32>}def new(+node_depth: Nat, +root_depth: Nat) -> Links:  Links{Array.new(U32, node_depth, 0), Array.new(U32, node_depth, 0), Array.new(U32, root_depth, 0)}def decode_pick(+x: U32, zero: Bool) -> Maybe<&2, U32>:  match zero:    case True{}:      None{}    case False{}:      Some{x}def decode(+x: U32) -> Maybe<&2, U32>:  decode_pick(x, U32.is_eq(x, 0))def encode(m: Maybe<&2, U32>) -> U32:  match m:    case None{}:      0    case Some{x}:      xdef next_got(prevs: Array<U32>, heads: Array<U32>, r: Array<U32> & U32) -> Links & Maybe<&2, U32>:  (nexts, +x) = r  (Links{nexts, prevs, heads}, decode(x))def prev_got(nexts: Array<U32>, heads: Array<U32>, r: Array<U32> & U32) -> Links & Maybe<&2, U32>:  (prevs, +x) = r  (Links{nexts, prevs, heads}, decode(x))def head_got(nexts: Array<U32>, prevs: Array<U32>, r: Array<U32> & U32) -> Links & Maybe<&2, U32>:  (heads, +x) = r  (Links{nexts, prevs, heads}, decode(x))def next(s: Links, n: U32) -> Links & Maybe<&2, U32>:  Links{nexts, prevs, heads} = s  next_got(prevs, heads, Array.get(U32, nexts, n))def prev(s: Links, n: U32) -> Links & Maybe<&2, U32>:  Links{nexts, prevs, heads} = s  prev_got(nexts, heads, Array.get(U32, prevs, n))def get_head(s: Links, r: U32) -> Links & Maybe<&2, U32>:  Links{nexts, prevs, heads} = s  head_got(nexts, prevs, Array.get(U32, heads, r))def set_next(s: Links, n: U32, m: Maybe<&2, U32>) -> Links:  Links{nexts, prevs, heads} = s  Links{Array.set(U32, nexts, n, encode(m)), prevs, heads}def set_prev(s: Links, n: U32, m: Maybe<&2, U32>) -> Links:  Links{nexts, prevs, heads} = s  Links{nexts, Array.set(U32, prevs, n, encode(m)), heads}def set_head(s: Links, r: U32, m: Maybe<&2, U32>) -> Links:  Links{nexts, prevs, heads} = s  Links{nexts, prevs, Array.set(U32, heads, r, encode(m))}def set_head_nonempty(s: Links, r: U32, n: U32) -> Links:  set_head(s, r, Some{n})# Detach member n of root r in O(1).def remove(s: Links, +r: U32, +n: U32) -> Links:  IL.remove(~Links, ~U32, ~U32, ~next, ~prev, ~set_next, ~set_prev, ~set_head, s, r, n)# Link detached entity n at the front of root r in O(1).def prepend(s: Links, +r: U32, +n: U32) -> Links:  IL.prepend_as(~Links, ~U32, ~U32, ~U32, ~get_head, ~set_next, ~set_prev, ~set_head_nonempty, s, r, r, n)