feat(library/tactic): add trick for 'embedding' tactics inside Lean expressions

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

library/standard/tactic.lean

@@ -0,0 +1,29 @@
+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.
+-- tactic_value is just a "dummy" for creating the "fake"
+inductive tactic (A : Type) : Type :=
+| tactic_value {} : tactic A
+-- 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 A) into a tactic that sythesizes a term
+-- of type A
+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 apply {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/library/tactic/CMakeLists.txt

@@ -1,4 +1,5 @@
-add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp)
+add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp
+expr_to_tactic.cpp)
 
 # simplify_tactic.cpp)
 

src/library/tactic/expr_to_tactic.cpp

@@ -0,0 +1,97 @@
+/*
+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 <unordered_map>
+#include "kernel/instantiate.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+typedef std::unordered_map<name, expr_to_tactic_fn, name_hash, name_eq> expr_to_tactic_map;
+expr_to_tactic_map & get_expr_to_tactic_map() {
+    static expr_to_tactic_map g_map;
+    return g_map;
+}
+
+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) {
+    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);
+        } else if (auto it = 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(env, v);
+            }
+        }
+        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()));
+    } else {
+        throw exception("failed to convert expression into tactic");
+    }
+}
+
+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_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)));
+        });
+}
+
+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); });
+
+// We encode the 'by' expression that is used to trigger tactic execution.
+// This is a trick to avoid creating a new kind of expression.
+// 'by' macros are temporary objects used by the elaborator,
+// and have no semantic significance.
+[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'by' expression"); }
+static name g_by_name("by");
+class by_macro_cell : public macro_definition_cell {
+public:
+    virtual name get_name() const { return g_by_name; }
+    virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(); }
+    virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(); }
+    virtual void write(serializer &) const { throw_ex(); }
+};
+
+static macro_definition g_by(new by_macro_cell());
+expr mk_by(expr const & e) {
+    return mk_macro(g_by, 1, &e);
+}
+
+bool is_by(expr const & e) {
+    return is_macro(e) && macro_def(e) == g_by;
+}
+
+expr const & get_by_arg(expr const & e) {
+    lean_assert(is_by(e));
+    return macro_arg(e, 0);
+}
+}

src/library/tactic/expr_to_tactic.h

@@ -0,0 +1,27 @@
+/*
+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 {
+typedef std::function<tactic(environment const & env, expr const & e)> 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_bin_tac {
+    register_bin_tac(name const & n, std::function<tactic(tactic const &, tactic const &)> f);
+};
+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);
+expr mk_by(expr const & e);
+bool is_by(expr const & e);
+expr const & get_by_arg(expr const & e);
+}