feat(library/vm/vm): add friendly invoke method

src/frontends/lean/old_elaborator.cpp

@@ -1920,16 +1920,7 @@ optional<tactic_state> old_elaborator::execute_tactic(expr const & tactic, tacti
     new_env = new_env.add(cd);
     new_env = vm_compile(new_env, new_env.get(tactic_name));
     vm_state S(new_env);
-    vm_obj initial_state = to_obj(s);
-    S.push(initial_state);
-    vm_decl d = *S.get_decl(tactic_name);
-    S.invoke_fn(tactic_name);
-    if (d.get_arity() == 0) {
-        /* main returned a closure, it did not process initial_state yet.
-           So, we force the execution. */
-        S.apply();
-    }
-    vm_obj r = S.top();
+    vm_obj r = S.invoke(tactic_name, to_obj(s));
     if (optional<tactic_state> new_s = is_tactic_success(r)) {
         return some_tactic_state(*new_s);
     } else if (optional<pair<format, tactic_state>> ex = is_tactic_exception(S, opts, r)) {

src/library/vm/vm.cpp

@@ -1120,6 +1120,27 @@ static void to_cbuffer(vm_obj const & fn, buffer<vm_obj> & args) {
     }
 }
 
+vm_obj vm_state::invoke(unsigned fn_idx, unsigned nargs, vm_obj const * as) {
+    lean_assert(fn_idx < m_decls.size());
+    vm_decl const & d = m_decls[fn_idx];
+    lean_assert(d.get_arity() <= nargs);
+    std::copy(as, as + nargs, std::back_inserter(m_stack));
+    invoke_fn(fn_idx);
+    if (d.get_arity() < nargs)
+        apply(nargs - d.get_arity());
+    vm_obj r = m_stack.back();
+    m_stack.pop_back();
+    return r;
+}
+
+vm_obj vm_state::invoke(name const & fn, unsigned nargs, vm_obj const * as) {
+    if (auto r = m_fn_name2idx.find(fn)) {
+        return invoke(*r, nargs, as);
+    } else {
+        throw exception(sstream() << "VM does not have code for '" << fn << "'");
+    }
+}
+
 vm_obj vm_state::invoke(vm_obj const & fn, vm_obj const & a1) {
     unsigned fn_idx   = cfn_idx(fn);
     vm_decl const & d = m_decls[fn_idx];

src/library/vm/vm.h

@@ -564,6 +564,23 @@ public:
     vm_obj invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj const & a3, vm_obj const & a4,
                   vm_obj const & a5, vm_obj const & a6, vm_obj const & a7, vm_obj const & a8);
     vm_obj invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args);
+
+    /** \brief Invoke fn_idx with nargs arguments and return the result */
+    vm_obj invoke(unsigned fn_idx, unsigned nargs, vm_obj const * as);
+    vm_obj invoke(unsigned fn_idx, std::initializer_list<vm_obj> const & as) {
+        return invoke(fn_idx, as.size(), as.begin());
+    }
+    vm_obj invoke(unsigned fn_idx, vm_obj const & a) {
+        return invoke(fn_idx, 1, &a);
+    }
+
+    vm_obj invoke(name const & fn, unsigned nargs, vm_obj const * as);
+    vm_obj invoke(name const & fn, std::initializer_list<vm_obj> const & as) {
+        return invoke(fn, as.size(), as.begin());
+    }
+    vm_obj invoke(name const & fn, vm_obj const & a) {
+        return invoke(fn, 1, &a);
+    }
 };
 
 /** \brief Return reference to thread local VM state object. */