From cb6ae247aaf6fa7da28255f1690b25947c30565e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Aug 2022 10:37:41 -0700 Subject: [PATCH] chore: remove `[specialize]` annotations from `fold` operations on `PersistentHashMap` They have little impact on performance, but increase the generated code size --- src/Std/Data/PersistentHashMap.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean index 6e5b736fcc..b0f8b40236 100644 --- a/src/Std/Data/PersistentHashMap.lean +++ b/src/Std/Data/PersistentHashMap.lean @@ -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