src/containers/bitset.bend checks

raw source on the hub · import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/bitset.bend as Bitset

3 imports

import Base
import ../math/pow2.bend as P2
import ./types/bitset.bend as E

Types

type Wd source · line 52 · raw

Data

W
```
@value:U32 -> Wd
```

type Bitset source · line 55 · raw

Type

BS

@len:Nat -> @depth:Nat -> @words:Array<Wd> -> Bitset

type WordOp source · line 65 · raw

Data

KOr
```
WordOp
```
KAnd
```
WordOp
```
KDiff
```
WordOp
```
KXor
```
WordOp
```

Definitions

def wval source · line 58 · raw

@x:Wd -> U32

def low source · line 71 · raw

@w:U32 -> Bool

def word_get source · line 74 · raw

@w:U32 -> @k:Nat -> Bool

def word_put source · line 77 · raw

@v:Bool -> @w:U32 -> @k:Nat -> U32

def word_op source · line 84 · raw

@k:WordOp -> @a:U32 -> @b:U32 -> U32

def bit_value source · line 95 · raw

@b:Bool -> Nat

def word_count source · line 103 · raw

@m:Nat -> @+w:U32 -> Nat

Number of set bits among the low m bits of w.

def member_pick source · line 110 · raw

@b:Bool -> @+off:Nat -> @rest:List<&2, Nat> -> List<&2, Nat>

def word_members source · line 118 · raw

@m:Nat -> @+w:U32 -> @+off:Nat -> @rest:List<&2, Nat> -> List<&2, Nat>

Indices (from off) of set bits among the low m bits of w, then rest.

def wordix source · line 131 · raw

@i:Nat -> Nat

The word index of bit i and the bit position inside that word. Base's Nat.div / Nat.mod are structural definitions the proofs can peel 32 steps at a time (proofs/bitset/index.bend) and the native backend evaluates in constant time.

def bitix source · line 134 · raw

@i:Nat -> Nat

def pow2 source · line 138 · raw

@d:Nat -> Nat

2^d.

def max_depth source · line 149 · raw

Nat

2^31 words = 2^36 bits: the capacity of the packed representation (the constant is never materialised as a value; depth_for simply stops at this depth). Every word index is then a representable U32 and Base's index masking over the word array is the identity.

def depth_go source · line 156 · raw

@fuel:Nat -> @+n:Nat -> @d:Nat -> @+cap:Nat -> @done:Bool -> Nat

The smallest depth whose 2^depth words hold n bits, capped at max_depth. fuel bounds the search structurally, cap is 2^d and done is the exit test n <= 32 * cap, so a depth that comes out of the loop below the cap always satisfies it (proofs/bitset/depth.bend).

def depth_for source · line 165 · raw

@+n:Nat -> Nat

def read_fin source · line 170 · raw

@p:Pair(Array<Wd>, Wd) -> Pair(Array<Wd>, U32)

def read source · line 175 · raw

@a:Array<Wd> -> @+d:Nat -> @+q:Nat -> Pair(Array<Wd>, U32)

Word q of the array (q < 2^depth).

def write source · line 179 · raw

@a:Array<Wd> -> @+d:Nat -> @+q:Nat -> @+v:U32 -> Array<Wd>

Replace word q.

def new_at source · line 185 · raw

@+n:Nat -> @+d:Nat -> Bitset

All-zero bitset of logical size n (see the capacity note).

def new source · line 188 · raw

@+n:Nat -> Bitset

def length source · line 191 · raw

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

def get_read source · line 198 · raw

@p:Pair(Array<Wd>, U32) -> @+n:Nat -> @+d:Nat -> @+b:Nat -> Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Bool>)

def get_if source · line 202 · raw

@ok:Bool -> @+n:Nat -> @+d:Nat -> @a:Array<Wd> -> @+i:Nat -> Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Bool>)

def get source · line 209 · raw

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

def assign_read source · line 216 · raw

@p:Pair(Array<Wd>, U32) -> @+n:Nat -> @+d:Nat -> @+q:Nat -> @+b:Nat -> @+v:Bool -> Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>)

def assign_if source · line 220 · raw

@ok:Bool -> @+n:Nat -> @+d:Nat -> @a:Array<Wd> -> @+i:Nat -> @+v:Bool -> Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>)

def assign source · line 227 · raw

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

def set source · line 233 · raw

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

Set bit i to 1.

def clear source · line 237 · raw

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

Set bit i to 0.

def bv8 source · line 244 · raw

@+w:U32 -> Nat

Sum of the populations of words q, q+1, ... (m of them). Eight bits per iteration: word_count_t unrolled (the same shifts and adds).

def word_count_8 source · line 247 · raw

@k:Nat -> @+w:U32 -> @+acc:Nat -> Nat

def count_word source · line 255 · raw

@+w:U32 -> @+acc:Nat -> @zero:Bool -> Nat

A zero word contributes nothing and is skipped.

def count_add source · line 262 · raw

@p:Pair(Array<Wd>, U32) -> @+acc:Nat -> Pair(Array<Wd>, Nat)

def count_go source · line 266 · raw

@m:Nat -> @p:Pair(Array<Wd>, Nat) -> @+d:Nat -> @+q:Nat -> Pair(Array<Wd>, Nat)

def count_fin source · line 274 · raw

@p:Pair(Array<Wd>, Nat) -> @+n:Nat -> @+d:Nat -> Pair(Bitset, Nat)

def count source · line 278 · raw

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

def word_desc source · line 289 · raw

@m:Nat -> @+w:U32 -> @+off:Nat -> @acc:List<&2, Nat> -> List<&2, Nat>

Indices of set bits, ascending. Walks the words from the last to the first so the list is built in ascending order without an append. The members of one word, by two TAIL loops: the set offsets are pushed in DESCENDING order onto a scratch list (low bit first), which is then reversed onto rest -- the same list word_members builds, without its non-tail recursion.

def members_word source · line 297 · raw

@+w:U32 -> @+off:Nat -> @rest:List<&2, Nat> -> @zero:Bool -> List<&2, Nat>

A zero word has no members and is skipped.

def members_cons source · line 304 · raw

@p:Pair(Array<Wd>, U32) -> @+off:Nat -> @rest:List<&2, Nat> -> Pair(Array<Wd>, List<&2, Nat>)

def members_go source · line 308 · raw

@m:Nat -> @p:Pair(Array<Wd>, List<&2, Nat>) -> @+d:Nat -> Pair(Array<Wd>, List<&2, Nat>)

def members_fin source · line 316 · raw

@p:Pair(Array<Wd>, List<&2, Nat>) -> @+n:Nat -> @+d:Nat -> Pair(Bitset, List<&2, Nat>)

def to_list source · line 320 · raw

@s:Bitset -> Pair(Bitset, List<&2, Nat>)

def zip_write source · line 327 · raw

@pa:Pair(Array<Wd>, U32) -> @pb:Pair(Array<Wd>, U32) -> @+k:WordOp -> @+d:Nat -> @+q:Nat -> Pair(Array<Wd>, Array<Wd>)

def zip_step source · line 332 · raw

@p:Pair(Array<Wd>, Array<Wd>) -> @+k:WordOp -> @+d:Nat -> @+q:Nat -> Pair(Array<Wd>, Array<Wd>)

def zip_go source · line 336 · raw

@m:Nat -> @p:Pair(Array<Wd>, Array<Wd>) -> @+k:WordOp -> @+d:Nat -> @+q:Nat -> Pair(Array<Wd>, Array<Wd>)

def burn_list source · line 344 · raw

@xs:List<&1, Wd> -> Unit

Discard a linear array (dispose below is the public form).

def burn source · line 353 · raw

@a:Array<Wd> -> Unit

Releasing the word array is dropping it: Base.Array is linear, so the runtime frees the block when the last reference is erased.

def dispose source · line 358 · raw

@s:Bitset -> Unit

Release a bitset. Base.Array is linear, so a caller that stops using a bitset has to say so; every operation above gives the bitset back instead.

def clone_fin source · line 364 · raw

@p:Pair(Array<Wd>, Array<Wd>) -> @+n:Nat -> @+d:Nat -> Pair(Bitset, Bitset)

Two independent bitsets with the same contents (the linear form of sharing).

def clone source · line 368 · raw

@s:Bitset -> Pair(Bitset, Bitset)

def dispose2_go source · line 374 · raw

@u:Unit -> @v:Unit -> Unit

Release two bitsets.

def dispose2 source · line 379 · raw

@s:Bitset -> @t:Bitset -> Unit

def zip_fin source · line 382 · raw

@p:Pair(Array<Wd>, Array<Wd>) -> @+n:Nat -> @+d:Nat -> @+m:Nat -> @+e:Nat -> Pair(Bitset, Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>))

def combine_if source · line 386 · raw

@ok:Bool -> @+k:WordOp -> @+n:Nat -> @+d:Nat -> @a:Array<Wd> -> @+m:Nat -> @+e:Nat -> @b:Array<Wd> -> Pair(Bitset, Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>))

def combine_b source · line 393 · raw

@+k:WordOp -> @+n:Nat -> @+d:Nat -> @a:Array<Wd> -> @t:Bitset -> Pair(Bitset, Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>))

def combine source · line 400 · raw

@+k:WordOp -> @s:Bitset -> @t:Bitset -> Pair(Bitset, Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>))

The operands are given back unchanged apart from the result written into the left one: a linear API has to return what it borrowed.

def union source · line 405 · raw

@s:Bitset -> @t:Bitset -> Pair(Bitset, Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>))

def intersection source · line 408 · raw

@s:Bitset -> @t:Bitset -> Pair(Bitset, Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>))

def difference source · line 411 · raw

@s:Bitset -> @t:Bitset -> Pair(Bitset, Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>))

def xor source · line 414 · raw

@s:Bitset -> @t:Bitset -> Pair(Bitset, Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>))

def fill_drop source · line 419 · raw

@s:Bitset -> @x:Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit> -> Bitset

def fill_set source · line 426 · raw

@p:Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>) -> Bitset

def fill_pick source · line 430 · raw

@b:Bool -> @s:Bitset -> @+i:Nat -> Bitset

def fill source · line 437 · raw

@bs:List<&2, Bool> -> @+i:Nat -> @s:Bitset -> Bitset

def bool_count source · line 444 · raw

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

def from_bools source · line 452 · raw

@+bs:List<&2, Bool> -> Bitset

Bitset whose logical bits are exactly bs (bit 0 first).

def drop_right_go source · line 462 · raw

@s:Bitset -> @u:Unit -> @x:Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit> -> Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>)

def drop_right source · line 467 · raw

@p:Pair(Bitset, Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>)) -> Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>)

def comb_go source · line 471 · raw

@ok:Bool -> @+k:WordOp -> @+n:Nat -> @+d:Nat -> @a:Array<Wd> -> @+ys:List<&2, Bool> -> Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>)

def comb_bits source · line 478 · raw

@+k:WordOp -> @s:Bitset -> @+ys:List<&2, Bool> -> Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>)

def obs_unit source · line 485 · raw

@r:Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>) -> Pair(Bitset, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs)

def obs_pair_done source · line 489 · raw

@s:Bitset -> @u:Unit -> @x:Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit> -> Pair(Bitset, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs)

def obs_pair source · line 496 · raw

@r:Pair(Bitset, Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Unit>)) -> Pair(Bitset, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs)

The trace runner owns the operand it built from the operation, so it releases it once the combination has been applied.

def obs_bit source · line 500 · raw

@r:Pair(Bitset, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Error, Bool>) -> Pair(Bitset, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs)

def obs_nat source · line 504 · raw

@r:Pair(Bitset, Nat) -> Pair(Bitset, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs)

def obs_list source · line 508 · raw

@r:Pair(Bitset, List<&2, Nat>) -> Pair(Bitset, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs)

def step source · line 512 · raw

@s:Bitset -> @op:0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Op -> Pair(Bitset, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs)

def record source · line 536 · raw

@acc:List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs> -> @r:Pair(Bitset, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs) -> Pair(Bitset, List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs>)

def step_acc source · line 540 · raw

@op:0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Op -> @st:Pair(Bitset, List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs>) -> Pair(Bitset, List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs>)

def run_acc source · line 544 · raw

@ops:List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Op> -> @st:Pair(Bitset, List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs>) -> Pair(Bitset, List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs>)

def finish source · line 551 · raw

@st:Pair(Bitset, List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs>) -> Pair(Bitset, List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs>)

def run source · line 555 · raw

@ops:List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Op> -> @s:Bitset -> Pair(Bitset, List<&2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/types/bitset.Obs>)