From 5efa628e43079ceca87d80a179d727fd8e8edfa5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Aug 2020 06:56:15 -0700
Subject: [PATCH] chore: split `Lift.lean` into `MonadLift.lean`,
 `MonadFunctor.lean`, and `MonadRun.lean`

---
 src/Init/Control.lean              |  6 ++-
 src/Init/Control/Except.lean       |  5 +-
 src/Init/Control/Id.lean           |  4 +-
 src/Init/Control/Lift.lean         | 82 ------------------------------
 src/Init/Control/MonadControl.lean |  2 +-
 src/Init/Control/MonadFunctor.lean | 35 +++++++++++++
 src/Init/Control/MonadLift.lean    | 42 +++++++++++++++
 src/Init/Control/MonadRun.lean     | 23 +++++++++
 src/Init/Control/Option.lean       |  2 +-
 9 files changed, 113 insertions(+), 88 deletions(-)
 delete mode 100644 src/Init/Control/Lift.lean
 create mode 100644 src/Init/Control/MonadFunctor.lean
 create mode 100644 src/Init/Control/MonadLift.lean
 create mode 100644 src/Init/Control/MonadRun.lean

diff --git a/src/Init/Control.lean b/src/Init/Control.lean
index 435f2268ae..d2aa8404f8 100644
--- a/src/Init/Control.lean
+++ b/src/Init/Control.lean
@@ -8,7 +8,10 @@ import Init.Control.Applicative
 import Init.Control.Functor
 import Init.Control.Alternative
 import Init.Control.Monad
-import Init.Control.Lift
+import Init.Control.MonadLift
+import Init.Control.MonadFunctor
+import Init.Control.MonadRun
+import Init.Control.MonadControl
 import Init.Control.State
 import Init.Control.StateRef
 import Init.Control.Id
@@ -16,4 +19,3 @@ import Init.Control.Except
 import Init.Control.Reader
 import Init.Control.Option
 import Init.Control.Conditional
-import Init.Control.MonadControl
diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index ebeec00c46..7b40b0e916 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -6,10 +6,13 @@ Authors: Jared Roesch, Sebastian Ullrich
 The Except monad transformer.
 -/
 prelude
+import Init.Data.ToString
 import Init.Control.Alternative
 import Init.Control.MonadControl
 import Init.Control.Id
-import Init.Data.ToString
+import Init.Control.MonadFunctor
+import Init.Control.MonadRun
+
 universes u v w u'
 
 inductive Except (ε : Type u) (α : Type v)
diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean
index d6d3235067..20107fd0bd 100644
--- a/src/Init/Control/Id.lean
+++ b/src/Init/Control/Id.lean
@@ -6,7 +6,9 @@ Authors: Sebastian Ullrich
 The identity Monad.
 -/
 prelude
-import Init.Control.Lift
+import Init.Control.MonadLift
+import Init.Control.MonadRun
+
 universe u
 
 def Id (type : Type u) : Type u := type
diff --git a/src/Init/Control/Lift.lean b/src/Init/Control/Lift.lean
deleted file mode 100644
index bb8cd0aaeb..0000000000
--- a/src/Init/Control/Lift.lean
+++ /dev/null
@@ -1,82 +0,0 @@
-/-
-Copyright (c) 2016 Gabriel Ebner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
-
-Classy functions for lifting monadic actions of different shapes.
-
-This theory is roughly modeled after the Haskell 'layers' package https://hackage.haskell.org/package/layers-0.1.
-Please see https://hackage.haskell.org/package/layers-0.1/docs/Documentation-Layers-Overview.html for an exhaustive discussion of the different approaches to lift functions.
--/
-prelude
-import Init.Control.Monad
-import Init.Coe
-
-universes u v w
-
-/-- A Function for lifting a computation from an inner Monad to an outer Monad.
-    Like [MonadTrans](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Class.html),
-    but `n` does not have to be a monad transformer.
-    Alternatively, an implementation of [MonadLayer](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer) without `layerInvmap` (so far). -/
-class MonadLift (m : Type u → Type v) (n : Type u → Type w) :=
-(monadLift : ∀ {α}, m α → n α)
-
-/-- The reflexive-transitive closure of `MonadLift`.
-    `monadLift` is used to transitively lift monadic computations such as `StateT.get` or `StateT.put s`.
-    Corresponds to [MonadLift](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLift). -/
-class MonadLiftT (m : Type u → Type v) (n : Type u → Type w) :=
-(monadLift : ∀ {α}, m α → n α)
-
-export MonadLiftT (monadLift)
-
-abbrev liftM := @monadLift
-
-@[inline] def liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
-a ← liftM $ x;
-pure $ coe a
-
-instance monadLiftTrans (m n o) [MonadLiftT m n] [MonadLift n o] : MonadLiftT m o :=
-⟨fun α ma => MonadLift.monadLift (monadLift ma : n α)⟩
-
-instance monadLiftRefl (m) : MonadLiftT m m :=
-⟨fun α => id⟩
-
-/-- A functor in the category 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).
-
-
-    Remark: other libraries equate `m` and `m'`, and `n` and `n'`. We need to distinguish them to be able to implement
-    ogadgets such as `MonadStateAdapter` and `MonadReaderAdapter`. -/
-class MonadFunctor (m m' : Type u → Type v) (n n' : Type u → Type w) :=
-(monadMap {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
-
-/-- The reflexive-transitive closure of `MonadFunctor`.
-    `monadMap` is used to transitively lift Monad morphisms such as `StateT.zoom`.
-    A generalization of [MonadLiftFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadLiftFunctor), which can only lift endomorphisms (i.e. m = m', n = n'). -/
-class MonadFunctorT (m m' : Type u → Type v) (n n' : Type u → Type w) :=
-(monadMap {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
-
-export MonadFunctorT (monadMap)
-
-instance monadFunctorTrans (m m' n n' o o') [MonadFunctorT m m' n n'] [MonadFunctor n n' o o'] :
-  MonadFunctorT m m' o o' :=
-⟨fun α f => MonadFunctor.monadMap (fun β => (monadMap @f : n β → n' β))⟩
-
-instance monadFunctorRefl (m m') : MonadFunctorT m m' m m' :=
-⟨fun α f => f⟩
-
-/-- Run a Monad stack to completion.
-    `run` should be the composition of the transformers' individual `run` functions.
-    This class mostly saves some typing when using highly nested Monad stacks:
-    ```
-    @[reducible] def MyMonad := ReaderT myCfg $ StateT myState $ ExceptT myErr id
-    -- def MyMonad.run {α : Type} (x : MyMonad α) (cfg : myCfg) (st : myState) := ((x.run cfg).run st).run
-    def MyMonad.run {α : Type} (x : MyMonad α) := MonadRun.run x
-    ```
-    -/
-class MonadRun (out : outParam $ Type u → Type v) (m : Type u → Type v) :=
-(run {α : Type u} : m α → out α)
-
-export MonadRun (run)
diff --git a/src/Init/Control/MonadControl.lean b/src/Init/Control/MonadControl.lean
index 2d5622481b..493543a502 100644
--- a/src/Init/Control/MonadControl.lean
+++ b/src/Init/Control/MonadControl.lean
@@ -6,7 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura
 See: https://lexi-lambda.github.io/blog/2019/09/07/demystifying-monadbasecontrol/
 -/
 prelude
-import Init.Control.Lift
+import Init.Control.MonadLift
 
 universes u v w
 
diff --git a/src/Init/Control/MonadFunctor.lean b/src/Init/Control/MonadFunctor.lean
new file mode 100644
index 0000000000..46cdac6266
--- /dev/null
+++ b/src/Init/Control/MonadFunctor.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich, Leonardo de Moura
+-/
+prelude
+import Init.Control.MonadLift
+
+universes u v w
+
+/-- A functor in the category 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).
+
+
+    Remark: other libraries equate `m` and `m'`, and `n` and `n'`. We need to distinguish them to be able to implement
+    ogadgets such as `MonadStateAdapter` and `MonadReaderAdapter`. -/
+class MonadFunctor (m m' : Type u → Type v) (n n' : Type u → Type w) :=
+(monadMap {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
+
+/-- The reflexive-transitive closure of `MonadFunctor`.
+    `monadMap` is used to transitively lift Monad morphisms such as `StateT.zoom`.
+    A generalization of [MonadLiftFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadLiftFunctor), which can only lift endomorphisms (i.e. m = m', n = n'). -/
+class MonadFunctorT (m m' : Type u → Type v) (n n' : Type u → Type w) :=
+(monadMap {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
+
+export MonadFunctorT (monadMap)
+
+instance monadFunctorTrans (m m' n n' o o') [MonadFunctorT m m' n n'] [MonadFunctor n n' o o'] :
+  MonadFunctorT m m' o o' :=
+⟨fun α f => MonadFunctor.monadMap (fun β => (monadMap @f : n β → n' β))⟩
+
+instance monadFunctorRefl (m m') : MonadFunctorT m m' m m' :=
+⟨fun α f => f⟩
diff --git a/src/Init/Control/MonadLift.lean b/src/Init/Control/MonadLift.lean
new file mode 100644
index 0000000000..7215013fe5
--- /dev/null
+++ b/src/Init/Control/MonadLift.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2016 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Sebastian Ullrich
+
+Classy functions for lifting monadic actions of different shapes.
+
+This theory is roughly modeled after the Haskell 'layers' package https://hackage.haskell.org/package/layers-0.1.
+Please see https://hackage.haskell.org/package/layers-0.1/docs/Documentation-Layers-Overview.html for an exhaustive discussion of the different approaches to lift functions.
+-/
+prelude
+import Init.Control.Monad
+import Init.Coe
+
+universes u v w
+
+/-- A Function for lifting a computation from an inner Monad to an outer Monad.
+    Like [MonadTrans](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Class.html),
+    but `n` does not have to be a monad transformer.
+    Alternatively, an implementation of [MonadLayer](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer) without `layerInvmap` (so far). -/
+class MonadLift (m : Type u → Type v) (n : Type u → Type w) :=
+(monadLift : ∀ {α}, m α → n α)
+
+/-- The reflexive-transitive closure of `MonadLift`.
+    `monadLift` is used to transitively lift monadic computations such as `StateT.get` or `StateT.put s`.
+    Corresponds to [MonadLift](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLift). -/
+class MonadLiftT (m : Type u → Type v) (n : Type u → Type w) :=
+(monadLift : ∀ {α}, m α → n α)
+
+export MonadLiftT (monadLift)
+
+abbrev liftM := @monadLift
+
+@[inline] def liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
+a ← liftM $ x;
+pure $ coe a
+
+instance monadLiftTrans (m n o) [MonadLiftT m n] [MonadLift n o] : MonadLiftT m o :=
+⟨fun α ma => MonadLift.monadLift (monadLift ma : n α)⟩
+
+instance monadLiftRefl (m) : MonadLiftT m m :=
+⟨fun α => id⟩
diff --git a/src/Init/Control/MonadRun.lean b/src/Init/Control/MonadRun.lean
new file mode 100644
index 0000000000..2263dd5cbd
--- /dev/null
+++ b/src/Init/Control/MonadRun.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich, Leonardo de Moura
+-/
+prelude
+import Init.Control.MonadLift
+
+universes u v
+
+/-- Run a Monad stack to completion.
+    `run` should be the composition of the transformers' individual `run` functions.
+    This class mostly saves some typing when using highly nested Monad stacks:
+    ```
+    @[reducible] def MyMonad := ReaderT myCfg $ StateT myState $ ExceptT myErr id
+    -- def MyMonad.run {α : Type} (x : MyMonad α) (cfg : myCfg) (st : myState) := ((x.run cfg).run st).run
+    def MyMonad.run {α : Type} (x : MyMonad α) := MonadRun.run x
+    ```
+    -/
+class MonadRun (out : outParam $ Type u → Type v) (m : Type u → Type v) :=
+(run {α : Type u} : m α → out α)
+
+export MonadRun (run)
diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index 8b0b741080..c1b194d112 100644
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Init.Control.Alternative
-import Init.Control.Lift
+import Init.Control.MonadLift
 import Init.Control.Except
 
 universes u v