From e044030cd28da233bd3c20869654284c80a47e58 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 7 Mar 2018 10:37:27 +0100
Subject: [PATCH] doc(init/category/cont): add docs and test

---
 library/init/category/cont.lean | 20 +++++++++++++++++---
 tests/lean/run/cont.lean        | 17 +++++++++++++++++
 2 files changed, 34 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/cont.lean

diff --git a/library/init/category/cont.lean b/library/init/category/cont.lean
index 4f5f692e4c..b2c0da7281 100644
--- a/library/init/category/cont.lean
+++ b/library/init/category/cont.lean
@@ -10,13 +10,19 @@ 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_cc {α β : Type u} : ((α → m β) → m α) → m α)
+/- 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 α
 
@@ -33,10 +39,18 @@ section
   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⟩
+  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/tests/lean/run/cont.lean b/tests/lean/run/cont.lean
new file mode 100644
index 0000000000..2918b0fdee
--- /dev/null
+++ b/tests/lean/run/cont.lean
@@ -0,0 +1,17 @@
+import system.io
+
+-- 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,
+    (list.range 10).mmap' $ λ i,
+      call_cc $ λ continue, do {
+        when (i % 2 = 0) $
+          continue (),
+        when (i > 7) $
+          break (),
+        modify (+1) >> pure ()
+      },
+   get
+
+#eval do ((), 4) ← (cont_example.run (λ _, pure ())).run 0,
+         pure ()