From 5599c9ca679f3ff227f99b45bab5a0d41dbb4b52 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 1 Mar 2018 15:10:47 +0100
Subject: [PATCH] feat(init/category): misc enhancements from the tactic
 refactoring

---
 library/init/category/except.lean     | 40 +++++++++++++++++++++++----
 library/init/category/monad_fail.lean |  9 +++++-
 library/init/category/state.lean      |  7 +++--
 3 files changed, 48 insertions(+), 8 deletions(-)

diff --git a/library/init/category/except.lean b/library/init/category/except.lean
index 4fac075446..c80d2efc35 100644
--- a/library/init/category/except.lean
+++ b/library/init/category/except.lean
@@ -5,10 +5,10 @@ Authors: Jared Roesch, Sebastian Ullrich
 -/
 
 prelude
-import init.category.transformers
+import init.category.alternative init.category.transformers
 universes u v w
 
-inductive except (ε α : Type u)
+inductive except (ε : Type u) (α : Type v)
 | error {} : ε → except
 | ok {} : α → except
 
@@ -16,24 +16,51 @@ class monad_except (ε : out_param (Type u)) (m : Type v → Type w) :=
 (throw {} {α : Type v} : ε → m α)
 (catch {} {α : Type v} : m α → (ε → m α) → m α)
 
+namespace monad_except
+variables {ε : Type u} {m : Type v → Type w}
+
+protected def orelse [monad_except ε m] {α : Type v} (t₁ t₂ : m α) : m α :=
+catch t₁ $ λ _, t₂
+
+/- Alternative orelse operator that allows to select which exception should be used.
+   The default is to use the first exception since the standard `orelse` uses the second. -/
+meta def orelse' [monad_except ε m] {α : Type v} (t₁ t₂ : m α) (use_first_ex := tt) : m α :=
+catch t₁ $ λ e₁, catch t₂ $ λ e₂, throw (if use_first_ex then e₁ else e₂)
+end monad_except
+
 export monad_except (throw catch)
 
 namespace except
 section
   parameter {ε : Type u}
 
-  protected def return {α : Type u} (a : α) : except ε α :=
+  protected def return {α : Type v} (a : α) : except ε α :=
   except.ok a
 
-  protected def map {α β : Type u} (f : α → β) : except ε α → except ε β
+  protected def map {α β : Type v} (f : α → β) : except ε α → except ε β
   | (except.error err) := except.error err
   | (except.ok v) := except.ok $ f v
 
-  protected def bind {α β : Type u} (ma : except ε α) (f : α → except ε β) : except ε β :=
+  protected def map_error {ε' : Type u} {α : Type v} (f : ε → ε') : except ε α → except ε' α
+  | (except.error err) := except.error $ f err
+  | (except.ok v) := except.ok v
+
+  protected def bind {α β : Type v} (ma : except ε α) (f : α → except ε β) : except ε β :=
   match ma with
   | (except.error err) := except.error err
   | (except.ok v) := f v
   end
+
+  protected def to_bool {α : Type v} : except ε α → bool
+  | (except.ok _)    := tt
+  | (except.error _) := ff
+
+  protected def to_option {α : Type v} : except ε α → option α
+  | (except.ok a)    := some a
+  | (except.error _) := none
+
+  instance : monad (except ε) :=
+  { pure := @return, bind := @bind }
 end
 end except
 
@@ -59,6 +86,9 @@ section
   protected def lift {α : Type u} (t : m α) : except_t ε m α :=
   ⟨except.ok <$> t⟩
 
+  instance : has_monad_lift m (except_t ε m) :=
+  ⟨@except_t.lift⟩
+
   protected def catch {α : Type u} (ma : except_t ε m α) (handle : ε → except_t ε m α) : except_t ε m α :=
   ⟨ma.run >>= λ res, match res with
    | except.ok a    := pure (except.ok a)
diff --git a/library/init/category/monad_fail.lean b/library/init/category/monad_fail.lean
index 4761f93517..3a07baaf94 100644
--- a/library/init/category/monad_fail.lean
+++ b/library/init/category/monad_fail.lean
@@ -4,12 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.category.monad init.data.string.basic
+import init.category.transformers init.data.string.basic
 
 universes u v
 
 class monad_fail (m : Type u → Type v) extends monad m :=
 (fail : Π {a}, string → m a)
 
+-- deriving monad from monad_fail should happen only as a last resort
+attribute [instance, priority 1] monad_fail.to_monad
+
 def match_failed {α : Type u} {m : Type u → Type v} [monad_fail m] : m α :=
 monad_fail.fail m "match failed"
+
+-- TODO(Sebastian): Could take `has_monad_lift_t`, except that the refl instances will make it loop
+instance monad_fail_lift (m n : Type u → Type v) [has_monad_lift m n] [monad_fail m] [monad_n : monad n] : monad_fail n :=
+{ fail := λ α s, monad_lift (monad_fail.fail m s : m α), ..monad_n }
diff --git a/library/init/category/state.lean b/library/init/category/state.lean
index 18a5c2ffa4..a185cef27b 100644
--- a/library/init/category/state.lean
+++ b/library/init/category/state.lean
@@ -20,7 +20,7 @@ section
   variable  [monad m]
   variables {α β : Type u}
 
-  protected def run (st : σ) (x : state_t σ m α) : m (α × σ) :=
+  @[inline] protected def run (st : σ) (x : state_t σ m α) : m (α × σ) :=
   state_t.run' x st
 
   protected def pure (a : α) : state_t σ m α :=
@@ -56,7 +56,7 @@ section
   protected def lift {α : Type u} (t : m α) : state_t σ m α :=
   ⟨λ s, do a ← t, return (a, s)⟩
 
-  instance has_monad_lift_lift (m) [monad m] : has_monad_lift m (state_t σ m) :=
+  instance (m) [monad m] : has_monad_lift m (state_t σ m) :=
   ⟨@state_t.lift σ m _⟩
 
   protected def map {σ m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : state_t σ m α → state_t σ m' α :=
@@ -90,6 +90,9 @@ variables {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [monad m
 @[inline] def get : n σ :=
 @monad_lift _ _ _ _ (state_t.get : state_t σ m _)
 
+@[inline] def get_type (σ : Type u) [has_monad_lift_t (state_t σ m) n] : n σ :=
+get
+
 @[inline] def put (st : σ) : n punit :=
 monad_lift (state_t.put st : state_t σ m _)