From 5ff9e24b1781cbf37eb1ed3da660c579e9cccfe3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 19 Sep 2018 15:22:19 -0700
Subject: [PATCH] feat(library/init/control): do not use unnecessary structures

It confuses the compiler.
---
 library/init/control/except.lean     | 37 +++++++++++++-------------
 library/init/control/option.lean     | 29 +++++++++++----------
 library/init/control/reader.lean     | 33 +++++++++++------------
 library/init/control/state.lean      | 39 ++++++++++++++--------------
 library/init/io.lean                 | 24 +++++++++--------
 library/init/lean/parser/module.lean |  2 +-
 6 files changed, 86 insertions(+), 78 deletions(-)

diff --git a/library/init/control/except.lean b/library/init/control/except.lean
index dec0f4348f..5454a126bb 100644
--- a/library/init/control/except.lean
+++ b/library/init/control/except.lean
@@ -70,42 +70,42 @@ instance : monad (except ε) :=
 end
 end except
 
+def except_t (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
+m (except ε α)
 
-structure except_t (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
-(run : m (except ε α))
-
-attribute [pp_using_anonymous_constructor] except_t
+@[inline] def except_t.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : except_t ε m α) : m (except ε α) :=
+x
 
 namespace except_t
 section
 parameters {ε : Type u} {m : Type u → Type v} [monad m]
 
 @[inline] protected def return {α : Type u} (a : α) : except_t ε m α :=
-⟨pure $ except.ok a⟩
+(pure (except.ok a) : m (except ε α))
 
 @[inline] protected def bind_cont {α β : Type u} (f : α → except_t ε m β) : except ε α → m (except ε β)
-| (except.ok a)    := (f a).run
+| (except.ok a)    := f a
 | (except.error e) := pure (except.error e)
 
 @[inline] protected def bind {α β : Type u} (ma : except_t ε m α) (f : α → except_t ε m β) : except_t ε m β :=
-⟨ma.run >>= bind_cont f⟩
+(ma >>= bind_cont f : m (except ε β))
 
 @[inline] protected def lift {α : Type u} (t : m α) : except_t ε m α :=
-⟨except.ok <$> t⟩
+(except.ok <$> t : m (except ε α))
 
 instance except_t_of_except : has_monad_lift (except ε) (except_t ε m) :=
-⟨λ α e, ⟨pure e⟩⟩
+⟨λ α e, (pure e : m (except ε α))⟩
 
 instance : has_monad_lift m (except_t ε m) :=
 ⟨@except_t.lift⟩
 
 @[inline] 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)
-| except.error e := (handle e).run⟩
+(ma >>= λ res, match res with
+ | except.ok a    := pure (except.ok a)
+ | except.error e := (handle e) : m (except ε α))
 
 @[inline] protected def monad_map {m'} [monad m'] {α} (f : ∀ {α}, m α → m' α) : except_t ε m α → except_t ε m' α :=
-λ x, ⟨f x.run⟩
+λ x, f x
 
 instance (m') [monad m'] : monad_functor m m' (except_t ε m) (except_t ε m') :=
 ⟨@monad_map m' _⟩
@@ -114,7 +114,7 @@ instance : monad (except_t ε m) :=
 { pure := @return, bind := @bind }
 
 @[inline] protected def adapt {ε' α : Type u} (f : ε → ε') : except_t ε m α → except_t ε' m α :=
-λ x, ⟨except.map_error f <$> x.run⟩
+λ x, (except.map_error f <$> x : m (except ε' α))
 end
 end except_t
 
@@ -142,8 +142,9 @@ end monad_except
 
 export monad_except (throw catch)
 
-instance (m ε) [monad m] : monad_except ε (except_t ε m) :=
-{ throw := λ α, except_t.mk ∘ pure ∘ except.error, catch := @except_t.catch ε _ _ }
+instance (m : Type u → Type v) (ε : Type u) [monad m] : monad_except ε (except_t ε m) :=
+{ throw := λ α e, (pure (except.error e) : m (except ε α)),
+  catch := @except_t.catch ε _ _ }
 
 instance (ε) : monad_except ε (except ε) :=
 { throw := λ α, except.error, catch := @except.catch _ }
@@ -171,8 +172,8 @@ instance [monad m] : monad_except_adapter ε ε' (except_t ε m) (except_t ε' m
 end
 
 instance (ε m out) [monad_run out m] : monad_run (λ α, out (except ε α)) (except_t ε m) :=
-⟨λ α, run ∘ except_t.run⟩
+⟨λ α, run⟩
 
 -- useful for implicit failures in do-notation
-instance (m) [monad m] : monad_fail (except_t string m) :=
+instance (m : Type → Type) [monad m] : monad_fail (except_t string m) :=
 ⟨λ _, throw⟩
diff --git a/library/init/control/option.lean b/library/init/control/option.lean
index 00059ce991..6fa9cccc11 100644
--- a/library/init/control/option.lean
+++ b/library/init/control/option.lean
@@ -8,31 +8,34 @@ import init.control.alternative init.control.lift init.control.except
 
 universes u v
 
-structure option_t (m : Type u → Type v) (α : Type u) : Type v :=
-(run : m (option α))
+def option_t (m : Type u → Type v) (α : Type u) : Type v :=
+m (option α)
+
+@[inline] def option_t.run {m : Type u → Type v} {α : Type u} (x : option_t m α) : m (option α) :=
+x
 
 namespace option_t
   variables {m : Type u → Type v} [monad m] {α β : Type u}
 
   @[inline] protected def bind_cont {α β : Type u} (f : α → option_t m β) : option α → m (option β)
-  | (some a) := (f a).run
+  | (some a) := f a
   | none     := pure none
 
   @[inline] protected def bind (ma : option_t m α) (f : α → option_t m β) : option_t m β :=
-  ⟨ma.run >>= option_t.bind_cont f⟩
+  (ma >>= option_t.bind_cont f : m (option β))
 
   @[inline] protected def pure (a : α) : option_t m α :=
-  ⟨pure (some a)⟩
+  (pure (some a) : m (option α))
 
   instance : monad (option_t m) :=
   { pure := @option_t.pure _ _, bind := @option_t.bind _ _ }
 
   protected def orelse (ma : option_t m α) (mb : option_t m α) : option_t m α :=
-  ⟨do some a ← ma.run | mb.run,
-      pure (some a)⟩
+  (do { some a ← ma | mb,
+        pure (some a) } : m (option α))
 
   @[inline] protected def fail : option_t m α :=
-  ⟨pure none⟩
+  (pure none : m (option α))
 
   instance : alternative (option_t m) :=
   { failure := @option_t.fail m _,
@@ -40,24 +43,24 @@ namespace option_t
     ..option_t.monad }
 
   @[inline] protected def lift (ma : m α) : option_t m α :=
-  ⟨some <$> ma⟩
+  (some <$> ma : m (option α))
 
   instance : has_monad_lift m (option_t m) :=
   ⟨@option_t.lift _ _⟩
 
   @[inline] protected def monad_map {m'} [monad m'] {α} (f : ∀ {α}, m α → m' α) : option_t m α → option_t m' α :=
-  λ x, ⟨f x.run⟩
+  λ x, f x
 
   instance (m') [monad m'] : monad_functor m m' (option_t m) (option_t m') :=
   ⟨λ α, option_t.monad_map⟩
 
   protected def catch (ma : option_t m α) (handle : unit → option_t m α) : option_t m α :=
-  ⟨do some a ← ma.run | (handle ()).run,
-      pure a⟩
+  (do { some a ← ma | (handle ()),
+        pure a } : m (option α))
 
   instance : monad_except unit (option_t m) :=
   { throw := λ _ _, option_t.fail, catch := @option_t.catch _ _ }
 
   instance (m out) [monad_run out m] : monad_run (λ α, out (option α)) (option_t m) :=
-  ⟨λ α, monad_run.run ∘ option_t.run⟩
+  ⟨λ α, monad_run.run⟩
 end option_t
diff --git a/library/init/control/reader.lean b/library/init/control/reader.lean
index 3a86086962..0286fee546 100644
--- a/library/init/control/reader.lean
+++ b/library/init/control/reader.lean
@@ -11,13 +11,14 @@ import init.control.lift init.control.id init.control.alternative init.control.e
 universes u v w
 
 /-- An implementation of [ReaderT](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Reader.html#t:ReaderT) -/
-structure reader_t (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-(run : ρ → m α)
+def reader_t (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+ρ → m α
+
+@[inline] def reader_t.run {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : reader_t ρ m α) (r : ρ) : m α :=
+x r
 
 @[reducible] def reader (ρ : Type u) := reader_t ρ id
 
-attribute [pp_using_anonymous_constructor] reader_t
-
 namespace reader_t
 section
   variable  {ρ : Type u}
@@ -26,38 +27,38 @@ section
   variables {α β : Type u}
 
   @[inline] protected def read : reader_t ρ m ρ :=
-  ⟨pure⟩
+  pure
 
   @[inline] protected def pure (a : α) : reader_t ρ m α :=
-  ⟨λ r, pure a⟩
+  λ r, pure a
 
   @[inline] protected def bind (x : reader_t ρ m α) (f : α → reader_t ρ m β) : reader_t ρ m β :=
-  ⟨λ r, do a ← x.run r,
-           (f a).run r⟩
+  λ r, do a ← x r,
+          f a r
 
   instance : monad (reader_t ρ m) :=
   { pure := @reader_t.pure _ _ _, bind := @reader_t.bind _ _ _ }
 
   @[inline] protected def lift (a : m α) : reader_t ρ m α :=
-  ⟨λ r, a⟩
+  λ r, a
 
   instance (m) [monad m] : has_monad_lift m (reader_t ρ m) :=
   ⟨@reader_t.lift ρ m _⟩
 
   @[inline] protected def monad_map {ρ m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : reader_t ρ m α → reader_t ρ m' α :=
-  λ x, ⟨λ r, f (x.run r)⟩
+  λ x, λ r, f (x r)
 
   instance (ρ m m') [monad m] [monad m'] : monad_functor m m' (reader_t ρ m) (reader_t ρ m') :=
   ⟨@reader_t.monad_map ρ m m' _ _⟩
 
   @[inline] protected def adapt {ρ' : Type u} [monad m] {α : Type u} (f : ρ' → ρ) : reader_t ρ m α → reader_t ρ' m α :=
-  λ x, ⟨λ r, x.run (f r)⟩
+  λ x r, x (f r)
 
   protected def orelse [alternative m] {α : Type u} (x₁ x₂ : reader_t ρ m α) : reader_t ρ m α :=
-  ⟨λ s, x₁.run s <|> x₂.run s⟩
+  λ s, x₁ s <|> x₂ s
 
   protected def failure [alternative m] {α : Type u} : reader_t ρ m α :=
-  ⟨λ s, failure⟩
+  λ s, failure
 
   instance [alternative m] : alternative (reader_t ρ m) :=
   { failure := @reader_t.failure _ _ _ _,
@@ -65,7 +66,7 @@ section
 
   instance (ε) [monad m] [monad_except ε m] : monad_except ε (reader_t ρ m) :=
   { throw := λ α, reader_t.lift ∘ throw,
-    catch := λ α x c, ⟨λ r, catch (x.run r) (λ e, (c e).run r)⟩ }
+    catch := λ α x c r, catch (x r) (λ e, (c e) r) }
 end
 end reader_t
 
@@ -118,7 +119,7 @@ instance [monad m] : monad_reader_adapter ρ ρ' (reader_t ρ m) (reader_t ρ' m
 end
 
 instance (ρ : Type u) (m out) [monad_run out m] : monad_run (λ α, ρ → out α) (reader_t ρ m) :=
-⟨λ α x, run ∘ x.run⟩
+⟨λ α x, run ∘ x⟩
 
 class monad_reader_runner (ρ : Type u) (m m' : Type u → Type u) :=
 (run_reader {} {α : Type u} : m α → ρ → m' α)
@@ -131,5 +132,5 @@ instance monad_reader_runner_trans {n n' : Type u → Type u} [monad_functor m m
 ⟨λ α x r, monad_map (λ α (y : m α), (run_reader y r : m' α)) x⟩
 
 instance reader_t.monad_state_runner [monad m] : monad_reader_runner ρ (reader_t ρ m) m :=
-⟨λ α x r, x.run r⟩
+⟨λ α x r, x r⟩
 end
diff --git a/library/init/control/state.lean b/library/init/control/state.lean
index e0da06a931..68241bc286 100644
--- a/library/init/control/state.lean
+++ b/library/init/control/state.lean
@@ -10,10 +10,11 @@ import init.control.alternative init.control.lift
 import init.control.id init.control.except
 universes u v w
 
-structure state_t (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-(run : σ → m (α × σ))
+def state_t (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+σ → m (α × σ)
 
-attribute [pp_using_anonymous_constructor] state_t
+@[inline] def state_t.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : state_t σ m α) (s : σ) : m (α × σ) :=
+x s
 
 @[reducible] def state (σ α : Type u) : Type u := state_t σ id α
 
@@ -25,56 +26,56 @@ section
   variables {α β : Type u}
 
   @[inline] protected def pure (a : α) : state_t σ m α :=
-  ⟨λ s, pure (a, s)⟩
+  λ s, pure (a, s)
 
   @[inline] protected def bind (x : state_t σ m α) (f : α → state_t σ m β) : state_t σ m β :=
-  ⟨λ s, do (a, s') ← x.run s,
-           (f a).run s'⟩
+  λ s, do (a, s') ← x s,
+          f a s'
 
   instance : monad (state_t σ m) :=
   { pure := @state_t.pure _ _ _, bind := @state_t.bind _ _ _ }
 
   @[inline] protected def orelse [alternative m] {α : Type u} (x₁ x₂ : state_t σ m α) : state_t σ m α :=
-  ⟨λ s, x₁.run s <|> x₂.run s⟩
+  λ s, x₁ s <|> x₂ s
 
   @[inline] protected def failure [alternative m] {α : Type u} : state_t σ m α :=
-  ⟨λ s, failure⟩
+  λ s, failure
 
   instance [alternative m] : alternative (state_t σ m) :=
   { failure := @state_t.failure _ _ _ _,
     orelse  := @state_t.orelse _ _ _ _ }
 
   @[inline] protected def get : state_t σ m σ :=
-  ⟨λ s, pure (s, s)⟩
+  λ s, pure (s, s)
 
   @[inline] protected def put : σ → state_t σ m punit :=
-  λ s', ⟨λ s, pure (punit.star, s')⟩
+  λ s' s, pure (punit.star, s')
 
   @[inline] protected def modify (f : σ → σ) : state_t σ m punit :=
-  ⟨λ s, pure (punit.star, f s)⟩
+  λ s, pure (punit.star, f s)
 
   @[inline] protected def lift {α : Type u} (t : m α) : state_t σ m α :=
-  ⟨λ s, do a ← t, pure (a, s)⟩
+  λ s, do a ← t, pure (a, s)
 
   instance : has_monad_lift m (state_t σ m) :=
   ⟨@state_t.lift σ m _⟩
 
   @[inline] protected def monad_map {σ m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) :
     state_t σ m α → state_t σ m' α :=
-  λ x, ⟨λ st, f (x.run st)⟩
+  λ x s, f (x s)
 
   instance (σ m m') [monad m] [monad m'] : monad_functor m m' (state_t σ m) (state_t σ m') :=
   ⟨@state_t.monad_map σ m m' _ _⟩
 
   @[inline] protected def adapt {σ σ' σ'' α : Type u} {m : Type u → Type v} [monad m] (split : σ → σ' × σ'')
     (join : σ' → σ'' → σ) (x : state_t σ' m α) : state_t σ m α :=
-  ⟨λ st, do let (st, ctx) := split st,
-            (a, st') ← x.run st,
-            pure (a, join st' ctx)⟩
+  λ st, do let (st, ctx) := split st,
+           (a, st') ← x st,
+           pure (a, join st' ctx)
 
   instance (ε) [monad_except ε m] : monad_except ε (state_t σ m) :=
   { throw := λ α, state_t.lift ∘ throw,
-    catch := λ α x c, ⟨λ s, catch (x.run s) (λ e, state_t.run (c e) s)⟩ }
+    catch := λ α x c s, catch (x s) (λ e, c e s) }
 end
 end state_t
 
@@ -162,7 +163,7 @@ instance [monad m] : monad_state_adapter σ σ' (state_t σ m) (state_t σ' m) :
 end
 
 instance (σ : Type u) (m out : Type u → Type v) [functor m] [monad_run out m] : monad_run (λ α, σ → out α) (state_t σ m) :=
-⟨λ α x, run ∘ (λ σ, prod.fst <$> (x.run σ))⟩
+⟨λ α x, run ∘ (λ σ, prod.fst <$> (x σ))⟩
 
 class monad_state_runner (σ : Type u) (m m' : Type u → Type u) :=
 (run_state {} {α : Type u} : m α → σ → m' α)
@@ -175,5 +176,5 @@ instance monad_state_runner_trans {n n' : Type u → Type u} [monad_functor m m'
 ⟨λ α x s, monad_map (λ α (y : m α), (run_state y s : m' α)) x⟩
 
 instance state_t.monad_state_runner [monad m] : monad_state_runner σ (state_t σ m) m :=
-⟨λ α x s, prod.fst <$> x.run s⟩
+⟨λ α x s, prod.fst <$> x s⟩
 end
diff --git a/library/init/io.lean b/library/init/io.lean
index c27a574f50..cafdf1fa34 100644
--- a/library/init/io.lean
+++ b/library/init/io.lean
@@ -47,7 +47,7 @@ open fs
 constant iterate {α β : Type} : α → (α → io (sum α β)) → io β
 
 def iterate_eio {α β : Type} (a : α) (f : α → eio (sum α β)) : eio β :=
-except_t.mk $ iterate a $ λ r, do
+iterate a $ λ r, do
   r ← (f r).run,
   match r with
   | except.ok (sum.inl r) := pure (sum.inl r)
@@ -67,9 +67,8 @@ constant handle.get_line : handle → eio string
 
 def lift_eio {m : Type → Type} {ε α : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m]
   (x : eio α) : m α :=
-do e : except io.error α ← monad_lift x.run, -- uses [monad_io m] instance
-   monad_except.lift_except e                -- uses [monad_except ε m] [has_lift_t io.error ε] instances
-
+do e : except io.error α ← monad_lift (except_t.run x), -- uses [monad_io m] instance
+   monad_except.lift_except e                           -- uses [monad_except ε m] [has_lift_t io.error ε] instances
 end prim
 
 section
@@ -264,7 +263,7 @@ local attribute [reducible] io
     TODO(Leo): replace `state_t io.real_world id` with `io` as soon as we fix inductive_cmd
 -/
 inductive coroutine_io (α δ β: Type) : Type
-| mk    {} : (α → state_t io.real_world id (coroutine_result_core.{0 0 0} coroutine_io α δ β)) → coroutine_io
+| mk    {} : (α → io.real_world → (coroutine_result_core.{0 0 0} coroutine_io α δ β) × io.real_world) → coroutine_io
 
 abbreviation coroutine_result_io (α δ β: Type) : Type :=
 coroutine_result_core.{0 0 0} (coroutine_io α δ β) α δ β
@@ -276,6 +275,9 @@ universes v w r s
 namespace coroutine_io
 variables {α δ β γ : Type}
 
+@[inline] def mk_st {α δ β: Type} (k : α → state_t io.real_world id (coroutine_result_io α δ β)) : coroutine_io α δ β :=
+mk k
+
 export coroutine_result_core (done yielded)
 
 /-- `resume c a` resumes/invokes the coroutine_io `c` with input `a`. -/
@@ -283,16 +285,16 @@ export coroutine_result_core (done yielded)
 | (mk k) a := k a
 
 @[inline] protected def pure (b : β) : coroutine_io α δ β :=
-mk $ λ _, pure (done b)
+mk_st $ λ _, pure $ done b
 
 /-- Read the input argument passed to the coroutine.
     Remark: should we use a different name? I added an instance [monad_reader] later. -/
 @[inline] protected def read : coroutine_io α δ α :=
-mk $ λ a, pure (done a)
+mk_st $ λ a, pure $ done a
 
 /-- Return the control to the invoker with result `d` -/
 @[inline] protected def yield (d : δ) : coroutine_io α δ punit :=
-mk $ λ a : α, pure $ yielded d (coroutine_io.pure ⟨⟩)
+mk_st $ λ (a : α), pure $ yielded d (coroutine_io.pure ⟨⟩)
 
 /-
 TODO(Leo): following relations have been commented because Lean4 is currently
@@ -338,7 +340,7 @@ open well_founded_tactics
 -/
 
 protected def bind : coroutine_io α δ β → (β → coroutine_io α δ γ) → coroutine_io α δ γ
-| (mk k) f := mk $ λ a, k a >>= λ r,
+| (mk k) f := mk_st $ λ a, k a >>= λ r,
     match r, rfl : ∀ (n : _), n = r → _ with
     | done b, _      := coroutine_io.resume (f b) a
     | yielded d c, h :=
@@ -347,7 +349,7 @@ protected def bind : coroutine_io α δ β → (β → coroutine_io α δ γ) 
 --  using_well_founded { dec_tac := unfold_wf_rel *> process_lex (tactic.assumption) }
 
 def pipe : coroutine_io α δ β → coroutine_io δ γ β → coroutine_io α γ β
-| (mk k₁) (mk k₂) := mk $ λ a, do
+| (mk k₁) (mk k₂) := mk_st $ λ a, do
   r ← k₁ a,
   match r, rfl : ∀ (n : _), n = r → _ with
   | done b, h        := pure (done b)
@@ -371,6 +373,6 @@ instance (α δ : Type) : coroutine.monad_coroutine α δ (coroutine_io α δ) :
 { yield  := coroutine_io.yield }
 
 instance : monad_io (coroutine_io α δ) :=
-{ monad_lift := λ _ x, mk (λ _, done <$> x) }
+{ monad_lift := λ _ x, mk_st (λ _, done <$> x) }
 
 end coroutine_io
diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean
index 8bb30d2dc8..48f948e046 100644
--- a/library/init/lean/parser/module.lean
+++ b/library/init/lean/parser/module.lean
@@ -26,7 +26,7 @@ end
 abbreviation module_parser := module_parser_m syntax
 
 instance module_parser_m.lift_basic_parser_m : monad_basic_read module_parser_m :=
-{ monad_lift := λ α x, ⟨λ r, ⟨λ st it, pure (((x.run r).run st) it)⟩⟩ }
+{ monad_lift := λ α x r st it, pure (((x.run r).run st) it) }
 
 @[derive parser.has_view parser.has_tokens]
 def prelude.parser : module_parser :=