refactor(library/tactic): add auxiliary module 'library/tactic/elaborate'

src/frontends/lua/register_modules.cpp

@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include "util/numerics/register_module.h"
 #include "util/sexpr/register_module.h"
 #include "library/register_module.h"
-// #include "library/simplifier/register_module.h"
 #include "library/tactic/register_module.h"
 #include "frontends/lean/register_module.h"
 
@@ -17,7 +16,6 @@ void register_modules() {
     register_numerics_module();
     register_sexpr_module();
     register_core_module();
-    // register_simplifier_module();
     register_tactic_module();
     register_frontend_lean_module();
 }

src/library/reducible.h

@@ -35,7 +35,7 @@ bool is_reducible_off(environment const & env, name const & n);
 
 /** \brief Create a type checker that takes the "reducibility" hints into account. */
 std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
-                                              bool relax_main_opaque, bool only_main_reducible = false);
+                                              bool relax_main_opaque = true, bool only_main_reducible = false);
 std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible = false);
 
 void initialize_reducible();

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
-exact_tactic.cpp expr_to_tactic.cpp init_module.cpp)
+exact_tactic.cpp expr_to_tactic.cpp elaborate.cpp init_module.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/apply_tactic.cpp

@@ -19,8 +19,8 @@ Author: Leonardo de Moura
 #include "library/occurs.h"
 #include "library/metavar_closure.h"
 #include "library/type_util.h"
-#include "library/tactic/apply_tactic.h"
 #include "library/tactic/expr_to_tactic.h"
+#include "library/tactic/apply_tactic.h"
 
 namespace lean {
 /**

src/library/tactic/apply_tactic.h

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "util/lua.h"
-#include "library/tactic/tactic.h"
+#include "library/tactic/elaborate.h"
 namespace lean {
 tactic apply_tactic(elaborate_fn const & fn, expr const & e, bool rev_goals = false, bool relax_main_opaque = true);
 tactic eassumption_tactic(bool relax_main_opaque = true);

src/library/tactic/elaborate.cpp

@@ -0,0 +1,35 @@
+/*
+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 "library/unifier.h"
+#include "library/tactic/elaborate.h"
+
+namespace lean {
+optional<expr> elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab,
+                                         proof_state & s, expr const & e) {
+    name_generator ngen = s.get_ngen();
+    substitution subst  = s.get_subst();
+    goals const & gs    = s.get_goals();
+    if (empty(gs))
+        return none_expr();
+    auto ecs = elab(head(gs), ngen.mk_child(), e);
+    expr new_e = ecs.first;
+    buffer<constraint> cs;
+    to_buffer(ecs.second, cs);
+    to_buffer(s.get_postponed(), cs);
+    unifier_config cfg(ios.get_options());
+    unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), subst, cfg);
+    if (auto p = rseq.pull()) {
+        substitution new_subst     = p->first.first;
+        constraints  new_postponed = p->first.second;
+        new_e = new_subst.instantiate(new_e);
+        s = proof_state(gs, new_subst, ngen, new_postponed);
+        return some_expr(new_e);
+    } else {
+        return none_expr();
+    }
+}
+}

src/library/tactic/elaborate.h

@@ -0,0 +1,28 @@
+/*
+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 Function for elaborating expressions nested in tactics.
+    Some tactics contain nested expression (aka pre-terms) that need to be elaborated.
+*/
+typedef std::function<pair<expr, constraints>(goal const &, name_generator const &, expr const &)> elaborate_fn;
+
+/** \brief Try to elaborate expression \c e using the elaboration function \c elab. The elaboration is performed
+    with respect to (local context of) the first goal in \c s. The constraints generated during elaboration
+    are solved using the higher-order unifier. When solving the constraints any postponed constraint in \c s
+    is also considered. Only the first solution returned by the unifier is considered.
+    If the whole process succeeds, then the elaborated expression is returned, and the proof state is updated.
+    The following fields in the name generator may be updated: name-generator and substitution.
+
+    If the proof state has no goal, the elaboration or unifier fails, then none is returned and the proof state
+    is not modified.
+*/
+optional<expr> elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab,
+                                         proof_state & s, expr const & e);
+}

src/library/tactic/exact_tactic.cpp

@@ -5,42 +5,29 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/type_checker.h"
-#include "library/unifier.h"
 #include "library/reducible.h"
 #include "library/tactic/tactic.h"
+#include "library/tactic/elaborate.h"
 #include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
 tactic exact_tactic(elaborate_fn const & elab, expr const & e) {
     return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
-            name_generator ngen = s.get_ngen();
+            proof_state new_s = s;
-            substitution subst  = s.get_subst();
+            if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e)) {
-            goals const & gs    = s.get_goals();
+                name_generator ngen = new_s.get_ngen();
-            if (empty(gs))
+                substitution subst  = new_s.get_subst();
-                return none_proof_state();
+                goals const & gs    = new_s.get_goals();
-            goal const & g      = head(gs);
+                goal const & g      = head(gs);
-            expr       new_e;
+                auto tc     = mk_type_checker(env, ngen.mk_child());
-            buffer<constraint> cs;
+                auto e_t_cs = tc->infer(*new_e);
-            auto ecs = elab(g, ngen.mk_child(), e);
+                expr t      = subst.instantiate(g.get_type());
-            new_e    = ecs.first;
-            to_buffer(ecs.second, cs);
-            to_buffer(s.get_postponed(), cs);
-            unifier_config cfg(ios.get_options());
-            unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), subst, cfg);
-            if (auto p = rseq.pull()) {
-                substitution new_subst     = p->first.first;
-                constraints  new_postponed = p->first.second;
-                new_e = new_subst.instantiate(new_e);
-                bool relax_main_opaque = true;
-                auto tc     = mk_type_checker(env, ngen.mk_child(), relax_main_opaque);
-                auto e_t_cs = tc->infer(new_e);
-                expr t      = new_subst.instantiate(g.get_type());
                 auto dcs    = tc->is_def_eq(e_t_cs.first, t);
                 if (dcs.first && !dcs.second && !e_t_cs.second) {
-                    expr new_p = g.abstract(new_e);
+                    expr new_p = g.abstract(*new_e);
                     check_has_no_local(new_p, e, "exact");
-                    new_subst.assign(g.get_name(), new_p);
+                    subst.assign(g.get_name(), new_p);
-                    return some(proof_state(tail(gs), new_subst, ngen, new_postponed));
+                    return some(proof_state(new_s, tail(gs), subst, ngen));
                 }
             }
             return none_proof_state();
@@ -48,9 +35,7 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e) {
 }
 
 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));

src/library/tactic/expr_to_tactic.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/pos_info_provider.h"
 #include "library/tactic/tactic.h"
+#include "library/tactic/elaborate.h"
 
 namespace lean {
 /**

src/library/tactic/proof_state.h

@@ -22,10 +22,12 @@ class proof_state {
     constraints      m_postponed;
 public:
     proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed);
+    proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen):
+        proof_state(gs, subst, ngen, s.m_postponed) {}
     proof_state(proof_state const & s, goals const & gs, substitution const & subst):
-        proof_state(gs, subst, s.m_ngen, s.m_postponed) {}
+        proof_state(s, gs, subst, s.m_ngen) {}
     proof_state(proof_state const & s, goals const & gs, name_generator const & ngen):
-        proof_state(gs, s.m_subst, ngen, s.m_postponed) {}
+        proof_state(s, gs, s.m_subst, ngen) {}
     proof_state(proof_state const & s, goals const & gs):
         proof_state(s, gs, s.m_subst) {}
     proof_state(proof_state const & s, name_generator const & ngen):

src/library/tactic/tactic.h

@@ -14,11 +14,6 @@ Author: Leonardo de Moura
 #include "library/tactic/proof_state.h"
 
 namespace lean {
-/** \brief Function for elaborating expressions nested in tactics.
-    Some tactics contain nested expression (aka pre-terms) that need to be elaborated.
-*/
-typedef std::function<pair<expr, constraints>(goal const &, name_generator const &, expr const &)> elaborate_fn;
-
 /** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */
 void check_has_no_local(expr const & v, expr const & e, char const * tac_name);