refactor(library/tactic): remove dead code, make proof_state a smart pointer, cleanup

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

src/library/tactic/boolean.cpp

@@ -71,6 +71,7 @@ tactic conj_tactic(bool all) {
             }
         });
 }
+
 tactic imp_tactic(name const & H_name, bool all) {
     return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             expr impfn = mk_implies_fn();
@@ -109,6 +110,7 @@ tactic imp_tactic(name const & H_name, bool all) {
             }
         });
 }
+
 tactic conj_hyp_tactic(bool all) {
     return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             expr andfn = mk_and_fn();
@@ -147,9 +149,9 @@ tactic conj_hyp_tactic(bool all) {
                         proof_map new_m(m);
                         for (auto const & info : proof_info) {
                             name const & goal_name     = info.first;
-                            auto const & expanded_hyp = info.second;
+                            auto const & expanded_hyps = info.second;
                             expr pr                    = find(m, goal_name); // proof for the new conclusion
-                            for (auto const & H_name_prop : expanded_hyp) {
+                            for (auto const & H_name_prop : expanded_hyps) {
                                 name const & H_name   = H_name_prop.first;
                                 expr const & H_prop   = H_name_prop.second;
                                 expr const & H_1      = mk_constant(name(H_name, 1));

src/library/tactic/goal.cpp

@@ -44,6 +44,7 @@ format goal::pp(formatter const & fmt, options const & opts) const {
 name goal::mk_unique_hypothesis_name(name const & suggestion) const {
     name n = suggestion;
     unsigned i = 0;
+    // TODO(Leo): investigate if this method is a performance bottleneck
     while (true) {
         bool ok = true;
         for (auto const & p : m_hypotheses) {

src/library/tactic/proof_state.cpp

@@ -11,7 +11,7 @@ namespace lean {
 format proof_state::pp(formatter const & fmt, options const & opts) const {
     format r;
     bool first = true;
-    for (auto const & p : m_goals) {
+    for (auto const & p : get_goals()) {
         if (first)
             first = false;
         else
@@ -21,12 +21,6 @@ format proof_state::pp(formatter const & fmt, options const & opts) const {
     return r;
 }
 
-void swap(proof_state & s1, proof_state & s2) {
-    swap(s1.m_goals, s2.m_goals);
-    swap(s1.m_menv, s2.m_menv);
-    swap(s1.m_proof_builder, s2.m_proof_builder);
-}
-
 static name g_main("main");
 
 proof_state to_proof_state(environment const & env, context const & ctx, expr const & t) {

src/library/tactic/proof_state.h

@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <utility>
+#include <algorithm>
+#include "util/rc.h"
 #include "util/interrupt.h"
 #include "util/optional.h"
 #include "library/tactic/goal.h"
@@ -14,22 +16,32 @@ Author: Leonardo de Moura
 namespace lean {
 typedef list<std::pair<name, goal>> goals;
 class proof_state {
+    struct cell {
+        MK_LEAN_RC();
         goals                       m_goals;
         metavar_env                 m_menv;
         proof_builder               m_proof_builder;
+        void dealloc() { delete this; }
+        cell():m_rc(1) {}
+        cell(goals const & gs, metavar_env const & menv, proof_builder const & p):
+            m_rc(1), m_goals(gs), m_menv(menv), m_proof_builder(p) {}
+    };
+    cell * m_ptr;
 public:
-    proof_state() {}
-    proof_state(list<std::pair<name, goal>> const & gs, metavar_env const & menv, proof_builder const & p):
-        m_goals(gs), m_menv(menv), m_proof_builder(p) {}
-    proof_state(proof_state const & s, goals const & gs, proof_builder const & p):
-        m_goals(gs), m_menv(s.m_menv), m_proof_builder(p) {}
-    friend void swap(proof_state & s1, proof_state & s2);
-    list<std::pair<name, goal>> const & get_goals() const { return m_goals; }
-    metavar_env const & get_menv() const { return m_menv; }
-    proof_builder const & get_proof_builder() const { return m_proof_builder; }
+    proof_state():m_ptr(new cell()) {}
+    proof_state(proof_state const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    proof_state(proof_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+    proof_state(goals const & gs, metavar_env const & menv, proof_builder const & p):m_ptr(new cell(gs, menv, p)) {}
+    proof_state(proof_state const & s, goals const & gs, proof_builder const & p):m_ptr(new cell(gs, s.m_ptr->m_menv, p)) {}
+    ~proof_state() { if (m_ptr) m_ptr->dec_ref(); }
+    friend void swap(proof_state & a, proof_state & b) { std::swap(a.m_ptr, b.m_ptr); }
+    proof_state & operator=(proof_state const & s) { LEAN_COPY_REF(proof_state, s); }
+    proof_state & operator=(proof_state && s) { LEAN_MOVE_REF(proof_state, s); }
+    goals const & get_goals() const { lean_assert(m_ptr); return m_ptr->m_goals; }
+    metavar_env const & get_menv() const { lean_assert(m_ptr); return m_ptr->m_menv; }
+    proof_builder const & get_proof_builder() const { lean_assert(m_ptr); return m_ptr->m_proof_builder; }
     format pp(formatter const & fmt, options const & opts) const;
 };
-void swap(proof_state & s1, proof_state & s2);
 
 proof_state to_proof_state(environment const & env, context const & ctx, expr const & t);
 

src/library/tactic/tactic.cpp

@@ -50,11 +50,11 @@ tactic fail_tactic() {
 }
 
 tactic now_tactic() {
-    return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state_seq {
+    return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             if (!empty(s.get_goals()))
-                return proof_state_seq();
+                return none_proof_state();
             else
-                return to_proof_state_seq(s);
+                return some(s);
         });
 }
 

src/library/tactic/tactic.h

@@ -26,6 +26,16 @@ public:
     virtual proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) const = 0;
 };
 
+template<typename F>
+class tactic_cell_tpl : public tactic_cell {
+    F m_f;
+public:
+    tactic_cell_tpl(F && f):m_f(f) {}
+    virtual proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) const {
+        return m_f(env, io, s);
+    }
+};
+
 class tactic {
 protected:
     tactic_cell * m_ptr;
@@ -44,16 +54,6 @@ public:
     expr solve(environment const & env, io_state const & io, context const & ctx, expr const & t);
 };
 
-template<typename F>
-class simple_tactic_cell : public tactic_cell {
-    F m_f;
-public:
-    simple_tactic_cell(F && f):m_f(f) {}
-    virtual proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) const {
-        return m_f(env, io, s);
-    }
-};
-
 /**
    \brief Create a tactic using the given functor.
    The functor must contain the operator:
@@ -63,7 +63,7 @@ public:
    </code>
 */
 template<typename F>
-tactic mk_tactic(F && f) { return tactic(new simple_tactic_cell<F>(std::forward<F>(f))); }
+tactic mk_tactic(F && f) { return tactic(new tactic_cell_tpl<F>(std::forward<F>(f))); }
 
 template<typename F>
 inline proof_state_seq mk_proof_state_seq(F && f) {
@@ -112,19 +112,6 @@ tactic mk_tactic01(F && f) {
             });
 }
 
-inline proof_state_seq to_proof_state_seq(proof_state const & s) {
-    return mk_proof_state_seq([=]() { return some(mk_pair(s, proof_state_seq())); });
-}
-
-inline proof_state_seq to_proof_state_seq(proof_state_seq::maybe_pair const & p) {
-    lean_assert(p);
-    return mk_proof_state_seq([=]() { return some(mk_pair(p->first, p->second)); });
-}
-
-inline proof_state_seq to_proof_state_seq(proof_state const & s, proof_state_seq const & t) {
-    return mk_proof_state_seq([=]() { return some(mk_pair(s, t)); });
-}
-
 /**
    \brief Return a "do nothing" tactic (aka skip).
 */

src/util/optional.h

@@ -97,8 +97,6 @@ public:
     }
 };
 
-template<typename T>
-optional<T> some(T && t) {
-    return optional<T>(std::forward<T>(t));
-}
+template<typename T> optional<T> some(T const & t) { return optional<T>(t); }
+template<typename T> optional<T> some(T && t) { return optional<T>(std::forward<T>(t)); }
 }