From 77d3a788e836561a01aed94de00b22feab5bd6ca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 27 Apr 2018 08:33:08 -0700
Subject: [PATCH] refactor(init): `init/category` ==> `init.control`

---
 library/init/category/default.lean                  | 10 ----------
 library/init/{category => control}/alternative.lean |  2 +-
 library/init/{category => control}/applicative.lean |  2 +-
 library/init/{category => control}/combinators.lean |  2 +-
 library/init/control/default.lean                   | 10 ++++++++++
 library/init/{category => control}/except.lean      |  2 +-
 library/init/{category => control}/functor.lean     |  0
 library/init/{category => control}/id.lean          |  2 +-
 library/init/{category => control}/lawful.lean      |  4 ++--
 library/init/{category => control}/lift.lean        |  4 ++--
 library/init/{category => control}/monad.lean       |  2 +-
 library/init/{category => control}/monad_fail.lean  |  2 +-
 library/init/{category => control}/option.lean      |  2 +-
 library/init/{category => control}/reader.lean      |  2 +-
 library/init/{category => control}/state.lean       |  4 ++--
 library/init/data/list/instances.lean               |  2 +-
 library/init/data/option/basic.lean                 |  2 +-
 library/init/data/option/instances.lean             |  2 +-
 library/init/data/set.lean                          |  2 +-
 library/init/default.lean                           |  4 ++--
 library/init/lean/ir/ir.lean                        |  2 +-
 library/init/lean/parser/parser.lean                |  2 +-
 library/init/meta/exceptional.lean                  |  2 +-
 library/init/meta/expr.lean                         |  2 +-
 library/init/meta/interaction_monad.lean            |  2 +-
 library/init/meta/interactive.lean                  |  2 +-
 library/init/meta/rb_map.lean                       |  2 +-
 library/init/meta/tactic.lean                       |  2 +-
 28 files changed, 39 insertions(+), 39 deletions(-)
 delete mode 100644 library/init/category/default.lean
 rename library/init/{category => control}/alternative.lean (96%)
 rename library/init/{category => control}/applicative.lean (97%)
 rename library/init/{category => control}/combinators.lean (97%)
 create mode 100644 library/init/control/default.lean
 rename library/init/{category => control}/except.lean (99%)
 rename library/init/{category => control}/functor.lean (100%)
 rename library/init/{category => control}/id.lean (94%)
 rename library/init/{category => control}/lawful.lean (98%)
 rename library/init/{category => control}/lift.lean (97%)
 rename library/init/{category => control}/monad.lean (96%)
 rename library/init/{category => control}/monad_fail.lean (91%)
 rename library/init/{category => control}/option.lean (96%)
 rename library/init/{category => control}/reader.lean (98%)
 rename library/init/{category => control}/state.lean (98%)

diff --git a/library/init/category/default.lean b/library/init/category/default.lean
deleted file mode 100644
index 3c87180843..0000000000
--- a/library/init/category/default.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.category.applicative init.category.functor init.category.alternative
-import init.category.monad init.category.lift init.category.lawful
-import init.category.state init.category.id init.category.except init.category.reader
-import init.category.option
diff --git a/library/init/category/alternative.lean b/library/init/control/alternative.lean
similarity index 96%
rename from library/init/category/alternative.lean
rename to library/init/control/alternative.lean
index b949938fab..991f21ae3b 100644
--- a/library/init/category/alternative.lean
+++ b/library/init/control/alternative.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.logic init.category.applicative
+import init.logic init.control.applicative
 universes u v
 
 class has_orelse (f : Type u → Type v) : Type (max (u+1) v) :=
diff --git a/library/init/category/applicative.lean b/library/init/control/applicative.lean
similarity index 97%
rename from library/init/category/applicative.lean
rename to library/init/control/applicative.lean
index 472ee7a23b..12ebd495e2 100644
--- a/library/init/category/applicative.lean
+++ b/library/init/control/applicative.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import init.category.functor
+import init.control.functor
 open function
 universes u v
 
diff --git a/library/init/category/combinators.lean b/library/init/control/combinators.lean
similarity index 97%
rename from library/init/category/combinators.lean
rename to library/init/control/combinators.lean
index dfaca4584e..4da1b19ae1 100644
--- a/library/init/category/combinators.lean
+++ b/library/init/control/combinators.lean
@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 Monad combinators, as in Haskell's Control.Monad.
 -/
 prelude
-import init.category.monad init.category.alternative init.data.list.basic
+import init.control.monad init.control.alternative init.data.list.basic
 universes u v w
 
 def list.mmap {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m (list β)
diff --git a/library/init/control/default.lean b/library/init/control/default.lean
new file mode 100644
index 0000000000..cde32ca680
--- /dev/null
+++ b/library/init/control/default.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.control.applicative init.control.functor init.control.alternative
+import init.control.monad init.control.lift init.control.lawful
+import init.control.state init.control.id init.control.except init.control.reader
+import init.control.option
diff --git a/library/init/category/except.lean b/library/init/control/except.lean
similarity index 99%
rename from library/init/category/except.lean
rename to library/init/control/except.lean
index a3788dd83b..21adb410eb 100644
--- a/library/init/category/except.lean
+++ b/library/init/control/except.lean
@@ -7,7 +7,7 @@ The except monad transformer.
 -/
 
 prelude
-import init.category.alternative init.category.lift
+import init.control.alternative init.control.lift
 universes u v w
 
 inductive except (ε : Type u) (α : Type v)
diff --git a/library/init/category/functor.lean b/library/init/control/functor.lean
similarity index 100%
rename from library/init/category/functor.lean
rename to library/init/control/functor.lean
diff --git a/library/init/category/id.lean b/library/init/control/id.lean
similarity index 94%
rename from library/init/category/id.lean
rename to library/init/control/id.lean
index a85afc6894..33787f7110 100644
--- a/library/init/category/id.lean
+++ b/library/init/control/id.lean
@@ -6,7 +6,7 @@ Authors: Sebastian Ullrich
 The identity monad.
 -/
 prelude
-import init.category.lift
+import init.control.lift
 universe u
 
 @[inline] def id_bind {α β : Type u} (x : α) (f : α → id β) : id β := f x
diff --git a/library/init/category/lawful.lean b/library/init/control/lawful.lean
similarity index 98%
rename from library/init/category/lawful.lean
rename to library/init/control/lawful.lean
index 61e75201f4..aa456246bb 100644
--- a/library/init/category/lawful.lean
+++ b/library/init/control/lawful.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
 prelude
-import init.category.monad init.meta.interactive
-import init.category.state init.category.except init.category.reader init.category.option
+import init.control.monad init.meta.interactive
+import init.control.state init.control.except init.control.reader init.control.option
 universes u v
 
 open function
diff --git a/library/init/category/lift.lean b/library/init/control/lift.lean
similarity index 97%
rename from library/init/category/lift.lean
rename to library/init/control/lift.lean
index f9a16c99d7..bc9d17baac 100644
--- a/library/init/category/lift.lean
+++ b/library/init/control/lift.lean
@@ -10,7 +10,7 @@ Please see https://hackage.haskell.org/package/layers-0.1/docs/Documentation-Lay
 -/
 prelude
 import init.function init.coe
-import init.category.monad
+import init.control.monad
 
 universes u v w
 
@@ -43,7 +43,7 @@ instance has_monad_lift_t_refl (m) : has_monad_lift_t m m :=
 @[simp] lemma monad_lift_refl {m : Type u → Type v} {α} : (monad_lift : m α → m α) = id := rfl
 
 
-/-- A functor in the category of monads. Can be used to lift monad-transforming functions.
+/-- A functor in the control of monads. Can be used to lift monad-transforming functions.
     Based on pipes' [MFunctor](https://hackage.haskell.org/package/pipes-2.4.0/docs/Control-MFunctor.html),
     but not restricted to monad transformers.
     Alternatively, an implementation of [MonadTransFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadTransFunctor). -/
diff --git a/library/init/category/monad.lean b/library/init/control/monad.lean
similarity index 96%
rename from library/init/category/monad.lean
rename to library/init/control/monad.lean
index 59329a71a9..ced07732bc 100644
--- a/library/init/category/monad.lean
+++ b/library/init/control/monad.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Luke Nelson, Jared Roesch, Sebastian Ullrich
 -/
 prelude
-import init.category.applicative
+import init.control.applicative
 universes u v
 
 open function
diff --git a/library/init/category/monad_fail.lean b/library/init/control/monad_fail.lean
similarity index 91%
rename from library/init/category/monad_fail.lean
rename to library/init/control/monad_fail.lean
index 7088d34395..466a690ebc 100644
--- a/library/init/category/monad_fail.lean
+++ b/library/init/control/monad_fail.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.category.lift init.data.string.basic
+import init.control.lift init.data.string.basic
 
 universes u v
 
diff --git a/library/init/category/option.lean b/library/init/control/option.lean
similarity index 96%
rename from library/init/category/option.lean
rename to library/init/control/option.lean
index e022dd476d..00059ce991 100644
--- a/library/init/category/option.lean
+++ b/library/init/control/option.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import init.category.alternative init.category.lift init.category.except
+import init.control.alternative init.control.lift init.control.except
 
 universes u v
 
diff --git a/library/init/category/reader.lean b/library/init/control/reader.lean
similarity index 98%
rename from library/init/category/reader.lean
rename to library/init/control/reader.lean
index b13b12910c..3a86086962 100644
--- a/library/init/category/reader.lean
+++ b/library/init/control/reader.lean
@@ -7,7 +7,7 @@ The reader monad transformer for passing immutable state.
 -/
 
 prelude
-import init.category.lift init.category.id init.category.alternative init.category.except
+import init.control.lift init.control.id init.control.alternative init.control.except
 universes u v w
 
 /-- An implementation of [ReaderT](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Reader.html#t:ReaderT) -/
diff --git a/library/init/category/state.lean b/library/init/control/state.lean
similarity index 98%
rename from library/init/category/state.lean
rename to library/init/control/state.lean
index 7a41681661..6d6e2ca2b6 100644
--- a/library/init/category/state.lean
+++ b/library/init/control/state.lean
@@ -6,8 +6,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 The state monad transformer.
 -/
 prelude
-import init.category.alternative init.category.lift
-import init.category.id init.category.except
+import init.control.alternative init.control.lift
+import init.control.id init.control.except
 universes u v w
 
 structure state_t (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean
index dfff729dab..9d0fcb4777 100644
--- a/library/init/data/list/instances.lean
+++ b/library/init/data/list/instances.lean
@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.data.list.basic
-import init.category.lawful
+import init.control.lawful
 open list
 
 universes u v
diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean
index cfd9075157..cb1ec8a04e 100644
--- a/library/init/data/option/basic.lean
+++ b/library/init/data/option/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.logic init.category.monad init.category.alternative
+import init.logic init.control.monad init.control.alternative
 open decidable
 
 universes u v
diff --git a/library/init/data/option/instances.lean b/library/init/data/option/instances.lean
index 35f6aa7a51..fd5234b896 100644
--- a/library/init/data/option/instances.lean
+++ b/library/init/data/option/instances.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.data.option.basic
 import init.meta.tactic
-import init.category.lawful
+import init.control.lawful
 
 universes u v
 
diff --git a/library/init/data/set.lean b/library/init/data/set.lean
index af3a7d5dc3..5a46b625ff 100644
--- a/library/init/data/set.lean
+++ b/library/init/data/set.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta.interactive
-import init.category.lawful
+import init.control.lawful
 
 universes u v
 def set (α : Type u) := α → Prop
diff --git a/library/init/default.lean b/library/init/default.lean
index 13d326eb78..3b39c487af 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.core init.logic init.category init.data.basic init.version
-import init.propext init.funext init.category.combinators init.function init.classical
+import init.core init.logic init.control init.data.basic init.version
+import init.propext init.funext init.function init.classical
 import init.util init.coe init.wf init.meta init.meta.well_founded_tactics init.data
 
 @[user_attribute]
diff --git a/library/init/lean/ir/ir.lean b/library/init/lean/ir/ir.lean
index a9875804a9..169da93103 100644
--- a/library/init/lean/ir/ir.lean
+++ b/library/init/lean/ir/ir.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.rbmap init.data.int init.category.state init.category.except init.category.combinators
+import init.data.rbmap init.data.int init.control.state init.control.except init.control.combinators
 
 /-
 Missing
diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 90a6dd34c6..592b7702df 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -8,7 +8,7 @@ paper:
 https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/parsec-paper-letter.pdf
 -/
 prelude
-import init.data.to_string init.data.string.basic init.data.list.basic init.category.except
+import init.data.to_string init.data.string.basic init.data.list.basic init.control.except
 namespace lean
 namespace parser
 
diff --git a/library/init/meta/exceptional.lean b/library/init/meta/exceptional.lean
index 6cd1719bf7..039f46933e 100644
--- a/library/init/meta/exceptional.lean
+++ b/library/init/meta/exceptional.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.category.monad init.meta.format init.util
+import init.control.monad init.meta.format init.util
 /-
 Remark: we use a function that produces a format object as the exception information.
 Motivation: the formatting object may be big, and we may create it on demand.
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index d38dd75fb7..b70714e2a4 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.level init.category.monad init.meta.rb_map
+import init.meta.level init.control.monad init.meta.rb_map
 universes u v
 open native
 structure pos :=
diff --git a/library/init/meta/interaction_monad.lean b/library/init/meta/interaction_monad.lean
index 724b4f4963..13bdac5311 100644
--- a/library/init/meta/interaction_monad.lean
+++ b/library/init/meta/interaction_monad.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import init.function init.data.option.basic init.util
-import init.category.combinators init.category.monad init.category.alternative init.category.monad_fail
+import init.control.combinators init.control.monad init.control.alternative init.control.monad_fail
 import init.data.nat.div init.meta.exceptional init.meta.format init.meta.environment
 import init.meta.pexpr init.data.repr init.data.string.basic init.data.to_string
 
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index d6fb7bf493..62f2a59ee3 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic
-import init.category.combinators
+import init.control.combinators
 import init.meta.interactive_base init.meta.derive init.meta.match_tactic
 import init.meta.congr_tactic
 
diff --git a/library/init/meta/rb_map.lean b/library/init/meta/rb_map.lean
index fef707583d..c69e4ee46e 100644
--- a/library/init/meta/rb_map.lean
+++ b/library/init/meta/rb_map.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
 prelude
-import init.data.ordering.basic init.function init.meta.name init.meta.format init.category.monad
+import init.data.ordering.basic init.function init.meta.name init.meta.format init.control.monad
 
 open format
 
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 48b0819050..08b3b08386 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.function init.data.option.basic init.util
-import init.category.combinators init.category.monad init.category.alternative init.category.monad_fail
+import init.control.combinators init.control.monad init.control.alternative init.control.monad_fail
 import init.data.nat.div init.meta.exceptional init.meta.format init.meta.environment
 import init.meta.pexpr init.data.repr init.data.string.basic init.meta.interaction_monad