Std.Data.HashSet

noncomputable def Std.HashSetBucket (α : Type u) :

Type u

Equations

Std.HashSetBucket α = { b // Array.size b > 0 }

def Std.HashSetBucket.update {α : Type u} (data : Std.HashSetBucket α) (i : USize) (d : List α) (h : USize.toNat i < Array.size data.val) :

Std.HashSetBucket α

Equations

Std.HashSetBucket.update data i d h = { val := Array.uset data.val i d h, property := (_ : Array.size (Array.uset data.val i d h) > 0) }

source

structure Std.HashSetImp (α : Type u) :

Type u

size : Nat
buckets : Std.HashSetBucket α

source

def Std.mkHashSetImp {α : Type u} (nbuckets : optParam Nat 8) :

Std.HashSetImp α

Equations

Std.mkHashSetImp nbuckets = let n := if nbuckets = 0 then 8 else nbuckets; { size := 0, buckets := { val := mkArray n [], property := (_ : Array.size (mkArray (if nbuckets = 0 then 8 else nbuckets) []) > 0) } }

source

def Std.HashSetImp.mkIdx {n : Nat} (h : n > 0) (u : USize) :

{ u // USize.toNat u < n }

Equations

Std.HashSetImp.mkIdx h u = { val := u % n, property := (_ : USize.toNat (u % n) < n) }

source

@[inline]

def Std.HashSetImp.reinsertAux {α : Type u} (hashFn : α → UInt64) (data : Std.HashSetBucket α) (a : α) :

Std.HashSetBucket α

Equations

Std.HashSetImp.reinsertAux hashFn data a = let x := Std.HashSetImp.mkIdx (_ : Array.size data.val > 0) (UInt64.toUSize (hashFn a)); match x with | { val := i, property := h } => Std.HashSetBucket.update data i (a :: Array.uget data.val i h) h

source

@[inline]

def Std.HashSetImp.foldBucketsM {α : Type u} {δ : Type w} {m : Type w → Type w} [inst : Monad m] (data : Std.HashSetBucket α) (d : δ) (f : δ → α → m δ) :

m δ

Equations

Std.HashSetImp.foldBucketsM data d f = Array.foldlM (fun d as => List.foldlM f d as) d data.val 0 (Array.size data.val)

source

@[inline]

def Std.HashSetImp.foldBuckets {α : Type u} {δ : Type w} (data : Std.HashSetBucket α) (d : δ) (f : δ → α → δ) :

δ

Equations

Std.HashSetImp.foldBuckets data d f = Id.run (Std.HashSetImp.foldBucketsM data d f)

source

@[inline]

def Std.HashSetImp.foldM {α : Type u} {δ : Type w} {m : Type w → Type w} [inst : Monad m] (f : δ → α → m δ) (d : δ) (h : Std.HashSetImp α) :

m δ

Equations

Std.HashSetImp.foldM f d h = Std.HashSetImp.foldBucketsM h.buckets d f

source

@[inline]

def Std.HashSetImp.fold {α : Type u} {δ : Type w} (f : δ → α → δ) (d : δ) (m : Std.HashSetImp α) :

δ

Equations

Std.HashSetImp.fold f d m = Std.HashSetImp.foldBuckets m.buckets d f

source

def Std.HashSetImp.find? {α : Type u} [inst : BEq α] [inst : Hashable α] (m : Std.HashSetImp α) (a : α) :

Option α

Equations

Std.HashSetImp.find? m a = match m with | { size := x, buckets := buckets } => let x := Std.HashSetImp.mkIdx (_ : Array.size buckets.val > 0) (UInt64.toUSize (hash a)); match x with | { val := i, property := h } => List.find? (fun a' => a == a') (Array.uget buckets.val i h)

source

def Std.HashSetImp.contains {α : Type u} [inst : BEq α] [inst : Hashable α] (m : Std.HashSetImp α) (a : α) :

Bool

Equations

Std.HashSetImp.contains m a = match m with | { size := x, buckets := buckets } => let x := Std.HashSetImp.mkIdx (_ : Array.size buckets.val > 0) (UInt64.toUSize (hash a)); match x with | { val := i, property := h } => List.contains (Array.uget buckets.val i h) a

source

partial def Std.HashSetImp.moveEntries {α : Type u} [inst : Hashable α] (i : Nat) (source : Array (List α)) (target : Std.HashSetBucket α) :

Std.HashSetBucket α

source

def Std.HashSetImp.expand {α : Type u} [inst : Hashable α] (size : Nat) (buckets : Std.HashSetBucket α) :

Std.HashSetImp α

Equations

Std.HashSetImp.expand size buckets = let nbuckets := Array.size buckets.val * 2; let_fun this := (_ : Array.size buckets.val * 2 > 0); let new_buckets := { val := mkArray nbuckets [], property := (_ : Array.size (mkArray nbuckets []) > 0) }; { size := size, buckets := Std.HashSetImp.moveEntries 0 buckets.val new_buckets }

source

def Std.HashSetImp.insert {α : Type u} [inst : BEq α] [inst : Hashable α] (m : Std.HashSetImp α) (a : α) :

Std.HashSetImp α

Equations

Std.HashSetImp.insert m a = match m with | { size := size, buckets := buckets } => let x := Std.HashSetImp.mkIdx (_ : Array.size buckets.val > 0) (UInt64.toUSize (hash a)); match x with | { val := i, property := h } => let bkt := Array.uget buckets.val i h; if List.contains bkt a = true then { size := size, buckets := Std.HashSetBucket.update buckets i (List.replace bkt a a) h } else let size' := size + 1; let buckets' := Std.HashSetBucket.update buckets i (a :: bkt) h; if size' ≤ Array.size buckets.val then { size := size', buckets := buckets' } else Std.HashSetImp.expand size' buckets'

source

def Std.HashSetImp.erase {α : Type u} [inst : BEq α] [inst : Hashable α] (m : Std.HashSetImp α) (a : α) :

Std.HashSetImp α

Equations

Std.HashSetImp.erase m a = match m with | { size := size, buckets := buckets } => let x := Std.HashSetImp.mkIdx (_ : Array.size buckets.val > 0) (UInt64.toUSize (hash a)); match x with | { val := i, property := h } => let bkt := Array.uget buckets.val i h; if List.contains bkt a = true then { size := size - 1, buckets := Std.HashSetBucket.update buckets i (List.erase bkt a) h } else m

source

inductive Std.HashSetImp.WellFormed {α : Type u} [inst : BEq α] [inst : Hashable α] :

Std.HashSetImp α → Prop

mkWff: ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (n : Nat), Std.HashSetImp.WellFormed (Std.mkHashSetImp n)
insertWff: ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.HashSetImp α) (a : α), Std.HashSetImp.WellFormed m → Std.HashSetImp.WellFormed (Std.HashSetImp.insert m a)
eraseWff: ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.HashSetImp α) (a : α), Std.HashSetImp.WellFormed m → Std.HashSetImp.WellFormed (Std.HashSetImp.erase m a)

source

noncomputable def Std.HashSet (α : Type u) [inst : BEq α] [inst : Hashable α] :

Type u

Equations

Std.HashSet α = { m // Std.HashSetImp.WellFormed m }

source

def Std.mkHashSet {α : Type u} [inst : BEq α] [inst : Hashable α] (nbuckets : optParam Nat 8) :

Std.HashSet α

Equations

Std.mkHashSet nbuckets = { val := Std.mkHashSetImp nbuckets, property := (_ : Std.HashSetImp.WellFormed (Std.mkHashSetImp nbuckets)) }

source

@[inline]

def Std.HashSet.empty {α : Type u_1} [inst : BEq α] [inst : Hashable α] :

Std.HashSet α

Equations

Std.HashSet.empty = Std.mkHashSet

source

instance Std.HashSet.instInhabitedHashSet {α : Type u_1} [inst : BEq α] [inst : Hashable α] :

Inhabited (Std.HashSet α)

Equations

Std.HashSet.instInhabitedHashSet = { default := Std.mkHashSet }

source

instance Std.HashSet.instEmptyCollectionHashSet {α : Type u_1} [inst : BEq α] [inst : Hashable α] :

EmptyCollection (Std.HashSet α)

Equations

Std.HashSet.instEmptyCollectionHashSet = { emptyCollection := Std.mkHashSet }

source

@[inline]

def Std.HashSet.insert {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → α → Std.HashSet α

Equations

Std.HashSet.insert m a = match m with | { val := m, property := hw } => { val := Std.HashSetImp.insert m a, property := (_ : Std.HashSetImp.WellFormed (Std.HashSetImp.insert m a)) }

source

@[inline]

def Std.HashSet.erase {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → α → Std.HashSet α

Equations

Std.HashSet.erase m a = match m with | { val := m, property := hw } => { val := Std.HashSetImp.erase m a, property := (_ : Std.HashSetImp.WellFormed (Std.HashSetImp.erase m a)) }

source

@[inline]

def Std.HashSet.find? {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → α → Option α

Equations

Std.HashSet.find? m a = match m with | { val := m, property := x } => Std.HashSetImp.find? m a

source

@[inline]

def Std.HashSet.contains {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → α → Bool

Equations

Std.HashSet.contains m a = match m with | { val := m, property := x } => Std.HashSetImp.contains m a

source

@[inline]

def Std.HashSet.foldM {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → {m : Type w → Type w} → [inst : Monad m] → (δ → α → m δ) → δ → Std.HashSet α → m δ

Equations

Std.HashSet.foldM f init h = match h with | { val := h, property := x } => Std.HashSetImp.foldM f init h

source

@[inline]

def Std.HashSet.fold {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → (δ → α → δ) → δ → Std.HashSet α → δ

Equations

Std.HashSet.fold f init m = match m with | { val := m, property := x } => Std.HashSetImp.fold f init m

source

@[inline]

def Std.HashSet.size {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → Nat

Equations

Std.HashSet.size m = match m with | { val := { size := sz, buckets := x }, property := x_1 } => sz

source

@[inline]

def Std.HashSet.isEmpty {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → Bool

Equations

Std.HashSet.isEmpty m = decide (Std.HashSet.size m = 0)

source

def Std.HashSet.toList {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → List α

Equations

Std.HashSet.toList m = Std.HashSet.fold (fun r a => a :: r) [] m

source

def Std.HashSet.toArray {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → Array α

Equations

Std.HashSet.toArray m = Std.HashSet.fold (fun r a => Array.push r a) #[] m

source

def Std.HashSet.numBuckets {α : Type u} :

{x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → Nat

Equations

Std.HashSet.numBuckets m = Array.size m.val.buckets.val