refactor(init/category): replace has_scope_impure with more general m…

…onad_control class

library/init/category/except.lean

@@ -111,10 +111,9 @@ end except_t
 instance (m ε) [monad m] : monad_except ε (except_t ε m) :=
 { throw := λ α, except_t.mk ∘ pure ∘ except.error, catch := @except_t.catch ε _ _ }
 
-instance (ε m) [monad m] [has_scope_impure m] : has_scope_impure (except_t ε m) :=
-⟨λ α f x, ⟨do some x ← scope_impure_opt @f (x ()).run
-                | pure (pure none),
-              pure (some <$> x)⟩⟩
+instance (ε : Type u) (m) [monad m] : monad_control.{u} (except ε) m (except_t ε m) :=
+{ monad_lift_control := λ α f, ⟨except.ok <$> f (λ β, except_t.run)⟩,
+  restore := λ α e, ⟨pure e⟩ }
 
 instance (ε m out) [monad_run out m] : monad_run (λ α, out (except ε α)) (except_t ε m) :=
 ⟨λ α, run ∘ except_t.run, λ α, except_t.mk ∘ unrun⟩

library/init/category/id.lean

@@ -16,6 +16,3 @@ universe u
 
 @[inline] instance : monad_run id id :=
 ⟨@id, @id⟩
-
-@[inline] instance : has_scope_impure id :=
-⟨λ α f x, f (x ())⟩

library/init/category/lift.lean

@@ -56,7 +56,32 @@ instance monad_functor_t_refl (m m') : monad_functor_t m m' m m' :=
 @[simp] lemma monad_map_refl {m m' : Type u → Type v} (f : ∀ {α}, m α → m' α) {α} : (monad_map @f : m α → m' α) = f := rfl
 
 
-/-- Run a monad stack to completion. -/
+/-- Lift control operations such as `catch` - http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadLayerControl -/
+class monad_control (st : out_param $ Type u → Type u) (m : Type u → Type u) (n : Type u → Type u) :=
+(monad_lift_control {α : Type u} : ((∀ {β}, n β → m (st β)) → m α) → n α)
+(restore {} {α : Type u} : st α → n α)
+
+/-- The reflexive-transitive closure of `monad_control`. -/
+class monad_control_t (st : out_param $ Type u → Type u) (m : Type u → Type u) (n : Type u → Type u) :=
+(monad_lift_control {α : Type u} : ((∀ {β}, n β → m (st β)) → m α) → n α)
+(restore {} {α : Type u} : st α → n α)
+
+export monad_control_t (monad_lift_control restore)
+
+instance monad_control_t_trans (st st' m n o) [monad_control st n o] [monad_control_t st' m n] [has_monad_lift n o] [monad m] [monad o] : monad_control_t (st' ∘ st) m o :=
+{ monad_lift_control := λ α f, monad_control.monad_lift_control $ λ run,
+    monad_lift_control $ λ (run' : ∀ {β}, n β → m (st' β)),
+      f $ λ β, run' ∘ run,
+  restore := λ α s, monad_lift (restore m s : n _) >>= monad_control.restore n }
+
+instance has_monad_control_t_refl (m) [monad m] : monad_control_t id m m :=
+{ monad_lift_control := λ α f, f $ λ β, id,
+  restore := λ α, pure }
+
+
+/-- Run a monad stack to completion.
+    `run` should be the composition of the transformers' individual `run` functions.
+    `unrun` should be its inverse. -/
 class monad_run (out : out_param $ Type u → Type v) (m : Type u → Type v) :=
 (run {} {α : Type u} : m α → out α)
 (unrun {} {α : Type u} : out α → m α)
@@ -66,13 +91,14 @@ export monad_run (run unrun)
 
 /-- Lift an impure scoping function.
     The helper functions in init.util take a thunk of a pure computation and execute it under some side
-    effect. For monads like `state_t` that are "lazy", i.e. evaluate to a closure, we have to special
-    case these operations to go inside these binders and work on the strict "core". -/
-class has_scope_impure (m : Type u → Type v) :=
-(scope_impure_opt {} {α : Type u} : (∀ {β : Type u}, thunk β → option β) → thunk (m α) → m (option α))
-
-export has_scope_impure (scope_impure_opt)
-
-@[inline] meta def scope_impure {m : Type u → Type v} [monad m] [has_scope_impure m] {α : Type u} :
+    effect. For monads like `state_t` that are "lazy", i.e. evaluate to a closure, we use
+    `monad_lift_control` to go inside these binders and work on the strict "core". -/
+@[inline] meta def scope_impure_opt {st : Type u → Type u} {m : Type u → Type u} [monad m] [monad_control_t st id m] {α : Type u} :
+  (∀ {β : Type u}, thunk β → option β) → m α → m (option α) :=
+λ f x, do some s' ← monad_lift_control (λ (run : ∀ {β}, m β → id (st β)), (f (run x)))
+           | pure none,
+          some <$> restore id s'
+
+@[inline] meta def scope_impure {st : Type u → Type u} {m : Type u → Type u} [monad m] [monad_control_t st id m] {α : Type u} :
   (∀ {β : Type u}, thunk β → β) → m α → m α :=
-λ f x, scope_impure_opt (λ β, some ∘ f) x >>= λ o, option.rec undefined pure o
+λ f x, monad_lift_control (λ run, (f (run x) : id (st α))) >>= restore id

library/init/category/state.lean

@@ -120,11 +120,9 @@ def zoom {σ σ'} {m n n'} [monad m] {α : Type u} (get : σ → σ') (set : σ'
   [monad_state_functor σ' σ m n n'] : n α → n' α :=
 monad_map $ λ α, (state_t.zoom get set : state_t σ' m α → state_t σ m α)
 
-instance (σ m) [monad m] [has_scope_impure m] : has_scope_impure (state_t σ m) :=
--- note: needs to go inside binder
-⟨λ α f x, ⟨λ s, do some ⟨a, s'⟩ ← scope_impure_opt @f ((x ()).run s)
-                     | pure (none, s),
-                   pure (some a, s')⟩⟩
+instance (σ : Type u) (m) [monad m] : monad_control.{u} (× σ) m (state_t σ m) :=
+{ monad_lift_control := λ α f, ⟨λ s, (λ a, (a, s)) <$> f (λ β, state_t.run s)⟩,
+  restore := λ α ⟨a, s⟩, ⟨λ s', pure (a, s)⟩ }
 
 
 instance (σ m out) [monad_run out m] : monad_run (λ α, σ → out (α × σ)) (state_t σ m) :=

library/init/meta/interaction_monad.lean

@@ -46,7 +46,7 @@ meta instance : monad m := { bind := @bind }
 meta instance : monad_run _ m := infer_instance
 meta instance : monad_except _ m := infer_instance
 meta instance : monad_state_lift _ _ m := infer_instance
-meta instance : has_scope_impure m := infer_instance
+meta instance : monad_control_t _ id m := infer_instance
 end
 
 meta def run := interaction_monad.monad_run.run

library/init/meta/smt/smt_tactic.lean

@@ -65,7 +65,7 @@ meta instance : monad smt_tactic := by apply_instance
 meta instance : alternative smt_tactic := by apply_instance
 meta instance : monad_state_lift _ _ smt_tactic := by apply_instance
 meta instance : monad_except _ smt_tactic := by apply_instance
-meta instance : has_scope_impure smt_tactic := by apply_instance
+meta instance : monad_control_t _ id smt_tactic := by apply_instance
 end
 
 /- We don't use the default state_t lift operation because only