From df8bbf543808645d7eccff417ce6a5cc45d4cc72 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Oct 2019 18:58:40 -0700
Subject: [PATCH] chore: remove Init.Control.Combinators

Reason: it contains a bunch of little functions that are supposed to
be defined in other modules.
---
 library/Init/Control/Applicative.lean         |   8 ++
 library/Init/Control/Combinators.lean         | 133 ------------------
 library/Init/Control/Default.lean             |   1 -
 library/Init/Control/Monad.lean               |  11 ++
 library/Init/Data/List/Control.lean           | 121 ++++++++++++++++
 library/Init/Data/List/Default.lean           |   1 +
 library/Init/Data/Nat/Control.lean            |  42 ++++++
 library/Init/Data/Nat/Default.lean            |   1 +
 library/Init/Lean/AbstractMetavarContext.lean |   1 +
 library/Init/Lean/Compiler/IR/Borrow.lean     |   1 +
 library/Init/Lean/Compiler/IR/Boxing.lean     |   3 +-
 .../Lean/Compiler/IR/ElimDeadBranches.lean    |   1 +
 .../Lean/Compiler/IR/ExpandResetReuse.lean    |   1 +
 library/Init/Lean/Options.lean                |   3 +-
 library/Init/Lean/Path.lean                   |   2 +-
 library/Init/Lean/TypeClass/Context.lean      |   1 +
 16 files changed, 193 insertions(+), 138 deletions(-)
 delete mode 100644 library/Init/Control/Combinators.lean
 create mode 100644 library/Init/Data/List/Control.lean
 create mode 100644 library/Init/Data/Nat/Control.lean

diff --git a/library/Init/Control/Applicative.lean b/library/Init/Control/Applicative.lean
index 5bde41de2c..2de9cd3cdf 100644
--- a/library/Init/Control/Applicative.lean
+++ b/library/Init/Control/Applicative.lean
@@ -32,3 +32,11 @@ class Applicative (f : Type u → Type v) extends Functor f, HasPure f, HasSeq f
 (map      := fun _ _ x y => pure x <*> y)
 (seqLeft  := fun α β a b => const β <$> a <*> b)
 (seqRight := fun α β a b => const α id <$> a <*> b)
+
+@[macroInline]
+def when {m : Type → Type u} [Applicative m] (c : Prop) [h : Decidable c] (t : m Unit) : m Unit :=
+if c then t else pure ()
+
+@[macroInline]
+def unless {m : Type → Type u} [Applicative m] (c : Prop) [h : Decidable c] (e : m Unit) : m Unit :=
+if c then pure () else e
diff --git a/library/Init/Control/Combinators.lean b/library/Init/Control/Combinators.lean
deleted file mode 100644
index c861c3247e..0000000000
--- a/library/Init/Control/Combinators.lean
+++ /dev/null
@@ -1,133 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Avigad, Leonardo de Moura
-
-Monad Combinators, as in Haskell's Control.Monad.
--/
-prelude
-import Init.Control.Monad
-import Init.Control.Alternative
-import Init.Data.List.Basic
-
-universes u v w u₁ u₂ u₃
-
-def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α :=
-bind a id
-
-@[macroInline]
-def when {m : Type → Type u} [Applicative m] (c : Prop) [h : Decidable c] (t : m Unit) : m Unit :=
-if c then t else pure ()
-
-@[macroInline]
-def unless {m : Type → Type u} [Applicative m] (c : Prop) [h : Decidable c] (e : m Unit) : m Unit :=
-if c then pure () else e
-
-@[macroInline]
-def condM {m : Type → Type u} [Monad m] {α : Type} (mbool : m Bool) (tm fm : m α) : m α :=
-do b ← mbool; cond b tm fm
-
-@[macroInline]
-def whenM {m : Type → Type u} [Monad m] (c : m Bool) (t : m Unit) : m Unit :=
-condM c t (pure ())
-
-namespace Nat
-
-@[specialize] def forMAux {m} [Applicative m] (f : Nat → m Unit) (n : Nat) : Nat → m Unit
-| 0   => pure ()
-| i+1 => f (n-i-1) *> forMAux i
-
-@[inline] def forM {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit :=
-forMAux f n n
-
-@[specialize] def forRevMAux {m} [Applicative m] (f : Nat → m Unit) : Nat → m Unit
-| 0   => pure ()
-| i+1 => f i *> forRevMAux i
-
-@[inline] def forRevM {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit :=
-forRevMAux f n
-
-@[specialize] def foldMAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (n : Nat) : Nat → α → m α
-| 0,   a => pure a
-| i+1, a => f (n-i-1) a >>= foldMAux i
-
-@[inline] def foldM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
-foldMAux f n n a
-
-@[specialize] def foldRevMAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) : Nat → α → m α
-| 0,   a => pure a
-| i+1, a => f i a >>= foldRevMAux i
-
-@[inline] def mfoldRev {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
-foldRevMAux f n a
-
--- TODO: enable after we have support for marking arguments that should be considered for specialization.
-/-
-@[specialize]
-def mrepeat {m} [Monad m] : Nat → m Unit → m Unit
-| 0     f := pure ()
-| (k+1) f := f *> mrepeat k f
--/
-end Nat
-
-namespace List
-
-@[specialize]
-def mapM {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
-| []    => pure []
-| a::as => List.cons <$> (f a) <*> mapM as
-
-@[specialize]
-def mapM₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m (List γ)
-| a::as, b::bs => List.cons <$> (f a b) <*> mapM₂ as bs
-| _,     _     => pure []
-
-@[specialize]
-def forM {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
-| []     => pure ⟨⟩
-| h :: t => f h *> forM t
-
-@[specialize]
-def forM₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m PUnit
-| a::as, b::bs => f a b *> forM₂ as bs
-| _,     _     => pure ⟨⟩
-
-@[specialize]
-def filterM {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : List α → m (List α)
-| []     => pure []
-| h :: t => do b ← f h; t' ← filterM t; cond b (pure (h :: t')) (pure t')
-
-@[specialize]
-def foldlM {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;
-  foldlM f s' r
-
-@[specialize]
-def foldrM {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' ← foldrM f s r;
-  f h s'
-
-@[specialize]
-def firstM {m : Type u → Type v} [Monad m] [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β
-| []    => failure
-| a::as => f a <|> firstM as
-
-@[specialize]
-def anyM {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
-| []    => pure false
-| a::as => do b ← f a; match b with
-  | true  => pure true
-  | false =>  anyM as
-
-@[specialize]
-def allM {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
-| []    => pure true
-| a::as => do b ← f a; match b with
-  | true  => allM as
-  | false => pure false
-
-end List
diff --git a/library/Init/Control/Default.lean b/library/Init/Control/Default.lean
index c384a7061f..4e5551ee91 100644
--- a/library/Init/Control/Default.lean
+++ b/library/Init/Control/Default.lean
@@ -14,5 +14,4 @@ import Init.Control.Id
 import Init.Control.Except
 import Init.Control.Reader
 import Init.Control.Option
-import Init.Control.Combinators
 import Init.Control.Conditional
diff --git a/library/Init/Control/Monad.lean b/library/Init/Control/Monad.lean
index 01a1930068..8878ff9d0f 100644
--- a/library/Init/Control/Monad.lean
+++ b/library/Init/Control/Monad.lean
@@ -32,3 +32,14 @@ instance monadInhabited' {α : Type u} {m : Type u → Type v} [Monad m] : Inhab
 
 instance monadInhabited {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) :=
 ⟨pure $ default _⟩
+
+def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α :=
+bind a id
+
+@[macroInline]
+def condM {m : Type → Type u} [Monad m] {α : Type} (mbool : m Bool) (tm fm : m α) : m α :=
+do b ← mbool; cond b tm fm
+
+@[macroInline]
+def whenM {m : Type → Type u} [Monad m] (c : m Bool) (t : m Unit) : m Unit :=
+condM c t (pure ())
diff --git a/library/Init/Data/List/Control.lean b/library/Init/Data/List/Control.lean
new file mode 100644
index 0000000000..920d7f257c
--- /dev/null
+++ b/library/Init/Data/List/Control.lean
@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import Init.Control.Monad
+import Init.Control.Alternative
+
+namespace List
+universes u v w u₁ u₂
+
+/-
+Remark: we can define `mapM`, `mapM₂` and `forM` using `Applicative` instead of `Monad`.
+Example:
+```
+def mapM {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
+| []    => pure []
+| a::as => List.cons <$> (f a) <*> mapM as
+```
+
+However, we consider `f <$> a <*> b` an anti-idiom because the generated code
+may produce unnecessary closure allocations.
+Suppose `m` is a `Monad`, and it uses the default implementation for `Applicative.seq`.
+Then, the compiler expands `f <$> a <*> b <*> c` into something equivalent to
+```
+(Functor.map f a >>= fun g_1 => Functor.map g_1 b) >>= fun g_2 => Functor.map g_2 c
+```
+In an ideal world, the compiler may eliminate the temporary closures `g_1` and `g_2` after it inlines
+`Functor.map` and `Monad.bind`. However, this can easily fail. For example, suppose
+`Functor.map f a >>= fun g_1 => Functor.map g_1 b` expanded into a match-expression.
+This is not unreasonable and can happen in many different ways, e.g., we are using a monad that
+may throw exceptions. Then, the compiler has to decide whether it will create a join-point for
+the continuation of the match or float it. If the compiler decides to float, then it will
+be able to eliminate the closures, but it may not be feasible since floating match expressions
+may produce exponential blowup in the code size.
+
+Finally, we rarely use `mapM` with something that is not a `Monad`.
+
+Users that want to use `mapM` with `Applicative` should use `mapA` instead.
+-/
+
+@[specialize]
+def mapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
+| []    => pure []
+| a::as => do b ← f a; bs ← mapM as; pure (b :: bs)
+
+@[specialize]
+def mapM₂ {m : Type u → Type v} [Monad m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m (List γ)
+| a::as, b::bs => do c ← f a b; cs ← mapM₂ as bs; pure (c :: cs)
+| _,     _     => pure []
+
+@[specialize]
+def mapA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
+| []    => pure []
+| a::as => List.cons <$> f a <*> mapA as
+
+@[specialize]
+def mapA₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m (List γ)
+| a::as, b::bs => List.cons <$> f a b <*> mapA₂ as bs
+| _,     _     => pure []
+
+@[specialize]
+def forM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
+| []     => pure ⟨⟩
+| h :: t => do f h; forM t
+
+@[specialize]
+def forM₂ {m : Type u → Type v} [Monad m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m PUnit
+| a::as, b::bs => do f a b; forM₂ as bs
+| _,     _     => pure ⟨⟩
+
+@[specialize]
+def forA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
+| []     => pure ⟨⟩
+| h :: t => f h *> forA t
+
+@[specialize]
+def forA₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m PUnit
+| a::as, b::bs => f a b *> forA₂ as bs
+| _,     _     => pure ⟨⟩
+
+@[specialize]
+def filterM {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : List α → m (List α)
+| []     => pure []
+| h :: t => do b ← f h; t' ← filterM t; cond b (pure (h :: t')) (pure t')
+
+@[specialize]
+def foldlM {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;
+  foldlM f s' r
+
+@[specialize]
+def foldrM {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' ← foldrM f s r;
+  f h s'
+
+@[specialize]
+def firstM {m : Type u → Type v} [Monad m] [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β
+| []    => failure
+| a::as => f a <|> firstM as
+
+@[specialize]
+def anyM {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
+| []    => pure false
+| a::as => do b ← f a; match b with
+  | true  => pure true
+  | false =>  anyM as
+
+@[specialize]
+def allM {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
+| []    => pure true
+| a::as => do b ← f a; match b with
+  | true  => allM as
+  | false => pure false
+
+end List
diff --git a/library/Init/Data/List/Default.lean b/library/Init/Data/List/Default.lean
index 7c3e818ba1..9af534e509 100644
--- a/library/Init/Data/List/Default.lean
+++ b/library/Init/Data/List/Default.lean
@@ -7,3 +7,4 @@ prelude
 import Init.Data.List.Basic
 import Init.Data.List.BasicAux
 import Init.Data.List.Instances
+import Init.Data.List.Control
diff --git a/library/Init/Data/Nat/Control.lean b/library/Init/Data/Nat/Control.lean
new file mode 100644
index 0000000000..334d285715
--- /dev/null
+++ b/library/Init/Data/Nat/Control.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import Init.Control.Monad
+import Init.Control.Alternative
+import Init.Data.Nat.Basic
+
+namespace Nat
+universes u v
+
+@[specialize] def forMAux {m} [Applicative m] (f : Nat → m Unit) (n : Nat) : Nat → m Unit
+| 0   => pure ()
+| i+1 => f (n-i-1) *> forMAux i
+
+@[inline] def forM {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit :=
+forMAux f n n
+
+@[specialize] def forRevMAux {m} [Applicative m] (f : Nat → m Unit) : Nat → m Unit
+| 0   => pure ()
+| i+1 => f i *> forRevMAux i
+
+@[inline] def forRevM {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit :=
+forRevMAux f n
+
+@[specialize] def foldMAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (n : Nat) : Nat → α → m α
+| 0,   a => pure a
+| i+1, a => f (n-i-1) a >>= foldMAux i
+
+@[inline] def foldM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
+foldMAux f n n a
+
+@[specialize] def foldRevMAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) : Nat → α → m α
+| 0,   a => pure a
+| i+1, a => f i a >>= foldRevMAux i
+
+@[inline] def mfoldRev {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
+foldRevMAux f n a
+
+end Nat
diff --git a/library/Init/Data/Nat/Default.lean b/library/Init/Data/Nat/Default.lean
index 6e5092226b..cf7be93c6e 100644
--- a/library/Init/Data/Nat/Default.lean
+++ b/library/Init/Data/Nat/Default.lean
@@ -7,3 +7,4 @@ prelude
 import Init.Data.Nat.Basic
 import Init.Data.Nat.Div
 import Init.Data.Nat.Bitwise
+import Init.Data.Nat.Control
diff --git a/library/Init/Lean/AbstractMetavarContext.lean b/library/Init/Lean/AbstractMetavarContext.lean
index cc0bc61166..d338a1992a 100644
--- a/library/Init/Lean/AbstractMetavarContext.lean
+++ b/library/Init/Lean/AbstractMetavarContext.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Control.Reader
 import Init.Control.Conditional
 import Init.Data.Option
+import Init.Data.List
 import Init.Lean.LocalContext
 
 /-
diff --git a/library/Init/Lean/Compiler/IR/Borrow.lean b/library/Init/Lean/Compiler/IR/Borrow.lean
index f2cae7c76e..b6c79f6546 100644
--- a/library/Init/Lean/Compiler/IR/Borrow.lean
+++ b/library/Init/Lean/Compiler/IR/Borrow.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Data.Nat
 import Init.Lean.Compiler.ExportAttr
 import Init.Lean.Compiler.IR.CompilerM
 import Init.Lean.Compiler.IR.NormIds
diff --git a/library/Init/Lean/Compiler/IR/Boxing.lean b/library/Init/Lean/Compiler/IR/Boxing.lean
index 252eec94a0..e824ec94f2 100644
--- a/library/Init/Lean/Compiler/IR/Boxing.lean
+++ b/library/Init/Lean/Compiler/IR/Boxing.lean
@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.AssocList
 import Init.Control.EState
 import Init.Control.Reader
+import Init.Data.AssocList
+import Init.Data.Nat
 import Init.Lean.Runtime
 import Init.Lean.Compiler.ClosedTermCache
 import Init.Lean.Compiler.ExternAttr
diff --git a/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean b/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean
index db66a5d6b2..9ebf265428 100644
--- a/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean
+++ b/library/Init/Lean/Compiler/IR/ElimDeadBranches.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Control.Reader
 import Init.Data.Option
+import Init.Data.Nat
 import Init.Lean.Compiler.IR.Format
 import Init.Lean.Compiler.IR.Basic
 import Init.Lean.Compiler.IR.CompilerM
diff --git a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
index ab1d45a4c4..5cd1174f5c 100644
--- a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Control.State
 import Init.Control.Reader
+import Init.Data.Nat
 import Init.Lean.Compiler.IR.CompilerM
 import Init.Lean.Compiler.IR.NormIds
 import Init.Lean.Compiler.IR.FreeVars
diff --git a/library/Init/Lean/Options.lean b/library/Init/Lean/Options.lean
index 762434ced1..8004b3a2ae 100644
--- a/library/Init/Lean/Options.lean
+++ b/library/Init/Lean/Options.lean
@@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich and Leonardo de Moura
 -/
 prelude
-import Init.Lean.KVMap
 import Init.System.IO
-import Init.Control.Combinators
 import Init.Data.ToString
+import Init.Lean.KVMap
 
 namespace Lean
 
diff --git a/library/Init/Lean/Path.lean b/library/Init/Lean/Path.lean
index f76160c72d..b872c601cd 100644
--- a/library/Init/Lean/Path.lean
+++ b/library/Init/Lean/Path.lean
@@ -7,7 +7,7 @@ prelude
 import Init.System.IO
 import Init.System.FilePath
 import Init.Data.Array
-import Init.Control.Combinators
+import Init.Data.List.Control
 import Init.Lean.Name
 
 namespace Lean
diff --git a/library/Init/Lean/TypeClass/Context.lean b/library/Init/Lean/TypeClass/Context.lean
index 140c262690..3660c2010c 100644
--- a/library/Init/Lean/TypeClass/Context.lean
+++ b/library/Init/Lean/TypeClass/Context.lean
@@ -8,6 +8,7 @@ Custom unifier for tabled typeclass resolution.
 Note: this file will be removed once the unifier is implemented in Lean.
 -/
 prelude
+import Init.Data.Nat
 import Init.Data.PersistentArray
 import Init.Lean.Expr
 import Init.Lean.MetavarContext