feat(library/tactic): add pretty printer for goal and proof_state objects, add solve method for tactics, add trivial example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/tactic/goal.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <utility>
 #include <vector>
+#include <algorithm>
 #include "util/name_set.h"
 #include "util/buffer.h"
 #include "kernel/for_each_fn.h"
@@ -18,6 +19,28 @@ namespace lean {
 
 goal::goal(list<std::pair<name, expr>> 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<std::pair<name, expr>> 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<expr> && consts):
     m_constants(consts) {
 }
@@ -56,7 +79,7 @@ static name mk_unique_name(name_set & s, name const & suggestion) {
 
 std::pair<goal, goal_proof_fn> 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<context_entry> entries;
@@ -103,6 +126,7 @@ std::pair<goal, goal_proof_fn> 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)));
 }

src/library/tactic/goal.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <vector>
 #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<std::pair<name, expr>> 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;
 };
 
 /**

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);

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);
 

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;

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<typename F>
@@ -89,7 +91,6 @@ public:
     }
 };
 
-
 template<typename F>
 tactic mk_tactic(F && f) { return tactic(new simple_tactic_cell<F>(std::forward<F>(f))); }
 

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() {