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

feat(frontends/lean/parser): allow the user to use a theorem/axiom name as an argument for the apply tactic command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-05 19:03:12 -08:00
parent c1afefb873
commit 1b176204b4
3 changed files with 38 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -42,6 +42,7 @@ Author: Leonardo de Moura
#include "library/elaborator/elaborator_exception.h"
#include "library/tactic/proof_state.h"
#include "library/tactic/tactic.h"
#include "library/tactic/apply_tactic.h"
#include "frontends/lean/frontend.h"
#include "frontends/lean/frontend_elaborator.h"
#include "frontends/lean/parser.h"
@ -1272,16 +1273,21 @@ class parser::imp {
throw tactic_cmd_error(sstream() << "invalid script-block, it must return a tactic", tac_pos, s);
});
} else {
name tac_name = check_identifier_next("invalid apply command, identifier or 'script-block' expected");
using_script([&](lua_State * L) {
lua_getglobal(L, tac_name.to_string().c_str());
try {
t = to_tactic_ext(L, -1);
} catch (...) {
throw tactic_cmd_error(sstream() << "unknown tactic '" << tac_name << "'", tac_pos, s);
}
lua_pop(L, 1);
});
name n = check_identifier_next("invalid apply command, identifier or 'script-block' expected");
object const & o = m_frontend.find_object(n);
if (o && (o.is_theorem() || o.is_axiom())) {
t = apply_tactic(n);
} else {
using_script([&](lua_State * L) {
lua_getglobal(L, n.to_string().c_str());
try {
t = to_tactic_ext(L, -1);
} catch (...) {
throw tactic_cmd_error(sstream() << "unknown tactic '" << n << "'", tac_pos, s);
}
lua_pop(L, 1);
});
}
}
proof_state_seq::maybe_pair r;
code_with_callbacks([&]() {

6
tests/lean/interactive/t6.lean Normal file
View file

@ -0,0 +1,6 @@
Theorem T1 (a b : Bool) : a => b => a /\ b.
apply imp_tactic.
apply imp_tactic.
apply Conj.
apply assumption_tactic.
done.

16
tests/lean/interactive/t6.lean.expected.out Normal file
View file

@ -0,0 +1,16 @@
Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
# Set: pp::colors
Set: pp::unicode
Proof state:
a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
## Proof state:
H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
## Proof state:
H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
## Proof state:
H::1 : b, H : a, a : Bool, b : Bool ⊢ a
H::1 : b, H : a, a : Bool, b : Bool ⊢ b
## Proof state:
no goals
## Proved: T1
#