feat(library/vm,library/tactic/vm_monitor): use optionT to define vm monad

library/init/meta/vm.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.tactic
+import init.meta.tactic init.option
 
 meta constant vm_obj : Type
 
@@ -51,11 +51,15 @@ meta constant olean     : vm_decl → option name
 meta constant args_info : vm_decl → list vm_local_info
 end vm_decl
 
-meta constant vm : Type → Type
-meta constant vm.functor : functor vm
-meta constant vm.monad   : monad vm
+meta constant vm_core : Type → Type
+meta constant vm_core.map {A B : Type} : (A → B) → vm_core A → vm_core B
+meta constant vm_core.ret {A : Type} : A → vm_core A
+meta constant vm_core.bind {A B : Type} : vm_core A → (A → vm_core B) → vm_core B
 
-attribute [instance] vm.functor vm.monad
+meta instance : monad vm_core :=
+⟨@vm_core.map, @vm_core.ret, @vm_core.bind⟩
+
+@[reducible] meta def vm (A : Type) : Type := optionT.{1 1} vm_core A
 
 namespace vm
 meta constant get         : name → vm vm_decl

src/library/compiler/erase_irrelevant.cpp

@@ -302,9 +302,7 @@ class erase_irrelevant_fn : public compiler_step_visitor {
     }
 
     static bool is_builtin_state_monad(expr const & e) {
-        return
-            is_constant(e, get_monadIO_name()) ||
-            is_constant(e, get_vm_monad_name());
+        return is_constant(e, get_monadIO_name());
     }
 
     expr visit_monad_bind(expr const & e, buffer<expr> const & args) {

src/library/constants.cpp

@@ -383,7 +383,6 @@ name const * g_unit = nullptr;
 name const * g_unit_cases_on = nullptr;
 name const * g_unit_star = nullptr;
 name const * g_user_attribute = nullptr;
-name const * g_vm_monad = nullptr;
 name const * g_vm_monitor = nullptr;
 name const * g_weak_order = nullptr;
 name const * g_well_founded = nullptr;
@@ -773,7 +772,6 @@ void initialize_constants() {
     g_unit_cases_on = new name{"unit", "cases_on"};
     g_unit_star = new name{"unit", "star"};
     g_user_attribute = new name{"user_attribute"};
-    g_vm_monad = new name{"vm", "monad"};
     g_vm_monitor = new name{"vm_monitor"};
     g_weak_order = new name{"weak_order"};
     g_well_founded = new name{"well_founded"};
@@ -1164,7 +1162,6 @@ void finalize_constants() {
     delete g_unit_cases_on;
     delete g_unit_star;
     delete g_user_attribute;
-    delete g_vm_monad;
     delete g_vm_monitor;
     delete g_weak_order;
     delete g_well_founded;
@@ -1554,7 +1551,6 @@ name const & get_unit_name() { return *g_unit; }
 name const & get_unit_cases_on_name() { return *g_unit_cases_on; }
 name const & get_unit_star_name() { return *g_unit_star; }
 name const & get_user_attribute_name() { return *g_user_attribute; }
-name const & get_vm_monad_name() { return *g_vm_monad; }
 name const & get_vm_monitor_name() { return *g_vm_monitor; }
 name const & get_weak_order_name() { return *g_weak_order; }
 name const & get_well_founded_name() { return *g_well_founded; }

src/library/constants.h

@@ -385,7 +385,6 @@ name const & get_unit_name();
 name const & get_unit_cases_on_name();
 name const & get_unit_star_name();
 name const & get_user_attribute_name();
-name const & get_vm_monad_name();
 name const & get_vm_monitor_name();
 name const & get_weak_order_name();
 name const & get_well_founded_name();

src/library/constants.txt

@@ -378,7 +378,6 @@ unit
 unit.cases_on
 unit.star
 user_attribute
-vm.monad
 vm_monitor
 weak_order
 well_founded

src/library/tactic/vm_monitor.cpp

@@ -17,8 +17,24 @@ static vm_obj _vm_monitor_register(vm_obj const & vm_n, vm_obj const & vm_s) {
     LEAN_TACTIC_CATCH(s);
 }
 
+static vm_obj vm_core_map(vm_obj const &, vm_obj const &, vm_obj const & fn, vm_obj const & a, vm_obj const & s) {
+    vm_obj v = invoke(a, s);
+    return invoke(fn, v);
+}
+
+static vm_obj vm_core_ret(vm_obj const &, vm_obj const & a, vm_obj const & /* s */) {
+    return a;
+}
+
+static vm_obj vm_core_bind(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & b, vm_obj const & s) {
+    return invoke(b, invoke(a, s), s);
+}
+
 void initialize_vm_monitor() {
     DECLARE_VM_BUILTIN(name({"vm_monitor", "register"}),  _vm_monitor_register);
+    DECLARE_VM_BUILTIN(name({"vm_core", "map"}),  vm_core_map);
+    DECLARE_VM_BUILTIN(name({"vm_core", "ret"}),  vm_core_ret);
+    DECLARE_VM_BUILTIN(name({"vm_core", "bind"}), vm_core_bind);
 }
 
 void finalize_vm_monitor() {

src/library/vm/vm.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_name.h"
+#include "library/vm/vm_option.h"
 #include "library/vm/vm_expr.h"
 
 #ifndef LEAN_DEFAULT_PROFILER
@@ -1060,6 +1061,19 @@ void vm_state::debugger_init() {
     m_debugger_state_ptr.reset(new debugger_state(m_env));
 }
 
+/* Reference to the VM that is currently running. */
+LEAN_THREAD_VALUE(vm_state *, g_vm_state, nullptr);
+
+scope_vm_state::scope_vm_state(vm_state & s):
+    m_prev(g_vm_state) {
+    g_vm_state = &s;
+}
+
+scope_vm_state::~scope_vm_state() {
+    g_vm_state = m_prev;
+}
+
+/* Reference to the VM that is currently being debugged. */
 LEAN_THREAD_VALUE(vm_state *, g_vm_state_debugged, nullptr);
 
 vm_state & get_vm_state_being_debugged() {
@@ -1068,12 +1082,15 @@ vm_state & get_vm_state_being_debugged() {
 }
 
 void vm_state::debugger_step() {
-    flet<vm_state*> set(g_vm_state_debugged, this);
+    flet<vm_state*> set1(g_vm_state_debugged, this);
     auto & vm_dbg  = m_debugger_state_ptr->m_vm;
-    m_debugger_state_ptr->m_state =
+    flet<vm_state*> set2(g_vm_state, &vm_dbg);
+    vm_obj r       =
         vm_dbg.invoke(m_debugger_state_ptr->m_step_fn,
                       m_debugger_state_ptr->m_state,
                       mk_vm_unit());
+    if (!is_none(r))
+        m_debugger_state_ptr->m_state = get_some_value(r);
 }
 
 void vm_state::update_env(environment const & env) {
@@ -1130,17 +1147,6 @@ void vm_state::invoke_builtin(vm_decl const & d) {
     m_pc++;
 }
 
-LEAN_THREAD_VALUE(vm_state *, g_vm_state, nullptr);
-
-scope_vm_state::scope_vm_state(vm_state & s):
-    m_prev(g_vm_state) {
-    g_vm_state = &s;
-}
-
-scope_vm_state::~scope_vm_state() {
-    g_vm_state = m_prev;
-}
-
 void vm_state::invoke_cfun(vm_decl const & d) {
     flet<vm_state *> Set(g_vm_state, this);
     auto & S       = m_stack;

tests/lean/run/basic_monitor1.lean

@@ -0,0 +1,12 @@
+meta def basic_monitor : vm_monitor nat :=
+{ init := 0, step := λ s, return (trace ("step " ++ s^.to_string)  (λ u, s+1)) >> failure }
+
+run_command vm_monitor.register `basic_monitor
+
+set_option debugger true
+
+def f : nat → nat
+| 0     := 0
+| (a+1) := f a
+
+vm_eval trace "a" (λ u, f 4)