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

feat(library/tactic/apply_tactic): allow apply_tac Lua binding to take expressions as argument

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-24 16:03:16 -08:00
parent 6cc57cc4b5
commit 75cf751959
3 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1391,8 +1391,7 @@ class parser::imp {
next();
expr pr = parse_expr();
check_rparen_next("invalid apply command, ')' expected");
expr pr_type = m_env->infer_type(pr);
return ::lean::apply_tactic(pr, pr_type);
return ::lean::apply_tactic(pr);
} else {
name n = check_identifier_next("invalid apply command, identifier, '(' expr ')', or 'script-block' expected");
optional<object> o = m_env->find_object(n);

9
src/library/tactic/apply_tactic.cpp
View file

@ -143,8 +143,9 @@ static optional<proof_state> apply_tactic(ro_environment const & env, proof_stat
}
}
tactic apply_tactic(expr const & th, expr const & th_type, bool all) {
tactic apply_tactic(expr const & th, bool all) {
return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
expr th_type = type_inferer(env)(th, context(), s.get_menv().copy());
return apply_tactic(env, s, th, th_type, all);
});
}
@ -161,7 +162,11 @@ tactic apply_tactic(name const & th_name, bool all) {
int mk_apply_tactic(lua_State * L) {
int nargs = lua_gettop(L);
return push_tactic(L, apply_tactic(to_name_ext(L, 1), nargs >= 2 ? lua_toboolean(L, 2) : true));
bool all = nargs >= 2 ? lua_toboolean(L, 2) : true;
if (is_expr(L, 1))
return push_tactic(L, apply_tactic(to_expr(L, 1), all));
else
return push_tactic(L, apply_tactic(to_name_ext(L, 1), all));
}
void open_apply_tactic(lua_State * L) {

2
src/library/tactic/apply_tactic.h
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include "library/tactic/tactic.h"
namespace lean {
tactic apply_tactic(expr const & th, expr const & th_type, bool all = true);
tactic apply_tactic(expr const & th, bool all = true);
tactic apply_tactic(name const & th_name, bool all = true);
void open_apply_tactic(lua_State * L);
}