src/containers/bitlist.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/src/containers/bitlist.bend as Bitlist

5 imports

import Base
import ./bitset.bend as B
import ./dynamic_array.bend as D
import ./types/dynamic_array.bend as DE
import ./types/bitlist.bend as E

Types

type Bitlist source · line 33 · raw

Type

BL

@limit:Maybe<&2, Nat> -> @len:Nat -> @words:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> Bitlist

Definitions

def new source · line 36 · raw

Bitlist

def with_limit source · line 39 · raw

@+n:Nat -> Bitlist

def below source · line 43 · raw

@lim:Maybe<&2, Nat> -> @+n:Nat -> Bool

Room for one more bit under the limit.

def length source · line 50 · raw

@s:Bitlist -> Pair(Bitlist, Nat)

def limit source · line 54 · raw

@s:Bitlist -> Pair(Bitlist, Maybe<&2, Nat>)

def get_word source · line 60 · raw

@+i:Nat -> @+lim:Maybe<&2, Nat> -> @+n:Nat -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>) -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>)

def get_if source · line 67 · raw

@ok:Bool -> @+lim:Maybe<&2, Nat> -> @+n:Nat -> @w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> @+i:Nat -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>)

def get source · line 74 · raw

@s:Bitlist -> @+i:Nat -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>)

def assign_set source · line 80 · raw

@+lim:Maybe<&2, Nat> -> @+n:Nat -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>) -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

def assign_word source · line 88 · raw

@+i:Nat -> @+v:Bool -> @+lim:Maybe<&2, Nat> -> @+n:Nat -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>) -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

Rewrite bit i of its word (the word read is r); the list gets length n.

def assign_if source · line 95 · raw

@ok:Bool -> @+lim:Maybe<&2, Nat> -> @+n:Nat -> @w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> @+i:Nat -> @+v:Bool -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

def assign source · line 102 · raw

@s:Bitlist -> @+i:Nat -> @+v:Bool -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

def set source · line 106 · raw

@s:Bitlist -> @+i:Nat -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

def unset source · line 109 · raw

@s:Bitlist -> @+i:Nat -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

def push_new source · line 114 · raw

@+lim:Maybe<&2, Nat> -> @+n:Nat -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>) -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

def push_in source · line 122 · raw

@+lim:Maybe<&2, Nat> -> @+n:Nat -> @w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> @+v:Bool -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

Bit n already lies in a stored word, where it is zero (masked tail).

def push_where source · line 129 · raw

@inside:Bool -> @+lim:Maybe<&2, Nat> -> @+n:Nat -> @w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> @+v:Bool -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

def push_room source · line 136 · raw

@+lim:Maybe<&2, Nat> -> @+n:Nat -> @+v:Bool -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat) -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

def push_if source · line 140 · raw

@ok:Bool -> @+lim:Maybe<&2, Nat> -> @+n:Nat -> @w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> @+v:Bool -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

def push source · line 147 · raw

@s:Bitlist -> @+v:Bool -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>)

def pop_set source · line 153 · raw

@+lim:Maybe<&2, Nat> -> @+m:Nat -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>) -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>)

def pop_bit source · line 161 · raw

@+lim:Maybe<&2, Nat> -> @+m:Nat -> @w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> @+x:U32 -> @+b:Bool -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>)

The last bit b of word x: a set bit is cleared so the tail stays zero.

def pop_word source · line 168 · raw

@+lim:Maybe<&2, Nat> -> @+m:Nat -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>) -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>)

def pop_at source · line 175 · raw

@+lim:Maybe<&2, Nat> -> @+n:Nat -> @w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>)

def pop source · line 182 · raw

@s:Bitlist -> Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>)

def clear source · line 188 · raw

@s:Bitlist -> Bitlist

def count_add source · line 194 · raw

@g:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>) -> @+acc:Nat -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat)

def count_go source · line 201 · raw

@k:Nat -> @p:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat) -> @+q:Nat -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat)

def count_fin source · line 209 · raw

@+lim:Maybe<&2, Nat> -> @+n:Nat -> @p:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat) -> Pair(Bitlist, Nat)

def count_len source · line 213 · raw

@+lim:Maybe<&2, Nat> -> @+n:Nat -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat) -> Pair(Bitlist, Nat)

def count source · line 217 · raw

@s:Bitlist -> Pair(Bitlist, Nat)

def word_bits source · line 224 · raw

@m:Nat -> @+x:U32 -> @rest:List<&2, Bool> -> List<&2, Bool>

The low m bits of x, bit 0 first, in front of rest.

def bits_add source · line 233 · raw

@+m:Nat -> @acc:List<&2, Bool> -> @g:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, U32>) -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, List<&2, Bool>)

Word q holds bits 32q .. 32q+31; of the first n bits it contributes min(32, n - 32q) (none once 32q >= n).

def bits_go source · line 241 · raw

@k:Nat -> @st:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, List<&2, Bool>) -> @+n:Nat -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, List<&2, Bool>)

The first n bits, emitted from the last stored word down to word 0.

def to_list_fin source · line 249 · raw

@+lim:Maybe<&2, Nat> -> @+n:Nat -> @p:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, List<&2, Bool>) -> Pair(Bitlist, List<&2, Bool>)

def to_list_len source · line 253 · raw

@+lim:Maybe<&2, Nat> -> @+n:Nat -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Nat) -> Pair(Bitlist, List<&2, Bool>)

def to_list source · line 257 · raw

@s:Bitlist -> Pair(Bitlist, List<&2, Bool>)

def from_push source · line 263 · raw

@p:Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>) -> Bitlist

def from_go source · line 267 · raw

@bs:List<&2, Bool> -> @s:Bitlist -> Bitlist

def from_bools source · line 275 · raw

@bs:List<&2, Bool> -> Bitlist

The bits of bs, in order, in an unbounded bitlist.

def obs_nat source · line 280 · raw

@r:Pair(Bitlist, Nat) -> Pair(Bitlist, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)

def obs_bit source · line 284 · raw

@r:Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>) -> Pair(Bitlist, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)

def obs_unit source · line 288 · raw

@r:Pair(Bitlist, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Unit>) -> Pair(Bitlist, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)

def obs_limit source · line 292 · raw

@r:Pair(Bitlist, Maybe<&2, Nat>) -> Pair(Bitlist, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)

def obs_bits source · line 296 · raw

@r:Pair(Bitlist, List<&2, Bool>) -> Pair(Bitlist, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)

def step source · line 300 · raw

@s:Bitlist -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> Pair(Bitlist, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)

def record source · line 321 · raw

@acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs> -> @r:Pair(Bitlist, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs) -> Pair(Bitlist, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs>)

def run_acc source · line 325 · raw

@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @st:Pair(Bitlist, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs>) -> Pair(Bitlist, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs>)

def finish source · line 333 · raw

@st:Pair(Bitlist, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs>) -> Pair(Bitlist, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs>)

def run source · line 337 · raw

@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> @s:Bitlist -> Pair(Bitlist, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs>)