spec/containers/hash_table.bend checks

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

3 imports

import Base
import ../lib/common.bend as SC
import ../../src/containers/hash_table.bend as H

Types

type Entry source · line 9 · raw

@-V:Data -> Data

E

@-V:Data -> @key:String -> @val:V -> Entry<V>

Definitions

def chr_eq source · line 12 · raw

@a:Char -> @b:Char -> Bool

def str_eq source · line 17 · raw

@a:String -> @b:String -> Bool

def mem source · line 74 · raw

@+k:String -> @ks:List<&2, String> -> Bool

def nodup source · line 81 · raw

@ks:List<&2, String> -> Bool

def Equivalent_Keys.key_refl source · line 148 · raw

@+a:String -> Type

Equivalent_Keys

def Equivalent_Keys.key_sym source · line 152 · raw

@+a:String -> @+b:String -> Type

Equivalent_Keys

def Equivalent_Keys.key_trans source · line 156 · raw

@+a:String -> @+b:String -> @+c:String -> @+hab:{str_eq(a, b) == True{} : Bool} -> @+hbc:{str_eq(b, c) == True{} : Bool} -> Type

Equivalent_Keys

def Equivalent_Keys.key_same source · line 160 · raw

@+a:String -> @+b:String -> @+h:{str_eq(a, b) == True{} : Bool} -> Type

Equivalent_Keys

Templates

template lookup source · line 28 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @+k:String -> Maybe<&2, V>

template is_some source · line 35 · raw

@-V:Data -> @m:Maybe<&2, V> -> Bool

template has source · line 42 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @+k:String -> Bool

template set source · line 46 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @+k:String -> @+x:V -> List<&2, Entry<V>>

Replace the entry of k in place, or add it at the end.

template remove source · line 53 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @+k:String -> List<&2, Entry<V>>

template keys source · line 60 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> List<&2, String>

template size source · line 67 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> Nat

template get_m source · line 88 · raw

@-V:Data -> @dflt:V -> @m:Maybe<&2, V> -> V

template get source · line 96 · raw

@-V:Data -> @dflt:V -> @m:List<&2, Entry<V>> -> @+key:String -> V

the value of key, or dflt

template KeysPost source · line 136 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> Type

---- keys ---- The key sequence (SPARK's Keys): no key twice, as long as the map, and holding exactly the keys the model has.

template SetPost source · line 140 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @m2:List<&2, Entry<V>> -> @key:String -> @x:V -> Type

---- set (SPARK's Include: insert, or replace the value) ----

template DelPost source · line 144 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @m2:List<&2, Entry<V>> -> @key:String -> Type

---- pop and del (SPARK's Delete/Exclude) ----

template Equivalent_Keys.key_respect source · line 164 · raw

@-A:Data -> @-f:(@_:String -> A) -> @+a:String -> @+b:String -> @+h:{str_eq(a, b) == True{} : Bool} -> Type

Equivalent_Keys

template Include.set_post source · line 168 · raw

@-V:Data -> @-m:List<&2, Entry<V>> -> @-m2:List<&2, Entry<V>> -> @-key:String -> @-x:V -> @-hp:Pair(@+q:String -> {lookup(V, m2, q) == lookup(V, set(V, m, key, x), q) : Maybe<&2, V>}, {size(V, m2) == size(V, set(V, m, key, x)) : Nat}) -> @+hnd:{nodup(keys(V, m2)) == True{} : Bool} -> @hk:(@+hq0:{has(V, m, key) == True{} : Bool} -> {keys(V, m2) == keys(V, m) : List<&2, String>}) -> Type

Include (729)

template Element.element_value source · line 176 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @+key:String -> @+x:V -> @+hl:{lookup(V, m, key) == Some{x} : Maybe<&2, V>} -> @r:V -> Type

Element (SPARKlib formal-hashed-maps.ads): Element (Container, Key) = Get (Model, Key)

template Element.element_default source · line 181 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @+key:String -> @+dflt:V -> @+hl:{lookup(V, m, key) == None{} : Maybe<&2, V>} -> @r:V -> Type

Element without the key: get returns the caller's default (the Pre of Element is Contains; here the absent case is defined, not excluded)

template Contains.contains_value source · line 185 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @+key:String -> @r:Bool -> Type

Contains: Contains (Container, Key) = Has_Key (Model, Key)

template Length.length_value source · line 189 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @+n:Nat -> Type

Length: Length (Container) = M.Length (Model)

template Length.length_frame source · line 193 · raw

@-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.HashMap<&2, V> -> Type

Length is a query: the map is returned unchanged

template Empty_Map.new_model source · line 197 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> Type

Empty_Map: Is_Empty (Model), Length = 0, no key present

template Empty_Map.new_length source · line 200 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> Type

template Empty_Map.new_absent source · line 203 · raw

@-V:Data -> @m:List<&2, Entry<V>> -> @+key:String -> Type