max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/control): do not use unnecessary structures

Browse source 
It confuses the compiler.
This commit is contained in:
Leonardo de Moura 2018-09-19 15:22:19 -07:00
parent 28877282ce
commit 5ff9e24b17
6 changed files with 86 additions and 78 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
library/init/control/except.lean
View file

@ -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⟩

29
library/init/control/option.lean
View file

@ -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

33
library/init/control/reader.lean
View file

@ -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

39
library/init/control/state.lean
View file

@ -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

24
library/init/io.lean
View file

@ -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

2
library/init/lean/parser/module.lean
View file

@ -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 :=