From 2d9c950144bf3257a2a9d49f31865b4f398f2745 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Apr 2015 21:13:27 -0700 Subject: [PATCH] feat(library/tactic/constructor_tactic): allow 'constructor' tactic without index see issue #500 --- hott/init/tactic.hlean | 10 +-- library/init/tactic.lean | 10 +-- src/frontends/lean/parser.cpp | 23 +++++- src/frontends/lean/parser.h | 3 +- src/library/constants.cpp | 12 +++ src/library/constants.h | 3 + src/library/constants.txt | 3 + src/library/tactic/constructor_tactic.cpp | 92 +++++++++++++---------- src/library/tactic/expr_to_tactic.cpp | 35 ++++++--- src/library/tactic/expr_to_tactic.h | 1 + tests/lean/run/constr_tac3.lean | 7 ++ 11 files changed, 136 insertions(+), 63 deletions(-) create mode 100644 tests/lean/run/constr_tac3.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index d552f8420..c1d90cee1 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -100,11 +100,11 @@ opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := bui opaque definition lettac (id : identifier) (e : expr) : tactic := builtin -opaque definition constructor (k : num) : tactic := builtin -opaque definition existsi (e : expr) : tactic := builtin -opaque definition split : tactic := builtin -opaque definition left : tactic := builtin -opaque definition right : tactic := builtin +opaque definition constructor (k : option num) : tactic := builtin +opaque definition existsi (e : expr) : tactic := builtin +opaque definition split : tactic := builtin +opaque definition left : tactic := builtin +opaque definition right : tactic := builtin definition try (t : tactic) : tactic := or_else t id definition repeat1 (t : tactic) : tactic := and_then t (repeat t) diff --git a/library/init/tactic.lean b/library/init/tactic.lean index d04191452..7c8ed0d72 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -100,11 +100,11 @@ opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := bui opaque definition lettac (id : identifier) (e : expr) : tactic := builtin -opaque definition constructor (k : num) : tactic := builtin -opaque definition existsi (e : expr) : tactic := builtin -opaque definition split : tactic := builtin -opaque definition left : tactic := builtin -opaque definition right : tactic := builtin +opaque definition constructor (k : option num) : tactic := builtin +opaque definition existsi (e : expr) : tactic := builtin +opaque definition split : tactic := builtin +opaque definition left : tactic := builtin +opaque definition right : tactic := builtin definition try (t : tactic) : tactic := or_else t id definition repeat1 (t : tactic) : tactic := and_then t (repeat t) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 2dc6caf63..9c16dcb07 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1223,13 +1223,15 @@ expr parser::parse_id() { return id_to_expr(id, p); } -expr parser::parse_numeral_expr() { +expr parser::parse_numeral_expr(bool user_notation) { auto p = pos(); mpz n = get_num_val().get_numerator(); next(); if (!m_has_num) m_has_num = has_num_decls(m_env); - list vals = get_mpz_notation(m_env, n); + list vals; + if (user_notation) + vals = get_mpz_notation(m_env, n); if (!*m_has_num && !vals) { throw parser_error("numeral cannot be encoded as expression, environment does not contain the type 'num' " "nor notation was defined for the given numeral " @@ -1370,6 +1372,11 @@ static bool is_tactic_opt_identifier_list_type(expr const & e) { return is_constant(e) && const_name(e) == get_tactic_opt_identifier_list_name(); } +static bool is_option_num(expr const & e) { + return is_app(e) && is_constant(app_fn(e)) && const_name(app_fn(e)) == get_option_name() && + is_constant(app_arg(e)) && const_name(app_arg(e)) == get_num_name(); +} + static bool is_tactic_command_type(expr e) { while (is_pi(e)) e = binding_body(e); @@ -1456,6 +1463,16 @@ expr parser::parse_tactic_opt_id_list() { } } +expr parser::parse_tactic_option_num() { + auto p = pos(); + if (curr_is_numeral()) { + expr n = parse_numeral_expr(false); + return mk_app(save_pos(mk_constant(get_option_some_name()), p), n, p); + } else { + return save_pos(mk_constant(get_option_none_name()), p); + } +} + expr parser::parse_tactic_nud() { if (curr_is_identifier()) { auto id_pos = pos(); @@ -1480,6 +1497,8 @@ expr parser::parse_tactic_nud() { r = mk_app(r, parse_tactic_id_list(), id_pos); } else if (is_tactic_opt_identifier_list_type(d)) { r = mk_app(r, parse_tactic_opt_id_list(), id_pos); + } else if (unary && is_option_num(d)) { + r = mk_app(r, parse_tactic_option_num(), id_pos); } else { unsigned prec = unary ? 1 : get_max_prec(); r = mk_app(r, parse_expr(prec), id_pos); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index f417062f3..4d461ed0e 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -194,7 +194,7 @@ class parser { expr parse_nud_notation(); expr parse_led_notation(expr left); expr parse_nud(); - expr parse_numeral_expr(); + expr parse_numeral_expr(bool user_notation = true); expr parse_decimal_expr(); expr parse_string_expr(); expr parse_binder_core(binder_info const & bi, unsigned rbp); @@ -228,6 +228,7 @@ class parser { elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp); optional is_tactic_command(name & id); + expr parse_tactic_option_num(); expr parse_tactic_led(expr left); expr parse_tactic_nud(); expr mk_tactic_expr_list(buffer const & args, pos_info const & p); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 4c738bff8..95aa578b6 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -44,6 +44,9 @@ name const * g_not = nullptr; name const * g_num = nullptr; name const * g_num_zero = nullptr; name const * g_num_pos = nullptr; +name const * g_option = nullptr; +name const * g_option_some = nullptr; +name const * g_option_none = nullptr; name const * g_or = nullptr; name const * g_or_elim = nullptr; name const * g_or_intro_left = nullptr; @@ -166,6 +169,9 @@ void initialize_constants() { g_num = new name{"num"}; g_num_zero = new name{"num", "zero"}; g_num_pos = new name{"num", "pos"}; + g_option = new name{"option"}; + g_option_some = new name{"option", "some"}; + g_option_none = new name{"option", "none"}; g_or = new name{"or"}; g_or_elim = new name{"or", "elim"}; g_or_intro_left = new name{"or", "intro_left"}; @@ -289,6 +295,9 @@ void finalize_constants() { delete g_num; delete g_num_zero; delete g_num_pos; + delete g_option; + delete g_option_some; + delete g_option_none; delete g_or; delete g_or_elim; delete g_or_intro_left; @@ -411,6 +420,9 @@ name const & get_not_name() { return *g_not; } name const & get_num_name() { return *g_num; } name const & get_num_zero_name() { return *g_num_zero; } name const & get_num_pos_name() { return *g_num_pos; } +name const & get_option_name() { return *g_option; } +name const & get_option_some_name() { return *g_option_some; } +name const & get_option_none_name() { return *g_option_none; } name const & get_or_name() { return *g_or; } name const & get_or_elim_name() { return *g_or_elim; } name const & get_or_intro_left_name() { return *g_or_intro_left; } diff --git a/src/library/constants.h b/src/library/constants.h index 842998427..2d2a63eec 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -46,6 +46,9 @@ name const & get_not_name(); name const & get_num_name(); name const & get_num_zero_name(); name const & get_num_pos_name(); +name const & get_option_name(); +name const & get_option_some_name(); +name const & get_option_none_name(); name const & get_or_name(); name const & get_or_elim_name(); name const & get_or_intro_left_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index a5f4703e1..04ee7a80f 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -39,6 +39,9 @@ not num num.zero num.pos +option +option.some +option.none or or.elim or.intro_left diff --git a/src/library/tactic/constructor_tactic.cpp b/src/library/tactic/constructor_tactic.cpp index 4c59a2c35..c1907477d 100644 --- a/src/library/tactic/constructor_tactic.cpp +++ b/src/library/tactic/constructor_tactic.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/lazy_list_fn.h" #include "kernel/instantiate.h" #include "kernel/inductive/inductive.h" #include "library/constants.h" @@ -21,19 +22,14 @@ namespace lean { If \c given_args is provided, then the tactic fixes the given arguments. It creates a subgoal for each remaining argument. */ -tactic constructor_tactic(elaborate_fn const & elab, unsigned _i, optional num_constructors, list const & given_args) { +tactic constructor_tactic(elaborate_fn const & elab, optional _i, optional num_constructors, list const & given_args) { auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) { goals const & gs = s.get_goals(); if (empty(gs)) { throw_no_goal_if_enabled(s); return proof_state_seq(); } - if (_i == 0) { - throw_tactic_exception_if_enabled(s, "invalid 'constructor' tactic, index must be greater than zero"); - return proof_state_seq(); - } constraint_seq cs; - unsigned i = _i - 1; name_generator ngen = s.get_ngen(); auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque()); goal const & g = head(gs); @@ -51,42 +47,58 @@ tactic constructor_tactic(elaborate_fn const & elab, unsigned _i, optional= c_names.size()) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, goal is an inductive datatype, " - << "but it has only " << c_names.size() << " constructor(s)"); - return proof_state_seq(); - } - expr C = mk_constant(c_names[i], const_levels(I)); - unsigned num_params = *inductive::get_num_params(env, const_name(I)); - if (I_args.size() < num_params) - return proof_state_seq(); - proof_state new_s(s, ngen); - C = mk_app(C, num_params, I_args.data()); - expr C_type = tc->whnf(tc->infer(C, cs), cs); - bool report_unassigned = true; - bool enforce_type = true; - for (expr const & arg : given_args) { - if (!is_pi(C_type)) { - throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, " - << "too many arguments have been provided"); + + auto try_constructor = [&](proof_state const & s, unsigned i) { + if (i >= c_names.size()) { + throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, goal is an inductive datatype, " + << "but it has only " << c_names.size() << " constructor(s)"); return proof_state_seq(); } - try { - if (auto new_arg = elaborate_with_respect_to(env, ios, elab, new_s, arg, some_expr(binding_domain(C_type)), - report_unassigned, enforce_type)) { - C = mk_app(C, *new_arg); - C_type = tc->whnf(instantiate(binding_body(C_type), *new_arg), cs); - } else { + expr C = mk_constant(c_names[i], const_levels(I)); + unsigned num_params = *inductive::get_num_params(env, const_name(I)); + if (I_args.size() < num_params) + return proof_state_seq(); + proof_state new_s(s, ngen); + C = mk_app(C, num_params, I_args.data()); + expr C_type = tc->whnf(tc->infer(C, cs), cs); + bool report_unassigned = true; + bool enforce_type = true; + for (expr const & arg : given_args) { + if (!is_pi(C_type)) { + throw_tactic_exception_if_enabled(s, sstream() << "invalid 'constructor' tactic, " + << "too many arguments have been provided"); return proof_state_seq(); } - } catch (exception &) { - if (new_s.report_failure()) - throw; + try { + if (auto new_arg = elaborate_with_respect_to(env, ios, elab, new_s, arg, some_expr(binding_domain(C_type)), + report_unassigned, enforce_type)) { + C = mk_app(C, *new_arg); + C_type = tc->whnf(instantiate(binding_body(C_type), *new_arg), cs); + } else { + return proof_state_seq(); + } + } catch (exception &) { + if (new_s.report_failure()) + throw; + return proof_state_seq(); + } + } + return apply_tactic_core(env, ios, new_s, C, cs); + }; + + if (_i) { + if (*_i == 0) { + throw_tactic_exception_if_enabled(s, "invalid 'constructor' tactic, index must be greater than zero"); return proof_state_seq(); } + return try_constructor(s, *_i - 1); + } else { + proof_state new_s = s.update_report_failure(false); + proof_state_seq r; + for (unsigned i = 0; i < c_names.size(); i++) + r = append(r, try_constructor(new_s, i)); + return r; } - - return apply_tactic_core(env, ios, new_s, C, cs); }; return tactic(fn); } @@ -94,26 +106,26 @@ tactic constructor_tactic(elaborate_fn const & elab, unsigned _i, optional(), list()); }); register_tac(name{"tactic", "split"}, [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { - return constructor_tactic(fn, 1, optional(1), list()); + return constructor_tactic(fn, optional(1), optional(1), list()); }); register_tac(name{"tactic", "left"}, [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { - return constructor_tactic(fn, 1, optional(2), list()); + return constructor_tactic(fn, optional(1), optional(2), list()); }); register_tac(name{"tactic", "right"}, [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) { - return constructor_tactic(fn, 2, optional(2), list()); + return constructor_tactic(fn, optional(2), optional(2), list()); }); register_tac(name{"tactic", "existsi"}, [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { check_tactic_expr(app_arg(e), "invalid 'existsi' tactic, invalid argument"); expr arg = get_tactic_expr_expr(app_arg(e)); - return constructor_tactic(fn, 1, optional(1), list(arg)); + return constructor_tactic(fn, optional(1), optional(1), list(arg)); }); } diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index dd958897e..bc56c3517 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -228,21 +228,36 @@ static name_generator next_name_generator() { return name_generator(name(*g_tmp_prefix, r)); } +unsigned get_unsigned(type_checker & tc, expr const & e, expr const & ref) { + optional k = to_num(e); + if (!k) + k = to_num(tc.whnf(e).first); + if (!k) + throw expr_to_tactic_exception(ref, "invalid tactic, second argument must be a numeral"); + if (!k->is_unsigned_int()) + throw expr_to_tactic_exception(ref, + "invalid tactic, second argument does not fit in " + "a machine unsigned integer"); + return k->get_unsigned_int(); +} + unsigned get_unsigned_arg(type_checker & tc, expr const & e, unsigned i) { buffer args; get_app_args(e, args); if (i >= args.size()) throw expr_to_tactic_exception(e, "invalid tactic, insufficient number of arguments"); - optional k = to_num(args[i]); - if (!k) - k = to_num(tc.whnf(args[1]).first); - if (!k) - throw expr_to_tactic_exception(e, "invalid tactic, second argument must be a numeral"); - if (!k->is_unsigned_int()) - throw expr_to_tactic_exception(e, - "invalid tactic, second argument does not fit in " - "a machine unsigned integer"); - return k->get_unsigned_int(); + return get_unsigned(tc, args[i], e); +} + +optional get_optional_unsigned(type_checker & tc, expr const & e) { + if (is_app(e) && is_constant(get_app_fn(e))) { + if (const_name(get_app_fn(e)) == get_option_some_name()) { + return optional(get_unsigned(tc, app_arg(e), e)); + } else if (const_name(get_app_fn(e)) == get_option_none_name()) { + return optional(); + } + } + throw expr_to_tactic_exception(e, "invalid tactic, argument is not an option num"); } tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index cd64260d7..e8782f1bb 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -30,6 +30,7 @@ tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr con name const & get_tactic_name(); unsigned get_unsigned_arg(type_checker & tc, expr const & e, unsigned i); +optional get_optional_unsigned(type_checker & tc, expr const & e); expr const & get_tactic_expr_type(); expr const & get_tactic_identifier_type(); diff --git a/tests/lean/run/constr_tac3.lean b/tests/lean/run/constr_tac3.lean new file mode 100644 index 000000000..fe33067c5 --- /dev/null +++ b/tests/lean/run/constr_tac3.lean @@ -0,0 +1,7 @@ +open nat + +example (n m : ℕ) (H : n < m) : n < succ m := +begin + constructor, + exact H +end