From 27fd35148c867f52babc8b1c9eee12fc626fbc76 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Aug 2021 10:57:57 -0700 Subject: [PATCH] refactor: dependent instances annotations --- src/Std/Data/HashMap.lean | 14 +++++++------- src/Std/Data/HashSet.lean | 12 ++++++------ src/Std/Data/PersistentHashMap.lean | 25 ++++++++++++------------- src/Std/Data/PersistentHashSet.lean | 20 ++++++++++---------- 4 files changed, 35 insertions(+), 36 deletions(-) diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean index d575e9be08..7cf5b079a1 100644 --- a/src/Std/Data/HashMap.lean +++ b/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 diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean index 5710ff4e93..6369abd1c1 100644 --- a/src/Std/Data/HashSet.lean +++ b/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 diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean index 85bbbb98d9..7c6f1dacc8 100644 --- a/src/Std/Data/PersistentHashMap.lean +++ b/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 := diff --git a/src/Std/Data/PersistentHashSet.lean b/src/Std/Data/PersistentHashSet.lean index bdba3cd56f..1d444f3181 100644 --- a/src/Std/Data/PersistentHashSet.lean +++ b/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 () }