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

refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement rename tactic

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-22 15:29:53 -07:00
parent 5e15ac0c92
commit 9a316092d1
4 changed files with 17 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/tools/tactic.lean
View file

@ -43,7 +43,8 @@ opaque definition beta : tactic := builtin
inductive expr : Type :=
builtin : expr
opaque definition apply (e : expr) : tactic := builtin
opaque definition apply (e : expr) : tactic := builtin
opaque definition rename (a b : expr) : tactic := builtin
opaque definition unfold {B : Type} (b : B) : tactic := builtin
opaque definition exact {B : Type} (b : B) : tactic := builtin

8
src/frontends/lean/builtin_tactics.cpp
View file

@ -6,7 +6,6 @@ Author: Leonardo de Moura
*/
#include <limits>
#include "library/explicit.h"
#include "library/tactic/rename_tactic.h"
#include "library/tactic/intros_tactic.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/parse_table.h"
@ -17,12 +16,6 @@ namespace lean {
using notation::transition;
using notation::mk_ext_action;
static expr parse_rename(parser & p, unsigned, expr const *, pos_info const & pos) {
name from = p.check_id_next("invalid 'rename' tactic, identifier expected");
name to = p.check_id_next("invalid 'rename' tactic, identifier expected");
return p.save_pos(mk_rename_tactic_macro(from, to), pos);
}
static expr parse_intros(parser & p, unsigned, expr const *, pos_info const & pos) {
buffer<name> ns;
while (p.curr_is_identifier()) {
@ -34,7 +27,6 @@ static expr parse_intros(parser & p, unsigned, expr const *, pos_info const & po
void init_nud_tactic_table(parse_table & r) {
expr x0 = mk_var(0);
r = r.add({transition("rename", mk_ext_action(parse_rename))}, x0);
r = r.add({transition("intros", mk_ext_action(parse_intros))}, x0);
}

2
src/frontends/lean/token_table.cpp
View file

@ -76,7 +76,7 @@ void init_token_table(token_table & t) {
{".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
{"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"local", 0},
{"rename", 0}, {"intros", 0}, {nullptr, 0}};
{"intros", 0}, {nullptr, 0}};
char const * commands[] =
{"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion",

19
src/library/tactic/rename_tactic.cpp
View file

@ -49,15 +49,24 @@ expr mk_rename_tactic_macro(name const & from, name const & to) {
return mk_tactic_macro(*g_rename_tactic_name, 2, args);
}
static name const & get_rename_arg(expr const & _e) {
check_tactic_expr(_e, "invalid 'rename' tactic, arguments must be identifiers");
expr const & e = get_tactic_expr_expr(_e);
if (is_constant(e))
return const_name(e);
else if (is_local(e))
return local_pp_name(e);
else
throw expr_to_tactic_exception(e, "invalid 'rename' tactic, arguments must be identifiers");
}
void initialize_rename_tactic() {
g_rename_tactic_name = new name({"tactic", "rename"});
auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
check_macro_args(e, 2, "invalid 'rename' tactic, it must have two arguments");
if (!is_constant(macro_arg(e, 0)) || !is_constant(macro_arg(e, 1)))
throw expr_to_tactic_exception(e, "invalid 'rename' tactic, arguments must be identifiers");
return rename_tactic(const_name(macro_arg(e, 0)), const_name(macro_arg(e, 1)));
return rename_tactic(get_rename_arg(app_arg(app_fn(e))),
get_rename_arg(app_arg(e)));
};
register_tactic_macro(*g_rename_tactic_name, fn);
register_tac(*g_rename_tactic_name, fn);
}
void finalize_rename_tactic() {