structure Data.Key (α : Type) : Type

A typed key for vault access. A Key α can only store/retrieve values of type α. Keys are created via Key.new and are globally unique.

$$\text{Key}(\alpha) \cong \mathbb{N}$$

• id : Nat

@[implicit_reducible]

instance Data.instBEqKey {α✝ : Type} [BEq α✝] : BEq (Key α✝)

Equations

• Data.instBEqKey = { beq := Data.instBEqKey.beq }

def Data.instBEqKey.beq {α✝ : Type} [BEq α✝] : Key α✝ → Key α✝ → Bool

Equations

• Data.instBEqKey.beq { id := a } { id := b } = (a == b)
• Data.instBEqKey.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.instHashableKey {α✝ : Type} [Hashable α✝] : Hashable (Key α✝)

Equations

• Data.instHashableKey = { hash := Data.instHashableKey.hash }

def Data.instHashableKey.hash {α✝ : Type} [Hashable α✝] : Key α✝ → UInt64

Equations

• Data.instHashableKey.hash { id := a } = mixHash 0 (hash a)

structure Data.Vault : Type

A type-safe heterogeneous map. Values of different types can coexist, each accessible only through its corresponding typed Key.

$$\text{Vault} = \text{HashMap}(\mathbb{N}, \text{Any})$$

• store : Std.HashMap Nat Data.Any

def Data.Key.new {α : Type} : IO (Key α)

Allocate a fresh typed key. Each call returns a distinct key. $$\text{new} : \text{IO}(\text{Key}\ \alpha)$$

Equations

• Data.Key.new = do let u ← Data.newUnique pure { id := u.id }

@[inline]

def Data.Vault.empty : Vault

The empty vault. $$\text{empty} : \text{Vault},\quad |\text{empty}| = 0$$

Equations

• Data.Vault.empty = { store := ∅ }

@[implicit_reducible]

instance Data.Vault.instInhabited : Inhabited Vault

Equations

• Data.Vault.instInhabited = { default := Data.Vault.empty }

@[inline]

def Data.Vault.size (v : Vault) : Nat

Number of entries in the vault. $$\text{size}(v)$$

Equations

• v.size = (Data.Vault.store✝ v).size

@[implemented_by _private.Hale.Vault.Data.Vault.0.Data.Vault.insertImpl]

opaque Data.Vault.insert {α : Type} (key : Key α) (val : α) (v : Vault) : Vault

Insert a value into the vault under the given key. If the key already has a value, it is replaced. $$\text{insert}(k, x, v) = v[k \mapsto x]$$

@[implemented_by _private.Hale.Vault.Data.Vault.0.Data.Vault.lookupImpl]

opaque Data.Vault.lookup {α : Type} (key : Key α) (v : Vault) : Option α

Look up the value associated with a key. Returns none if the key is not present. $$\text{lookup}(k, v) = v[k]$$

@[inline]

def Data.Vault.delete {α : Type} (key : Key α) (v : Vault) : Vault

Delete a key and its associated value from the vault. $$\text{delete}(k, v) = v \setminus \{k\}$$

Equations

• Data.Vault.delete key v = { store := (Data.Vault.store✝ v).erase (Data.Key.id✝ key) }

@[inline]

def Data.Vault.adjust {α : Type} (f : α → α) (key : Key α) (v : Vault) : Vault

Adjust the value at a key, if present. $$\text{adjust}(f, k, v) = \begin{cases} v[k \mapsto f(v[k])] & k \in v \\ v & k \notin v \end{cases}$$

Equations

• Data.Vault.adjust f key v = match Data.Vault.lookup key v with | some val => Data.Vault.insert key (f val) v | none => v

def Data.Vault.union (v1 v2 : Vault) : Vault

Union of two vaults. Right-biased: values from v2 take precedence. $$\text{union}(v_1, v_2) = v_2 \cup v_1$$

Equations

• One or more equations did not get rendered due to their size.