chore(library): add helper functions

src/library/tactic/tactic_state.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/constants.h"
 #include "library/type_context.h"
 #include "library/pp_options.h"
 #include "library/trace.h"
@@ -23,6 +24,12 @@ tactic_state::tactic_state(environment const & env, options const & o, metavar_c
     m_ptr = new (get_vm_allocator().allocate(sizeof(tactic_state_cell))) tactic_state_cell(env, o, ctx, gs, main);
 }
 
+optional<metavar_decl> tactic_state::get_main_goal() const {
+    if (empty(goals()))
+        return optional<metavar_decl>();
+    return mctx().get_metavar_decl(head(goals()));
+}
+
 tactic_state mk_tactic_state_for(environment const & env, options const & o, local_context const & lctx, expr const & type) {
     metavar_context mctx;
     expr main = mctx.mk_metavar_decl(lctx, type);
@@ -124,6 +131,62 @@ vm_obj tactic_state_format_expr(vm_obj const & s, vm_obj const & e) {
     return to_obj(to_tactic_state(s).pp_expr(fmtf, to_expr(e)));
 }
 
+vm_obj mk_tactic_success(vm_obj const & a, tactic_state const & s) {
+    return mk_vm_constructor(0, a, to_obj(s));
+}
+
+vm_obj mk_tactic_success(tactic_state const & s) {
+    return mk_tactic_success(mk_vm_unit(), s);
+}
+
+vm_obj mk_tactic_exception(vm_obj const & fn) {
+    return mk_vm_constructor(1, fn);
+}
+
+vm_obj mk_tactic_exception(format const & fmt) {
+    vm_state const & s = get_vm_state();
+    vm_decl K = *s.get_decl(get_combinator_K_name());
+    return mk_tactic_exception(mk_vm_closure(K.get_idx(), mk_vm_unit(), mk_vm_unit(), to_obj(fmt)));
+}
+
+vm_obj mk_tactic_exception(char const * msg) {
+    return mk_tactic_exception(format(msg));
+}
+
+vm_obj mk_no_goals_exception() {
+    return mk_tactic_exception("tactic failed, there are no goals to be solved");
+}
+
+struct type_context_cache_helper {
+    typedef std::unique_ptr<type_context_cache> cache_ptr;
+    cache_ptr m_cache_ptr;
+
+    void reset(environment const & env, options const & o) {
+        m_cache_ptr.reset(new type_context_cache(env, o));
+    }
+
+    bool compatible_env(environment const & env) {
+        environment const & curr_env = m_cache_ptr->env();
+        return env.is_descendant(curr_env) && curr_env.is_descendant(env);
+    }
+
+    void ensure_compatible(environment const & env, options const & o) {
+        if (!m_cache_ptr || !compatible_env(env) || !is_eqp(o, m_cache_ptr->get_options()))
+            reset(env, o);
+    }
+};
+
+MK_THREAD_LOCAL_GET_DEF(type_context_cache_helper, get_tch);
+
+type_context_cache & get_type_context_cache_for(environment const & env, options const & o) {
+    get_tch().ensure_compatible(env, o);
+    return *get_tch().m_cache_ptr.get();
+}
+
+type_context_cache & get_type_context_cache_for(tactic_state const & s) {
+    return get_type_context_cache_for(s.env(), s.get_options());
+}
+
 void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic_state", "env"}),         tactic_state_env);
     DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}), tactic_state_format_expr);

src/library/tactic/tactic_state.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 #include "kernel/environment.h"
 #include "library/metavar_context.h"
+#include "library/type_context.h"
 
 namespace lean {
 class tactic_state_cell {
@@ -38,6 +39,7 @@ public:
     tactic_state(tactic_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
     ~tactic_state() { if (m_ptr) m_ptr->dec_ref(); }
 
+    optional<metavar_decl> get_main_goal() const;
     tactic_state_cell * raw() const { return m_ptr; }
     options const & get_options() const { lean_assert(m_ptr); return m_ptr->m_options; }
     environment const & env() const { lean_assert(m_ptr); return m_ptr->m_env; }
@@ -66,6 +68,24 @@ tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx
 tactic_state const & to_tactic_state(vm_obj const & o);
 vm_obj to_obj(tactic_state const & s);
 
+vm_obj mk_tactic_success(vm_obj const & a, tactic_state const & s);
+vm_obj mk_tactic_success(tactic_state const & s);
+vm_obj mk_tactic_exception(vm_obj const & fn);
+vm_obj mk_tactic_exception(format const & fmt);
+vm_obj mk_tactic_exception(char const * msg);
+vm_obj mk_no_goals_exception();
+
+type_context_cache & get_type_context_cache_for(environment const & env, options const & o);
+type_context_cache & get_type_context_cache_for(tactic_state const & s);
+
+inline type_context mk_type_context_for(tactic_state const & s, metavar_context & mctx,
+                                        transparency_mode m = transparency_mode::Semireducible) {
+    local_context lctx;
+    if (auto d = s.get_main_goal()) lctx = d->get_context();
+    mctx = s.mctx();
+    return type_context(mctx, lctx, get_type_context_cache_for(s), m);
+}
+
 void initialize_tactic_state();
 void finalize_tactic_state();
 }

src/library/type_context.h

@@ -106,6 +106,10 @@ public:
        \pre !frozen_mode() */
     local_context freeze_local_instances(metavar_context & mctx, local_context const & lctx);
 
+    environment const & env() const { return m_env; }
+
+    options const & get_options() const { return m_options; }
+
     bool frozen_mode() const { return m_frozen_mode; }
 
     /** \brief Auxiliary object used to set position information for the type class resolution trace. */

src/library/vm/vm.cpp

@@ -81,6 +81,25 @@ vm_obj mk_vm_closure(unsigned fn_idx, unsigned sz, vm_obj const * data) {
     return mk_vm_composite(vm_obj_kind::Closure, fn_idx, sz, data);
 }
 
+vm_obj mk_vm_closure(unsigned cidx, vm_obj const & o1) {
+    return mk_vm_closure(cidx, 1, &o1);
+}
+
+vm_obj mk_vm_closure(unsigned cidx, vm_obj const & o1, vm_obj const & o2) {
+    vm_obj args[2] = {o1, o2};
+    return mk_vm_closure(cidx, 2, args);
+}
+
+vm_obj mk_vm_closure(unsigned cidx, vm_obj const & o1, vm_obj const & o2, vm_obj const & o3) {
+    vm_obj args[3] = {o1, o2, o3};
+    return mk_vm_closure(cidx, 3, args);
+}
+
+vm_obj mk_vm_closure(unsigned cidx, vm_obj const & o1, vm_obj const & o2, vm_obj const & o3, vm_obj const & o4) {
+    vm_obj args[4] = {o1, o2, o3, o4};
+    return mk_vm_closure(cidx, 4, args);
+}
+
 vm_mpz::vm_mpz(mpz const & v):
     vm_obj_cell(vm_obj_kind::MPZ),
     m_value(v) {
@@ -1577,6 +1596,11 @@ vm_obj invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args) {
     return g_vm_state->invoke(fn, nargs, args);
 }
 
+vm_state const & get_vm_state() {
+    lean_assert(g_vm_state);
+    return *g_vm_state;
+}
+
 void vm_state::invoke_global(vm_decl const & d) {
     m_call_stack.emplace_back(m_code, m_fn_idx, d.get_arity(), m_pc+1, m_bp);
     m_code            = d.get_code();

src/library/vm/vm.h

@@ -143,6 +143,10 @@ vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_closure(unsigned fnidx, unsigned sz, vm_obj const * args);
+vm_obj mk_vm_closure(unsigned cidx, vm_obj const &);
+vm_obj mk_vm_closure(unsigned cidx, vm_obj const &, vm_obj const &);
+vm_obj mk_vm_closure(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &);
+vm_obj mk_vm_closure(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_mpz(mpz const & n);
 inline vm_obj mk_vm_external(vm_external * obj) { lean_assert(obj && obj->get_rc() == 0); return vm_obj(obj); }
 /* helper functions for creating natural numbers */
@@ -552,6 +556,9 @@ public:
     vm_obj invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args);
 };
 
+/** \brief Return reference to thread local VM state object. */
+vm_state const & get_vm_state();
+
 /** \brief Add builtin implementation for the function named \c n.
     All environment objects will contain this builtin.
     \pre These procedures can only be invoked at initialization time. */