feat(frontends/lean): remove build_tactic_cmds, and use expressions for representing tactics

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

library/standard/standard.lean

@@ -0,0 +1 @@
+import logic tactic

library/standard/tactic.lean

@@ -1,6 +1,5 @@
 import logic
 
-namespace tactic
 -- This is just a trick to embed the 'tactic language' as a
 -- Lean expression. We should view (tactic A) as automation
 -- that when execute produces a term of type A.
@@ -15,15 +14,17 @@ inductive tactic (A : Type) : Type :=
 definition then_tac   {A : Type} (t1 t2 : tactic A) : tactic A := tactic_value
 definition orelse_tac {A : Type} (t1 t2 : tactic A) : tactic A := tactic_value
 definition repeat_tac {A : Type} (t : tactic A) : tactic A := tactic_value
-definition now   {A : Type} : tactic A := tactic_value
-definition state {A : Type} : tactic A := tactic_value
-definition fail  {A : Type} : tactic A := tactic_value
-definition id    {A : Type} : tactic A := tactic_value
-definition beta  {A : Type} : tactic A := tactic_value
+definition now_tac    {A : Type} : tactic A := tactic_value
+definition exact_tac  {A : Type} : tactic A := tactic_value
+definition state_tac  {A : Type} : tactic A := tactic_value
+definition fail_tac   {A : Type} : tactic A := tactic_value
+definition id_tac     {A : Type} : tactic A := tactic_value
+definition beta_tac   {A : Type} : tactic A := tactic_value
 definition apply      {A : Type} {B : Type} (b : B) : tactic A := tactic_value
+definition unfold_tac {A : Type} {B : Type} (b : B) : tactic A := tactic_value
 
 infixl `;`:200         := then_tac
 infixl `|`:100         := orelse_tac
 notation `!`:max t:max := repeat_tac t
-end
+
 

src/frontends/lean/CMakeLists.txt

@@ -1,7 +1,7 @@
 add_library(lean_frontend register_module.cpp token_table.cpp
 scanner.cpp parse_table.cpp parser_config.cpp parser.cpp
-parser_pos_provider.cpp builtin_cmds.cpp builtin_tactic_cmds.cpp
-builtin_exprs.cpp interactive.cpp notation_cmd.cpp calc.cpp
+parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
+interactive.cpp notation_cmd.cpp calc.cpp
 decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
 dependencies.cpp parser_bindings.cpp)
 

src/frontends/lean/builtin_exprs.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
+#include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/calc.h"
@@ -133,10 +134,8 @@ static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const
 }
 
 static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
-    tactic t = p.parse_tactic();
-    expr r = p.save_pos(mk_expr_placeholder(), pos);
-    p.save_hint(r, t);
-    return r;
+    expr t = p.parse_expr();
+    return p.save_pos(mk_by(t), pos);
 }
 
 static expr parse_proof(parser & p, expr const & prop) {
@@ -148,10 +147,8 @@ static expr parse_proof(parser & p, expr const & prop) {
         // parse: 'by' tactic
         auto pos = p.pos();
         p.next();
-        tactic t = p.parse_tactic();
-        expr r = p.save_pos(mk_expr_placeholder(some_expr(prop)), pos);
-        p.save_hint(r, t);
-        return r;
+        expr t = p.parse_expr();
+        return p.save_pos(mk_by(t), pos);
     } else if (p.curr_is_token(g_using)) {
         // parse: 'using' locals* ',' proof
         auto using_pos = p.pos();

src/frontends/lean/builtin_tactic_cmds.cpp

@@ -1,68 +0,0 @@
-/*
-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/tactic/tactic.h"
-#include "frontends/lean/parser.h"
-
-namespace lean {
-static name g_bang("!");
-tactic parse_fail_tactic(parser &, pos_info const &) { return fail_tactic(); }
-tactic parse_id_tactic(parser &, pos_info const &) { return id_tactic(); }
-tactic parse_now_tactic(parser &, pos_info const &) { return now_tactic(); }
-tactic parse_beta_tactic(parser &, pos_info const &) { return beta_tactic(); }
-tactic parse_print_tactic(parser & p, pos_info const & pos) {
-    return trace_state_tactic(p.get_stream_name(), pos);
-}
-tactic parse_assumption_tactic(parser &, pos_info const &) { return assumption_tactic(); }
-tactic parse_apply_tactic(parser & p, pos_info const &) { return p.parse_apply(); }
-
-tactic parse_unfold_tactic(parser & p, pos_info const &) {
-    auto pos = p.pos();
-    expr id  = p.parse_expr();
-    if (!is_constant(id))
-        throw parser_error("invalid 'unfold' tactic, constant expected", pos);
-    return unfold_tactic(const_name(id));
-}
-
-tactic parse_repeat_tactic(parser & p, pos_info const &) {
-    tactic t = p.parse_tactic();
-    if (p.curr_is_numeral()) {
-        unsigned n = p.parse_small_nat();
-        return repeat_at_most(t, n);
-    } else {
-        return repeat(t);
-    }
-}
-
-tactic parse_echo_tactic(parser & p, pos_info const &) {
-    if (!p.curr_is_string())
-        throw parser_error("invalid 'echo' tactic, string expected", p.pos());
-    tactic r = trace_tactic(p.get_str_val());
-    p.next();
-    return r;
-}
-
-void add_tactic(tactic_cmd_table & t, tactic_cmd_info && info) { t.insert(info.get_name(), info); }
-
-tactic_cmd_table get_builtin_tactic_cmds() {
-    tactic_cmd_table t;
-    add_tactic(t, tactic_cmd_info("fail", "always fail tactic", parse_fail_tactic));
-    add_tactic(t, tactic_cmd_info("print", "print current goals", parse_print_tactic));
-    add_tactic(t, tactic_cmd_info("now",  "succeeds only if all goals have been solved", parse_now_tactic));
-    add_tactic(t, tactic_cmd_info("echo", "trace tactic: display message", parse_echo_tactic));
-    add_tactic(t, tactic_cmd_info("unfold", "unfold definition", parse_unfold_tactic));
-    add_tactic(t, tactic_cmd_info("repeat", "repeat tactic", parse_repeat_tactic));
-    add_tactic(t, tactic_cmd_info("beta", "beta-reduction tactic", parse_beta_tactic));
-    add_tactic(t, tactic_cmd_info("apply", "apply tactic", parse_apply_tactic));
-    add_tactic(t, tactic_cmd_info("!", "repeat tactic", parse_repeat_tactic));
-    add_tactic(t, tactic_cmd_info("id", "do nothing tactic", parse_id_tactic));
-    add_tactic(t, tactic_cmd_info("assumption", "solve goal if there is an assumption that is identical to the conclusion",
-                                  parse_assumption_tactic));
-    add_tactic(t, tactic_cmd_info("exact", "solve goal if there is an assumption that is identical to the conclusion",
-                                  parse_assumption_tactic));
-    return t;
-}
-}

src/frontends/lean/builtin_tactic_cmds.h

@@ -1,11 +0,0 @@
-/*
-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 "frontends/lean/cmd_table.h"
-namespace lean {
-tactic_cmd_table get_builtin_tactic_cmds();
-}

src/frontends/lean/cmd_table.h

@@ -13,9 +13,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 class parser;
-
 typedef std::function<environment(parser&)> command_fn;
-typedef std::function<tactic(parser&, pos_info const &)> tactic_command_fn;
 
 template<typename F>
 struct cmd_info_tmpl {
@@ -32,10 +30,6 @@ public:
 };
 
 typedef cmd_info_tmpl<command_fn>              cmd_info;
-typedef cmd_info_tmpl<tactic_command_fn> tactic_cmd_info;
-
 typedef rb_map<name, cmd_info, name_quick_cmp> cmd_table;
-typedef rb_map<name, tactic_cmd_info, name_quick_cmp> tactic_cmd_table;
-
 inline void add_cmd(cmd_table & t, cmd_info const & cmd) { t.insert(cmd.get_name(), cmd); }
 }

src/frontends/lean/elaborator.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/list_fn.h"
 #include "util/lazy_list_fn.h"
 #include "util/sstream.h"
+#include "util/name_map.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
@@ -23,25 +24,28 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/unifier.h"
 #include "library/tactic/tactic.h"
+#include "library/tactic/expr_to_tactic.h"
 #include "library/error_handling/error_handling.h"
-#include "frontends/lean/hint_table.h"
 
 namespace lean {
 class elaborator {
     typedef list<expr> context;
     typedef std::vector<constraint> constraints;
+    typedef name_map<expr> tactic_hints;
+    typedef name_map<expr> mvar2meta;
 
     environment         m_env;
     io_state            m_ios;
     unifier_plugin      m_plugin;
     name_generator      m_ngen;
-    hint_table          m_hints;
     type_checker        m_tc;
     substitution        m_subst;
     context             m_ctx;
     pos_info_provider * m_pos_provider;
     justification       m_accumulated; // accumulate justification of eagerly used substitutions
     constraints         m_constraints;
+    tactic_hints        m_tactic_hints;
+    mvar2meta           m_mvar2meta;
 
     /**
         \brief Auxiliary object for creating backtracking points.
@@ -115,10 +119,10 @@ class elaborator {
 
 public:
     elaborator(environment const & env, io_state const & ios, name_generator const & ngen,
-               hint_table const & htable, substitution const & s, context const & ctx, pos_info_provider * pp):
+               substitution const & s, context const & ctx, pos_info_provider * pp):
         m_env(env), m_ios(ios),
         m_plugin([](constraint const &, name_generator const &) { return lazy_list<list<constraint>>(); }),
-        m_ngen(ngen), m_hints(htable), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, optional<module_idx>(0))),
+        m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, optional<module_idx>(0))),
         m_subst(s), m_ctx(ctx), m_pos_provider(pp) {
     }
 
@@ -278,7 +282,22 @@ public:
        \see mk_metavar
     */
     expr mk_meta(optional<expr> const & type, tag g) {
-        return apply_context(mk_metavar(type, g), g);
+        expr mvar = mk_metavar(type, g);
+        expr meta = apply_context(mvar, g);
+        m_mvar2meta.insert(mlocal_name(mvar), meta);
+        return meta;
+    }
+
+    /**
+        \brief Convert the metavariable to the metavariable application that captures
+        the context where it was defined.
+
+    */
+    optional<expr> mvar_to_meta(expr mvar) {
+        if (auto it = m_mvar2meta.find(mlocal_name(mvar)))
+            return some_expr(*it);
+        else
+            return none_expr();
     }
 
     expr visit_expecting_type(expr const & e) {
@@ -293,6 +312,8 @@ public:
             return mk_meta(some_expr(t), e.get_tag());
         else if (is_choice(e))
             return visit_choice(e, some_expr(t));
+        else if (is_by(e))
+            return visit_by(e, some_expr(t));
         else
             return visit(e);
     }
@@ -310,6 +331,14 @@ public:
         return m;
     }
 
+    expr visit_by(expr const & e, optional<expr> const & t) {
+        lean_assert(is_by(e));
+        expr m   = mk_meta(t, e.get_tag());
+        expr tac = visit(get_by_arg(e));
+        m_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac);
+        return m;
+    }
+
     /**
         \brief Make sure \c f is really a function, if it is not, try to apply coercions.
         The result is a pair <tt>new_f, f_type</tt>, where new_f is the new value for \c f,
@@ -535,6 +564,8 @@ public:
             return visit_placeholder(e);
         } else if (is_choice(e)) {
             return visit_choice(e, none_expr());
+        } else if (is_by(e)) {
+            return visit_by(e, none_expr());
         } else {
             switch (e.kind()) {
             case expr_kind::Local:      return e;
@@ -584,15 +615,18 @@ public:
 
     void collect_metavars(expr const & e, buffer<expr> & mvars) {
         for_each(e, [&](expr const & e, unsigned) {
-                if (is_metavar(e)) { mvars.push_back(e); return false; /* do not visit its type */ }
+                if (is_metavar(e)) {
+                    mvars.push_back(e);
+                    return false; /* do not visit its type */
+                }
                 return has_metavar(e);
             });
     }
 
-    optional<tactic> get_tactic_for(expr const & mvar) {
-        auto it = m_hints.find(mvar.get_tag());
-        if (it) {
-            return optional<tactic>(*it);
+    optional<tactic> get_tactic_for(substitution const & substitution, expr const & mvar) {
+        if (auto it = m_tactic_hints.find(mlocal_name(mvar))) {
+            expr pre_tac = substitution.instantiate_metavars_wo_jst(*it);
+            return optional<tactic>(expr_to_tactic(m_env, pre_tac, m_pos_provider));
         } else {
             // TODO(Leo): m_env tactic hints
             return optional<tactic>();
@@ -609,9 +643,16 @@ public:
         buffer<expr> mvars;
         collect_metavars(e, mvars);
         for (auto mvar : mvars) {
+            if (auto meta = mvar_to_meta(mvar)) {
+                buffer<expr> locals;
+                get_app_args(*meta, locals);
+                for (expr & l : locals)
+                    l = subst.instantiate_metavars_wo_jst(l);
                 mvar = update_mlocal(mvar, subst.instantiate_metavars_wo_jst(mlocal_type(mvar)));
-            proof_state ps = to_proof_state(mvar, m_ngen.mk_child());
-            if (optional<tactic> t = get_tactic_for(mvar)) {
+                meta = ::lean::mk_app(mvar, locals);
+                expr type = m_tc.infer(*meta);
+                proof_state ps = to_proof_state(*meta, type, m_ngen.mk_child());
+                if (optional<tactic> t = get_tactic_for(subst, mvar)) {
                     proof_state_seq seq = (*t)(m_env, m_ios, ps);
                     if (auto r = seq.pull()) {
                         substitution s = r->first.get_subst();
@@ -627,6 +668,7 @@ public:
                     }
                 }
             }
+        }
         return subst.instantiate_metavars_wo_jst(e);
     }
 
@@ -700,21 +742,21 @@ public:
 static name g_tmp_prefix = name::mk_internal_unique_name();
 
 expr elaborate(environment const & env, io_state const & ios, expr const & e, name_generator const & ngen,
-               hint_table const & htable, substitution const & s, list<expr> const & ctx, pos_info_provider * pp) {
-    return elaborator(env, ios, ngen, htable, s, ctx, pp)(e);
+               substitution const & s, list<expr> const & ctx, pos_info_provider * pp) {
+    return elaborator(env, ios, ngen, s, ctx, pp)(e);
 }
 
-expr elaborate(environment const & env, io_state const & ios, expr const & e, hint_table const & htable, pos_info_provider * pp) {
-    return elaborate(env, ios, e, name_generator(g_tmp_prefix), htable, substitution(), list<expr>(), pp);
+expr elaborate(environment const & env, io_state const & ios, expr const & e, pos_info_provider * pp) {
+    return elaborate(env, ios, e, name_generator(g_tmp_prefix), substitution(), list<expr>(), pp);
 }
 
 std::pair<expr, expr> elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v,
-                                hint_table const & htable, pos_info_provider * pp) {
-    return elaborator(env, ios, name_generator(g_tmp_prefix), htable, substitution(), list<expr>(), pp)(t, v, n);
+                                pos_info_provider * pp) {
+    return elaborator(env, ios, name_generator(g_tmp_prefix), substitution(), list<expr>(), pp)(t, v, n);
 }
 
 expr elaborate(environment const & env, io_state const & ios, expr const & e, expr const & expected_type, name_generator const & ngen,
-               hint_table const & htable, list<expr> const & ctx, pos_info_provider * pp) {
-    return elaborator(env, ios, ngen, htable, substitution(), ctx, pp)(e, expected_type);
+               list<expr> const & ctx, pos_info_provider * pp) {
+    return elaborator(env, ios, ngen, substitution(), ctx, pp)(e, expected_type);
 }
 }

src/frontends/lean/elaborator.h

@@ -10,16 +10,13 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/metavar.h"
 #include "library/io_state.h"
-#include "frontends/lean/hint_table.h"
 
 namespace lean {
 expr elaborate(environment const & env, io_state const & ios, expr const & e, name_generator const & ngen,
-               hint_table const & htable = hint_table(), substitution const & s = substitution(),
-               list<expr> const & ctx = list<expr>(), pos_info_provider * pp = nullptr);
+               substitution const & s = substitution(), list<expr> const & ctx = list<expr>(), pos_info_provider * pp = nullptr);
 expr elaborate(environment const & env, io_state const & ios, expr const & e, expr const & expected_type, name_generator const & ngen,
-               hint_table const & htable = hint_table(), list<expr> const & ctx = list<expr>(), pos_info_provider * pp = nullptr);
-expr elaborate(environment const & env, io_state const & ios, expr const & e, hint_table const & htable = hint_table(),
-               pos_info_provider * pp = nullptr);
+               list<expr> const & ctx = list<expr>(), pos_info_provider * pp = nullptr);
+expr elaborate(environment const & env, io_state const & ios, expr const & e, pos_info_provider * pp = nullptr);
 std::pair<expr, expr> elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v,
-                                hint_table const & htable = hint_table(), pos_info_provider * pp = nullptr);
+                                pos_info_provider * pp = nullptr);
 }

src/frontends/lean/parser.cpp

@@ -26,7 +26,6 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/scoped_ext.h"
 #include "library/error_handling/error_handling.h"
-#include "library/tactic/apply_tactic.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/parser_bindings.h"
 #include "frontends/lean/notation_cmd.h"
@@ -485,22 +484,22 @@ expr parser::mk_Type() {
 
 expr parser::elaborate(expr const & e) {
     parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
-    return ::lean::elaborate(m_env, m_ios, e, m_hints, &pp);
+    return ::lean::elaborate(m_env, m_ios, e, &pp);
 }
 
 expr parser::elaborate(expr const & e, name_generator const & ngen, list<expr> const & ctx) {
     parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
-    return ::lean::elaborate(m_env, m_ios, e, ngen, m_hints, substitution(), ctx, &pp);
+    return ::lean::elaborate(m_env, m_ios, e, ngen, substitution(), ctx, &pp);
 }
 
 expr parser::elaborate(environment const & env, expr const & e) {
     parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
-    return ::lean::elaborate(env, m_ios, e, m_hints, &pp);
+    return ::lean::elaborate(env, m_ios, e, &pp);
 }
 
 std::pair<expr, expr> parser::elaborate(name const & n, expr const & t, expr const & v) {
     parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
-    return ::lean::elaborate(m_env, m_ios, n, t, v, m_hints, &pp);
+    return ::lean::elaborate(m_env, m_ios, n, t, v, &pp);
 }
 
 [[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) {
@@ -922,156 +921,6 @@ expr parser::abstract(unsigned num_ps, expr const * ps, expr const & e, bool lam
     return rec_save_pos(r, p);
 }
 
-/** \brief Throw an exception if \c e contains a local constant that is not marked as contextual in \c local_decls */
-static void check_only_contextual_locals(expr const & e, local_expr_decls const & local_decls, pos_info const & pos) {
-    for_each(e, [&](expr const & e, unsigned) {
-            if (is_local(e)) {
-                auto it = local_decls.find(mlocal_name(e));
-                lean_assert(it);
-                if (!local_info(*it).is_contextual())
-                    throw parser_error(sstream() << "invalid 'apply' tactic, it references non-contextual local '"
-                                       << local_pp_name(e) << "'", pos);
-            }
-            return has_local(e);
-        });
-}
-
-
-/** \brief Return a list of all contextual parameters in local_decls */
-static list<expr> collect_contextual_parameters(local_expr_decls const & local_decls) {
-    buffer<expr> tmp;
-    for (expr const & p : local_decls.get_values()) {
-        if (is_local(p) && local_info(p).is_contextual())
-            tmp.push_back(p);
-    }
-    return to_list(tmp.begin(), tmp.end());
-}
-
-tactic parser::parse_exact_apply() {
-    parse_expr();
-    return id_tactic();
-#if 0
-    auto p = pos();
-    expr e = parse_expr();
-    check_only_contextual_locals(e, m_local_decls, p);
-    list<expr> ctx = collect_contextual_parameters(m_local_decls);
-    return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
-            if (empty(s.get_goals()))
-                return none_proof_state();
-            name gname      = head(s.get_goals()).first;
-            goal g          = head(s.get_goals()).second;
-            goals new_gs    = tail(s.get_goals());
-            auto const &   s_locals = s.get_init_locals();
-            // Remark: the proof state initial hypotheses (s_locals) are essentially ctx "after elaboration".
-            // So, to process \c e, we must first replace its local constants with (s_locals).
-            name_generator ngen     = s.ngen();
-            lean_assert(length(s_locals) == length(ctx));
-            buffer<expr> locals;
-            auto it1 = ctx;
-            auto it2 = s_locals;
-            while (!is_nil(it1) && !is_nil(it2)) {
-                auto const & p = head(it1);
-                locals.push_back(p);
-                it1 = tail(it1);
-                it2 = tail(it2);
-            }
-            std::reverse(locals.begin(), locals.end());
-            expr new_e = abstract_locals(e, locals.size(), locals.data());
-            for (auto const & l : s_locals)
-                new_e = instantiate(new_e, l);
-            parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
-            new_e = ::lean::elaborate(env, ios, new_e, g.get_conclusion(), ngen.mk_child(),
-                                      m_hints, s_locals, &pp);
-            proof_builder new_pb = add_proof(s.get_pb(), gname, new_e);
-            return some_proof_state(proof_state(s, new_gs, new_pb, ngen));
-        });
-#endif
-}
-
-tactic parser::parse_apply() {
-    parse_expr();
-    return id_tactic();
-#if 0
-    auto p = pos();
-    expr e = parse_expr();
-    check_only_contextual_locals(e, m_local_decls, p);
-    list<expr> ctx = collect_contextual_parameters(m_local_decls);
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
-            name_generator ngen     = s.ngen();
-            auto const &   s_locals = s.get_init_locals();
-            expr           new_e    = elaborate(e, ngen.mk_child(), ctx);
-            proof_state    new_s(s, ngen);
-            buffer<expr> tmp;
-            for (auto const & p : ctx)
-                tmp.push_back(p);
-            std::reverse(tmp.begin(), tmp.end());
-            new_e = abstract_locals(new_e, tmp.size(), tmp.data());
-            for (auto const & l : s_locals)
-                new_e = instantiate(new_e, l);
-            return apply_tactic(new_e)(env, ios, new_s);
-        });
-#endif
-}
-
-tactic parser::parse_tactic(unsigned /* rbp */) {
-    if (curr_is_token(g_lparen) || curr_is_token(g_lbracket)) {
-        bool paren = curr_is_token(g_lparen);
-        next();
-        buffer<tactic> choices;
-        tactic r = parse_tactic();
-        while (true) {
-            if (curr_is_token(g_comma)) {
-                next();
-                r = then(r, parse_tactic());
-            } else if (curr_is_token(g_bar)) {
-                next();
-                choices.push_back(r);
-                r = parse_tactic();
-            } else {
-                break;
-            }
-        }
-        if (paren)
-            check_token_next(g_rparen, "invalid tactic sequence, ')' expected");
-        else
-            check_token_next(g_rbracket, "invalid tactic sequence, ']' expected");
-        if (choices.empty()) {
-            return r;
-        } else {
-            choices.push_back(r);
-            r = choices[0];
-            for (unsigned i = 1; i < choices.size(); i++) {
-                r = orelse(r, choices[i]);
-            }
-            return r;
-        }
-    } else if (curr_is_token(g_have) || curr_is_token(g_show) || curr_is_token(g_assume) ||
-               curr_is_token(g_take) || curr_is_token(g_fun)) {
-        return parse_exact_apply();
-    } else {
-        name id;
-        auto p = pos();
-        if (curr_is_identifier()) {
-            id = get_name_val();
-            next();
-        } else if (curr_is_keyword() || curr_is_command()) {
-            id = get_token_info().value();
-            next();
-        } else {
-            throw parser_error("invalid tactic, '(' or tactic command expected", p);
-        }
-        if (auto it = tactic_cmds().find(id)) {
-            return it->get_fn()(*this, p);
-        } else {
-            throw parser_error(sstream() << "unknown tactic command '" << id << "'", p);
-        }
-    }
-}
-
-void parser::save_hint(expr const & e, tactic const & t) {
-    m_hints.insert(get_tag(e), t);
-}
-
 void parser::parse_command() {
     lean_assert(curr() == scanner::token_kind::CommandKeyword);
     m_last_cmd_pos = pos();

src/frontends/lean/parser.h

@@ -19,7 +19,6 @@ Author: Leonardo de Moura
 #include "library/io_state.h"
 #include "library/io_state_stream.h"
 #include "library/kernel_bindings.h"
-#include "frontends/lean/hint_table.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/local_decls.h"
 #include "frontends/lean/parser_config.h"
@@ -57,7 +56,6 @@ class parser {
     unsigned                m_next_tag_idx;
     bool                    m_found_errors;
     pos_info_table_ptr      m_pos_table;
-    hint_table              m_hints;
     // If m_type_use_placeholder is true, then the token Type is parsed as Type.{_}.
     // if it is false, then it is parsed as Type.{l} where l is a fresh parameter,
     // and is automatically inserted into m_local_level_decls.
@@ -96,7 +94,6 @@ class parser {
     cmd_table const & cmds() const { return get_cmd_table(env()); }
     parse_table const & nud() const { return get_nud_table(env()); }
     parse_table const & led() const { return get_led_table(env()); }
-    tactic_cmd_table const & tactic_cmds() const { return get_tactic_cmd_table(env()); }
 
     unsigned curr_level_lbp() const;
     level parse_max_imax(bool is_max);
@@ -120,7 +117,6 @@ class parser {
     expr parse_binder_core(binder_info const & bi);
     void parse_binder_block(buffer<expr> & r, binder_info const & bi);
     void parse_binders_core(buffer<expr> & r);
-    tactic parse_exact_apply();
 
     friend environment section_cmd(parser & p);
     friend environment end_scoped_cmd(parser & p);
@@ -230,9 +226,6 @@ public:
     expr lambda_abstract(buffer<expr> const & ps, expr const & e) { return lambda_abstract(ps, e, pos_of(e)); }
     expr pi_abstract(buffer<expr> const & ps, expr const & e) { return pi_abstract(ps, e, pos_of(e)); }
 
-    tactic parse_tactic(unsigned rbp = 0);
-    tactic parse_apply();
-
     struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); };
     void add_local_level(name const & n, level const & l);
     void add_local_expr(name const & n, expr const & p);
@@ -255,9 +248,6 @@ public:
     struct placeholder_universe_scope { parser & m_p; bool m_old; placeholder_universe_scope(parser &); ~placeholder_universe_scope(); };
     expr mk_Type();
 
-    /** \brief Use tactic \c t for "synthesizing" the placeholder \c e. */
-    void save_hint(expr const & e, tactic const & t);
-
     /**
         \brief By default, when the parser finds a unknown identifier, it signs an error.
         This scope object temporarily changes this behavior. In any scope where this object

src/frontends/lean/parser_config.cpp

@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/builtin_cmds.h"
-#include "frontends/lean/builtin_tactic_cmds.h"
 
 namespace lean {
 using notation::transition;
@@ -218,10 +217,8 @@ parse_table const & get_led_table(environment const & env) {
 
 struct cmd_ext : public environment_extension {
     cmd_table m_cmds;
-    tactic_cmd_table m_tactic_cmds;
     cmd_ext() {
         m_cmds        = get_builtin_cmds();
-        m_tactic_cmds = get_builtin_tactic_cmds();
     }
 };
 
@@ -236,7 +233,4 @@ static cmd_ext const & get_extension(environment const & env) {
 cmd_table const & get_cmd_table(environment const & env) {
     return get_extension(env).m_cmds;
 }
-tactic_cmd_table const & get_tactic_cmd_table(environment const & env) {
-    return get_extension(env).m_tactic_cmds;
-}
 }

src/frontends/lean/parser_config.h

@@ -43,7 +43,6 @@ token_table const & get_token_table(environment const & env);
 parse_table const & get_nud_table(environment const & env);
 parse_table const & get_led_table(environment const & env);
 cmd_table const & get_cmd_table(environment const & env);
-tactic_cmd_table const & get_tactic_cmd_table(environment const & env);
 /** \brief Force notation from namespace \c n to shadow any existing notation */
 environment overwrite_notation(environment const & env, name const & n);
 }

src/library/tactic/apply_tactic.cpp

@@ -37,8 +37,9 @@ bool collect_simple_metas(expr const & e, buffer<expr> & result) {
     return !failed;
 }
 
-tactic apply_tactic(expr const & /* e */) {
+tactic apply_tactic(expr const & e) {
     return tactic([=](environment const &, io_state const &, proof_state const & s) {
+            std::cout << e << "\n";
             return s;
 #if 0
             if (s.is_final_state()) {

src/library/tactic/expr_to_tactic.cpp

@@ -5,8 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <unordered_map>
+#include <string>
 #include "kernel/instantiate.h"
 #include "library/tactic/expr_to_tactic.h"
+#include "library/tactic/apply_tactic.h"
 
 namespace lean {
 typedef std::unordered_map<name, expr_to_tactic_fn, name_hash, name_eq> expr_to_tactic_map;
@@ -19,13 +21,13 @@ void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn) {
     get_expr_to_tactic_map().insert(mk_pair(n, fn));
 }
 
-tactic expr_to_tactic(environment const & env, expr const & e) {
+tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const * p) {
     expr const & f = get_app_fn(e);
     if (is_constant(f)) {
         auto const & map = get_expr_to_tactic_map();
         auto it = map.find(const_name(f));
         if (it != map.end()) {
-            return it->second(env, e);
+            return it->second(env, e, p);
         } else if (auto it = env.find(const_name(f))) {
             if (it->is_definition()) {
                 buffer<expr> locals;
@@ -33,39 +35,62 @@ tactic expr_to_tactic(environment const & env, expr const & e) {
                 expr v = it->get_value();
                 v = instantiate_univ_params(v, it->get_univ_params(), const_levels(f));
                 v = apply_beta(v, locals.size(), locals.data());
-                return expr_to_tactic(env, v);
+                return expr_to_tactic(env, v, p);
             }
         }
         throw exception("failed to convert expression into tactic");
     } else if (is_lambda(f)) {
         buffer<expr> locals;
         get_app_rev_args(e, locals);
-        return expr_to_tactic(env, apply_beta(f, locals.size(), locals.data()));
+        return expr_to_tactic(env, apply_beta(f, locals.size(), locals.data()), p);
     } else {
         throw exception("failed to convert expression into tactic");
     }
 }
 
+register_simple_tac::register_simple_tac(name const & n, std::function<tactic()> f) {
+    register_expr_to_tactic(n, [=](environment const &, expr const &, pos_info_provider const *) {
+            return f();
+        });
+}
+
 register_bin_tac::register_bin_tac(name const & n, std::function<tactic(tactic const &, tactic const &)> f) {
-    register_expr_to_tactic(n, [=](environment const & env, expr const & e) {
-            return f(expr_to_tactic(env, app_arg(app_fn(e))),
-                     expr_to_tactic(env, app_arg(e)));
+    register_expr_to_tactic(n, [=](environment const & env, expr const & e, pos_info_provider const * p) {
+            return f(expr_to_tactic(env, app_arg(app_fn(e)), p),
+                     expr_to_tactic(env, app_arg(e), p));
         });
 }
 
 register_unary_tac::register_unary_tac(name const & n, std::function<tactic(tactic const &)> f) {
-    register_expr_to_tactic(n, [=](environment const & env, expr const & e) {
-            return f(expr_to_tactic(env, app_arg(e)));
+    register_expr_to_tactic(n, [=](environment const & env, expr const & e, pos_info_provider const * p) {
+            return f(expr_to_tactic(env, app_arg(e), p));
         });
 }
 
-static register_tac reg_id(name({"tactic", "id"}), [](environment const &, expr const &) { return id_tactic(); });
-static register_tac reg_now(name({"tactic", "now"}), [](environment const &, expr const &) { return now_tactic(); });
-static register_tac reg_fail(name({"tactic", "fail"}), [](environment const &, expr const &) { return fail_tactic(); });
-static register_tac reg_beta(name({"tactic", "beta"}), [](environment const &, expr const &) { return beta_tactic(); });
-static register_bin_tac reg_then(name({"tactic", "then_tac"}), [](tactic const & t1, tactic const & t2) { return then(t1, t2); });
-static register_bin_tac reg_orelse(name({"tactic", "orelse_tac"}), [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
-static register_unary_tac reg_repeat(name({"tactic", "repeat_tac"}), [](tactic const & t1) { return repeat(t1); });
+static register_simple_tac reg_id(name("id_tac"), []() { return id_tactic(); });
+static register_simple_tac reg_now(name("now_tac"), []() { return now_tactic(); });
+static register_simple_tac reg_exact(name("exact_tac"), []() { return assumption_tactic(); });
+static register_simple_tac reg_fail(name("fail_tac"), []() { return fail_tactic(); });
+static register_simple_tac reg_beta(name("beta_tac"), []() { return beta_tactic(); });
+static register_bin_tac reg_then(name("then_tac"), [](tactic const & t1, tactic const & t2) { return then(t1, t2); });
+static register_bin_tac reg_orelse(name("orelse_tac"), [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
+static register_unary_tac reg_repeat(name("repeat_tac"), [](tactic const & t1) { return repeat(t1); });
+static register_tac reg_state(name("state_tac"), [](environment const &, expr const & e, pos_info_provider const * p) {
+        if (p)
+            return trace_state_tactic(std::string(p->get_file_name()), p->get_pos_info(e));
+        else
+            return trace_state_tactic("unknown", mk_pair(0, 0));
+    });
+static register_tac reg_apply(name("apply"), [](environment const &, expr const & e, pos_info_provider const *) {
+        return apply_tactic(app_arg(e));
+    });
+static register_tac reg_unfold(name("unfold_tac"), [](environment 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));
+    });
 
 // We encode the 'by' expression that is used to trigger tactic execution.
 // This is a trick to avoid creating a new kind of expression.

src/library/tactic/expr_to_tactic.h

@@ -5,14 +5,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "kernel/pos_info_provider.h"
 #include "library/tactic/tactic.h"
 
 namespace lean {
-typedef std::function<tactic(environment const & env, expr const & e)> expr_to_tactic_fn;
+typedef std::function<tactic(environment const & env, expr const & e, pos_info_provider const *)> expr_to_tactic_fn;
 void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn);
 struct register_tac {
     register_tac(name const & n, expr_to_tactic_fn fn) { register_expr_to_tactic(n, fn); }
 };
+struct register_simple_tac {
+    register_simple_tac(name const & n, std::function<tactic()> f);
+};
 struct register_bin_tac {
     register_bin_tac(name const & n, std::function<tactic(tactic const &, tactic const &)> f);
 };
@@ -20,7 +24,7 @@ struct register_unary_tac {
     register_unary_tac(name const & n, std::function<tactic(tactic const &)> f);
 };
 
-tactic expr_to_tactic(environment const & env, expr const & e);
+tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const *p);
 expr mk_by(expr const & e);
 bool is_by(expr const & e);
 expr const & get_by_arg(expr const & e);

src/library/tactic/proof_state.cpp

@@ -57,32 +57,16 @@ goals map_goals(proof_state const & s, std::function<optional<goal>(goal const &
         });
 }
 
-proof_state to_proof_state(expr const & mvar, name_generator ngen) {
-    if (!is_metavar(mvar))
-        throw exception("invalid 'to_proof_state', argument is not a metavariable");
-    expr t = mlocal_type(mvar);
-    buffer<expr> ls;
-    while (is_pi(t)) {
-        expr l  = mk_local(ngen.next(), binding_name(t), binding_domain(t), binding_info(t));
-        ls.push_back(l);
-        t       = instantiate(binding_body(t), l);
-    }
-    expr meta = mk_app(mvar, ls);
-    goals gs(goal(meta, t));
-    return proof_state(gs, substitution(), ngen);
-}
-
-static name g_tmp_prefix = name::mk_internal_unique_name();
-proof_state to_proof_state(expr const & mvar) {
-    return to_proof_state(mvar, name_generator(g_tmp_prefix));
-}
-
 io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s) {
     options const & opts = out.get_options();
     out.get_stream() << mk_pair(s.pp(out.get_environment(), out.get_formatter(), opts), opts);
     return out;
 }
 
+proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen) {
+    return proof_state(goals(goal(meta, type)), substitution(), ngen);
+}
+
 DECL_UDATA(goals)
 
 static int mk_goals(lua_State * L) {
@@ -169,12 +153,13 @@ static int mk_proof_state(lua_State * L) {
     }
 }
 
+static name g_tmp_prefix = name::mk_internal_unique_name();
 static int to_proof_state(lua_State * L) {
     int nargs = lua_gettop(L);
-    if (nargs == 1)
-        return push_proof_state(L, to_proof_state(to_expr(L, 1)));
+    if (nargs == 2)
+        return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), name_generator(g_tmp_prefix)));
     else
-        return push_proof_state(L, to_proof_state(to_expr(L, 1), to_name_generator(L, 2)));
+        return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), to_name_generator(L, 3)));
 }
 
 static int proof_state_tostring(lua_State * L) {

src/library/tactic/proof_state.h

@@ -37,9 +37,7 @@ public:
 inline optional<proof_state> some_proof_state(proof_state const & s) { return some(s); }
 inline optional<proof_state> none_proof_state() { return optional<proof_state> (); }
 
-/** \brief Create a proof state for a metavariable \c mvar */
-proof_state to_proof_state(expr const & mvar, name_generator ngen);
-proof_state to_proof_state(expr const & mvar);
+proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen);
 
 goals map_goals(proof_state const & s, std::function<optional<goal>(goal const & g)> f);
 io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s);

tests/lean/run/have5.lean

@@ -1,11 +1,11 @@
-abbreviation Bool : Type.{1} := Type.{0}
+import standard
 variables a b c d : Bool
 axiom Ha : a
 axiom Hb : b
 axiom Hc : c
 print raw
-  have H1 : a, by id,
-  then have H2 : b, by id,
-  have H3 : c, by id,
-  then have H4 : d, by id,
+  have H1 : a, by exact_tac,
+  then have H2 : b, by exact_tac,
+  have H3 : c, by exact_tac,
+  then have H4 : d, by exact_tac,
   H4

tests/lean/run/t8.lean

@@ -1 +1,2 @@
-print raw (by id)
+import standard
+print raw (by exact_tac)

tests/lean/run/tactic1.lean

@@ -1,4 +1,5 @@
 import logic
+import tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by assumption
+:= by exact_tac

tests/lean/run/tactic10.lean

@@ -1,5 +1,6 @@
 import logic
 
+exit -- TODO
 theorem tst (a b : Bool) (H : a ↔ b) : b ↔ a
 := by (apply iff_intro,
        assume Hb, iff_mp_right H Hb,

tests/lean/run/tactic11.lean

@@ -1,5 +1,6 @@
 import logic
 
+exit -- TODO
 theorem tst (a b : Bool) (H : a ↔ b) : b ↔ a
 := have H1 [fact] : a → b, from iff_elim_left H,
    by (apply iff_intro,

tests/lean/run/tactic2.lean

@@ -1,4 +1,7 @@
 import logic
+import tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by [echo "executing simple tactic", assumption]
+:= by state_tac; exact_tac
+
+check tst

tests/lean/run/tactic3.lean

@@ -1,6 +1,10 @@
 import logic
+import tactic
+using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by [echo "first try",  print, now  |
-       echo "second try", fail       |
-       echo "third try", exact]
+:= by state_tac; now_tac  |
+      state_tac; fail_tac |
+      exact_tac
+
+check tst

tests/lean/run/tactic4.lean

@@ -1,6 +1,11 @@
-import logic
+import standard
 
 definition id {A : Type} (a : A) := a
 
+definition simple_tac {A : Bool} : tactic A
+:= unfold_tac @id.{1}; exact_tac
+
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by [unfold id, print, exact]
+:= by simple_tac
+
+check tst

tests/lean/run/tactic5.lean

@@ -1,6 +1,8 @@
-import logic
+import standard
 
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by [!(unfold id, print), exact]
+:= by !(unfold_tac @id; state_tac); exact_tac
+
+check tst

tests/lean/run/tactic6.lean

@@ -1,9 +1,8 @@
-import logic
+import standard
 
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by [!echo "message" 5, unfold id, exact]
+:= by unfold_tac id; exact_tac
 
-theorem tst2 {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by [repeat echo "message" 5, unfold id, exact]
+check tst

tests/lean/run/tactic7.lean

@@ -1,4 +1,5 @@
 import logic
 
+exit -- TODO
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
 := by (print, apply and_intro, print, exact, apply and_intro, print, !exact)

tests/lean/run/tactic8.lean

@@ -1,5 +1,6 @@
 import logic
 
+exit -- TODO
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
 := by (apply and_intro,
        show A, from H1,

tests/lean/run/tactic9.lean

@@ -1,4 +1,5 @@
 import logic
 
+exit -- TODO
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : ((fun x : Bool, x) A) ∧ B ∧ A
 := by (apply and_intro, beta, exact, apply and_intro, !exact)

tests/lua/proof_state1.lua

@@ -5,8 +5,8 @@ local eq = Const("eq")
 local a  = Local("a", A)
 local b  = Local("b", A)
 local H  = Local("H", eq(A, a, b))
-local m  = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))
-print(to_proof_state(m))
-local s    = to_proof_state(m)
+local m  = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))(A, a, b, H)
+print(to_proof_state(m, eq(A, a, b)))
+local s    = to_proof_state(m, eq(A, a, b))
 local g    = s:goals():head()
 print(g)

tests/lua/tactic1.lua

@@ -5,9 +5,8 @@ local eq = Const("eq")
 local a  = Local("a", A)
 local b  = Local("b", A)
 local H  = Local("H", eq(A, a, b))
-local m  = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))
-print(to_proof_state(m))
-local s  = to_proof_state(m)
+local m  = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))(A, a, b, H)
+local s  = to_proof_state(m, eq(A, a, b))
 local t = Then(Append(trace_tac("tst1a"), trace_tac("tst1b")),
                trace_tac("tst2"),
                Append(trace_tac("tst3"), assumption_tac()))