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

src/frontends/lean/builtin_exprs.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/expr_to_tactic.h"
+#include "library/tactic/exact_tactic.h"
 #include "library/typed_expr.h"
 #include "library/choice.h"
 #include "library/let.h"

src/library/tactic/CMakeLists.txt

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

src/library/tactic/exact_tactic.cpp

@@ -0,0 +1,50 @@
+/*
+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/type_checker.h"
+#include "library/tactic/tactic.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+tactic exact_tactic(expr const & _e) {
+    return tactic01([=](environment const & env, io_state const &, proof_state const & s) {
+            type_checker tc(env);
+            substitution subst  = s.get_subst();
+            goals const & gs    = s.get_goals();
+            goal const & g      = head(gs);
+            expr e              = subst.instantiate(_e);
+            auto e_t_cs         = tc.infer(e);
+            expr e_t            = subst.instantiate(e_t_cs.first);
+            expr t              = subst.instantiate(g.get_type());
+            auto dcs            = tc.is_def_eq(e_t, t);
+            if (dcs.first && !dcs.second && !e_t_cs.second) {
+                expr new_p = g.abstract(e);
+                check_has_no_local(new_p, _e, "exact");
+                subst.assign(g.get_name(), new_p);
+                return some(proof_state(s, tail(gs), subst));
+            } else {
+                return none_proof_state();
+            }
+        });
+}
+
+static expr * g_exact_tac_fn      = nullptr;
+
+expr const & get_exact_tac_fn() { return *g_exact_tac_fn; }
+
+void initialize_exact_tactic() {
+    name exact_tac_name({"tactic", "exact"});
+    g_exact_tac_fn      = new expr(Const(exact_tac_name));
+    register_tac(exact_tac_name,
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     // TODO(Leo): use elaborate_fn
+                     return exact_tactic(app_arg(e));
+                 });
+}
+void finalize_exact_tactic() {
+    delete g_exact_tac_fn;
+}
+}

src/library/tactic/exact_tactic.h

@@ -0,0 +1,16 @@
+/*
+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 {
+expr const & get_exact_tac_fn();
+/** \brief Solve first goal iff it is definitionally equal to type of \c e */
+tactic exact_tactic(expr const & e);
+void initialize_exact_tactic();
+void finalize_exact_tactic();
+}

src/library/tactic/expr_to_tactic.cpp

@@ -17,7 +17,6 @@ Author: Leonardo de Moura
 #include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
-static expr * g_exact_tac_fn      = nullptr;
 static expr * g_and_then_tac_fn   = nullptr;
 static expr * g_or_else_tac_fn    = nullptr;
 static expr * g_id_tac_fn         = nullptr;
@@ -26,7 +25,6 @@ static expr * g_determ_tac_fn     = nullptr;
 static expr * g_tac_type          = nullptr;
 static expr * g_builtin_tac       = nullptr;
 static expr * g_fixpoint_tac      = nullptr;
-expr const & get_exact_tac_fn() { return *g_exact_tac_fn; }
 expr const & get_and_then_tac_fn() { return *g_and_then_tac_fn; }
 expr const & get_or_else_tac_fn() { return *g_or_else_tac_fn; }
 expr const & get_id_tac_fn() { return *g_id_tac_fn; }
@@ -303,14 +301,12 @@ void initialize_expr_to_tactic() {
                                 });
 
     name builtin_tac_name(*g_tactic_name, "builtin");
-    name exact_tac_name(*g_tactic_name, "exact");
     name and_then_tac_name(*g_tactic_name, "and_then");
     name or_else_tac_name(*g_tactic_name, "or_else");
     name repeat_tac_name(*g_tactic_name, "repeat");
     name fixpoint_name(*g_tactic_name, "fixpoint");
     name determ_tac_name(*g_tactic_name, "determ");
     name id_tac_name(*g_tactic_name, "id");
-    g_exact_tac_fn      = new expr(Const(exact_tac_name));
     g_and_then_tac_fn   = new expr(Const(and_then_tac_name));
     g_or_else_tac_fn    = new expr(Const(or_else_tac_name));
     g_id_tac_fn         = new expr(Const(id_tac_name));
@@ -342,11 +338,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(exact_tac_name,
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
-                     // TODO(Leo): use elaborate_fn
-                     return exact_tactic(app_arg(e));
-                 });
     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));
@@ -381,7 +372,6 @@ void finalize_expr_to_tactic() {
     delete g_or_else_tac_fn;
     delete g_and_then_tac_fn;
     delete g_id_tac_fn;
-    delete g_exact_tac_fn;
     delete g_tactic_macros;
     delete g_map;
     delete g_tactic_name;

src/library/tactic/expr_to_tactic.h

@@ -41,7 +41,6 @@ bool is_by(expr const & t);
 expr const & get_by_arg(expr const & t);
 
 expr const & get_tactic_type();
-expr const & get_exact_tac_fn();
 expr const & get_and_then_tac_fn();
 expr const & get_or_else_tac_fn();
 expr const & get_id_tac_fn();

src/library/tactic/init_module.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/tactic/rename_tactic.h"
 #include "library/tactic/intros_tactic.h"
 #include "library/tactic/trace_tactic.h"
+#include "library/tactic/exact_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -19,9 +20,11 @@ void initialize_tactic_module() {
     initialize_rename_tactic();
     initialize_intros_tactic();
     initialize_trace_tactic();
+    initialize_exact_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_exact_tactic();
     finalize_trace_tactic();
     finalize_intros_tactic();
     finalize_rename_tactic();

src/library/tactic/tactic.cpp

@@ -200,28 +200,6 @@ tactic assumption_tactic() {
         });
 }
 
-tactic exact_tactic(expr const & _e) {
-    return tactic01([=](environment const & env, io_state const &, proof_state const & s) {
-            type_checker tc(env);
-            substitution subst  = s.get_subst();
-            goals const & gs    = s.get_goals();
-            goal const & g      = head(gs);
-            expr e              = subst.instantiate(_e);
-            auto e_t_cs         = tc.infer(e);
-            expr e_t            = subst.instantiate(e_t_cs.first);
-            expr t              = subst.instantiate(g.get_type());
-            auto dcs            = tc.is_def_eq(e_t, t);
-            if (dcs.first && !dcs.second && !e_t_cs.second) {
-                expr new_p = g.abstract(e);
-                check_has_no_local(new_p, _e, "exact");
-                subst.assign(g.get_name(), new_p);
-                return some(proof_state(s, tail(gs), subst));
-            } else {
-                return none_proof_state();
-            }
-        });
-}
-
 tactic beta_tactic() {
     return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             bool reduced = false;

src/library/tactic/tactic.h

@@ -134,8 +134,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 Solve first goal iff it is definitionally equal to \c e */
-tactic exact_tactic(expr const & e);
 /** \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. */