From 74ffa1e413f6a58192f997da5b2e38b4d594e2c4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 21 Mar 2025 10:49:55 +1100 Subject: [PATCH] chore: remove the old Lean.Data.HashMap implementation (#7519) This PR removes `Lean.Data.HashMap` and `HashSet`. These have been deprecated for 6 months, replaced by `Std.Data.HashMap` and `HashSet`. --- src/Lean/Compiler/IR/EmitLLVM.lean | 1 - src/Lean/Data.lean | 2 - src/Lean/Data/HashMap.lean | 292 ------------------ src/Lean/Data/HashSet.lean | 225 -------------- src/Lean/Data/NameMap.lean | 1 - src/Lean/Data/SMap.lean | 1 - src/Lean/Environment.lean | 1 - src/Lean/Level.lean | 2 - src/Lean/Meta/Canonicalizer.lean | 1 - .../Meta/Tactic/Grind/Arith/Offset/Types.lean | 1 + src/Lean/Util/Diff.lean | 1 - src/Lean/Util/MonadCache.lean | 1 - src/Lean/Util/PtrSet.lean | 2 - src/Lean/Util/SCC.lean | 1 - src/lake/Lake/Util/OrdHashSet.lean | 1 - tests/bench/liasolver.lean | 74 ++--- tests/lean/1206.lean | 6 +- tests/lean/lcnfTypes.lean | 1 - tests/lean/lcnfTypes.lean.expected.out | 1 - tests/lean/moduleOf.lean | 2 +- tests/lean/moduleOf.lean.expected.out | 2 +- tests/lean/optionGetD.lean | 6 +- tests/lean/run/3731.lean | 6 +- tests/lean/run/998Export.lean | 15 +- tests/lean/run/KyleAlg.lean | 2 +- tests/lean/run/PPTopDownAnalyze.lean | 1 - tests/lean/run/arthur1.lean | 8 +- tests/lean/run/arthur2.lean | 6 +- tests/lean/run/isDefEqProjIssue.lean | 6 +- 29 files changed, 56 insertions(+), 613 deletions(-) delete mode 100644 src/Lean/Data/HashMap.lean delete mode 100644 src/Lean/Data/HashSet.lean diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean index 34d6ff2886..b5f19ae04e 100644 --- a/src/Lean/Compiler/IR/EmitLLVM.lean +++ b/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 diff --git a/src/Lean/Data.lean b/src/Lean/Data.lean index 9f6a17d2d7..9c951729e9 100644 --- a/src/Lean/Data.lean +++ b/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 diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean deleted file mode 100644 index 8a1d55b248..0000000000 --- a/src/Lean/Data/HashMap.lean +++ /dev/null @@ -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 diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean deleted file mode 100644 index e85d3db8d0..0000000000 --- a/src/Lean/Data/HashSet.lean +++ /dev/null @@ -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 diff --git a/src/Lean/Data/NameMap.lean b/src/Lean/Data/NameMap.lean index 2792173c48..eed36180e1 100644 --- a/src/Lean/Data/NameMap.lean +++ b/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 diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean index 54a101731d..6b031a2e12 100644 --- a/src/Lean/Data/SMap.lean +++ b/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' diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 314b3856aa..0a16656fd7 100644 --- a/src/Lean/Environment.lean +++ b/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 diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index 6f3278e641..f4792609c0 100644 --- a/src/Lean/Level.lean +++ b/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 diff --git a/src/Lean/Meta/Canonicalizer.lean b/src/Lean/Meta/Canonicalizer.lean index 05c75189f0..dc7b1c9e72 100644 --- a/src/Lean/Meta/Canonicalizer.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Offset/Types.lean index d751aef5ed..08751f4184 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Types.lean +++ b/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 diff --git a/src/Lean/Util/Diff.lean b/src/Lean/Util/Diff.lean index d9167dbc68..426a8ee8a6 100644 --- a/src/Lean/Util/Diff.lean +++ b/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 diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean index 1b761f43a0..d543310778 100644 --- a/src/Lean/Util/MonadCache.lean +++ b/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 diff --git a/src/Lean/Util/PtrSet.lean b/src/Lean/Util/PtrSet.lean index 1a9e3bff55..52ad8c2220 100644 --- a/src/Lean/Util/PtrSet.lean +++ b/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 diff --git a/src/Lean/Util/SCC.lean b/src/Lean/Util/SCC.lean index fbd213c0fd..c568111f13 100644 --- a/src/Lean/Util/SCC.lean +++ b/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 /-! diff --git a/src/lake/Lake/Util/OrdHashSet.lean b/src/lake/Lake/Util/OrdHashSet.lean index 5312b48f7f..a8913c0021 100644 --- a/src/lake/Lake/Util/OrdHashSet.lean +++ b/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 diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean index 00edf8ee8e..0fc8023695 100644 --- a/tests/bench/liasolver.lean +++ b/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" diff --git a/tests/lean/1206.lean b/tests/lean/1206.lean index 9b617bdb9b..714a1b0beb 100644 --- a/tests/lean/1206.lean +++ b/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) diff --git a/tests/lean/lcnfTypes.lean b/tests/lean/lcnfTypes.lean index 4477bdafc8..2964957b81 100644 --- a/tests/lean/lcnfTypes.lean +++ b/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 diff --git a/tests/lean/lcnfTypes.lean.expected.out b/tests/lean/lcnfTypes.lean.expected.out index 8ed0fe8d9b..beda381e47 100644 --- a/tests/lean/lcnfTypes.lean.expected.out +++ b/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) diff --git a/tests/lean/moduleOf.lean b/tests/lean/moduleOf.lean index 0ed70033b8..3aba1981e2 100644 --- a/tests/lean/moduleOf.lean +++ b/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' diff --git a/tests/lean/moduleOf.lean.expected.out b/tests/lean/moduleOf.lean.expected.out index 561cf0e8da..b635affac1 100644 --- a/tests/lean/moduleOf.lean.expected.out +++ b/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' diff --git a/tests/lean/optionGetD.lean b/tests/lean/optionGetD.lean index e32e15a15a..a70ffe341e 100644 --- a/tests/lean/optionGetD.lean +++ b/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) diff --git a/tests/lean/run/3731.lean b/tests/lean/run/3731.lean index 650481889b..43093a09d7 100644 --- a/tests/lean/run/3731.lean +++ b/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 diff --git a/tests/lean/run/998Export.lean b/tests/lean/run/998Export.lean index deae77b44d..8b1423ae98 100644 --- a/tests/lean/run/998Export.lean +++ b/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 diff --git a/tests/lean/run/KyleAlg.lean b/tests/lean/run/KyleAlg.lean index 7992c5b69a..6c4f8031d1 100644 --- a/tests/lean/run/KyleAlg.lean +++ b/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) diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index bf41f81590..cd4431b19e 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/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 diff --git a/tests/lean/run/arthur1.lean b/tests/lean/run/arthur1.lean index 2adbb4a258..16e38b0a7a 100644 --- a/tests/lean/run/arthur1.lean +++ b/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 diff --git a/tests/lean/run/arthur2.lean b/tests/lean/run/arthur2.lean index 2f30c54c37..b79e0a8c8c 100644 --- a/tests/lean/run/arthur2.lean +++ b/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 diff --git a/tests/lean/run/isDefEqProjIssue.lean b/tests/lean/run/isDefEqProjIssue.lean index 12f9b462ca..6c2347f1f0 100644 --- a/tests/lean/run/isDefEqProjIssue.lean +++ b/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.