max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove [specialize] annotations from fold operations on PersistentHashMap

Browse source 
They have little impact on performance, but increase the generated code size
This commit is contained in:
Leonardo de Moura 2022-08-03 10:37:41 -07:00
parent cbd022e4eb
commit cb6ae247aa
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Std/Data/PersistentHashMap.lean
View file

@ -253,7 +253,7 @@ section
variable {m : Type w → Type w'} [Monad m]
variable {σ : Type w}
@[specialize] partial def foldlMAux (f : σ → α → β → m σ) : Node α β → σ → m σ
partial def foldlMAux (f : σ → α → β → m σ) : Node α β → σ → m σ
| Node.collision keys vals heq, acc =>
let rec traverse (i : Nat) (acc : σ) : m σ := do
if h : i < keys.size then
@ -271,16 +271,16 @@ variable {σ : Type w}
| Entry.ref node => foldlMAux f node acc)
acc
@[specialize] def foldlM {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
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 :=
def forM {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
map.foldlM (fun _ => f) ⟨⟩
@[specialize] def foldl {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
Id.run $ map.foldlM f init
def foldl {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
Id.run <| map.foldlM f init
@[specialize] protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
(map : PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ := do
let intoError : ForInStep σ → Except σ σ
| .done s => .error s