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

feat(frontends/lean/parse): allow script-code blocks to be used in the apply command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-28 21:48:30 -08:00
parent 67def8da21
commit 5dfb3b8b56
4 changed files with 85 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1052,23 +1052,39 @@ class parser::imp {
std::vector<lazy_list<proof_state>> stack;
while (true) {
auto p = pos();
name id = check_identifier_next("invalid tactic, identifier expected");
if (!curr_is_identifier()) {
diagnostic(m_frontend) << "current state:\n" << s << endl;
throw parser_error("invalid tactic, identifier expected", p);
}
name id = curr_name();
next();
if (id == g_apply) {
auto tac_name_pos = pos();
name tac_name = check_identifier_next("invalid apply command, identifier expected");
auto tac_pos = pos();
optional<tactic> t;
m_script_state->apply([&](lua_State * L) {
lua_getglobal(L, tac_name.to_string().c_str());
if (lua_type(L, -1) != LUA_TFUNCTION && !is_tactic(L, -1))
throw parser_error(sstream() << "unknown tactic '" << tac_name << "'", tac_name_pos);
if (lua_type(L, -1) == LUA_TFUNCTION) {
pcall(L, 0, 1, 0);
if (!is_tactic(L, -1))
throw parser_error(sstream() << "invalid function '" << tac_name << "', it does not return a tactic", tac_name_pos);
}
t = to_tactic(L, -1);
lua_pop(L, 1);
});
if (curr() == scanner::token::ScriptBlock) {
parse_script();
m_script_state->apply([&](lua_State * L) {
if (is_tactic(L, -1))
t = to_tactic(L, -1);
else
throw parser_error(sstream() << "invalid script-block, it must return a tactic", tac_pos);
});
} else {
name tac_name = check_identifier_next("invalid apply command, identifier or 'script-block' expected");
m_script_state->apply([&](lua_State * L) {
lua_getglobal(L, tac_name.to_string().c_str());
if (lua_type(L, -1) != LUA_TFUNCTION && !is_tactic(L, -1))
throw parser_error(sstream() << "unknown tactic '" << tac_name << "'", tac_pos);
if (lua_type(L, -1) == LUA_TFUNCTION) {
pcall(L, 0, 1, 0);
if (!is_tactic(L, -1))
throw parser_error(sstream() << "invalid function '" << tac_name << "', it does not return a tactic",
tac_pos);
}
t = to_tactic(L, -1);
lua_pop(L, 1);
});
}
lazy_list<proof_state> seq = (*t)(m_frontend, m_frontend.get_state(), s);
auto r = seq.pull();
if (r) {
@ -1076,7 +1092,7 @@ class parser::imp {
stack.push_back(r->second);
} else {
diagnostic(m_frontend) << "current state:\n" << s << endl;
throw parser_error(sstream() << "tactic '" << tac_name << "' failed", tac_name_pos);
throw parser_error(sstream() << "tactic failed", tac_pos);
}
} else if (id == g_done) {
if (s.is_proof_final_state()) {
@ -1098,6 +1114,8 @@ class parser::imp {
check_period_next("invalid theorem, '.' expected before tactical proof");
if (is_metavar(val)) {
// simple case
if (!m_type_inferer.is_proposition(type))
throw exception("failed to synthesize metavar, its type is not a proposition");
proof_state s = to_proof_state(m_frontend, context(), type);
return parse_tactic(s);
} else {
@ -1527,7 +1545,8 @@ class parser::imp {
regular(m_frontend) << "Available options:" << endl;
for (auto p : get_option_declarations()) {
auto opt = p.second;
regular(m_frontend) << " " << opt.get_name() << " (" << opt.kind() << ") " << opt.get_description() << " (default: " << opt.get_default_value() << ")" << endl;
regular(m_frontend) << " " << opt.get_name() << " (" << opt.kind() << ") "
<< opt.get_description() << " (default: " << opt.get_default_value() << ")" << endl;
}
} else {
throw parser_error("invalid help command", m_last_cmd_pos);

2
tests/lean/elab1.lean.expected.out
View file

@ -135,7 +135,7 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
Assumed: a
Assumed: b
Assumed: H
Error (line: 20, pos: 28) unexpected metavariable occurrence
Error (line: 22, pos: 0) failed to synthesize metavar, its type is not a proposition
Failed to solve
⊢ b ≈ a
Substitution

30
tests/lean/tactic2.lean Normal file
View file

@ -0,0 +1,30 @@
Variables p q r : Bool
Theorem T1 : p => q => p /\ q :=
Discharge (fun H1,
Discharge (fun H2,
let H1 : p := _,
H2 : q := _
in Conj H1 H2
)).
apply assumption_tactic (* solve first metavar *)
done
apply assumption_tactic (* solve second metavar *)
done
(**
simple_tac = REPEAT(imp_tactic() ^ conj_tactic() ^ assumption_tactic())
**)
Theorem T2 : p => q => p /\ q /\ p := _.
apply simple_tac
done
Show Environment 1
Theorem T3 : p => p /\ q => r => q /\ r /\ p := _.
apply (** return REPEAT(imp_tactic() ^ conj_tactic() ^ conj_hyp_tactic() ^ assumption_tactic()) **)
done
(* Display proof term generated by previous tactic *)
Show Environment 1

18
tests/lean/tactic2.lean.expected.out Normal file
View file

@ -0,0 +1,18 @@
Set: pp::colors
Set: pp::unicode
Assumed: p
Assumed: q
Assumed: r
Proved: T1
Proved: T2
Theorem T2 : p ⇒ q ⇒ p ∧ q ∧ p := Discharge (λ H : p, Discharge (λ H::1 : q, Conj H (Conj H::1 H)))
Proved: T3
Theorem T3 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
Discharge
(λ H : p,
Discharge
(λ H::1 : p ∧ q,
Discharge
(λ H::2 : r,
Conj (let H::1::2 := Conjunct2 H::1 in H::1::2)
(Conj H::2 (let H::1::1 := Conjunct1 H::1 in H::1::1)))))