refactor(library/tactic): move 'unfold' tactic to separate module

src/library/tactic/CMakeLists.txt

@@ -1,5 +1,5 @@
-add_library(tactic goal.cpp proof_state.cpp tactic.cpp
+add_library(tactic goal.cpp proof_state.cpp tactic.cpp elaborate.cpp
 apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp
-exact_tactic.cpp expr_to_tactic.cpp elaborate.cpp init_module.cpp)
+exact_tactic.cpp unfold_tactic.cpp expr_to_tactic.cpp init_module.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/expr_to_tactic.cpp

@@ -339,14 +339,6 @@ void initialize_expr_to_tactic() {
                      [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
     register_unary_tac(repeat_tac_name,
                        [](tactic const & t1) { return repeat(t1); });
-    register_tac(name(*g_tactic_name, "unfold"),
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
-                     expr id = get_app_fn(app_arg(e));
-                     if (!is_constant(id))
-                         return fail_tactic();
-                     else
-                         return unfold_tactic(const_name(id));
-                 });
     register_unary_num_tac(name(*g_tactic_name, "at_most"),
                            [](tactic const & t, unsigned k) { return take(t, k); });
     register_unary_num_tac(name(*g_tactic_name, "discard"),

src/library/tactic/init_module.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/tactic/intros_tactic.h"
 #include "library/tactic/trace_tactic.h"
 #include "library/tactic/exact_tactic.h"
+#include "library/tactic/unfold_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -21,9 +22,11 @@ void initialize_tactic_module() {
     initialize_intros_tactic();
     initialize_trace_tactic();
     initialize_exact_tactic();
+    initialize_unfold_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_unfold_tactic();
     finalize_exact_tactic();
     finalize_trace_tactic();
     finalize_intros_tactic();

src/library/tactic/tactic.cpp

@@ -16,7 +16,6 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
-#include "library/replace_visitor.h"
 #include "library/kernel_bindings.h"
 #include "library/tactic/tactic.h"
 #include "library/io_state_stream.h"
@@ -239,110 +238,6 @@ tactic focus(tactic const & t, unsigned i) {
         });
 }
 
-class unfold_core_fn : public replace_visitor {
-protected:
-    bool m_unfolded;
-
-    virtual expr visit_app(expr const & e) {
-        expr const & f = get_app_fn(e);
-        if (is_constant(f)) {
-            expr new_f = visit(f);
-            bool modified = new_f != f;
-            buffer<expr> new_args;
-            get_app_args(e, new_args);
-            for (unsigned i = 0; i < new_args.size(); i++) {
-                expr arg    = new_args[i];
-                new_args[i] = visit(arg);
-                if (!modified && new_args[i] != arg)
-                    modified = true;
-            }
-            if (is_lambda(new_f)) {
-                std::reverse(new_args.begin(), new_args.end());
-                return apply_beta(new_f, new_args.size(), new_args.data());
-            } else if (modified) {
-                return mk_app(new_f, new_args);
-            } else {
-                return e;
-            }
-        } else {
-            return replace_visitor::visit_app(e);
-        }
-    }
-public:
-    unfold_core_fn():m_unfolded(false) {}
-    bool unfolded() const { return m_unfolded; }
-};
-
-class unfold_fn : public unfold_core_fn {
-protected:
-    name const &              m_name;
-    level_param_names const & m_ps;
-    expr const &              m_def;
-
-    virtual expr visit_constant(expr const & c) {
-        if (const_name(c) == m_name) {
-            m_unfolded = true;
-            return instantiate_univ_params(m_def, m_ps, const_levels(c));
-        } else {
-            return c;
-        }
-    }
-
-public:
-    unfold_fn(name const & n, level_param_names const & ps, expr const & d):m_name(n), m_ps(ps), m_def(d) {}
-};
-
-class unfold_all_fn : public unfold_core_fn {
-protected:
-    environment m_env;
-
-    virtual expr visit_constant(expr const & c) {
-        optional<declaration> d = m_env.find(const_name(c));
-        if (d && d->is_definition() && (!d->is_opaque() || d->get_module_idx() == 0)) {
-            m_unfolded = true;
-            return instantiate_value_univ_params(*d, const_levels(c));
-        } else {
-            return c;
-        }
-    }
-
-public:
-    unfold_all_fn(environment const & env):m_env(env) {}
-};
-
-optional<proof_state> unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) {
-    bool reduced = false;
-    goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
-            expr new_meta = fn(g.get_meta());
-            expr new_type = fn(g.get_type());
-            if (new_meta != g.get_meta() || new_type != g.get_type())
-                reduced = true;
-            return some(goal(new_meta, new_type));
-        });
-    if (reduced) {
-        return some(proof_state(s, new_gs));
-    } else {
-        return none_proof_state();
-    }
-}
-
-tactic unfold_tactic(name const & n) {
-    return tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
-            optional<declaration> d = env.find(n);
-            if (!d || !d->is_definition() || (d->is_opaque() && d->get_module_idx() != 0))
-                return none_proof_state(); // tactic failed
-            unfold_fn fn(n, d->get_univ_params(), d->get_value());
-            return unfold_tactic_core(fn, s);
-        });
-}
-
-tactic unfold_tactic() {
-    return tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
-            unfold_all_fn fn(env);
-            return unfold_tactic_core(fn, s);
-        });
-}
-
 DECL_UDATA(proof_state_seq)
 static const struct luaL_Reg proof_state_seq_m[] = {
     {"__gc",            proof_state_seq_gc}, // never throws
@@ -464,13 +359,6 @@ static int mk_id_tactic(lua_State * L)          {  return push_tactic(L, id_tact
 static int mk_now_tactic(lua_State * L)         {  return push_tactic(L, now_tactic()); }
 static int mk_fail_tactic(lua_State * L)        {  return push_tactic(L, fail_tactic()); }
 static int mk_assumption_tactic(lua_State * L)  {  return push_tactic(L, assumption_tactic()); }
-static int mk_unfold_tactic(lua_State * L)      {
-    int nargs = lua_gettop(L);
-    if (nargs == 0)
-        return push_tactic(L, unfold_tactic());
-    else
-        return push_tactic(L, unfold_tactic(to_name_ext(L, 1)));
-}
 static int mk_beta_tactic(lua_State * L) {  return push_tactic(L, beta_tactic()); }
 static const struct luaL_Reg tactic_m[] = {
     {"__gc",            tactic_gc}, // never throws
@@ -510,7 +398,6 @@ void open_tactic(lua_State * L) {
     SET_GLOBAL_FUN(mk_now_tactic,         "now_tac");
     SET_GLOBAL_FUN(mk_fail_tactic,        "fail_tac");
     SET_GLOBAL_FUN(mk_assumption_tactic,  "assumption_tac");
-    SET_GLOBAL_FUN(mk_unfold_tactic,      "unfold_tac");
     SET_GLOBAL_FUN(mk_beta_tactic,        "beta_tac");
     SET_GLOBAL_FUN(mk_lua_tactic01,       "tactic01");
 

src/library/tactic/tactic.h

@@ -129,10 +129,6 @@ inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_
 */
 tactic focus(tactic const & t, unsigned i);
 inline tactic focus(tactic const & t) { return focus(t, 1); }
-/** \brief Return a tactic that unfolds the definition named \c n. */
-tactic unfold_tactic(name const & n);
-/** \brief Return a tactic that unfolds all (non-opaque) definitions. */
-tactic unfold_tactic();
 /** \brief Return a tactic that applies beta-reduction. */
 tactic beta_tactic();
 

src/library/tactic/unfold_tactic.cpp

@@ -0,0 +1,129 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/instantiate.h"
+#include "library/replace_visitor.h"
+#include "library/tactic/unfold_tactic.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+class unfold_core_fn : public replace_visitor {
+protected:
+    bool m_unfolded;
+
+    virtual expr visit_app(expr const & e) {
+        expr const & f = get_app_fn(e);
+        if (is_constant(f)) {
+            expr new_f = visit(f);
+            bool modified = new_f != f;
+            buffer<expr> new_args;
+            get_app_args(e, new_args);
+            for (unsigned i = 0; i < new_args.size(); i++) {
+                expr arg    = new_args[i];
+                new_args[i] = visit(arg);
+                if (!modified && new_args[i] != arg)
+                    modified = true;
+            }
+            if (is_lambda(new_f)) {
+                std::reverse(new_args.begin(), new_args.end());
+                return apply_beta(new_f, new_args.size(), new_args.data());
+            } else if (modified) {
+                return mk_app(new_f, new_args);
+            } else {
+                return e;
+            }
+        } else {
+            return replace_visitor::visit_app(e);
+        }
+    }
+public:
+    unfold_core_fn():m_unfolded(false) {}
+    bool unfolded() const { return m_unfolded; }
+};
+
+class unfold_fn : public unfold_core_fn {
+protected:
+    name const &              m_name;
+    level_param_names const & m_ps;
+    expr const &              m_def;
+
+    virtual expr visit_constant(expr const & c) {
+        if (const_name(c) == m_name) {
+            m_unfolded = true;
+            return instantiate_univ_params(m_def, m_ps, const_levels(c));
+        } else {
+            return c;
+        }
+    }
+
+public:
+    unfold_fn(name const & n, level_param_names const & ps, expr const & d):m_name(n), m_ps(ps), m_def(d) {}
+};
+
+class unfold_all_fn : public unfold_core_fn {
+protected:
+    environment m_env;
+
+    virtual expr visit_constant(expr const & c) {
+        optional<declaration> d = m_env.find(const_name(c));
+        if (d && d->is_definition() && (!d->is_opaque() || d->get_module_idx() == 0)) {
+            m_unfolded = true;
+            return instantiate_value_univ_params(*d, const_levels(c));
+        } else {
+            return c;
+        }
+    }
+
+public:
+    unfold_all_fn(environment const & env):m_env(env) {}
+};
+
+optional<proof_state> unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) {
+    bool reduced = false;
+    goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
+            expr new_meta = fn(g.get_meta());
+            expr new_type = fn(g.get_type());
+            if (new_meta != g.get_meta() || new_type != g.get_type())
+                reduced = true;
+            return some(goal(new_meta, new_type));
+        });
+    if (reduced) {
+        return some(proof_state(s, new_gs));
+    } else {
+        return none_proof_state();
+    }
+}
+
+tactic unfold_tactic(name const & n) {
+    return tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
+            optional<declaration> d = env.find(n);
+            if (!d || !d->is_definition() || (d->is_opaque() && d->get_module_idx() != 0))
+                return none_proof_state(); // tactic failed
+            unfold_fn fn(n, d->get_univ_params(), d->get_value());
+            return unfold_tactic_core(fn, s);
+        });
+}
+
+tactic unfold_tactic() {
+    return tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
+            unfold_all_fn fn(env);
+            return unfold_tactic_core(fn, s);
+        });
+}
+
+void initialize_unfold_tactic() {
+    register_tac(name({"tactic", "unfold"}),
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     expr id = get_app_fn(app_arg(e));
+                     if (!is_constant(id))
+                         return fail_tactic();
+                     else
+                         return unfold_tactic(const_name(id));
+                 });
+}
+void finalize_unfold_tactic() {
+}
+}

src/library/tactic/unfold_tactic.h

@@ -0,0 +1,18 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/tactic/tactic.h"
+
+namespace lean {
+/** \brief Return a tactic that unfolds the definition named \c n. */
+tactic unfold_tactic(name const & n);
+/** \brief Return a tactic that unfolds all (non-opaque) definitions. */
+tactic unfold_tactic();
+
+void initialize_unfold_tactic();
+void finalize_unfold_tactic();
+}