From ead827d6b7d4ce3308668bc658998cf25286a472 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Oct 2014 17:13:41 -0700 Subject: [PATCH] feat(frontends/lean): add `!` operator the "dual" of `@`, closes #220 --- src/frontends/lean/builtin_exprs.cpp | 13 +++++++++++++ src/frontends/lean/elaborator.cpp | 13 ++++++++++++- src/frontends/lean/token_table.cpp | 2 +- src/library/explicit.cpp | 20 ++++++++++++++----- src/library/explicit.h | 29 ++++++++++++++++++++-------- tests/lean/run/consume.lean | 11 +++++++++++ 6 files changed, 73 insertions(+), 15 deletions(-) create mode 100644 tests/lean/run/consume.lean diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 2c7ff3198..b3c2bbc3e 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -340,6 +340,18 @@ static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info con } } +static expr parse_consume_args_expr(parser & p, unsigned, expr const *, pos_info const & pos) { + expr e = p.parse_expr(get_max_prec()); + if (is_choice(e)) { + buffer new_choices; + for (unsigned i = 0; i < get_num_choices(e); i++) + new_choices.push_back(p.save_pos(mk_consume_args(get_choice(e, i)), pos)); + return p.save_pos(mk_choice(new_choices.size(), new_choices.data()), pos); + } else { + return p.save_pos(mk_consume_args(e), pos); + } +} + static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info const & pos) { buffer locals; while (!p.curr_is_token(get_comma_tk())) { @@ -400,6 +412,7 @@ parse_table init_nud_table() { r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0); r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0); r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0); + r = r.add({transition("!", mk_ext_action(parse_consume_args_expr))}, x0); r = r.add({transition("begin", mk_ext_action(parse_begin_end))}, x0); r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0); r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d226b03ba..0a297989c 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -781,7 +781,14 @@ public: } else if (is_typed_expr(e)) { return visit_typed_expr(e, cs); } else if (is_implicit(e)) { + // ignore annotation return visit_core(get_implicit_arg(e), cs); + } else if (is_consume_args(e)) { + // ignore annotation + return visit_core(get_consume_args_arg(e), cs); + } else if (is_explicit(e)) { + // ignore annotation + return visit_core(get_explicit_arg(e), cs); } else if (is_sorry(e)) { return visit_sorry(e); } else { @@ -819,11 +826,15 @@ public: } else if (is_explicit(get_app_fn(e))) { r = visit_core(e, cs); } else { + bool consume_args = false; if (is_implicit(e)) { r = get_implicit_arg(e); if (is_explicit(r)) r = get_explicit_arg(r); b = r; r = visit_core(r, cs); + } else if (is_consume_args(e)) { + consume_args = true; + r = visit_core(get_consume_args_arg(e), cs); } else { r = visit_core(e, cs); } @@ -831,7 +842,7 @@ public: expr r_type = whnf(infer_type(r, cs), cs); expr imp_arg; bool is_strict = true; - while (is_pi(r_type) && binding_info(r_type).is_implicit()) { + while (is_pi(r_type) && (consume_args || binding_info(r_type).is_implicit())) { imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs); r = mk_app(r, imp_arg, g); r_type = whnf(instantiate(binding_body(r_type), imp_arg), cs); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index b0debf4d1..008c66f78 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -72,7 +72,7 @@ void init_token_table(token_table & t) { {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0}, {"by", 0}, {"then", 0}, {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, - {"Type'", g_max_prec}, {"using", 0}, {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, + {"Type'", g_max_prec}, {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, diff --git a/src/library/explicit.cpp b/src/library/explicit.cpp index 3162b885a..2cbe4a917 100644 --- a/src/library/explicit.cpp +++ b/src/library/explicit.cpp @@ -13,32 +13,42 @@ namespace lean { static name * g_explicit_name = nullptr; static name * g_implicit_name = nullptr; static name * g_as_is_name = nullptr; +static name * g_consume_args_name = nullptr; expr mk_explicit(expr const & e) { return mk_annotation(*g_explicit_name, e); } bool is_explicit(expr const & e) { return is_annotation(e, *g_explicit_name); } bool is_nested_explicit(expr const & e) { return is_nested_annotation(e, *g_explicit_name); } +expr const & get_explicit_arg(expr const & e) { lean_assert(is_explicit(e)); return get_annotation_arg(e); } + expr mk_as_is(expr const & e) { return mk_annotation(*g_as_is_name, e); } bool is_as_is(expr const & e) { return is_annotation(e, *g_as_is_name); } +expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return get_annotation_arg(e); } + expr mk_implicit(expr const & e) { return mk_annotation(*g_implicit_name, e); } bool is_implicit(expr const & e) { return is_annotation(e, *g_implicit_name); } -expr const & get_explicit_arg(expr const & e) { lean_assert(is_explicit(e)); return get_annotation_arg(e); } -expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return get_annotation_arg(e); } expr const & get_implicit_arg(expr const & e) { lean_assert(is_implicit(e)); return get_annotation_arg(e); } +expr mk_consume_args(expr const & e) { return mk_annotation(*g_consume_args_name, e); } +bool is_consume_args(expr const & e) { return is_annotation(e, *g_consume_args_name); } +expr const & get_consume_args_arg(expr const & e) { lean_assert(is_consume_args(e)); return get_annotation_arg(e); } + void initialize_explicit() { - g_explicit_name = new name("@"); - g_implicit_name = new name("@^-1"); - g_as_is_name = new name("as_is"); + g_explicit_name = new name("@"); + g_implicit_name = new name("@^-1"); + g_as_is_name = new name("as_is"); + g_consume_args_name = new name("!"); register_annotation(*g_explicit_name); register_annotation(*g_implicit_name); register_annotation(*g_as_is_name); + register_annotation(*g_consume_args_name); } void finalize_explicit() { delete g_as_is_name; delete g_implicit_name; delete g_explicit_name; + delete g_consume_args_name; } static int mk_explicit(lua_State * L) { return push_expr(L, mk_explicit(to_expr(L, 1))); } diff --git a/src/library/explicit.h b/src/library/explicit.h index 7d7ffcdc3..4e8f3fc2b 100644 --- a/src/library/explicit.h +++ b/src/library/explicit.h @@ -17,30 +17,43 @@ expr mk_explicit(expr const & e); bool is_explicit(expr const & e); /** \brief See #is_nested_annotation */ bool is_nested_explicit(expr const & e); +/** \brief Return the argument of an explicit expression. + \pre is_explicit(e) +*/ +expr const & get_explicit_arg(expr const & e); + /** \brief Create an explicit expression that is accepted as is by the elaborator. */ expr mk_as_is(expr const & e); /** \brief Return true iff \c e was created with mk_as_is. */ bool is_as_is(expr const & e); +/** \brief Return the argument of an expression created using mk_as_is. + \pre is_as_is(e) +*/ +expr const & get_as_is_arg(expr const & e); + /** \brief Create an implicit expression '@^-1 f'. This only affects the elaborator behavior. This expression "cancels" the effect of '@' */ expr mk_implicit(expr const & e); /** \brief Return true iff \c e is an implicit expression. */ bool is_implicit(expr const & e); -/** \brief Return the argument of an explicit expression. - \pre is_explicit(e) -*/ -expr const & get_explicit_arg(expr const & e); -/** \brief Return the argument of an expression created using mk_as_is. - \pre is_as_is(e) -*/ -expr const & get_as_is_arg(expr const & e); /** \brief Return the argument of an implicit expression. \pre is_implicit(e) */ expr const & get_implicit_arg(expr const & e); + +/** \brief Create the expression '! e'. + This only affects the elaborator behavior. + It instructs the elaborator to keep adding '_' + for \c e arguments. +*/ +expr mk_consume_args(expr const & e); +/** \brief Return true iff \c e is an '!f' expression. */ +bool is_consume_args(expr const & e); +expr const & get_consume_args_arg(expr const & e); + void open_explicit(lua_State * L); void initialize_explicit(); void finalize_explicit(); diff --git a/tests/lean/run/consume.lean b/tests/lean/run/consume.lean new file mode 100644 index 000000000..0df1adee3 --- /dev/null +++ b/tests/lean/run/consume.lean @@ -0,0 +1,11 @@ +import logic + +definition pr2 {A : Type} (a b : A) := a + +check pr2 +check !pr2 +check !@pr2 +check @pr2 +check @!pr2 +check @@pr2 +check !!pr2