feat(library/tactic): expose more builtin tactics, cleanup expr_to_tactic procedure

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

library/standard/tactic.lean

@@ -1,36 +1,48 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic string
+import logic string num
 using string
+using num
 
 namespace tactic
 -- This is just a trick to embed the 'tactic language' as a
 -- Lean expression. We should view 'tactic' as automation
 -- that when execute produces a term.
--- tactic_value is just a "dummy" for creating the "fake"
--- definitions
+-- builtin_tactic is just a "dummy" for creating the
+-- definitions that are actually implemented in C++
 inductive tactic : Type :=
-| tactic_value : tactic
+| builtin_tactic : tactic
 -- Remark the following names are not arbitrary, the tactic module
 -- uses them when converting Lean expressions into actual tactic objects.
 -- The bultin 'by' construct triggers the process of converting a
 -- a term of type 'tactic' into a tactic that sythesizes a term
-definition and_then   (t1 t2 : tactic) : tactic := tactic_value
-definition or_else    (t1 t2 : tactic) : tactic := tactic_value
-definition repeat     (t : tactic) : tactic := tactic_value
-definition now        : tactic := tactic_value
-definition assumption : tactic := tactic_value
-definition state      : tactic := tactic_value
-definition fail       : tactic := tactic_value
-definition id         : tactic := tactic_value
-definition beta       : tactic := tactic_value
-definition apply      {B : Type} (b : B) : tactic := tactic_value
-definition unfold     {B : Type} (b : B) : tactic := tactic_value
-definition exact      {B : Type} (b : B) : tactic := tactic_value
-definition trace      (s : string) : tactic := tactic_value
+definition and_then   (t1 t2 : tactic) : tactic := builtin_tactic
+definition or_else    (t1 t2 : tactic) : tactic := builtin_tactic
+definition append     (t1 t2 : tactic) : tactic := builtin_tactic
+definition interleave (t1 t2 : tactic) : tactic := builtin_tactic
+definition par        (t1 t2 : tactic) : tactic := builtin_tactic
+definition repeat     (t : tactic) : tactic := builtin_tactic
+definition at_most    (t : tactic) (k : num)  : tactic := builtin_tactic
+definition focus_at   (t : tactic) (i : num)  : tactic := builtin_tactic
+definition try_for    (t : tactic) (ms : num) : tactic := builtin_tactic
+definition now        : tactic := builtin_tactic
+definition assumption : tactic := builtin_tactic
+definition state      : tactic := builtin_tactic
+definition fail       : tactic := builtin_tactic
+definition id         : tactic := builtin_tactic
+definition beta       : tactic := builtin_tactic
+definition apply      {B : Type} (b : B) : tactic := builtin_tactic
+definition unfold     {B : Type} (b : B) : tactic := builtin_tactic
+definition exact      {B : Type} (b : B) : tactic := builtin_tactic
+definition trace      (s : string) : tactic := builtin_tactic
 infixl `;`:200         := and_then
 infixl `|`:100         := or_else
-notation `!`:max t:max := repeat t
+notation `!` t:max     := repeat t
 notation `⟦` t `⟧`     := apply t
+definition try        (t : tactic) : tactic := t | id
+notation `?` t:max     := try t
+definition repeat1    (t : tactic) : tactic := t ; !t
+definition focus      (t : tactic) : tactic := focus_at t 0
+definition determ     (t : tactic) : tactic := at_most t 1
 end

src/library/tactic/expr_to_tactic.cpp

@@ -6,9 +6,11 @@ Author: Leonardo de Moura
 */
 #include <unordered_map>
 #include <string>
+#include "util/sstream.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
 #include "library/string.h"
+#include "library/num.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/tactic/apply_tactic.h"
 
@@ -23,26 +25,55 @@ 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(type_checker & tc, expr const & e, pos_info_provider const * p) {
-    expr f = get_app_fn(tc.whnf(e));
-    if (is_constant(f)) {
+static name g_tac("tactic"), g_builtin_tac(g_tac, "builtin_tactic");
+static name g_tac_name(g_tac, "tactic"), g_exact_tac_name(g_tac, "exact"), g_and_then_tac_name(g_tac, "and_then");
+static name g_or_else_tac_name(g_tac, "or_else"), g_repeat_tac_name(g_tac, "repeat");
+static expr g_exact_tac_fn(Const(g_exact_tac_name)), g_and_then_tac_fn(Const(g_and_then_tac_name));
+static expr g_or_else_tac_fn(Const(g_or_else_tac_name)), g_repeat_tac_fn(Const(g_repeat_tac_name));
+static expr g_tac_type(Const(g_tac_name));
+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_repeat_tac_fn() { return g_repeat_tac_fn; }
+expr const & get_tactic_type() { return g_tac_type; }
+
+static void throw_failed(expr const & e) {
+    throw expr_to_tactic_exception(e, "failed to convert expression into tactic");
+}
+
+/** \brief Return true if v is the constant tactic.builtin_tactic or the constant function that returns tactic.builtin_tactic */
+static bool is_builtin_tactic(expr const & v) {
+    if (is_lambda(v))
+        return is_builtin_tactic(binding_body(v));
+    else if (is_constant(v) && const_name(v) == g_builtin_tac)
+        return true;
+    else
+        return false;
+}
+
+tactic expr_to_tactic(type_checker & tc, expr e, pos_info_provider const * p) {
+    e = tc.whnf(e);
+    expr f = get_app_fn(e);
+    if (!is_constant(f))
+        throw_failed(e);
+    optional<declaration> it = tc.env().find(const_name(f));
+    if (!it || !it->is_definition())
+        throw_failed(e);
+    expr v = it->get_value();
+    if (is_builtin_tactic(v)) {
         auto const & map = get_expr_to_tactic_map();
-        auto it = map.find(const_name(f));
-        if (it != map.end()) {
-            return it->second(tc, e, p);
-        } else if (auto it = tc.env().find(const_name(f))) {
-            if (it->is_definition()) {
-                buffer<expr> locals;
-                get_app_rev_args(e, locals);
-                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(tc, v, p);
-            }
-        }
-        throw expr_to_tactic_exception(e, "failed to convert expression into tactic");
+        auto it2 = map.find(const_name(f));
+        if (it2 != map.end())
+            return it2->second(tc, e, p);
+        else
+            throw expr_to_tactic_exception(e, sstream() << "implementation for builtin tactic '" << const_name(f) << "' was not found");
     } else {
-        throw expr_to_tactic_exception(e, "failed to convert expression into tactic");
+        // unfold definition
+        buffer<expr> locals;
+        get_app_rev_args(e, locals);
+        v = instantiate_univ_params(v, it->get_univ_params(), const_levels(f));
+        v = apply_beta(v, locals.size(), locals.data());
+        return expr_to_tactic(tc, v, p);
     }
 }
 
@@ -80,16 +111,23 @@ register_unary_tac::register_unary_tac(name const & n, std::function<tactic(tact
         });
 }
 
-static name g_tac("tactic"), g_tac_name(g_tac, "tactic"), g_exact_tac_name(g_tac, "exact"), g_and_then_tac_name(g_tac, "and_then");
-static name g_or_else_tac_name(g_tac, "or_else"), g_repeat_tac_name(g_tac, "repeat");
-static expr g_exact_tac_fn(Const(g_exact_tac_name)), g_and_then_tac_fn(Const(g_and_then_tac_name));
-static expr g_or_else_tac_fn(Const(g_or_else_tac_name)), g_repeat_tac_fn(Const(g_repeat_tac_name));
-static expr g_tac_type(Const(g_tac_name));
-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_repeat_tac_fn() { return g_repeat_tac_fn; }
-expr const & get_tactic_type() { return g_tac_type; }
+register_unary_num_tac::register_unary_num_tac(name const & n, std::function<tactic(tactic const &, unsigned k)> f) {
+    register_expr_to_tactic(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) {
+            buffer<expr> args;
+            get_app_args(e, args);
+            if (args.size() != 2)
+                throw expr_to_tactic_exception(e, "invalid tactic, it must have two arguments");
+            tactic t = expr_to_tactic(tc, args[0], p);
+            optional<mpz> k = to_num(args[1]);
+            if (!k)
+                k = to_num(tc.whnf(args[1]));
+            if (!k)
+                throw expr_to_tactic_exception(e, "invalid tactic, second argument must be a numeral");
+            if (!k->is_unsigned_int())
+                throw expr_to_tactic_exception(e, "invalid tactic, second argument does not fit in a machine unsigned integer");
+            return f(t, k->get_unsigned_int());
+        });
+}
 
 static register_simple_tac reg_id(name(g_tac, "id"), []() { return id_tactic(); });
 static register_simple_tac reg_now(name(g_tac, "now"), []() { return now_tactic(); });
@@ -97,6 +135,9 @@ static register_simple_tac reg_assumption(name(g_tac, "assumption"), []() { retu
 static register_simple_tac reg_fail(name(g_tac, "fail"), []() { return fail_tactic(); });
 static register_simple_tac reg_beta(name(g_tac, "beta"), []() { return beta_tactic(); });
 static register_bin_tac reg_then(g_and_then_tac_name, [](tactic const & t1, tactic const & t2) { return then(t1, t2); });
+static register_bin_tac reg_append(name(g_tac, "append"), [](tactic const & t1, tactic const & t2) { return append(t1, t2); });
+static register_bin_tac reg_interleave(name(g_tac, "interleave"), [](tactic const & t1, tactic const & t2) { return interleave(t1, t2); });
+static register_bin_tac reg_par(name(g_tac, "par"), [](tactic const & t1, tactic const & t2) { return par(t1, t2); });
 static register_bin_tac reg_orelse(g_or_else_tac_name, [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
 static register_unary_tac reg_repeat(g_repeat_tac_name, [](tactic const & t1) { return repeat(t1); });
 static register_tac reg_state(name(g_tac, "state"), [](type_checker &, expr const & e, pos_info_provider const * p) {
@@ -130,7 +171,9 @@ static register_tac reg_unfold(name(g_tac, "unfold"), [](type_checker &, expr co
         else
             return unfold_tactic(const_name(id));
     });
-
+static register_unary_num_tac reg_at_most(name(g_tac, "at_most"), [](tactic const & t, unsigned k) { return take(t, k); });
+static register_unary_num_tac reg_focus_at(name(g_tac, "focus_at"), [](tactic const & t, unsigned k) { return focus(t, k); });
+static register_unary_num_tac reg_try_for(name(g_tac, "try_for"), [](tactic const & t, unsigned k) { return try_for(t, k); });
 
 // 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

@@ -10,7 +10,9 @@ Author: Leonardo de Moura
 
 namespace lean {
 class expr_to_tactic_exception : public tactic_exception {
-public: expr_to_tactic_exception(expr const & e, char const * msg):tactic_exception(e, msg) {}
+public:
+    expr_to_tactic_exception(expr const & e, char const * msg):tactic_exception(e, msg) {}
+    expr_to_tactic_exception(expr const & e, sstream const & strm):tactic_exception(e, strm) {}
 };
 
 typedef std::function<tactic(type_checker & tc, expr const & e, pos_info_provider const *)> expr_to_tactic_fn;
@@ -27,6 +29,9 @@ struct register_bin_tac {
 struct register_unary_tac {
     register_unary_tac(name const & n, std::function<tactic(tactic const &)> f);
 };
+struct register_unary_num_tac {
+    register_unary_num_tac(name const & n, std::function<tactic(tactic const &, unsigned)> f);
+};
 
 expr const & get_tactic_type();
 expr const & get_exact_tac_fn();

src/library/tactic/tactic.cpp

@@ -447,14 +447,11 @@ static int tactic_append(lua_State * L)         {  return push_tactic(L, append(
 static int tactic_interleave(lua_State * L)     {  return push_tactic(L, interleave(to_tactic(L, 1), to_tactic(L, 2))); }
 static int tactic_par(lua_State * L)            {  return push_tactic(L, par(to_tactic(L, 1), to_tactic(L, 2))); }
 static int tactic_repeat(lua_State * L)         {  return push_tactic(L, repeat(to_tactic(L, 1))); }
-static int tactic_repeat1(lua_State * L)        {  return push_tactic(L, repeat1(to_tactic(L, 1))); }
 static int tactic_repeat_at_most(lua_State * L) {  return push_tactic(L, repeat_at_most(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
 static int tactic_take(lua_State * L)           {  return push_tactic(L, take(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
-static int tactic_determ(lua_State * L)         {  return push_tactic(L, determ(to_tactic(L, 1))); }
 static int tactic_suppress_trace(lua_State * L) {  return push_tactic(L, suppress_trace(to_tactic(L, 1))); }
 static int tactic_try_for(lua_State * L)        {  return push_tactic(L, try_for(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
 static int tactic_using_params(lua_State * L)   {  return push_tactic(L, using_params(to_tactic(L, 1), to_options(L, 2))); }
-static int tactic_try(lua_State * L)            {  return push_tactic(L, orelse(to_tactic(L, 1), id_tactic())); }
 static int tactic_focus(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 1)
@@ -528,9 +525,7 @@ static const struct luaL_Reg tactic_m[] = {
     {"append",          safe_function<tactic_append>},
     {"interleave",      safe_function<tactic_interleave>},
     {"par",             safe_function<tactic_par>},
-    {"determ",          safe_function<tactic_determ>},
     {"repeat",          safe_function<tactic_repeat>},
-    {"repeat1",         safe_function<tactic_repeat1>},
     {"repeat_at_most",  safe_function<tactic_repeat_at_most>},
     {"take",            safe_function<tactic_take>},
     {"suppress_trace",  safe_function<tactic_suppress_trace>},
@@ -571,15 +566,12 @@ void open_tactic(lua_State * L) {
     SET_GLOBAL_FUN(nary_tactic<par>,        "Par");
     SET_GLOBAL_FUN(tactic_repeat,           "Repeat");
     SET_GLOBAL_FUN(tactic_repeat_at_most,   "RepeatAtMost");
-    SET_GLOBAL_FUN(tactic_repeat1,          "Repeat1");
     SET_GLOBAL_FUN(mk_lua_cond_tactic,      "Cond");
     SET_GLOBAL_FUN(mk_lua_when_tactic,      "When");
-    SET_GLOBAL_FUN(tactic_try,              "Try");
     SET_GLOBAL_FUN(tactic_try_for,          "TryFor");
     SET_GLOBAL_FUN(tactic_take,             "Take");
     SET_GLOBAL_FUN(tactic_using_params,     "Using");
     SET_GLOBAL_FUN(tactic_using_params,     "UsingParams");
-    SET_GLOBAL_FUN(tactic_determ,           "Determ");
     SET_GLOBAL_FUN(tactic_focus,            "Focus");
 }
 }

src/library/tactic/tactic.h

@@ -102,10 +102,6 @@ inline tactic par(tactic const & t1, tactic const & t2) { return par(t1, t2, 1);
    \brief Return a tactic that keeps applying \c t until it fails.
 */
 tactic repeat(tactic const & t);
-/**
-   \brief Similar to \c repeat, but applies \c t at least once.
-*/
-inline tactic repeat1(tactic const & t) { return then(t, repeat(t)); }
 /**
    \brief Similar to \c repeat, but execute \c t at most \c k times.
 
@@ -119,8 +115,6 @@ tactic repeat_at_most(tactic const & t, unsigned k);
    k elements from the sequence produced by \c t.
 */
 tactic take(tactic const & t, unsigned k);
-/** \brief Syntax sugar for take(t, 1) */
-inline tactic determ(tactic const & t) { return take(t, 1); }
 typedef std::function<bool(environment const & env, io_state const & ios, proof_state const & s)> proof_state_pred; // NOLINT
 /**
     \brief Return a tactic that applies the predicate \c p to the input state.