spec/containers/bitlist.bend checks

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

5 imports

import Base
import ../lib/common.bend as C
import ./bitset.bend as BS
import ../../src/containers/types/bitlist.bend as E
import ../lib/sequence.bend as V

Types

type Model source · line 26 · raw

Data

M

@limit:Maybe<&2, Nat> -> @cexp:Nat -> @bits:List<&2, Bool> -> Model

Definitions

def new source · line 29 · raw

Model

def with_limit source · line 32 · raw

@+n:Nat -> Model

def below source · line 36 · raw

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

One more bit fits under the limit and in the storage.

def room source · line 43 · raw

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

def count source · line 47 · raw

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

Number of True bits (the popcount of the bitset specification).

def bit source · line 50 · raw

@x:Maybe<&2, Bool> -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>

def last_bit source · line 57 · raw

@x:Maybe<&2, Bool> -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Error, Bool>

def assign_at source · line 65 · raw

@x:Maybe<&2, Bool> -> @+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @i:Nat -> @v:Bool -> Pair(Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)

Assign bit i; out of range leaves the list unchanged and fails.

def push_if source · line 72 · raw

@ok:Bool -> @+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @v:Bool -> Pair(Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)

def pop source · line 79 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @xs:List<&2, Bool> -> Pair(Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)

def step_parts source · line 86 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> Pair(Model, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs)

def step source · line 108 · raw

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

Every operation: the next model and the observation.

def cons_obs source · line 112 · raw

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

def run source · line 116 · raw

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

def push_all source · line 124 · raw

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

from_bools: the bits pushed one by one onto the unbounded list.

def from_bools source · line 131 · raw

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

def bits source · line 154 · raw

@m:Model -> List<&2, Bool>

def Replace_Element.get_assign_same source · line 160 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Replace_Element (384)

def Replace_Element.get_assign_other source · line 164 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+j:Nat -> @+v:Bool -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> Type

Replace_Element (384)

def Replace_Element.length_assign source · line 168 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Replace_Element (384)

def Append.length_push source · line 172 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Append (706)

def Append.get_push_last source · line 176 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Append (706)

def Delete_Last.pop_push source · line 180 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Delete_Last (866)

def Append.count_push source · line 184 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Append (706)

def nx source · line 222 · raw

@+m:Model -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> Model

def ob source · line 225 · raw

@+m:Model -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Obs

def limit source · line 228 · raw

@m:Model -> Maybe<&2, Nat>

def Length.length_result source · line 234 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> Type

Length (284)

def Length.length_frame source · line 238 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> Type

Length (284)

def Capacity.limit_result source · line 242 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> Type

Capacity (322)

def Capacity.limit_frame source · line 246 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> Type

Capacity (322)

def Implementation.count_result source · line 250 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> Type

implementation

def Iteration.to_list_model source · line 254 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> Type

iteration (Iter_Model, 1193)

def Iteration.to_list_frame source · line 258 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> Type

iteration (Iter_Model, 1193)

def Empty_Vector.new_empty source · line 262 · raw

Type

Empty_Vector (292)

def Empty_Vector.with_limit_empty source · line 266 · raw

@+n:Nat -> Type

Empty_Vector (292)

def To_Vector.from_bools_model source · line 270 · raw

@+bs:List<&2, Bool> -> @+c:Nat -> @+hc:{c == 31n : Nat} -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, bs), Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(c), 32n)) == True{} : Bool} -> Type

To_Vector (308)

def Clear.clear_length source · line 274 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> Type

Clear (341)

def Clear.clear_limit source · line 278 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> Type

Clear (341)

def Element.get_element source · line 282 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, xs, i) == Some{v} : Maybe<&2, Bool>} -> Type

Element (373)

def Element.get_frame source · line 286 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> Type

Element (373)

def Element.get_outside source · line 290 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), i) == True{} : Bool} -> Type

Element (373)

def Replace_Element.assign_length source · line 294 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Replace_Element (384)

def Replace_Element.assign_element source · line 298 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Replace_Element (384)

def Replace_Element.assign_except source · line 302 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Replace_Element (384)

def Replace_Element.assign_outside source · line 306 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+i:Nat -> @+v:Bool -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), i) == True{} : Bool} -> Type

Replace_Element (384)

def Append.push_length source · line 310 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Append (706)

def Append.push_prefix source · line 314 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Append (706)

def Append.push_element source · line 318 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Append (706)

def Append.push_full source · line 322 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+xs:List<&2, Bool> -> @+v:Bool -> @+h:{room(l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == False{} : Bool} -> Type

Append (706)

def Delete_Last.pop_length source · line 326 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+h:Bool -> @+t:List<&2, Bool> -> Type

Delete_Last (866)

def Delete_Last.pop_prefix source · line 330 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+h:Bool -> @+t:List<&2, Bool> -> Type

Delete_Last (866)

def Delete_Last.pop_result source · line 334 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> @+h:Bool -> @+t:List<&2, Bool> -> Type

Delete_Last (866)

def Delete_Last.pop_empty source · line 338 · raw

@+l:Maybe<&2, Nat> -> @+c:Nat -> Type

Delete_Last (866)