From da5c8e21df7d78e496a4375a185a6fa324a634bd Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 9 Mar 2018 00:26:34 +0100
Subject: [PATCH] chore(init/category/cont): move to test

---
 library/init/category/cont.lean    | 56 ---------------------
 library/init/category/default.lean |  1 -
 library/init/category/lawful.lean  | 23 +--------
 tests/lean/run/cont.lean           | 78 +++++++++++++++++++++++++++++-
 4 files changed, 78 insertions(+), 80 deletions(-)
 delete mode 100644 library/init/category/cont.lean

diff --git a/library/init/category/cont.lean b/library/init/category/cont.lean
deleted file mode 100644
index b2c0da7281..0000000000
--- a/library/init/category/cont.lean
+++ /dev/null
@@ -1,56 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
-
-The continuation monad transformer.
--/
-
-prelude
-import init.category.alternative init.category.combinators init.category.lift
-universes u v w
-
-/-- An implementation of [ContT](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Cont.html#t:ContT) -/
-structure cont_t (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-(run : (α → m ρ) → m ρ)
-
-attribute [pp_using_anonymous_constructor] cont_t
-
-/-- An implementation of [MonadCont done right](https://wiki.haskell.org/MonadCont_done_right) -/
-class monad_cont (m : Type u → Type v) :=
-/- Call a function with the current continuation (cc) as its argument, which can be called to
-   exit the function from anywhere inside it. -/
-(call_cc {α : Type u} : ((∀ {β}, α → m β) → m α) → m α)
-
-export monad_cont (call_cc)
-
-@[reducible] def cont (ρ α : Type u) : Type u := cont_t ρ id α
-
-namespace cont_t
-section
-  parameters {ρ : Type u} {m : Type u → Type v}
-
-  protected def pure {α : Type u} (a : α) : cont_t ρ m α :=
-  ⟨λ cc, cc a⟩
-
-  protected def bind {α β : Type u} (ma : cont_t ρ m α) (f : α → cont_t ρ m β) : cont_t ρ m β :=
-  ⟨λ cc, ma.run (λ a, (f a).run cc)⟩
-
-  instance : monad (cont_t ρ m) :=
-  { pure := @pure, bind := @bind }
-
-  protected def call_cc {α : Type u} (f : (∀ {β}, α → cont_t ρ m β) → cont_t ρ m α) : cont_t ρ m α :=
-  ⟨λ cc, (f (λ _ a, ⟨λ _, cc a⟩)).run cc⟩
-
-  instance : monad_cont (cont_t ρ m) :=
-  ⟨@call_cc⟩
-
-  protected def lift [_root_.monad m] {α : Type u} (x : m α) : cont_t ρ m α :=
-  ⟨λ cc, x >>= cc⟩
-
-  instance [_root_.monad m] : has_monad_lift m (cont_t ρ m) :=
-  ⟨@cont_t.lift _⟩
-
-  -- there is NO instance of `monad_functor` for `cont_t`
-end
-end cont_t
diff --git a/library/init/category/default.lean b/library/init/category/default.lean
index 0a97af71b5..24b33c8081 100644
--- a/library/init/category/default.lean
+++ b/library/init/category/default.lean
@@ -7,4 +7,3 @@ 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.cont
diff --git a/library/init/category/lawful.lean b/library/init/category/lawful.lean
index de6d5ab000..3cc0e388e2 100644
--- a/library/init/category/lawful.lean
+++ b/library/init/category/lawful.lean
@@ -5,7 +5,7 @@ Authors: Sebastian Ullrich
 -/
 prelude
 import init.category.monad init.meta.interactive
-import init.category.state init.category.except init.category.reader init.category.cont
+import init.category.state init.category.except init.category.reader
 universes u v
 
 open function
@@ -200,24 +200,3 @@ instance (ρ : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : i
 { id_map := by intros; apply reader_t.ext; intro; simp,
   pure_bind := by intros; apply reader_t.ext; intro; simp,
   bind_assoc := by intros; apply reader_t.ext; intro; simp [bind_assoc] }
-
-
-namespace cont_t
-  variable  {ρ : Type u}
-  variable  {m : Type u → Type v}
-  variables {α β : Type u}
-  variables (x : cont_t ρ m α)
-
-  lemma ext {x x' : cont_t ρ m α} (h : ∀ cc, x.run cc = x'.run cc) : x = x' :=
-  by cases x; cases x'; simp [show x = x', from funext h]
-
-  @[simp] lemma run_pure (a : α) (cc : α → m ρ) : (pure a : cont_t ρ m α).run cc = cc a := rfl
-  @[simp] lemma run_bind (f : α → cont_t ρ m β) (cc : β → m ρ) :
-    (x >>= f).run cc = x.run (λ a, (f a).run cc) := rfl
-  @[simp] lemma run_map (f : α → β) (cc : β → m ρ) : (f <$> x).run cc = x.run (cc ∘ f) := rfl
-end cont_t
-
-instance (ρ : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (cont_t ρ m) :=
-{ id_map := by intros; apply cont_t.ext; simp,
-  pure_bind := by intros; apply cont_t.ext; simp,
-  bind_assoc := by intros; apply cont_t.ext; simp }
diff --git a/tests/lean/run/cont.lean b/tests/lean/run/cont.lean
index 2918b0fdee..1707936b2b 100644
--- a/tests/lean/run/cont.lean
+++ b/tests/lean/run/cont.lean
@@ -1,5 +1,81 @@
-import system.io
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
 
+The continuation monad transformer.
+-/
+
+import init.category.alternative init.category.combinators init.category.lift
+import system.io
+universes u v w
+
+/-- An implementation of [ContT](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Cont.html#t:ContT) -/
+structure cont_t (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+(run : (α → m ρ) → m ρ)
+
+attribute [pp_using_anonymous_constructor] cont_t
+
+/-- An implementation of [MonadCont done right](https://wiki.haskell.org/MonadCont_done_right) -/
+class monad_cont (m : Type u → Type v) :=
+/- Call a function with the current continuation (cc) as its argument, which can be called to
+   exit the function from anywhere inside it. -/
+(call_cc {α : Type u} : ((∀ {β}, α → m β) → m α) → m α)
+
+export monad_cont (call_cc)
+
+@[reducible] def cont (ρ α : Type u) : Type u := cont_t ρ id α
+
+namespace cont_t
+section
+  parameters {ρ : Type u} {m : Type u → Type v}
+
+  protected def pure {α : Type u} (a : α) : cont_t ρ m α :=
+  ⟨λ cc, cc a⟩
+
+  protected def bind {α β : Type u} (ma : cont_t ρ m α) (f : α → cont_t ρ m β) : cont_t ρ m β :=
+  ⟨λ cc, ma.run (λ a, (f a).run cc)⟩
+
+  instance : monad (cont_t ρ m) :=
+  { pure := @pure, bind := @bind }
+
+  protected def call_cc {α : Type u} (f : (∀ {β}, α → cont_t ρ m β) → cont_t ρ m α) : cont_t ρ m α :=
+  ⟨λ cc, (f (λ _ a, ⟨λ _, cc a⟩)).run cc⟩
+
+  instance : monad_cont (cont_t ρ m) :=
+  ⟨@call_cc⟩
+
+  protected def lift [_root_.monad m] {α : Type u} (x : m α) : cont_t ρ m α :=
+  ⟨λ cc, x >>= cc⟩
+
+  instance [_root_.monad m] : has_monad_lift m (cont_t ρ m) :=
+  ⟨@cont_t.lift _⟩
+
+  -- there is NO instance of `monad_functor` for `cont_t`
+end
+end cont_t
+
+
+namespace cont_t
+  variable  {ρ : Type u}
+  variable  {m : Type u → Type v}
+  variables {α β : Type u}
+  variables (x : cont_t ρ m α)
+
+  lemma ext {x x' : cont_t ρ m α} (h : ∀ cc, x.run cc = x'.run cc) : x = x' :=
+  by cases x; cases x'; simp [show x = x', from funext h]
+
+  @[simp] lemma run_pure (a : α) (cc : α → m ρ) : (pure a : cont_t ρ m α).run cc = cc a := rfl
+  @[simp] lemma run_bind (f : α → cont_t ρ m β) (cc : β → m ρ) :
+    (x >>= f).run cc = x.run (λ a, (f a).run cc) := rfl
+  @[simp] lemma run_map (f : α → β) (cc : β → m ρ) : (f <$> x).run cc = x.run (cc ∘ f) := rfl
+end cont_t
+
+
+instance (ρ : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (cont_t ρ m) :=
+{ id_map := by intros; apply cont_t.ext; simp,
+  pure_bind := by intros; apply cont_t.ext; simp,
+  bind_assoc := by intros; apply cont_t.ext; simp }
 -- count the even numbers from 0 to 7 in a horrible, imperative way
 def cont_example : cont_t unit (state_t ℕ io) ℕ :=
 do call_cc $ λ break,