oops

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddharth Bhat
 -/
 prelude
-import Lean.Data.HashMap
 import Lean.Runtime
 import Lean.Compiler.NameMangling
 import Lean.Compiler.ExportAttr

src/Lean/Data.lean

@@ -6,8 +6,6 @@ Authors: Sebastian Ullrich
 prelude
 import Lean.Data.AssocList
 import Lean.Data.Format
-import Lean.Data.HashMap
-import Lean.Data.HashSet
 import Lean.Data.Json
 import Lean.Data.JsonRpc
 import Lean.Data.KVMap

src/Lean/Data/HashMap.lean

@@ -1,292 +0,0 @@
-/-
-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.Nat.Power2
-import Lean.Data.AssocList
-import Std.Data.HashMap.Basic
-import Std.Data.HashMap.Raw
-namespace Lean
-
-def HashMapBucket (α : Type u) (β : Type v) :=
-  { b : Array (AssocList α β) // b.size.isPowerOfTwo }
-
-def HashMapBucket.update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β) (h : i.toNat < data.val.size) : HashMapBucket α β :=
-  ⟨ data.val.uset i d h,
-    by erw [Array.size_set]; apply data.property ⟩
-
-@[simp] theorem HashMapBucket.size_update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β)
-    (h : i.toNat < data.val.size) : (data.update i d h).val.size = data.val.size := by
-  simp [update, Array.uset]
-
-structure HashMapImp (α : Type u) (β : Type v) where
-  size       : Nat
-  buckets    : HashMapBucket α β
-
-private def numBucketsForCapacity (capacity : Nat) : Nat :=
-  -- a "load factor" of 0.75 is the usual standard for hash maps
-  capacity * 4 / 3
-
-def mkHashMapImp {α : Type u} {β : Type v} (capacity := 8) : HashMapImp α β :=
-  { size       := 0
-    buckets    :=
-    ⟨mkArray (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil,
-     by simp; apply Nat.isPowerOfTwo_nextPowerOfTwo⟩ }
-
-namespace HashMapImp
-variable {α : Type u} {β : Type v}
-
-/- Remark: we use a C implementation because this function is performance critical. -/
-@[extern "lean_hashmap_mk_idx"]
-private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize // u.toNat < sz } :=
-  -- TODO: avoid `if` in the reference implementation
-  let u := hash.toUSize &&& (sz.toUSize - 1)
-  if h' : u.toNat < sz then
-    ⟨u, h'⟩
-  else
-    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
-
-@[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
-  let ⟨i, h⟩ := mkIdx (hashFn a) data.property
-  data.update i (AssocList.cons a b data.val[i]) h
-
-@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (d : δ) (f : δ → α → β → m δ) : m δ :=
-  data.val.foldlM (init := d) fun d b => b.foldlM f d
-
-@[inline] def foldBuckets {δ : Type w} (data : HashMapBucket α β) (d : δ) (f : δ → α → β → δ) : δ :=
-  Id.run $ foldBucketsM data d f
-
-@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (d : δ) (h : HashMapImp α β) : m δ :=
-  foldBucketsM h.buckets d f
-
-@[inline] def fold {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : HashMapImp α β) : δ :=
-  foldBuckets m.buckets d f
-
-@[inline] def forBucketsM {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (f : α → β → m PUnit) : m PUnit :=
-  data.val.forM fun b => b.forM f
-
-@[inline] def forM {m : Type w → Type w} [Monad m] (f : α → β → m PUnit) (h : HashMapImp α β) : m PUnit :=
-  forBucketsM h.buckets f
-
-def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
-  match m with
-  | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].findEntry? a
-
-def find? [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
-  match m with
-  | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].find? a
-
-def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
-  match m with
-  | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].contains a
-
-def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
-  if h : i < source.size then
-     let es  : AssocList α β   := source[i]
-     -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set i AssocList.nil
-     let target                := es.foldl (reinsertAux hash) target
-     moveEntries (i+1) source target
-  else target
-termination_by source.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
-  let bucketsNew : HashMapBucket α β := ⟨
-    mkArray (buckets.val.size * 2) AssocList.nil,
-    by simp; apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo buckets.property
-  ⟩
-  { size    := size,
-    buckets := moveEntries 0 buckets.val bucketsNew }
-
-@[inline] def insert [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β × Bool :=
-  match m with
-  | ⟨size, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    let bkt    := buckets.val[i]
-    if bkt.contains a then
-      -- make sure `bkt` is used linearly in the following call to `replace`
-      let buckets' := buckets.update i .nil h
-      (⟨size, buckets'.update i (bkt.replace a b) (by simpa [buckets'])⟩, true)
-    else
-      let size'    := size + 1
-      let buckets' := buckets.update i (AssocList.cons a b bkt) h
-      if numBucketsForCapacity size' ≤ buckets.val.size then
-        ({ size := size', buckets := buckets' }, false)
-      else
-        (expand size' buckets', false)
-
-@[inline] def insertIfNew [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β × Option β :=
-  match m with
-  | ⟨size, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    let bkt    := buckets.val[i]
-    if let some b := bkt.find? a then
-      (⟨size, buckets⟩, some b)
-    else
-      let size'    := size + 1
-      let buckets' := buckets.update i (AssocList.cons a b bkt) h
-      if numBucketsForCapacity size' ≤ buckets.val.size then
-        ({ size := size', buckets := buckets' }, none)
-      else
-        (expand size' buckets', none)
-
-
-def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
-  match m with
-  | ⟨ size, buckets ⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    let bkt    := buckets.val[i]
-    if bkt.contains a then
-      -- make sure `bkt` is used linearly in the following call to `erase`
-      let buckets' := buckets.update i .nil h
-      ⟨size - 1, buckets'.update i (bkt.erase a) (by simpa [buckets'])⟩
-    else
-      ⟨size, buckets⟩
-
-inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β → Prop where
-  | mkWff          : ∀ n,                    WellFormed (mkHashMapImp n)
-  | insertWff      : ∀ m a b, WellFormed m → WellFormed (insert m a b |>.1)
-  | insertIfNewWff : ∀ m a b, WellFormed m → WellFormed (insertIfNew m a b |>.1)
-  | eraseWff       : ∀ m a,   WellFormed m → WellFormed (erase m a)
-
-end HashMapImp
-
-def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
-  { m : HashMapImp α β // m.WellFormed }
-
-open Lean.HashMapImp
-
-def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (capacity := 8) : HashMap α β :=
-  ⟨ mkHashMapImp capacity, WellFormed.mkWff capacity ⟩
-
-namespace HashMap
-instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
-  default := mkHashMap
-
-instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) := ⟨mkHashMap⟩
-
-@[inline] def empty [BEq α] [Hashable α] : HashMap α β :=
-  mkHashMap
-
-variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
-
-def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β :=
-  match m with
-  | ⟨ m, hw ⟩ =>
-    match h:m.insert a b with
-    | (m', _) => ⟨ m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption ⟩
-
-/-- Similar to `insert`, but also returns a Boolean flag indicating whether an existing entry has been replaced with `a -> b`. -/
-def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
-  match m with
-  | ⟨ m, hw ⟩ =>
-    match h:m.insert a b with
-    | (m', replaced) => (⟨ m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption ⟩, replaced)
-
-/--
-Similar to `insert`, but returns `some old` if the map already had an entry `α → old`.
-If the result is `some old`, the resulting map is equal to `m`. -/
-def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option β :=
-  match m with
-  | ⟨ m, hw ⟩ =>
-    match h:m.insertIfNew a b with
-    | (m', old) => (⟨ m', by have aux := WellFormed.insertIfNewWff m a b hw; rw [h] at aux; assumption ⟩, old)
-
-@[inline] def erase (m : HashMap α β) (a : α) : HashMap α β :=
-  match m with
-  | ⟨ m, hw ⟩ => ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩
-
-@[inline] def findEntry? (m : HashMap α β) (a : α) : Option (α × β) :=
-  match m with
-  | ⟨ m, _ ⟩ => m.findEntry? a
-
-@[inline] def find? (m : HashMap α β) (a : α) : Option β :=
-  match m with
-  | ⟨ m, _ ⟩ => m.find? a
-
-@[inline] def findD (m : HashMap α β) (a : α) (b₀ : β) : β :=
-  (m.find? a).getD b₀
-
-@[inline] def find! [Inhabited β] (m : HashMap α β) (a : α) : β :=
-  match m.find? a with
-  | some b => b
-  | none   => panic! "key is not in the map"
-
-instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
-  getElem m k _ := m.find? k
-
-@[inline] def contains (m : HashMap α β) (a : α) : Bool :=
-  match m with
-  | ⟨ m, _ ⟩ => m.contains a
-
-@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (init : δ) (h : HashMap α β) : m δ :=
-  match h with
-  | ⟨ h, _ ⟩ => h.foldM f init
-
-@[inline] def fold {δ : Type w} (f : δ → α → β → δ) (init : δ) (m : HashMap α β) : δ :=
-  match m with
-  | ⟨ m, _ ⟩ => m.fold f init
-
-@[inline] def forM {m : Type w → Type w} [Monad m] (f : α → β → m PUnit) (h : HashMap α β) : m PUnit :=
-  match h with
-  | ⟨ h, _ ⟩ => h.forM f
-
-@[inline] def size (m : HashMap α β) : Nat :=
-  match m with
-  | ⟨ {size := sz, ..}, _ ⟩ => sz
-
-@[inline] def isEmpty (m : HashMap α β) : Bool :=
-  m.size = 0
-
-def toList (m : HashMap α β) : List (α × β) :=
-  m.fold (init := []) fun r k v => (k, v)::r
-
-def toArray (m : HashMap α β) : Array (α × β) :=
-  m.fold (init := #[]) fun r k v => r.push (k, v)
-
-def numBuckets (m : HashMap α β) : Nat :=
-  m.val.buckets.val.size
-
-variable [BEq α] [Hashable α]
-
-/-- Builds a `HashMap` from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences. -/
-def ofList (l : List (α × β)) : HashMap α β :=
-  l.foldl (init := HashMap.empty) (fun m p => m.insert p.fst p.snd)
-
-/-- Variant of `ofList` which accepts a function that combines values of duplicated keys. -/
-def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
-  l.foldl (init := HashMap.empty)
-    (fun m p =>
-      match m.find? p.fst with
-        | none   => m.insert p.fst p.snd
-        | some v => m.insert p.fst $ f v p.snd)
-
-attribute [deprecated Std.HashMap.insert (since := "2024-08-08")] HashMap.insert
-attribute [deprecated Std.HashMap.containsThenInsert (since := "2024-08-08")] HashMap.insert'
-attribute [deprecated Std.HashMap.insertIfNew (since := "2024-08-08")] HashMap.insertIfNew
-attribute [deprecated Std.HashMap.erase (since := "2024-08-08")] HashMap.erase
-attribute [deprecated "Use `m[k]?` instead." (since := "2024-08-08")] HashMap.findEntry?
-attribute [deprecated "Use `m[k]?` instead." (since := "2024-08-08")] HashMap.find?
-attribute [deprecated "Use `m[k]?.getD` instead." (since := "2024-08-08")] HashMap.findD
-attribute [deprecated "Use `m[k]!` instead." (since := "2024-08-08")] HashMap.find!
-attribute [deprecated Std.HashMap.contains (since := "2024-08-08")] HashMap.contains
-attribute [deprecated Std.HashMap.foldM (since := "2024-08-08")] HashMap.foldM
-attribute [deprecated Std.HashMap.fold (since := "2024-08-08")] HashMap.fold
-attribute [deprecated Std.HashMap.forM (since := "2024-08-08")] HashMap.forM
-attribute [deprecated Std.HashMap.size (since := "2024-08-08")] HashMap.size
-attribute [deprecated Std.HashMap.isEmpty (since := "2024-08-08")] HashMap.isEmpty
-attribute [deprecated Std.HashMap.toList (since := "2024-08-08")] HashMap.toList
-attribute [deprecated Std.HashMap.toArray (since := "2024-08-08")] HashMap.toArray
-attribute [deprecated "Deprecateed without a replacement." (since := "2024-08-08")] HashMap.numBuckets
-attribute [deprecated "Deprecateed without a replacement." (since := "2024-08-08")] HashMap.ofListWith
-
-end Lean.HashMap

src/Lean/Data/HashSet.lean

@@ -1,225 +0,0 @@
-/-
-Copyright (c) 2019 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.Nat.Power2
-import Std.Data.HashSet.Basic
-import Std.Data.HashSet.Raw
-namespace Lean
-universe u v w
-
-def HashSetBucket (α : Type u) :=
-  { b : Array (List α) // b.size.isPowerOfTwo }
-
-def HashSetBucket.update {α : Type u} (data : HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) : HashSetBucket α :=
-  ⟨ data.val.uset i d h,
-    by erw [Array.size_set]; apply data.property ⟩
-
-@[simp] theorem HashSetBucket.size_update {α : Type u} (data : HashSetBucket α) (i : USize) (d : List α) (h : i.toNat < data.val.size) :
-    (data.update i d h).val.size = data.val.size := by
-  simp [update, Array.uset]
-
-structure HashSetImp (α : Type u) where
-  size       : Nat
-  buckets    : HashSetBucket α
-
-def mkHashSetImp {α : Type u} (capacity := 8) : HashSetImp α :=
-  { size       := 0
-    buckets    :=
-    ⟨mkArray ((capacity * 4) / 3).nextPowerOfTwo [],
-     by simp; apply Nat.isPowerOfTwo_nextPowerOfTwo⟩ }
-
-namespace HashSetImp
-variable {α : Type u}
-
-/- Remark: we use a C implementation because this function is performance critical. -/
-@[extern "lean_hashset_mk_idx"]
-private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize // u.toNat < sz } :=
-  -- TODO: avoid `if` in the reference implementation
-  let u := hash.toUSize &&& (sz.toUSize - 1)
-  if h' : u.toNat < sz then
-    ⟨u, h'⟩
-  else
-    ⟨0, by simp; apply Nat.pos_of_isPowerOfTwo h⟩
-
-@[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
-  let ⟨i, h⟩ := mkIdx (hashFn a) data.property
-  data.update i (a :: data.val[i]) h
-
-@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (d : δ) (f : δ → α → m δ) : m δ :=
-  data.val.foldlM (init := d) fun d as => as.foldlM f d
-
-@[inline] def foldBuckets {δ : Type w} (data : HashSetBucket α) (d : δ) (f : δ → α → δ) : δ :=
-  Id.run $ foldBucketsM data d f
-
-@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → m δ) (d : δ) (h : HashSetImp α) : m δ :=
-  foldBucketsM h.buckets d f
-
-@[inline] def fold {δ : Type w} (f : δ → α → δ) (d : δ) (m : HashSetImp α) : δ :=
-  foldBuckets m.buckets d f
-
-@[inline] def forBucketsM {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (f : α → m PUnit) : m PUnit :=
-  data.val.forM fun as => as.forM f
-
-@[inline] def forM {m : Type w → Type w} [Monad m] (f : α → m PUnit) (h : HashSetImp α) : m PUnit :=
-  forBucketsM h.buckets f
-
-def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
-  match m with
-  | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].find? (fun a' => a == a')
-
-def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
-  match m with
-  | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    buckets.val[i].contains a
-
-def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
-  if h : i < source.size then
-     let es  : List α   := source[i]
-     -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.set i []
-     let target                := es.foldl (reinsertAux hash) target
-     moveEntries (i+1) source target
-  else
-    target
-termination_by source.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
-  let bucketsNew : HashSetBucket α := ⟨
-    mkArray (buckets.val.size * 2) [],
-    by simp; apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo buckets.property
-  ⟩
-  { size    := size,
-    buckets := moveEntries 0 buckets.val bucketsNew }
-
-def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
-  match m with
-  | ⟨size, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    let bkt    := buckets.val[i]
-    if bkt.contains a
-    then
-      -- make sure `bkt` is used linearly in the following call to `replace`
-      let buckets' := buckets.update i .nil h
-      ⟨size, buckets'.update i (bkt.replace a a) (by simpa [buckets'])⟩
-    else
-      let size'    := size + 1
-      let buckets' := buckets.update i (a :: bkt) h
-      if size' ≤ buckets.val.size
-      then { size := size', buckets := buckets' }
-      else expand size' buckets'
-
-def erase [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
-  match m with
-  | ⟨ size, buckets ⟩ =>
-    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
-    let bkt    := buckets.val[i]
-    if bkt.contains a then
-      -- make sure `bkt` is used linearly in the following call to `erase`
-      let buckets' := buckets.update i .nil h
-      ⟨size - 1, buckets'.update i (bkt.erase a) (by simpa [buckets'])⟩
-    else
-      ⟨size, buckets⟩
-
-inductive WellFormed [BEq α] [Hashable α] : HashSetImp α → Prop where
-  | mkWff     : ∀ n,                  WellFormed (mkHashSetImp n)
-  | insertWff : ∀ m a, WellFormed m → WellFormed (insert m a)
-  | eraseWff  : ∀ m a, WellFormed m → WellFormed (erase m a)
-
-end HashSetImp
-
-def HashSet (α : Type u) [BEq α] [Hashable α] :=
-  { m : HashSetImp α // m.WellFormed }
-
-open HashSetImp
-
-def mkHashSet {α : Type u} [BEq α] [Hashable α] (capacity := 8) : HashSet α :=
-  ⟨ mkHashSetImp capacity, WellFormed.mkWff capacity ⟩
-
-namespace HashSet
-@[inline] def empty [BEq α] [Hashable α] : HashSet α :=
-  mkHashSet
-
-instance [BEq α] [Hashable α] : Inhabited (HashSet α) where
-  default := mkHashSet
-
-instance [BEq α] [Hashable α] : EmptyCollection (HashSet α) := ⟨mkHashSet⟩
-
-variable {α : Type u} {_ : BEq α} {_ : Hashable α}
-
-@[inline] def insert (m : HashSet α) (a : α) : HashSet α :=
-  match m with
-  | ⟨ m, hw ⟩ => ⟨ m.insert a, WellFormed.insertWff m a hw ⟩
-
-@[inline] def erase (m : HashSet α) (a : α) : HashSet α :=
-  match m with
-  | ⟨ m, hw ⟩ => ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩
-
-@[inline] def find? (m : HashSet α) (a : α) : Option α :=
-  match m with
-  | ⟨ m, _ ⟩ => m.find? a
-
-@[inline] def contains (m : HashSet α) (a : α) : Bool :=
-  match m with
-  | ⟨ m, _ ⟩ => m.contains a
-
-@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → m δ) (init : δ) (h : HashSet α) : m δ :=
-  match h with
-  | ⟨ h, _ ⟩ => h.foldM f init
-
-@[inline] def fold {δ : Type w} (f : δ → α → δ) (init : δ) (m : HashSet α) : δ :=
-  match m with
-  | ⟨ m, _ ⟩ => m.fold f init
-
-@[inline] def forM {m : Type w → Type w} [Monad m] (h : HashSet α) (f : α → m PUnit) : m PUnit :=
-  match h with
-  | ⟨h, _⟩ => h.forM f
-
-instance : ForM m (HashSet α) α where
-  forM := HashSet.forM
-
-instance : ForIn m (HashSet α) α where
-  forIn := ForM.forIn
-
-@[inline] def size (m : HashSet α) : Nat :=
-  match m with
-  | ⟨ {size := sz, ..}, _ ⟩ => sz
-
-@[inline] def isEmpty (m : HashSet α) : Bool :=
-  m.size = 0
-
-def toList (m : HashSet α) : List α :=
-  m.fold (init := []) fun r a => a::r
-
-def toArray (m : HashSet α) : Array α :=
-  m.fold (init := #[]) fun r a => r.push a
-
-def numBuckets (m : HashSet α) : Nat :=
-  m.val.buckets.val.size
-
-/-- Insert many elements into a HashSet. -/
-def insertMany [ForIn Id ρ α] (s : HashSet α) (as : ρ) : HashSet α := Id.run do
-  let mut s := s
-  for a in as do
-    s := s.insert a
-  return s
-
-/--
-`O(|t|)` amortized. Merge two `HashSet`s.
--/
-@[inline]
-def merge {α : Type u} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α :=
-  t.fold (init := s) fun s a => s.insert a
-  -- We don't use `insertMany` here because it gives weird universes.
-
-attribute [deprecated Std.HashSet (since := "2024-08-08")] HashSet
-attribute [deprecated Std.HashSet.Raw (since := "2024-08-08")] HashSetImp
-attribute [deprecated Std.HashSet.Raw.empty (since := "2024-08-08")] mkHashSetImp
-attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] mkHashSet
-attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] HashSet.empty

src/Lean/Data/NameMap.lean

@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import Std.Data.HashSet.Basic
-import Lean.Data.HashSet
 import Lean.Data.RBMap
 import Lean.Data.RBTree
 import Lean.Data.SSet

src/Lean/Data/SMap.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Std.Data.HashMap.Basic
-import Lean.Data.HashMap
 import Lean.Data.PersistentHashMap
 universe u v w w'
 

src/Lean/Environment.lean

@@ -9,7 +9,6 @@ import Init.Data.Array.BinSearch
 import Init.Data.Stream
 import Init.System.Promise
 import Lean.ImportingFlag
-import Lean.Data.HashMap
 import Lean.Data.NameTrie
 import Lean.Data.SMap
 import Lean.Declaration

src/Lean/Level.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.QSort
-import Lean.Data.HashMap
-import Lean.Data.HashSet
 import Lean.Data.PersistentHashMap
 import Lean.Data.PersistentHashSet
 import Lean.Hygiene

src/Lean/Meta/Canonicalizer.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Data.HashMap
 import Lean.Util.ShareCommon
 import Lean.Meta.Basic
 import Lean.Meta.FunInfo

src/Lean/Meta/Tactic/Grind/Arith/Offset/Types.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Data.AssocList
 import Lean.Data.PersistentArray
 import Lean.Meta.Tactic.Grind.ENodeKey
 import Lean.Meta.Tactic.Grind.Arith.Util

src/Lean/Util/Diff.lean

@@ -6,7 +6,6 @@ Authors: David Thrane Christiansen
 prelude
 import Init.Data.Array.Subarray.Split
 import Init.Data.Range
-import Lean.Data.HashMap
 import Std.Data.HashMap.Basic
 import Init.Omega
 

src/Lean/Util/MonadCache.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Control.StateRef
-import Lean.Data.HashMap
 import Std.Data.HashMap.Basic
 
 namespace Lean

src/Lean/Util/PtrSet.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Hashable
-import Lean.Data.HashSet
-import Lean.Data.HashMap
 import Std.Data.HashSet.Basic
 import Std.Data.HashMap.Basic
 

src/Lean/Util/SCC.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Data.HashMap
 import Std.Data.HashMap.Basic
 namespace Lean.SCC
 /-!

src/lake/Lake/Util/OrdHashSet.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Lean.Data.HashSet
 import Std.Data.HashSet.Basic
 
 open Lean

tests/bench/liasolver.lean

@@ -3,8 +3,8 @@ Linear Diophantine equation solver
 
 Author: Marc Huisinga
 -/
-
-import Lean.Data.HashMap
+import Lean.Data.AssocList
+import Std.Data.HashMap
 
 open Lean
 
@@ -47,30 +47,12 @@ namespace Lean.AssocList
 
 end Lean.AssocList
 
-namespace Lean.HashMap
+namespace Std.HashMap
 
   variable [BEq α] [Hashable α]
 
-  @[inline] protected def forIn {δ : Type w} {m : Type w → Type w'} [Monad m]
-    (as : HashMap α β) (init : δ) (f : (α × β) → δ → m (ForInStep δ)) : m δ := do
-    forIn as.val.buckets.val init fun bucket acc => do
-      let (done, v) ← bucket.forIn (false, acc) fun v (_, acc) => do
-        let r ← f v acc
-        match r with
-        | ForInStep.done r' =>
-          return ForInStep.done (true, r')
-        | ForInStep.yield r' =>
-          return ForInStep.yield (false, r')
-      if done then
-        return ForInStep.done v
-      else
-        return ForInStep.yield v
-
-  instance : ForIn m (HashMap α β) (α × β) where
-    forIn := HashMap.forIn
-
   def modify! [Inhabited β] (xs : HashMap α β) (k : α) (f : β → β) : HashMap α β :=
-    let v := xs.find! k
+    let v := xs[k]!
     xs.erase k |>.insert k (f v)
 
   def any (xs : HashMap α β) (p : α → β → Bool) : Bool := Id.run <| do
@@ -80,28 +62,22 @@ namespace Lean.HashMap
     return false
 
   def mapValsM [Monad m] (f : β → m γ) (xs : HashMap α β) : m (HashMap α γ) :=
-    mkHashMap (capacity := xs.size) |> xs.foldM fun acc k v => return acc.insert k (←f v)
+    HashMap.empty (capacity := xs.size) |> xs.foldM fun acc k v => return acc.insert k (←f v)
 
   def mapVals (f : β → γ) (xs : HashMap α β) : HashMap α γ :=
-    mkHashMap (capacity := xs.size) |> xs.fold fun acc k v => acc.insert k (f v)
+    HashMap.empty (capacity := xs.size) |> xs.fold fun acc k v => acc.insert k (f v)
 
   def fastMapVals (f : α → β → β) (xs : HashMap α β) : HashMap α β :=
-    let size := xs.val.size
-    let buckets := xs.val.buckets.val.map (·.map f)
-    ⟨⟨size, ⟨buckets, sorry⟩⟩, sorry⟩
-
-  def filter (p : α → β → Bool) (xs : HashMap α β) : HashMap α β :=
-    let buckets := xs.val.buckets.val.map (·.filter p)
-    let size := buckets.foldl (fun acc bucket => bucket.foldl (fun acc _ _ => acc + 1) acc) 0
-    ⟨⟨size, ⟨buckets, sorry⟩⟩, sorry⟩
+    xs.map f
 
   def getAny? (x : HashMap α β) : Option (α × β) := Id.run <| do
-    for bucket in x.val.buckets.val do
-      for (k, v) in bucket do
-        return some (k, v)
+    for (k, v) in x do
+      return some (k, v)
     return none
 
-end Lean.HashMap
+end Std.HashMap
+
+open Std (HashMap)
 
 structure Equation where
   id     : Nat
@@ -114,10 +90,10 @@ def gcd (coeffs : HashMap Nat Int) : Nat :=
   let coeffsContent := coeffs.toArray
   match coeffsContent with
   | #[]           => panic! "Cannot calculate GCD of empty list of coefficients"
-  | #[(i, x)]     => x
+  | #[(_, x)]     => x
   | coeffsContent =>
     coeffsContent[0]!.2.gcd coeffsContent[1]!.2
-      |> coeffs.fold fun acc k v => acc.gcd v
+      |> coeffs.fold fun acc _ v => acc.gcd v
 
 namespace Equation
 
@@ -149,10 +125,10 @@ namespace Equation
     let V_fromEq := fromEq.coeffs
     let V_toEq := toEq.coeffs
     let k := varIdx
-    let sₖ := V_fromEq.find! k
-    let bₖ := V_toEq.find! k
+    let sₖ := V_fromEq[k]!
+    let bₖ := V_toEq[k]!
     let mut V_toEq := V_toEq.fastMapVals fun i bᵢ =>
-      match V_fromEq.find? i with
+      match V_fromEq[i]? with
       | none =>
         bᵢ
       | some aᵢ =>
@@ -178,7 +154,7 @@ namespace Equation
       const  := (-1)*e.const }
 
   def reorganizeFor (e : Equation) (varIdx : Nat) : Equation := Id.run <| do
-    let singletonCoeff := e.coeffs.find! varIdx
+    let singletonCoeff := e.coeffs[varIdx]!
     let mut e := { e with coeffs := e.coeffs.fastMapVals fun _ coeff => (-1)*coeff }
     if singletonCoeff = -1 then
       e := e.invert
@@ -196,7 +172,7 @@ namespace Equation
       match r? with
       | none =>
         r? := some (i, coeff)
-      | some (i', coeff') =>
+      | some (_, coeff') =>
         if coeff.natAbs < coeff'.natAbs then
           r? := some (i, coeff)
     return r?
@@ -231,11 +207,11 @@ def eliminateSingleton (p : Problem) (singletonEq : Equation) (varIdx : Nat) : P
 
 partial def eliminateSingletons (p : Problem) : Problem := Id.run <| do
   let mut r? : Option (Equation × Nat) := none
-  for (id, eq) in p.equations do
+  for (_, eq) in p.equations do
     match eq.findSingleton? with
     | none =>
       continue
-    | some (varIdx, coeff) =>
+    | some (varIdx, _) =>
       r? := some (eq, varIdx)
   match r? with
   | none =>
@@ -303,7 +279,7 @@ partial def readSolution? (p : Problem) : Option Solution := Id.run <| do
   return Solution.sat <| assignment.map (·.get!)
 where
   readSolution (varIdx : Nat) (assignment : Array (Option Int)) : Array (Option Int) := Id.run <| do
-    match p.solvedEquations.find? varIdx with
+    match p.solvedEquations[varIdx]? with
     | none =>
       return assignment.set! varIdx (some 0)
     | some eq =>
@@ -364,14 +340,14 @@ def main (args : List String) : IO UInt32 := do
   let header := headerLine.splitOn.toArray
   let nEquations ← header.ithVal 0 "amount of equations"
   let nVars ← header.ithVal 1 "amount of variables"
-  let mut equations : HashMap Nat Equation := mkHashMap
+  let mut equations : HashMap Nat Equation := ∅
   for line in lines[1:] do
     let elems := line.splitOn.toArray
     let nTerms ← elems.ithVal 0 "amount of equation terms"
     let 0 ← elems.ithVal (elems.size - 1) "end of line symbol"
       | error "Non-zero end of line symbol"
     let const ← elems.ithVal (elems.size - 2) "constant value"
-    let mut coeffs := mkHashMap
+    let mut coeffs := ∅
     for i in [1:elems.size-2:2] do
       let coeff ← elems.ithVal i "coefficient"
       let varIdx ← elems.ithVal (i + 1) "variable index"
@@ -386,7 +362,7 @@ def main (args : List String) : IO UInt32 := do
   | none =>
     IO.println "UNSAT"
   | some equations' =>
-    let problem : Problem := ⟨equations', mkHashMap, equations'.size, nVars.natAbs⟩
+    let problem : Problem := ⟨equations', ∅, equations'.size, nVars.natAbs⟩
     match solveProblem problem with
     | Solution.unsat =>
       IO.println "UNSAT"

tests/lean/1206.lean

@@ -1,11 +1,11 @@
-import Lean.Data.HashSet
+import Std.Data.HashSet
 
 set_option linter.unusedVariables true
 
 open Lean
 
-def boo : Id (HashSet Nat) := do
-  let mut vs : HashSet Nat := HashSet.empty
+def boo : Id (Std.HashSet Nat) := do
+  let mut vs : Std.HashSet Nat := ∅
   for i in List.range 10 do
     /- unused variable `vs` -/
     (_, vs) := (i, vs.insert i)

tests/lean/lcnfTypes.lean

@@ -134,4 +134,3 @@ set_option pp.explicit true
 #eval testMono ``Elab.Term.elabTerm
 #eval testMono ``Nat.add
 #eval testMono ``Fin.add
-#eval testMono ``HashSetBucket.update

tests/lean/lcnfTypes.lean.expected.out

@@ -52,4 +52,3 @@ Lean.Elab.Term.elabTerm : Syntax →
           lcErased → Context → lcErased → Core.Context → lcErased → PUnit → EStateM.Result Exception PUnit Expr
 Nat.add : Nat → Nat → Nat
 Fin.add : Nat → Nat → Nat → Nat
-Lean.HashSetBucket.update : lcErased → Array (List lcAny) → USize → List lcAny → lcErased → Array (List lcAny)

tests/lean/moduleOf.lean

@@ -8,7 +8,7 @@ def tst : MetaM Unit := do
   IO.println (← findModuleOf? `HAdd.hAdd)
   IO.println (← findModuleOf? `Lean.Core.CoreM)
   IO.println (← findModuleOf? `Lean.Elab.Term.elabTerm)
-  IO.println (← findModuleOf? `Lean.HashMap.insert)
+  IO.println (← findModuleOf? `Std.HashMap.insert)
   IO.println (← findModuleOf? `tst)
   IO.println (← findModuleOf? `f)
   IO.println (← findModuleOf? `foo) -- Error: unknown 'foo'

tests/lean/moduleOf.lean.expected.out

@@ -1,7 +1,7 @@
 (some Init.Prelude)
 (some Lean.CoreM)
 (some Lean.Elab.Term)
-(some Lean.Data.HashMap)
+(some Std.Data.HashMap.Basic)
 none
 none
 moduleOf.lean:16:0-16:5: error: unknown constant 'foo'

tests/lean/optionGetD.lean

@@ -1,11 +1,11 @@
-import Lean.Data.HashMap
+import Std.Data.HashMap
 
-def test (m : Lean.HashMap Nat Nat) : IO (Nat × Nat) := do
+def test (m : Std.HashMap Nat Nat) : IO (Nat × Nat) := do
   let start := 1
   let mut i := start
   let mut count := 0
   while i != 0 do
-    i := (m.find? i).getD (panic! "key is not in the map")
+    i := m[i]?.getD (panic! "key is not in the map")
     count := count + 1
   return (i, count)
 

tests/lean/run/3731.lean

@@ -1,4 +1,4 @@
-import Lean.Data.HashMap
+import Std.Data.HashMap
 open Lean
 
 /--
@@ -24,7 +24,7 @@ inductive Decl where
 /--
 A cache that is valid with respect to some `Array Decl`.
 -/
-def Cache (_decls : Array Decl) := HashMap Decl Nat
+abbrev Cache (_decls : Array Decl) := Std.HashMap Decl Nat
 
 /--
 Lookup a `decl` in a `cache`.
@@ -33,7 +33,7 @@ If this returns `some i`, `Cache.find?_poperty` can be used to demonstrate: `dec
 -/
 @[irreducible]
 def Cache.find? (cache : Cache decls) (decl : Decl) : Option Nat :=
-  match cache.val.find? decl with
+  match cache[decl]? with
   | some hit =>
     if h1:hit < decls.size then
       if decls[hit]'h1 = decl then

tests/lean/run/998Export.lean

@@ -1,6 +1,7 @@
 import Lean
 open Lean
 
+
 inductive Entry
 | name (n : Name)
 | level (n : Level)
@@ -9,17 +10,17 @@ inductive Entry
 deriving Inhabited
 
 structure Alloc (α) [BEq α] [Hashable α] where
-  map : HashMap α Nat
+  map : Std.HashMap α Nat
   next : Nat
 deriving Inhabited
 
 namespace Export
 
 structure State where
-  names : Alloc Name := ⟨HashMap.empty.insert Name.anonymous 0, 1⟩
-  levels : Alloc Level := ⟨HashMap.empty.insert levelZero 0, 1⟩
+  names : Alloc Name := ⟨(∅ : Std.HashMap Name Nat).insert Name.anonymous 0, 1⟩
+  levels : Alloc Level := ⟨(∅ : Std.HashMap Level Nat).insert levelZero 0, 1⟩
   exprs : Alloc Expr
-  defs : HashSet Name
+  defs : Std.HashSet Name
   stk : Array (Bool × Entry)
 deriving Inhabited
 
@@ -51,7 +52,7 @@ def alloc {α} [BEq α] [Hashable α] [OfState α] (a : α) : ExportM Nat := do
   pure n
 
 def exportName (n : Name) : ExportM Nat := do
-  match (← get).names.map.find? n with
+  match (← get).names.map[n]? with
   | some i => pure i
   | none => match n with
     | .anonymous => pure 0
@@ -61,7 +62,7 @@ def exportName (n : Name) : ExportM Nat := do
 attribute [simp] exportName
 
 def exportLevel (L : Level) : ExportM Nat := do
-  match (← get).levels.map.find? L with
+  match (← get).levels.map[L]? with
   | some i => pure i
   | none => match L with
     | Level.zero => pure 0
@@ -73,7 +74,7 @@ def exportLevel (L : Level) : ExportM Nat := do
       let i ← alloc L; IO.println s!"{i} #UIM {← exportLevel l₁} {← exportLevel l₂}"; pure i
     | Level.param n =>
       let i ← alloc L; IO.println s!"{i} #UP {← exportName n}"; pure i
-    | Level.mvar n => unreachable!
+    | Level.mvar _ => unreachable!
 
 -- TODO: this test has been broken for a while with a panic that was ignored by the test suite
 --attribute [simp] exportLevel

tests/lean/run/KyleAlg.lean

@@ -227,7 +227,7 @@ unsafe def Expr.dagSizeUnsafe (e : Expr) : IO Nat := do
   let (_, s) ← visit e |>.run ({}, 0)
   return s.2
 where
-  visit (e : Expr) : StateRefT (HashSet USize × Nat) IO Unit := do
+  visit (e : Expr) : StateRefT (Std.HashSet USize × Nat) IO Unit := do
     let addr := ptrAddrUnsafe e
     unless (← get).1.contains addr do
       modify fun (s, c) => (s.insert addr, c+1)

tests/lean/run/PPTopDownAnalyze.lean

@@ -358,7 +358,6 @@ set_option pp.analyze.trustSubtypeMk true in
 #testDelabN Array.mk.injEq
 #testDelabN Lean.PrefixTree.empty
 #testDelabN Lean.PersistentHashMap.getCollisionNodeSize.match_1
-#testDelabN Lean.HashMap.size.match_1
 #testDelabN and_false
 #testDelabN Lean.Server.FileWorker.handlePlainTermGoal
 #testDelabN Lean.Server.FileWorker.handlePlainGoal

tests/lean/run/arthur1.lean

@@ -1,4 +1,4 @@
-import Lean.Data.HashMap
+import Std.Data.HashMap
 
 inductive NEList (α : Type)
   | uno  : α → NEList α
@@ -67,7 +67,7 @@ inductive Value
   | lam  : Lambda → Value
   deriving Inhabited
 
-abbrev Context := Lean.HashMap String Value
+abbrev Context := Std.HashMap String Value
 
 inductive ErrorType
   | name | type | runTime
@@ -318,7 +318,7 @@ def State.step : State → State
 
   | expr (.lit l) ctx k => ret (.lit l) ctx k
   | expr (.list l) ctx k => ret (.list l) ctx k
-  | expr (.var n) ctx k => match ctx[n] with
+  | expr (.var n) ctx k => match ctx[n]? with
     | none   => error .name ctx $ notFound n
     | some v => ret v ctx k
   | expr (.lam l) ctx k => ret (.lam l) ctx k
@@ -362,7 +362,7 @@ def State.step : State → State
   | s@(done ..)  => s
 
 def Context.equiv (cₗ cᵣ : Context) : Prop :=
-  ∀ n : String, cₗ[n] = cᵣ[n]
+  ∀ n : String, cₗ[n]? = cᵣ[n]?
 
 def State.stepN : State → Nat → State
   | s, 0     => s

tests/lean/run/arthur2.lean

@@ -1,4 +1,4 @@
-import Lean.Data.HashMap
+import Std.Data.HashMap
 
 inductive NEList (α : Type)
   | uno  : α → NEList α
@@ -67,7 +67,7 @@ inductive Value
   | lam  : Lambda → Value
   deriving Inhabited
 
-abbrev Context := Lean.HashMap String Value
+abbrev Context := Std.HashMap String Value
 
 inductive ErrorType
   | name | type | runTime
@@ -318,7 +318,7 @@ def State.step : State → State
 
   | expr (.lit l) c k => ret (.lit l) c k
   | expr (.list l) c k => ret (.list l) c k
-  | expr (.var n) c k => match c[n] with
+  | expr (.var n) c k => match c[n]? with
     | none   => error .name c $ notFound n
     | some v => ret v c k
   | expr (.lam l) c k => ret (.lam l) c k

tests/lean/run/isDefEqProjIssue.lean

@@ -6,13 +6,13 @@ structure Test where
   x : Nat
 
 -- We need a data structure with functions that are not meant for reduction purposes.
-abbrev Cache := HashMap Nat Test
+abbrev Cache := Std.HashMap Nat Test
 
 def Cache.insert (cache : Cache) (key : Nat) (val : Test) : Cache :=
-  HashMap.insert cache key val
+  Std.HashMap.insert cache key val
 
 def Cache.find? (cache : Cache) (key : Nat) : Option Test :=
-  HashMap.find? cache key
+  cache[key]?
 
 -- This function just contains a call to a function that we definitely do not want to reduce.
 -- To illustrate that the problem is actually noticeable there are multiple implementations provided.