diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 2f83b18f8..0d690d136 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include +#include #include "util/name_set.h" #include "util/buffer.h" #include "kernel/for_each_fn.h" @@ -18,6 +19,28 @@ namespace lean { goal::goal(list> const & h, expr const & c):m_hypotheses(h), m_conclusion(c) {} +format goal::pp(formatter const & fmt, options const & opts) const { + unsigned indent = get_pp_indent(opts); + bool unicode = get_pp_unicode(opts); + format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); + buffer> tmp; + to_buffer(m_hypotheses, tmp); + bool first = true; + format r; + for (auto const & p : tmp) { + if (first) { + first = false; + } else { + r += compose(comma(), line()); + } + r += format{format(p.first), space(), colon(), nest(indent, compose(line(), fmt(p.second, opts)))}; + } + + r = group(r); + r += format{line(), turnstile, space(), nest(indent, fmt(m_conclusion, opts))}; + return group(r); +} + goal_proof_fn::goal_proof_fn(std::vector && consts): m_constants(consts) { } @@ -56,7 +79,7 @@ static name mk_unique_name(name_set & s, name const & suggestion) { std::pair to_goal(environment const & env, context const & ctx, expr const & t) { type_inferer inferer(env); - if (!inferer.is_proposition(t)) + if (!inferer.is_proposition(t, ctx)) throw exception("to goal failed, type is not a proposition"); name_set used_names = collect_used_names(ctx, t); buffer entries; @@ -103,6 +126,7 @@ std::pair to_goal(environment const & env, context const & } } expr conclusion = replacer(t); + std::reverse(consts.begin(), consts.end()); return mk_pair(goal(reverse_to_list(hypotheses.begin(), hypotheses.end()), conclusion), goal_proof_fn(std::move(consts))); } diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index d8fa4300c..1cad7bebc 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include "util/list.h" #include "util/name.h" +#include "kernel/formatter.h" #include "kernel/expr.h" #include "kernel/context.h" #include "kernel/environment.h" @@ -23,6 +24,7 @@ public: list> const & get_hypotheses() const { return m_hypotheses; } expr const & get_conclusion() const { return m_conclusion; } operator bool() const { return m_conclusion; } + format pp(formatter const & fmt, options const & opts) const; }; /** diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index a9c2b4d8c..9b486baed 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -9,6 +9,19 @@ Author: Leonardo de Moura #include "library/tactic/proof_state.h" namespace lean { +format proof_state::pp(formatter const & fmt, options const & opts) const { + format r; + bool first = true; + for (auto const & p : m_goals) { + if (first) + first = false; + else + r += line(); + r += group(format{format(p.first), colon(), line(), p.second.pp(fmt, opts)}); + } + return r; +} + void swap(proof_state & s1, proof_state & s2) { swap(s1.m_goals, s2.m_goals); swap(s1.m_menv, s2.m_menv); diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 2590b8477..a1b61d32b 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -28,6 +28,7 @@ public: metavar_env const & get_menv() const { return m_menv; } proof_builder const & get_proof_builder() const { return m_proof_builder; } justification_builder const & get_justification_builder() const { return m_justification_builder; } + format pp(formatter const & fmt, options const & opts) const; }; void swap(proof_state & s1, proof_state & s2); diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 9ac99f167..279d96a8e 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -48,6 +48,18 @@ tactic & tactic::operator=(tactic && s) { LEAN_MOVE_REF(tactic, s); } +expr tactic::solve(environment const & env, io_state const & io, proof_state const & s) { + tactic_result_ref r = operator()(s); + proof_state_ref final = r->next(env, io); + if (!final) + throw tactic_exception("tactic did not produce any result"); + if (!empty(final->get_goals())) + throw tactic_exception("tactic did not solve all goals"); + assignment a(final->get_menv()); + proof_map m; + return final->get_proof_builder()(m, env, a); +} + class then_tactic : public tactic_cell { tactic m_t1; tactic m_t2; diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index d11014876..ede5b3453 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -56,6 +56,8 @@ public: tactic & operator=(tactic && s); tactic_result_ref operator()(proof_state const & s) { return m_ptr->operator()(s); } + + expr solve(environment const & env, io_state const & io, proof_state const & s); }; template @@ -89,7 +91,6 @@ public: } }; - template tactic mk_tactic(F && f) { return tactic(new simple_tactic_cell(std::forward(f))); } diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index 668ac7343..d49081946 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -16,6 +16,7 @@ using namespace lean; static void tst1() { environment env; + io_state io(options(), mk_simple_formatter()); import_all(env); env.add_var("p", Bool); env.add_var("q", Bool); @@ -24,10 +25,10 @@ static void tst1() { context ctx; ctx = extend(ctx, "H1", p); ctx = extend(ctx, "H2", q); - // proof_state s1 = to_proof_state(env, ctx, mk_var(0)); - // tactic t = then(assumption_tactic(), now_tactic()); - // tactic_result_ref r = t(s1); - // proof_state_ref s2 = r->next(); + proof_state s = to_proof_state(env, ctx, p); + std::cout << s.pp(mk_simple_formatter(), options()) << "\n"; + tactic t = then(assumption_tactic(), now_tactic()); + std::cout << "proof: " << t.solve(env, io, s) << "\n"; } int main() {