nbuckets lens for hash_map

hash_map_lens.lean

import data.hash_map
universes u v w

def lens (α β : Type u) :=
∀ (f : Type u → Type w) [functor f], (β → f β) → (α → f α)

def lens.compose {α β δ : Type u} (l₂ : lens α β) (l₁ : lens β δ): lens α δ :=
λ f h, @l₂ f h ∘ @l₁ f h

instance : applicative id :=
{pure := λ _ a, a,
 seq  := λ _ _ f a, f a}

def lens.modify {α β : Type u} (l : lens α β) (a : α) (b : β → β) : α :=
l id b a

def lens.set {α β : Type u} (l : lens α β) (a : α) (b : β) : α :=
l^.modify a (λ _, b)

def fconst (α : Type v) (β : Type u) : Type v :=
α

instance (α : Type v) : functor (fconst α) :=
{map := λ (β δ : Type u) f a, a}

def lens.get {α β : Type u} (l : lens α β) (a : α) : β :=
l (fconst _) (λ b, b) a

def pi₁ {α β : Type u} : lens (α × β) α :=
λ f h g ⟨a, b⟩, @fmap f h _ _ (λ x, (x, b)) (g a)

def pi₂ {α β : Type u} : lens (α × β) β :=
λ f h g ⟨a, b⟩, @fmap f h _ _ (λ x, (a, x)) (g b)

#eval lens.get pi₁ (10, 20)
#eval lens.get pi₂ (10, 20)
#eval lens.set pi₂ (10, 20) 100
#eval lens.set (pi₁^.compose pi₁) ((10, 20), 30) 1
#eval lens.set (pi₁^.compose pi₂) ((10, 20), 30) 1
#eval lens.set pi₂ (((10, 20), 30) : (nat × nat) × nat) 1
#eval lens.get (pi₁^.compose pi₂) ((10, 20), 30)
#eval lens.modify (pi₁^.compose pi₂) ((10, 20), 30) (+1)

namespace hash_map

def resize_buckets {α β} [decidable_eq α] (h : hash_map α β) (nbuckets : ℕ) (nz_buckets : nbuckets > 0) : hash_map α β :=
if h^.nbuckets = nbuckets then h else
⟨h^.hash_fn, h^.size, nbuckets, nz_buckets,
fold_buckets h^.buckets (mk_array nbuckets []) $
  λ r a b, reinsert_aux h^.hash_fn nz_buckets r a b⟩

def nbuckets_lens {α : Type} {β} [decidable_eq α] : lens (hash_map α β) {n : ℕ // n > 0} :=
λ f inst g h, @fmap f inst _ _ (λ new_buckets : {n : ℕ // n > 0}, resize_buckets h new_buckets^.val new_buckets^.property) (g ⟨h^.nbuckets, h^.nz_buckets⟩)

end hash_map

more_polymorphic_lenses.lean

import data.hash_map
universes u v w

def lens (α : Type u) (β : Type v) :=
∀ (f : Type (max u v) → Type w) [functor f], (β → f (ulift.{u} β)) → (α → f (ulift α))

def lens.compose {α β δ : Type u} (l₂ : lens α β) (l₁ : lens β δ): lens α δ :=
λ f h, @l₂ f h ∘ @l₁ f h

instance : applicative id :=
{pure := λ _ a, a,
 seq  := λ _ _ f a, f a}

def lens.modify {α β : Type u} (l : lens α β) (a : α) (b : β → β) : α :=
(l id (ulift.up ∘ b) a)^.down

def lens.set {α β : Type u} (l : lens α β) (a : α) (b : β) : α :=
l^.modify a (λ _, b)

def fconst (α : Type v) (β : Type u) : Type v :=
α

instance (α : Type v) : functor (fconst α) :=
{map := λ (β δ : Type u) f a, a}

def lens.get {α β : Type u} (l : lens α β) (a : α) : β :=
l (fconst _) (λ b, b) a

def pi₁ {α β : Type u} : lens (α × β) α :=
λ f h g ⟨a, b⟩,  @fmap f h _ _ (λ x : ulift α, ulift.up.{u} (ulift.down.{u} x, b)) (g a)

def pi₂ {α β : Type u} : lens (α × β) β :=
λ f h g ⟨a, b⟩, @fmap f h _ _ (λ x : ulift β, ulift.up.{u} (a, ulift.down.{u} x)) (g b)

#eval lens.get pi₁ (10, 20)
#eval lens.get pi₂ (10, 20)
#eval lens.set pi₂ (10, 20) 100
#eval lens.set (pi₁^.compose pi₁) ((10, 20), 30) 1
#eval lens.set (pi₁^.compose pi₂) ((10, 20), 30) 1
#eval lens.set pi₂ (((10, 20), 30) : (nat × nat) × nat) 1
#eval lens.get (pi₁^.compose pi₂) ((10, 20), 30)
#eval lens.modify (pi₁^.compose pi₂) ((10, 20), 30) (+1)

namespace hash_map

def resize_buckets {α β} [decidable_eq α] (h : hash_map α β) (nbuckets : ℕ) (nz_buckets : nbuckets > 0) : hash_map α β :=
if h^.nbuckets = nbuckets then h else
⟨h^.hash_fn, h^.size, nbuckets, nz_buckets,
fold_buckets h^.buckets (mk_array nbuckets []) $
  λ r a b, reinsert_aux h^.hash_fn nz_buckets r a b⟩

def nbuckets_lens {α : Type} {β} [decidable_eq α] : lens (hash_map α β) {n : ℕ // n > 0} :=
λ f inst g h, @fmap f inst _ _ (λ new_buckets : ulift {n : ℕ // n > 0}, ulift.up $ resize_buckets h new_buckets^.down^.val new_buckets^.down^.property) (g ⟨h^.nbuckets, h^.nz_buckets⟩)

end hash_map