139 lines
5.2 KiB
Text
139 lines
5.2 KiB
Text
/-
|
||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Author: Leonardo de Moura
|
||
-/
|
||
prelude
|
||
import init.data.array.basic init.data.assoclist
|
||
import init.data.option.basic init.data.hashable
|
||
universes u v w
|
||
|
||
def HashMapBucket (α : Type u) (β : Type v) :=
|
||
{ b : Array (AssocList α β) // b.size > 0 }
|
||
|
||
def HashMapBucket.update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β) (h : i.toNat < data.val.size) : HashMapBucket α β :=
|
||
⟨ data.val.updt i d h,
|
||
transRelRight Greater (Array.szUpdateEq (data.val) ⟨USize.toNat i, h⟩ d) data.property ⟩
|
||
|
||
structure HashMapImp (α : Type u) (β : Type v) :=
|
||
(size : Nat)
|
||
(buckets : HashMapBucket α β)
|
||
|
||
def mkHashMapImp {α : Type u} {β : Type v} (nbuckets := 8) : HashMapImp α β :=
|
||
let n := if nbuckets = 0 then 8 else nbuckets in
|
||
{ size := 0,
|
||
buckets :=
|
||
⟨ mkArray n AssocList.nil,
|
||
have p₁ : (mkArray n (@AssocList.nil α β)).size = n, from szMkArrayEq _ _,
|
||
have p₂ : n = (if nbuckets = 0 then 8 else nbuckets), from rfl,
|
||
have p₃ : (if nbuckets = 0 then 8 else nbuckets) > 0, from
|
||
match nbuckets with
|
||
| 0 := Nat.zeroLtSucc _
|
||
| (Nat.succ x) := Nat.zeroLtSucc _,
|
||
transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ }
|
||
|
||
namespace HashMapImp
|
||
variables {α : Type u} {β : Type v}
|
||
|
||
def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
|
||
⟨u %ₙ n, USize.modnLt _ h⟩
|
||
|
||
def reinsertAux (hashFn : α → USize) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
|
||
let ⟨i, h⟩ := mkIdx data.property (hashFn a) in
|
||
data.update i (AssocList.cons a b (data.val.idx i h)) h
|
||
|
||
def foldBuckets {δ : Type w} (data : HashMapBucket α β) (d : δ) (f : δ → α → β → δ) : δ :=
|
||
data.val.foldl (λ b d, b.foldl f d) d
|
||
|
||
def find [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
|
||
match m with
|
||
| ⟨_, buckets⟩ :=
|
||
let ⟨i, h⟩ := mkIdx buckets.property (hash a) in
|
||
(buckets.val.idx i h).find a
|
||
|
||
def contains [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
|
||
match m with
|
||
| ⟨_, buckets⟩ :=
|
||
let ⟨i, h⟩ := mkIdx buckets.property (hash a) in
|
||
(buckets.val.idx i h).contains a
|
||
|
||
def fold {δ : Type w} (m : HashMapImp α β) (d : δ) (f : δ → α → β → δ) : δ :=
|
||
foldBuckets m.buckets d f
|
||
|
||
def insert [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
|
||
match m with
|
||
| ⟨size, buckets⟩ :=
|
||
let ⟨i, h⟩ := mkIdx buckets.property (hash a) in
|
||
let bkt := buckets.val.idx i h in
|
||
if bkt.contains a
|
||
then ⟨size, buckets.update i (bkt.replace a b) h⟩
|
||
else let size' := size + 1 in
|
||
let buckets' := buckets.update i (AssocList.cons a b bkt) h in
|
||
if size' <= buckets.val.size
|
||
then ⟨size', buckets'⟩
|
||
else let nbuckets' := buckets.val.size * 2 in
|
||
let aux₁ : nbuckets' > 0 := Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero) in
|
||
let aux₂ : (mkArray nbuckets' (@AssocList.nil α β)).size = nbuckets' := szMkArrayEq _ _ in
|
||
⟨ size',
|
||
foldBuckets buckets' ⟨mkArray nbuckets' AssocList.nil, aux₂.symm ▸ aux₁⟩ (reinsertAux hash) ⟩
|
||
|
||
def erase [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
|
||
match m with
|
||
| ⟨ size, buckets ⟩ :=
|
||
let ⟨i, h⟩ := mkIdx buckets.property (hash a) in
|
||
let bkt := buckets.val.idx i h in
|
||
if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
|
||
else m
|
||
|
||
inductive WellFormed [HasBeq α] [Hashable α] : HashMapImp α β → Prop
|
||
| mkWff : ∀ n, WellFormed (mkHashMapImp n)
|
||
| insertWff : ∀ m a b, WellFormed m → WellFormed (insert m a b)
|
||
| eraseWff : ∀ m a, WellFormed m → WellFormed (erase m a)
|
||
|
||
end HashMapImp
|
||
|
||
def HashMap (α : Type u) (β : Type v) [HasBeq α] [Hashable α] :=
|
||
{ m : HashMapImp α β // m.WellFormed }
|
||
|
||
open HashMapImp
|
||
|
||
def mkHashMap {α : Type u} {β : Type v} [HasBeq α] [Hashable α] (nbuckets := 8) : HashMap α β :=
|
||
⟨ mkHashMapImp nbuckets, WellFormed.mkWff nbuckets ⟩
|
||
|
||
namespace HashMap
|
||
variables {α : Type u} {β : Type v} [HasBeq α] [Hashable α]
|
||
|
||
instance : Inhabited (HashMap α β) :=
|
||
⟨mkHashMap⟩
|
||
|
||
instance : HasEmptyc (HashMap α β) :=
|
||
⟨mkHashMap⟩
|
||
|
||
@[inline] def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β :=
|
||
match m with
|
||
| ⟨ m, hw ⟩ := ⟨ m.insert a b, WellFormed.insertWff m a b hw ⟩
|
||
|
||
@[inline] def erase (m : HashMap α β) (a : α) : HashMap α β :=
|
||
match m with
|
||
| ⟨ m, hw ⟩ := ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩
|
||
|
||
@[inline] def find (m : HashMap α β) (a : α) : Option β :=
|
||
match m with
|
||
| ⟨ m, _ ⟩ := m.find a
|
||
|
||
@[inline] def contains (m : HashMap α β) (a : α) : Bool :=
|
||
match m with
|
||
| ⟨ m, _ ⟩ := m.contains a
|
||
|
||
@[inline] def fold {δ : Type w} (m : HashMap α β) (d : δ) (f : δ → α → β → δ) : δ :=
|
||
match m with
|
||
| ⟨ m, _ ⟩ := m.fold d f
|
||
|
||
@[inline] def size (m : HashMap α β) : Nat :=
|
||
match m with
|
||
| ⟨ {size := sz, ..}, _ ⟩ := sz
|
||
|
||
@[inline] def empty (m : HashMap α β) : Bool :=
|
||
m.size = 0
|
||
|
||
end HashMap
|