refactor: dependent instances annotations

src/Std/Data/HashMap.lean

@@ -128,12 +128,15 @@ def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (nbuckets := 8)
   ⟨ mkHashMapImp nbuckets, WellFormed.mkWff nbuckets ⟩
 
 namespace HashMap
-variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
-
-instance : Inhabited (HashMap α β) where
+instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
   default := mkHashMap
 
-instance : EmptyCollection (HashMap α β) := ⟨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
@@ -194,9 +197,6 @@ def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
 @[inline] def isEmpty (m : HashMap α β) : Bool :=
   m.size = 0
 
-@[inline] def empty : HashMap α β :=
-  mkHashMap
-
 def toList (m : HashMap α β) : List (α × β) :=
   m.fold (init := []) fun r k v => (k, v)::r
 

src/Std/Data/HashSet.lean

@@ -114,12 +114,15 @@ def mkHashSet {α : Type u} [BEq α] [Hashable α] (nbuckets := 8) : HashSet α
   ⟨ mkHashSetImp nbuckets, WellFormed.mkWff nbuckets ⟩
 
 namespace HashSet
-variable {α : Type u} [BEq α] [Hashable α]
+@[inline] def empty [BEq α] [Hashable α] : HashSet α :=
+  mkHashSet
 
-instance : Inhabited (HashSet α) where
+instance [BEq α] [Hashable α] : Inhabited (HashSet α) where
   default := mkHashSet
 
-instance : EmptyCollection (HashSet α) := ⟨mkHashSet⟩
+instance [BEq α] [Hashable α] : EmptyCollection (HashSet α) := ⟨mkHashSet⟩
+
+variable {α : Type u} {_ : BEq α} {_ : Hashable α}
 
 @[inline] def insert (m : HashSet α) (a : α) : HashSet α :=
   match m with
@@ -152,9 +155,6 @@ instance : EmptyCollection (HashSet α) := ⟨mkHashSet⟩
 @[inline] def isEmpty (m : HashSet α) : Bool :=
   m.size = 0
 
-@[inline] def empty : HashSet α :=
-  mkHashSet
-
 def toList (m : HashSet α) : List α :=
   m.fold (init := []) fun r a => a::r
 

src/Std/Data/PersistentHashMap.lean

@@ -38,7 +38,6 @@ structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] w
 abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β
 
 namespace PersistentHashMap
-variable {α : Type u} {β : Type v}
 
 def empty [BEq α] [Hashable α] : PersistentHashMap α β := {}
 
@@ -125,7 +124,7 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize
         if k == k' then Entry.entry k v
         else Entry.ref $ mkCollisionNode k' v' k v
 
-def insert [BEq α] [Hashable α] : PersistentHashMap α β → α → β → PersistentHashMap α β
+def insert {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → β → PersistentHashMap α β
   | { root := n, size := sz }, k, v => { root := insertAux n (hash k |>.toUSize) 1 k v, size := sz + 1 }
 
 partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option β :=
@@ -144,16 +143,16 @@ partial def findAux [BEq α] : Node α β → USize → α → Option β
     | Entry.entry k' v => if k == k' then some v else none
   | Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k
 
-def find? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option β
+def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option β
   | { root := n, .. }, k => findAux n (hash k |>.toUSize) k
 
-@[inline] def getOp [BEq α] [Hashable α] (self : PersistentHashMap α β) (idx : α) : Option β :=
+@[inline] def getOp {_ : BEq α} {_ : Hashable α} (self : PersistentHashMap α β) (idx : α) : Option β :=
   self.find? idx
 
-@[inline] def findD [BEq α] [Hashable α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
+@[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 
-@[inline] def find! [BEq α] [Hashable α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β :=
+@[inline] def find! {_ : BEq α} {_ : Hashable α} [Inhabited β] (m : PersistentHashMap α β) (a : α) : β :=
   match m.find? a with
   | some b => b
   | none   => panic! "key is not in the map"
@@ -174,7 +173,7 @@ partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α
     | Entry.entry k' v => if k == k' then some (k', v) else none
   | Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k
 
-def findEntry? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option (α × β)
+def findEntry? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option (α × β)
   | { root := n, .. }, k => findEntryAux n (hash k |>.toUSize) k
 
 partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Bool :=
@@ -240,7 +239,7 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
         | none        => (Node.entries (entries.set! j (Entry.ref newNode)), true)
         | some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true)
 
-def erase [BEq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
+def erase {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → PersistentHashMap α β
   | { root := n, size := sz }, k =>
     let h := hash k |>.toUSize
     let (n, del) := eraseAux n h k
@@ -267,17 +266,17 @@ variable {σ : Type w}
     | Entry.ref node  => foldlMAux f node acc)
     acc
 
-@[specialize] def foldlM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
+@[specialize] def foldlM {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
   foldlMAux f map.root init
 
-@[specialize] def forM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
+@[specialize] def forM {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
   map.foldlM (fun _ => f) ⟨⟩
 
-@[specialize] def foldl [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
+@[specialize] def foldl {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
   Id.run $ map.foldlM f init
 end
 
-def toList [BEq α] [Hashable α] (m : PersistentHashMap α β) : List (α × β) :=
+def toList {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : List (α × β) :=
   m.foldl (init := []) fun ps k v => (k, v) :: ps
 
 structure Stats where
@@ -304,7 +303,7 @@ partial def collectStats : Node α β → Stats → Nat → Stats
       | Entry.entry _ _ => stats)
       stats
 
-def stats [BEq α] [Hashable α] (m : PersistentHashMap α β) : Stats :=
+def stats {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : Stats :=
   collectStats m.root {} 1
 
 def Stats.toString (s : Stats) : String :=

src/Std/Data/PersistentHashSet.lean

@@ -15,20 +15,20 @@ abbrev PHashSet (α : Type u) [BEq α] [Hashable α] := PersistentHashSet α
 
 namespace PersistentHashSet
 
-variable {α : Type u} [BEq α] [Hashable α]
+@[inline] def empty [BEq α] [Hashable α] : PersistentHashSet α :=
+  { set := PersistentHashMap.empty }
+
+instance [BEq α] [Hashable α] : Inhabited (PersistentHashSet α) where
+  default := empty
+
+instance [BEq α] [Hashable α] : EmptyCollection (PersistentHashSet α) :=
+  ⟨empty⟩
+
+variable {_ : BEq α} {_ : Hashable α}
 
 @[inline] def isEmpty (s : PersistentHashSet α) : Bool :=
   s.set.isEmpty
 
-@[inline] def empty : PersistentHashSet α :=
-  { set := PersistentHashMap.empty }
-
-instance : Inhabited (PersistentHashSet α) where
-  default := empty
-
-instance : EmptyCollection (PersistentHashSet α) :=
-  ⟨empty⟩
-
 @[inline] def insert (s : PersistentHashSet α) (a : α) : PersistentHashSet α :=
   { set := s.set.insert a () }