michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/tactic/constructor_tactic): allow 'constructor' tactic without index

Browse source 
see issue #500
This commit is contained in:
Leonardo de Moura 2015-04-30 21:13:27 -07:00
parent 15e52b06df
commit 2d9c950144
11 changed files with 136 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
hott/init/tactic.hlean
View file

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

10
library/init/tactic.lean
View file

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

23
src/frontends/lean/parser.cpp
View file

@ -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<expr> vals = get_mpz_notation(m_env, n);
list<expr> 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);

3
src/frontends/lean/parser.h
View file

@ -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<expr> 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<expr> const & args, pos_info const & p);

12
src/library/constants.cpp
View file

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

3
src/library/constants.h
View file

@ -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();

3
src/library/constants.txt
View file

@ -39,6 +39,9 @@ not
num
num.zero
num.pos
option
option.some
option.none
or
or.elim
or.intro_left

92
src/library/tactic/constructor_tactic.cpp
View file

@ -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<unsigned> num_constructors, list<expr> const & given_args) {
tactic constructor_tactic(elaborate_fn const & elab, optional<unsigned> _i, optional<unsigned> num_constructors, list<expr> 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<unsig
<< "but it does not have " << *num_constructors << " constructor(s)");
return proof_state_seq();
}
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();
}
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<unsig
void initialize_constructor_tactic() {
register_tac(name{"tactic", "constructor"},
[](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
unsigned i = get_unsigned_arg(tc, e, 0);
auto i = get_optional_unsigned(tc, app_arg(e));
return constructor_tactic(fn, i, optional<unsigned>(), list<expr>());
});
register_tac(name{"tactic", "split"},
[](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
return constructor_tactic(fn, 1, optional<unsigned>(1), list<expr>());
return constructor_tactic(fn, optional<unsigned>(1), optional<unsigned>(1), list<expr>());
});
register_tac(name{"tactic", "left"},
[](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
return constructor_tactic(fn, 1, optional<unsigned>(2), list<expr>());
return constructor_tactic(fn, optional<unsigned>(1), optional<unsigned>(2), list<expr>());
});
register_tac(name{"tactic", "right"},
[](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
return constructor_tactic(fn, 2, optional<unsigned>(2), list<expr>());
return constructor_tactic(fn, optional<unsigned>(2), optional<unsigned>(2), list<expr>());
});
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<unsigned>(1), list<expr>(arg));
return constructor_tactic(fn, optional<unsigned>(1), optional<unsigned>(1), list<expr>(arg));
});
}

35
src/library/tactic/expr_to_tactic.cpp
View file

@ -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<mpz> 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<expr> args;
get_app_args(e, args);
if (i >= args.size())
throw expr_to_tactic_exception(e, "invalid tactic, insufficient number of arguments");
optional<mpz> 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<unsigned> 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<unsigned>(get_unsigned(tc, app_arg(e), e));
} else if (const_name(get_app_fn(e)) == get_option_none_name()) {
return optional<unsigned>();
}
}
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) {

1
src/library/tactic/expr_to_tactic.h
View file

@ -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<unsigned> get_optional_unsigned(type_checker & tc, expr const & e);
expr const & get_tactic_expr_type();
expr const & get_tactic_identifier_type();

7
tests/lean/run/constr_tac3.lean Normal file
View file

@ -0,0 +1,7 @@
open nat
example (n m : ℕ) (H : n < m) : n < succ m :=
begin
constructor,
exact H
end