src/containers/intrusive_links.bend checks
raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/containers/intrusive_links.bend as Intrusive_links
2 imports
import Base import ./intrusive_doubly_linked_list.bend as IL
Types
type Links source · line 10 · raw
Type
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.
Links@nexts:Array<U32> -> @prevs:Array<U32> -> @heads:Array<U32> -> Links
Definitions
def new source · line 13 · raw
@+node_depth:Nat -> @+root_depth:Nat -> Links
def decode_pick source · line 16 · raw
@+x:U32 -> @zero:Bool -> Maybe<&2, U32>
def decode source · line 23 · raw
@+x:U32 -> Maybe<&2, U32>
def encode source · line 26 · raw
@m:Maybe<&2, U32> -> U32
def next_got source · line 33 · raw
@prevs:Array<U32> -> @heads:Array<U32> -> @r:Pair(Array<U32>, U32) -> Pair(Links, Maybe<&2, U32>)
def prev_got source · line 37 · raw
@nexts:Array<U32> -> @heads:Array<U32> -> @r:Pair(Array<U32>, U32) -> Pair(Links, Maybe<&2, U32>)
def head_got source · line 41 · raw
@nexts:Array<U32> -> @prevs:Array<U32> -> @r:Pair(Array<U32>, U32) -> Pair(Links, Maybe<&2, U32>)
def next source · line 45 · raw
@s:Links -> @n:U32 -> Pair(Links, Maybe<&2, U32>)
def prev source · line 49 · raw
@s:Links -> @n:U32 -> Pair(Links, Maybe<&2, U32>)
def get_head source · line 53 · raw
@s:Links -> @r:U32 -> Pair(Links, Maybe<&2, U32>)
def set_next source · line 57 · raw
@s:Links -> @n:U32 -> @m:Maybe<&2, U32> -> Links
def set_prev source · line 61 · raw
@s:Links -> @n:U32 -> @m:Maybe<&2, U32> -> Links
def set_head source · line 65 · raw
@s:Links -> @r:U32 -> @m:Maybe<&2, U32> -> Links
def set_head_nonempty source · line 69 · raw
@s:Links -> @r:U32 -> @n:U32 -> Links
def remove source · line 73 · raw
@s:Links -> @+r:U32 -> @+n:U32 -> Links
Detach member n of root r in O(1).
def prepend source · line 77 · raw
@s:Links -> @+r:U32 -> @+n:U32 -> Links
Link detached entity n at the front of root r in O(1).