From 16558bf082467e64a021eab51b2a978a6bec7fd3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 9 Mar 2017 10:28:59 +0100 Subject: [PATCH] refactor(library,library): rename pre_monad to has_bind --- library/init/category/monad.lean | 16 +++++++------- src/frontends/lean/builtin_cmds.cpp | 2 +- src/frontends/lean/tactic_notation.cpp | 4 ++-- src/library/compiler/erase_irrelevant.cpp | 2 +- src/library/constants.cpp | 24 ++++++++++----------- src/library/constants.h | 6 +++--- src/library/constants.txt | 6 +++--- tests/lean/elab3.lean.expected.out | 4 ++-- tests/lean/run/check_constants.lean | 6 +++--- tests/lean/type_class_bug.lean.expected.out | 6 +++--- 10 files changed, 38 insertions(+), 38 deletions(-) diff --git a/library/init/category/monad.lean b/library/init/category/monad.lean index 7de9980012..63403fc6cb 100644 --- a/library/init/category/monad.lean +++ b/library/init/category/monad.lean @@ -7,19 +7,19 @@ prelude import init.category.applicative universes u v -class pre_monad (m : Type u → Type v) := +class has_bind (m : Type u → Type v) := (bind : Π {α β : Type u}, m α → (α → m β) → m β) -@[inline] def bind {m : Type u → Type v} [pre_monad m] {α β : Type u} : m α → (α → m β) → m β := -pre_monad.bind +@[inline] def bind {m : Type u → Type v} [has_bind m] {α β : Type u} : m α → (α → m β) → m β := +has_bind.bind -@[inline] def pre_monad.and_then {α β : Type u} {m : Type u → Type v} [pre_monad m] (x : m α) (y : m β) : m β := +@[inline] def has_bind.and_then {α β : Type u} {m : Type u → Type v} [has_bind m] (x : m α) (y : m β) : m β := do x, y infixl ` >>= `:2 := bind -infixl ` >> `:2 := pre_monad.and_then +infixl ` >> `:2 := has_bind.and_then -class monad (m : Type u → Type v) extends applicative m, pre_monad m : Type (max u+1 v) := +class monad (m : Type u → Type v) extends applicative m, has_bind m : Type (max u+1 v) := (seq := λ α β f x, bind f $ λ f, bind x $ λ x, pure (f x)) -- implied by `seq`, but a bit simpler (map := λ α β f x, bind x $ λ x, pure (f x)) @@ -27,6 +27,6 @@ class monad (m : Type u → Type v) extends applicative m, pre_monad m : Type (m def return {m : Type u → Type v} [monad m] {α : Type u} : α → m α := pure -/- Identical to pre_monad.and_then, but it is not inlined. -/ -def pre_monad.seq {α β : Type u} {m : Type u → Type v} [pre_monad m] (x : m α) (y : m β) : m β := +/- Identical to has_bind.and_then, but it is not inlined. -/ +def has_bind.seq {α β : Type u} {m : Type u → Type v} [has_bind m] (x : m α) (y : m β) : m β := do x, y diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index bbd8a49c14..4b68d12e3a 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -533,7 +533,7 @@ static environment run_command_cmd(parser & p) { metavar_context mctx; expr tactic = p.parse_expr(); expr try_triv = mk_app(mk_constant(get_tactic_try_name()), mk_constant(get_tactic_triv_name())); - tactic = mk_app(mk_constant(get_pre_monad_and_then_name()), tactic, try_triv); + tactic = mk_app(mk_constant(get_has_bind_and_then_name()), tactic, try_triv); expr val = mk_typed_expr(mk_true(), mk_by(tactic)); bool check_unassigned = false; elaborate(env, opts, "_run_command", mctx, local_context(), val, check_unassigned); diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index 11dfd5c91f..ff8139ff8e 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -114,7 +114,7 @@ static expr mk_tactic_solve1(parser & p, expr tac, pos_info const & pos, name co } static expr concat(parser & p, expr const & tac1, expr const & tac2, pos_info const & pos) { - return p.save_pos(mk_app(mk_constant(get_pre_monad_seq_name()), tac1, tac2), pos); + return p.save_pos(mk_app(mk_constant(get_has_bind_seq_name()), tac1, tac2), pos); } static optional is_auto_quote_tactic(parser & p, name const & tac_class) { @@ -526,7 +526,7 @@ expr parse_auto_quote_tactic_block(parser & p, unsigned, expr const *, pos_info p.next(); expr next = parse_tactic(p, tac_class, use_rstep, report_error); erase_quoted_terms_pos_info(p, next); - r = p.mk_app({p.save_pos(mk_constant(get_pre_monad_and_then_name()), pos), r, next}, pos); + r = p.mk_app({p.save_pos(mk_constant(get_has_bind_and_then_name()), pos), r, next}, pos); } p.check_token_next(get_rbracket_tk(), "invalid auto-quote tactic block, ']' expected"); return r; diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index 49d8c104f6..13cacc3f8e 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -418,7 +418,7 @@ class erase_irrelevant_fn : public compiler_step_visitor { return visit_quot_mk(args); } else if (n == get_subtype_rec_name()) { return visit_subtype_rec(args); - } else if (n == get_monad_bind_name() || n == get_pre_monad_bind_name()) { + } else if (n == get_monad_bind_name() || n == get_has_bind_bind_name()) { return visit_monad_bind(e, args); } else if (n == get_applicative_pure_name()) { return visit_applicative_pure(e, args); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index f04e501764..0327060cc4 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -82,6 +82,9 @@ name const * g_funext = nullptr; name const * g_ge = nullptr; name const * g_gt = nullptr; name const * g_has_add = nullptr; +name const * g_has_bind_bind = nullptr; +name const * g_has_bind_and_then = nullptr; +name const * g_has_bind_seq = nullptr; name const * g_has_div = nullptr; name const * g_has_mul = nullptr; name const * g_has_inv = nullptr; @@ -296,9 +299,6 @@ name const * g_pprod_snd = nullptr; name const * g_propext = nullptr; name const * g_pexpr = nullptr; name const * g_pexpr_subst = nullptr; -name const * g_pre_monad_bind = nullptr; -name const * g_pre_monad_and_then = nullptr; -name const * g_pre_monad_seq = nullptr; name const * g_to_pexpr = nullptr; name const * g_quot_mk = nullptr; name const * g_quot_lift = nullptr; @@ -457,6 +457,9 @@ void initialize_constants() { g_ge = new name{"ge"}; g_gt = new name{"gt"}; g_has_add = new name{"has_add"}; + g_has_bind_bind = new name{"has_bind", "bind"}; + g_has_bind_and_then = new name{"has_bind", "and_then"}; + g_has_bind_seq = new name{"has_bind", "seq"}; g_has_div = new name{"has_div"}; g_has_mul = new name{"has_mul"}; g_has_inv = new name{"has_inv"}; @@ -671,9 +674,6 @@ void initialize_constants() { g_propext = new name{"propext"}; g_pexpr = new name{"pexpr"}; g_pexpr_subst = new name{"pexpr", "subst"}; - g_pre_monad_bind = new name{"pre_monad", "bind"}; - g_pre_monad_and_then = new name{"pre_monad", "and_then"}; - g_pre_monad_seq = new name{"pre_monad", "seq"}; g_to_pexpr = new name{"to_pexpr"}; g_quot_mk = new name{"quot", "mk"}; g_quot_lift = new name{"quot", "lift"}; @@ -833,6 +833,9 @@ void finalize_constants() { delete g_ge; delete g_gt; delete g_has_add; + delete g_has_bind_bind; + delete g_has_bind_and_then; + delete g_has_bind_seq; delete g_has_div; delete g_has_mul; delete g_has_inv; @@ -1047,9 +1050,6 @@ void finalize_constants() { delete g_propext; delete g_pexpr; delete g_pexpr_subst; - delete g_pre_monad_bind; - delete g_pre_monad_and_then; - delete g_pre_monad_seq; delete g_to_pexpr; delete g_quot_mk; delete g_quot_lift; @@ -1208,6 +1208,9 @@ name const & get_funext_name() { return *g_funext; } name const & get_ge_name() { return *g_ge; } name const & get_gt_name() { return *g_gt; } name const & get_has_add_name() { return *g_has_add; } +name const & get_has_bind_bind_name() { return *g_has_bind_bind; } +name const & get_has_bind_and_then_name() { return *g_has_bind_and_then; } +name const & get_has_bind_seq_name() { return *g_has_bind_seq; } name const & get_has_div_name() { return *g_has_div; } name const & get_has_mul_name() { return *g_has_mul; } name const & get_has_inv_name() { return *g_has_inv; } @@ -1422,9 +1425,6 @@ name const & get_pprod_snd_name() { return *g_pprod_snd; } name const & get_propext_name() { return *g_propext; } name const & get_pexpr_name() { return *g_pexpr; } name const & get_pexpr_subst_name() { return *g_pexpr_subst; } -name const & get_pre_monad_bind_name() { return *g_pre_monad_bind; } -name const & get_pre_monad_and_then_name() { return *g_pre_monad_and_then; } -name const & get_pre_monad_seq_name() { return *g_pre_monad_seq; } name const & get_to_pexpr_name() { return *g_to_pexpr; } name const & get_quot_mk_name() { return *g_quot_mk; } name const & get_quot_lift_name() { return *g_quot_lift; } diff --git a/src/library/constants.h b/src/library/constants.h index 9686747dc4..331197b463 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -84,6 +84,9 @@ name const & get_funext_name(); name const & get_ge_name(); name const & get_gt_name(); name const & get_has_add_name(); +name const & get_has_bind_bind_name(); +name const & get_has_bind_and_then_name(); +name const & get_has_bind_seq_name(); name const & get_has_div_name(); name const & get_has_mul_name(); name const & get_has_inv_name(); @@ -298,9 +301,6 @@ name const & get_pprod_snd_name(); name const & get_propext_name(); name const & get_pexpr_name(); name const & get_pexpr_subst_name(); -name const & get_pre_monad_bind_name(); -name const & get_pre_monad_and_then_name(); -name const & get_pre_monad_seq_name(); name const & get_to_pexpr_name(); name const & get_quot_mk_name(); name const & get_quot_lift_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index ce39a6b84c..4a85613d35 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -77,6 +77,9 @@ funext ge gt has_add +has_bind.bind +has_bind.and_then +has_bind.seq has_div has_mul has_inv @@ -291,9 +294,6 @@ pprod.snd propext pexpr pexpr.subst -pre_monad.bind -pre_monad.and_then -pre_monad.seq to_pexpr quot.mk quot.lift diff --git a/tests/lean/elab3.lean.expected.out b/tests/lean/elab3.lean.expected.out index cd1c0321ec..677f39791a 100644 --- a/tests/lean/elab3.lean.expected.out +++ b/tests/lean/elab3.lean.expected.out @@ -1,5 +1,5 @@ -@pre_monad.and_then.{0 0} unit unit tactic.{0} - (@monad.to_pre_monad.{0 0} tactic.{0} (@interaction_monad.monad.{0} tactic_state)) +@has_bind.and_then.{0 0} unit unit tactic.{0} + (@monad.to_has_bind.{0 0} tactic.{0} (@interaction_monad.monad.{0} tactic_state)) tactic.trace_state tactic.trace_state : tactic.{0} unit diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index 15397175cb..496705efc5 100644 --- a/tests/lean/run/check_constants.lean +++ b/tests/lean/run/check_constants.lean @@ -82,6 +82,9 @@ run_cmd script_check_id `funext run_cmd script_check_id `ge run_cmd script_check_id `gt run_cmd script_check_id `has_add +run_cmd script_check_id `has_bind.bind +run_cmd script_check_id `has_bind.and_then +run_cmd script_check_id `has_bind.seq run_cmd script_check_id `has_div run_cmd script_check_id `has_mul run_cmd script_check_id `has_inv @@ -296,9 +299,6 @@ run_cmd script_check_id `pprod.snd run_cmd script_check_id `propext run_cmd script_check_id `pexpr run_cmd script_check_id `pexpr.subst -run_cmd script_check_id `pre_monad.bind -run_cmd script_check_id `pre_monad.and_then -run_cmd script_check_id `pre_monad.seq run_cmd script_check_id `to_pexpr run_cmd script_check_id `quot.mk run_cmd script_check_id `quot.lift diff --git a/tests/lean/type_class_bug.lean.expected.out b/tests/lean/type_class_bug.lean.expected.out index 8dbe7da59e..39df5d0caf 100644 --- a/tests/lean/type_class_bug.lean.expected.out +++ b/tests/lean/type_class_bug.lean.expected.out @@ -1,13 +1,13 @@ -@bind.{0 0} list.{0} (@monad.to_pre_monad.{0 0} list.{0} list.monad.{0}) nat nat +@bind.{0 0} list.{0} (@monad.to_has_bind.{0 0} list.{0} list.monad.{0}) nat nat (@list.cons.{0} nat (@one.{0} nat nat.has_one) (@list.nil.{0} nat)) (λ (a : nat), @return.{0 0} list.{0} list.monad.{0} nat a) : list.{0} nat -@bind.{0 0} list.{0} (@monad.to_pre_monad.{0 0} list.{0} list.monad.{0}) nat (prod.{0 0} nat nat) +@bind.{0 0} list.{0} (@monad.to_has_bind.{0 0} list.{0} list.monad.{0}) nat (prod.{0 0} nat nat) (@list.cons.{0} nat (@one.{0} nat nat.has_one) (@list.cons.{0} nat (@bit0.{0} nat nat.has_add (@one.{0} nat nat.has_one)) (@list.cons.{0} nat (@bit1.{0} nat nat.has_one nat.has_add (@one.{0} nat nat.has_one)) (@list.nil.{0} nat)))) (λ (a : nat), - @bind.{0 0} list.{0} (@monad.to_pre_monad.{0 0} list.{0} list.monad.{0}) nat (prod.{0 0} nat nat) + @bind.{0 0} list.{0} (@monad.to_has_bind.{0 0} list.{0} list.monad.{0}) nat (prod.{0 0} nat nat) (@list.cons.{0} nat (@bit1.{0} nat nat.has_one nat.has_add (@one.{0} nat nat.has_one)) (@list.cons.{0} nat (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@one.{0} nat nat.has_one))) (@list.nil.{0} nat)))