src/containers/internal/dlist_storage.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/src/containers/internal/dlist_storage.bend as Dlist_storage
2 imports
import Base import ../types/internal_dlist.bend as E
Types
type DList source · line 36 · raw
@-T:Data -> Type
DL@-T:Data -> @tag:U32 -> @fresh:U32 -> @free:U32 -> @count:Nat -> @head:U32 -> @tail:U32 -> @depth:Nat -> @cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> DList<T>
type Cur source · line 320 · raw
@-T:Data -> Type
One loop, no mutual recursion: the state carries the next id to read.
C@-T:Data -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @acc:List<&2, T> -> @at:U32 -> Cur<T>
Definitions
def nil source · line 39 · raw
U32
def link source · line 43 · raw
@+i:U32 -> U32
The link to an element, and the element a (non-nil) link points to.
def slot source · line 46 · raw
@+l:U32 -> U32
def new_links source · line 52 · raw
@+depth:Nat -> Array<U32>
def pick_link source · line 59 · raw
@none:Bool -> @+l:U32 -> Maybe<&2, U32>
A link as the Maybe the public API reports.
def link_of source · line 69 · raw
@+l:U32 -> Maybe<&2, U32>
Point the link stored at element a (if a is a link, not nil) at q.
def set_next_go source · line 72 · raw
@nexts:Array<U32> -> @+a:U32 -> @+q:U32 -> @none:Bool -> Array<U32>
def set_next source · line 81 · raw
@nexts:Array<U32> -> @+a:U32 -> @+q:U32 -> Array<U32>
def grown_links source · line 87 · raw
@+depth:Nat -> @a:Array<U32> -> Array<U32>
def pick_end source · line 91 · raw
@none:Bool -> @+n:U32 -> @+e:U32 -> U32
The end pointer after linking n next to a (nil: n becomes that end).
def link_at source · line 139 · raw
@links:Array<U32> -> @+i:U32 -> Pair(Array<U32>, U32)
The neighbour link on one side of a live element.
def handle_go source · line 264 · raw
@+tag:U32 -> @+l:U32 -> @none:Bool -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>
def handle source · line 271 · raw
@+tag:U32 -> @+l:U32 -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>
Templates
template new_vals source · line 49 · raw
@-T:Data -> @+depth:Nat -> Array<Maybe<&2, T>>
template new source · line 55 · raw
@-T:Data -> @tag:U32 -> DList<T>
template grown_vals source · line 84 · raw
@-T:Data -> @+depth:Nat -> @a:Array<Maybe<&2, T>> -> Array<Maybe<&2, T>>
template link_in source · line 99 · raw
@-T:Data -> @+tag:U32 -> @+n:U32 -> @+nfresh:U32 -> @+nfree:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+a:U32 -> @+b:U32 -> @x:T -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)
Store x at slot n between the links a and b (either may be nil) and relink them.
template insert_room source · line 105 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+a:U32 -> @+b:U32 -> @x:T -> @room:Bool -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)
template insert_between source · line 112 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+a:U32 -> @+b:U32 -> @x:T -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)
template length source · line 115 · raw
@-T:Data -> @s:DList<T> -> Pair(DList<T>, Nat)
template push_front source · line 119 · raw
@-T:Data -> @s:DList<T> -> @x:T -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)
template push_back source · line 123 · raw
@-T:Data -> @s:DList<T> -> @x:T -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)
template done_handle source · line 127 · raw
@-T:Data -> @r:Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template fail_same source · line 135 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error)
template ins_side source · line 142 · raw
@-T:Data -> @after:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @+p:U32 -> @+n:U32 -> @x:T -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template ins_live2 source · line 149 · raw
@-T:Data -> @after:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @+i:U32 -> @x:T -> @pr:Pair(Array<U32>, U32) -> @nx:Pair(Array<U32>, U32) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template ins_found source · line 154 · raw
@-T:Data -> @after:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @x:T -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template insert_checked source · line 162 · raw
@-T:Data -> @after:Bool -> @ok:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @x:T -> @same:Bool -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template insert_before source · line 171 · raw
@-T:Data -> @s:DList<T> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle -> @x:T -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template insert_after source · line 176 · raw
@-T:Data -> @s:DList<T> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle -> @x:T -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template rm_links source · line 183 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @+v:T -> @pr:Pair(Array<U32>, U32) -> @nx:Pair(Array<U32>, U32) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>)
template rm_found source · line 189 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>)
template remove_checked source · line 197 · raw
@-T:Data -> @ok:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @same:Bool -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>)
template remove source · line 206 · raw
@-T:Data -> @s:DList<T> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>)
template value_of source · line 213 · raw
@-T:Data -> @m:Maybe<&2, T> -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>
template get_fin source · line 220 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @prevs:Array<U32> -> @nexts:Array<U32> -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>)
template get_checked source · line 224 · raw
@-T:Data -> @ok:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @same:Bool -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>)
template get source · line 233 · raw
@-T:Data -> @s:DList<T> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>)
template set_fin source · line 238 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @x:T -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Unit>)
template set_checked source · line 248 · raw
@-T:Data -> @ok:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @+x:T -> @same:Bool -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Unit>)
set swaps the new value in: one indexed access when the element is live; a stale slot is None and is written back as None.
template set source · line 257 · raw
@-T:Data -> @s:DList<T> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle -> @x:T -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Unit>)
template nbr_n source · line 274 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @r:Pair(Array<U32>, U32) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>>)
template nbr_p source · line 278 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @nexts:Array<U32> -> @r:Pair(Array<U32>, U32) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>>)
template nbr_fin source · line 282 · raw
@-T:Data -> @after:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @m:Maybe<&2, T> -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>>)
template nbr_read source · line 291 · raw
@-T:Data -> @after:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>>)
template nbr_checked source · line 295 · raw
@-T:Data -> @after:Bool -> @ok:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @same:Bool -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>>)
template next source · line 304 · raw
@-T:Data -> @s:DList<T> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>>)
template prev source · line 309 · raw
@-T:Data -> @s:DList<T> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>>)
template step_p source · line 323 · raw
@-T:Data -> @vals:Array<Maybe<&2, T>> -> @acc:List<&2, T> -> @r:Pair(Array<U32>, U32) -> Cur<T>
template step_m source · line 327 · raw
@-T:Data -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @acc:List<&2, T> -> @+at:U32 -> @m:Maybe<&2, T> -> Cur<T>
template step_v source · line 334 · raw
@-T:Data -> @prevs:Array<U32> -> @acc:List<&2, T> -> @+at:U32 -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Cur<T>
template step_back source · line 338 · raw
@-T:Data -> @c:Cur<T> -> Cur<T>
template walk source · line 342 · raw
@-T:Data -> @fuel:Nat -> @c:Cur<T> -> Cur<T>
template tl_fin source · line 349 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @nexts:Array<U32> -> @c:Cur<T> -> Pair(DList<T>, List<&2, T>)
template to_list source · line 353 · raw
@-T:Data -> @s:DList<T> -> Pair(DList<T>, List<&2, T>)
template ins_free_pop source · line 379 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+f:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @+a:U32 -> @+b:U32 -> @x:T -> @r:Pair(Array<U32>, U32) -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)
Allocate the top of the free stack: nx is the link it stored, which
becomes the new top. nexts[i] is overwritten by link_in, after the read.
template ins_free_pick source · line 383 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+a:U32 -> @+b:U32 -> @x:T -> @empty:Bool -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)
template insert_between_free source · line 390 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+a:U32 -> @+b:U32 -> @x:T -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)
template push_front_free source · line 393 · raw
@-T:Data -> @s:DList<T> -> @x:T -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)
template push_back_free source · line 397 · raw
@-T:Data -> @s:DList<T> -> @x:T -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle)
template rmf_links source · line 404 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @+i:U32 -> @v:T -> @pr:Pair(Array<U32>, U32) -> @nx:Pair(Array<U32>, U32) -> Pair(DList<T>, Maybe<&2, T>)
Unlink the element at slot i and push i on the free stack. set_next writes
at the NEIGHBOUR slots (both different from i), so the last write, which
stores the old top in nexts[i], cannot be overwritten.
template rmf_found source · line 410 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DList<T>, Maybe<&2, T>)
template pop_end source · line 418 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+l:U32 -> @empty:Bool -> Pair(DList<T>, Maybe<&2, T>)
template pop_front_free source · line 425 · raw
@-T:Data -> @s:DList<T> -> Pair(DList<T>, Maybe<&2, T>)
template pop_back_free source · line 429 · raw
@-T:Data -> @s:DList<T> -> Pair(DList<T>, Maybe<&2, T>)
template peek_fin source · line 433 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @prevs:Array<U32> -> @nexts:Array<U32> -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DList<T>, Maybe<&2, T>)
template peek_end source · line 437 · raw
@-T:Data -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+l:U32 -> @empty:Bool -> Pair(DList<T>, Maybe<&2, T>)
template peek_front source · line 444 · raw
@-T:Data -> @s:DList<T> -> Pair(DList<T>, Maybe<&2, T>)
template peek_back source · line 448 · raw
@-T:Data -> @s:DList<T> -> Pair(DList<T>, Maybe<&2, T>)
template obs_nat source · line 454 · raw
@-T:Data -> @r:Pair(DList<T>, Nat) -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>)
template obs_handle source · line 458 · raw
@-T:Data -> @r:Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle) -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>)
template obs_insert source · line 462 · raw
@-T:Data -> @r:Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>) -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>)
template obs_val source · line 466 · raw
@-T:Data -> @r:Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>) -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>)
template obs_unit source · line 470 · raw
@-T:Data -> @r:Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Unit>) -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>)
template obs_nbr source · line 474 · raw
@-T:Data -> @r:Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>>) -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>)
template obs_list source · line 478 · raw
@-T:Data -> @r:Pair(DList<T>, List<&2, T>) -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>)
template step source · line 482 · raw
@-T:Data -> @s:DList<T> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Op<T> -> Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>)
template record source · line 507 · raw
@-T:Data -> @acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>> -> @r:Pair(DList<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>) -> Pair(DList<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>>)
template step_acc source · line 511 · raw
@-T:Data -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Op<T> -> @st:Pair(DList<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>>) -> Pair(DList<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>>)
template run_acc source · line 515 · raw
@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Op<T>> -> @st:Pair(DList<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>>) -> Pair(DList<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>>)
template finish source · line 522 · raw
@-T:Data -> @st:Pair(DList<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>>) -> Pair(DList<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>>)
template run source · line 526 · raw
@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Op<T>> -> @s:DList<T> -> Pair(DList<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Obs<T>>)
template ins_side_reuse source · line 530 · raw
@-T:Data -> @after:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @+p:U32 -> @+n:U32 -> @x:T -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
Internal insertion variants for a generational public handle owner.
template ins_live2_reuse source · line 537 · raw
@-T:Data -> @after:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @+i:U32 -> @x:T -> @pr:Pair(Array<U32>, U32) -> @nx:Pair(Array<U32>, U32) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template ins_found_reuse source · line 542 · raw
@-T:Data -> @after:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @x:T -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template insert_checked_reuse source · line 550 · raw
@-T:Data -> @after:Bool -> @ok:Bool -> @+tag:U32 -> @+fresh:U32 -> @+free:U32 -> @+count:Nat -> @+head:U32 -> @+tail:U32 -> @+depth:Nat -> @+cap:U32 -> @vals:Array<Maybe<&2, T>> -> @prevs:Array<U32> -> @nexts:Array<U32> -> @+i:U32 -> @x:T -> @same:Bool -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template insert_before_reuse source · line 559 · raw
@-T:Data -> @s:DList<T> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle -> @x:T -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template insert_after_reuse source · line 564 · raw
@-T:Data -> @s:DList<T> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle -> @x:T -> Pair(DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Handle>)
template recycle_slot source · line 572 · raw
@-T:Data -> @s:DList<T> -> @+i:U32 -> DList<T>
Called only after a successful remove, by an owner that invalidated the removed handle's generation. The slot is already absent from the live list.