From effccf9a6d33be41afa11804148c07d0340b2da2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 15 Oct 2018 13:46:46 -0700
Subject: [PATCH] chore(library/init): mark a few combinators with
 `[specialize]`

---
 library/init/control/combinators.lean | 10 ++++++++++
 library/init/data/list/basic.lean     | 12 ++++++------
 2 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean
index 14d8b53380..d705ec8729 100644
--- a/library/init/control/combinators.lean
+++ b/library/init/control/combinators.lean
@@ -9,47 +9,57 @@ prelude
 import init.control.monad init.control.alternative init.data.list.basic init.coe
 universes u v w
 
+@[specialize]
 def nat.mrepeat {m} [monad m] (n : nat) (f : nat → m unit) : m unit :=
 n.repeat (λ i a, a *> f i) (pure ())
 
+@[specialize]
 def list.mmap {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m (list β)
 | []       := pure []
 | (h :: t) := do h' ← f h, t' ← list.mmap t, pure (h' :: t')
 
+@[specialize]
 def list.mmap' {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m punit
 | []       := pure ⟨⟩
 | (h :: t) := f h *> list.mmap' t
 
+@[specialize]
 def list.mfor {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m punit :=
 list.mmap' f
 
 def mjoin {m : Type u → Type u} [monad m] {α : Type u} (a : m (m α)) : m α :=
 bind a id
 
+@[specialize]
 def list.mfilter {m : Type → Type v} [monad m] {α : Type} (f : α → m bool) : list α → m (list α)
 | []       := pure []
 | (h :: t) := do b ← f h, t' ← list.mfilter t, cond b (pure (h :: t')) (pure t')
 
+@[specialize]
 def list.mfoldl {m : Type u → Type v} [monad m] {s : Type u} {α : Type w} : (s → α → m s) → s → list α → m s
 | f s [] := pure s
 | f s (h :: r) := do
   s' ← f s h,
   list.mfoldl f s' r
 
+@[specialize]
 def list.mfoldr {m : Type u → Type v} [monad m] {s : Type u} {α : Type w} : (α → s → m s) → s → list α → m s
 | f s [] := pure s
 | f s (h :: r) := do
   s' ← list.mfoldr f s r,
   f h s'
 
+@[specialize]
 def list.mfirst {m : Type u → Type v} [monad m] [alternative m] {α : Type w} {β : Type u} (f : α → m β) : list α → m β
 | []      := failure
 | (a::as) := f a <|> list.mfirst as
 
+@[specialize]
 def list.mexists {m : Type → Type u} [monad m] {α : Type v} (f : α → m bool) : list α → m bool
 | []      := pure ff
 | (a::as) := do b ← f a, if b then pure tt else list.mexists as
 
+@[specialize]
 def list.mforall {m : Type → Type u} [monad m] {α : Type v} (f : α → m bool) : list α → m bool
 | []      := pure tt
 | (a::as) := do b ← f a, if b then list.mforall as else pure ff
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index d323dbbb91..6cd66e5768 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -113,11 +113,11 @@ def reverse_core : list α → list α → list α
 def reverse : list α → list α :=
 λ l, reverse_core l []
 
-def map (f : α → β) : list α → list β
+@[specialize] def map (f : α → β) : list α → list β
 | []       := []
 | (a :: l) := f a :: map l
 
-def map₂ (f : α → β → γ) : list α → list β → list γ
+@[specialize] def map₂ (f : α → β → γ) : list α → list β → list γ
 | []      _       := []
 | _       []      := []
 | (x::xs) (y::ys) := f x y :: map₂ xs ys
@@ -183,18 +183,18 @@ def take : ℕ → list α → list α
 | (succ n) []       := []
 | (succ n) (x :: r) := x :: take n r
 
-def foldl (f : α → β → α) : α → list β → α
+@[specialize] def foldl (f : α → β → α) : α → list β → α
 | a []       := a
 | a (b :: l) := foldl (f a b) l
 
-def foldr (f : α → β → β) (b : β) : list α → β
+@[specialize] def foldr (f : α → β → β) (b : β) : list α → β
 | []       := b
 | (a :: l) := f a (foldr l)
 
-def any (l : list α) (p : α → bool) : bool :=
+@[inline] def any (l : list α) (p : α → bool) : bool :=
 foldr (λ a r, p a || r) ff l
 
-def all (l : list α) (p : α → bool) : bool :=
+@[inline] def all (l : list α) (p : α → bool) : bool :=
 foldr (λ a r, p a && r) tt l
 
 def bor  (l : list bool) : bool := any l id