feat(library/tactic/tactic_state): add vm_obj introspection

library/init/meta/vm.lean

@@ -9,16 +9,9 @@ import init.meta.tactic init.option
 meta constant vm_obj : Type
 
 inductive vm_obj_kind
-| vm_simple
-| vm_constructor
-| vm_closure
-| vm_mpz
-| vm_name
-| vm_level
-| vm_expr
-| vm_tactic_state
-| vm_format
-| vm_other
+| simple | constructor | closure | mpz
+| name | level | expr | declaration
+| environment | tactic_state | format | other
 
 namespace vm_obj
 meta constant kind            : vm_obj → vm_obj_kind
@@ -29,6 +22,8 @@ meta constant to_nat          : vm_obj → nat
 meta constant to_name         : vm_obj → name
 meta constant to_level        : vm_obj → level
 meta constant to_expr         : vm_obj → expr
+meta constant to_declaration  : vm_obj → declaration
+meta constant to_environment  : vm_obj → environment
 meta constant to_tactic_state : vm_obj → tactic_state
 meta constant to_format       : vm_obj → format
 end vm_obj
@@ -71,6 +66,7 @@ meta constant call_stack_fn   : nat → vm name
 meta constant curr_fn         : vm name
 meta constant bp              : vm nat
 meta constant pc              : vm nat
+meta constant obj_to_string   : vm_obj → vm string
 
 meta def trace {A : Type} [has_to_format A] (a : A) : vm unit :=
 do fmt ← return $ to_fmt a,

src/library/tactic/tactic_state.cpp

@@ -188,6 +188,10 @@ struct vm_tactic_state : public vm_external {
     }
 };
 
+bool is_tactic_state(vm_obj const & o) {
+    return is_external(o) && dynamic_cast<vm_tactic_state*>(to_external(o));
+}
+
 tactic_state const & to_tactic_state(vm_obj const & o) {
     lean_assert(is_external(o));
     lean_assert(dynamic_cast<vm_tactic_state*>(to_external(o)));

src/library/tactic/tactic_state.h

@@ -97,6 +97,7 @@ tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env,
    \remark It returns s is is_eqp(s.mctx(), mctx) and is_decl_eqp(s.get_main_goal_decl()->get_context(), lctx) */
 tactic_state set_mctx_lctx(tactic_state const & s, metavar_context const & mctx, local_context const & lctx);
 
+bool is_tactic_state(vm_obj const & o);
 tactic_state const & to_tactic_state(vm_obj const & o);
 vm_obj to_obj(tactic_state const & s);
 

src/library/tactic/vm_monitor.cpp

@@ -11,7 +11,11 @@ Author: Leonardo de Moura
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_string.h"
 #include "library/vm/vm_name.h"
+#include "library/vm/vm_level.h"
 #include "library/vm/vm_expr.h"
+#include "library/vm/vm_declaration.h"
+#include "library/vm/vm_environment.h"
+#include "library/vm/vm_format.h"
 #include "library/vm/vm_list.h"
 #include "library/tactic/tactic_state.h"
 
@@ -37,6 +41,125 @@ vm_obj vm_core_bind(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj con
     return invoke(b, invoke(a, s), s);
 }
 
+/*
+inductive vm_obj_kind
+| simple | constructor | closure | mpz
+| name | level | expr | declaration
+| environment | tactic_state | format | other
+*/
+vm_obj _vm_obj_kind(vm_obj const & o) {
+    switch (o.kind()) {
+    case vm_obj_kind::Simple: return mk_vm_simple(0);
+    case vm_obj_kind::Constructor: return mk_vm_simple(1);
+    case vm_obj_kind::Closure: return mk_vm_simple(2);
+    case vm_obj_kind::MPZ: return mk_vm_simple(3);
+    case vm_obj_kind::External:
+        if (is_name(o)) return mk_vm_simple(4);
+        else if (is_level(o)) return mk_vm_simple(5);
+        else if (is_expr(o)) return mk_vm_simple(6);
+        else if (is_declaration(o)) return mk_vm_simple(7);
+        else if (is_env(o)) return mk_vm_simple(8);
+        else if (is_tactic_state(o)) return mk_vm_simple(9);
+        else if (is_format(o)) return mk_vm_simple(10);
+        else return mk_vm_simple(11);
+    }
+    lean_unreachable();
+}
+
+vm_obj vm_obj_cidx(vm_obj const & o) {
+    switch (o.kind()) {
+    case vm_obj_kind::Simple:
+    case vm_obj_kind::Constructor:
+        return mk_vm_nat(cidx(o));
+    default:
+        return mk_vm_nat(0);
+    }
+}
+
+vm_obj vm_obj_fn_idx(vm_obj const & o) {
+    switch (o.kind()) {
+    case vm_obj_kind::Closure:
+        return mk_vm_nat(cfn_idx(o));
+    default:
+        return mk_vm_nat(0);
+    }
+}
+
+vm_obj vm_obj_fields(vm_obj const & o) {
+    switch (o.kind()) {
+    case vm_obj_kind::Constructor: {
+        unsigned i = csize(o);
+        vm_obj r   = mk_vm_simple(0);
+        while (i > 0) {
+            --i;
+            r = mk_vm_constructor(1, cfield(o, i), r);
+        }
+        return r;
+    }
+    default:
+        return mk_vm_simple(0);
+    }
+}
+
+vm_obj vm_obj_to_nat(vm_obj const & o) {
+    switch (o.kind()) {
+    case vm_obj_kind::Simple:
+    case vm_obj_kind::MPZ:
+        return o;
+    default:
+        return mk_vm_nat(0);
+    }
+}
+
+vm_obj vm_obj_to_name(vm_obj const & o) {
+    if (is_name(o))
+        return o;
+    else
+        return to_obj(name());
+}
+
+vm_obj vm_obj_to_level(vm_obj const & o) {
+    if (is_level(o))
+        return o;
+    else
+        return to_obj(level());
+}
+
+vm_obj vm_obj_to_expr(vm_obj const & o) {
+    if (is_expr(o))
+        return o;
+    else
+        return to_obj(expr());
+}
+
+vm_obj vm_obj_to_declaration(vm_obj const & o) {
+    if (is_declaration(o))
+        return o;
+    else
+        return to_obj(declaration());
+}
+
+vm_obj vm_obj_to_environment(vm_obj const & o) {
+    if (is_env(o))
+        return o;
+    else
+        return to_obj(environment());
+}
+
+vm_obj vm_obj_to_tactic_state(vm_obj const & o) {
+    if (is_tactic_state(o))
+        return o;
+    else
+        return to_obj(mk_tactic_state_for(environment(), options(), local_context(), mk_Prop()));
+}
+
+vm_obj vm_obj_to_format(vm_obj const & o) {
+    if (is_format(o))
+        return o;
+    else
+        return to_obj(format());
+}
+
 struct vm_vm_decl : public vm_external {
     vm_decl m_val;
     vm_vm_decl(vm_decl const & v):m_val(v) {}
@@ -156,27 +279,46 @@ vm_obj vm_curr_fn(vm_obj const & /*s*/) {
     return mk_vm_success(to_obj(get_vm_state_being_debugged().curr_fn()));
 }
 
+vm_obj vm_obj_to_string(vm_obj const & o, vm_obj const & /*s*/) {
+    std::ostringstream out;
+    get_vm_state_being_debugged().display(out, o);
+    return mk_vm_success(to_obj(out.str()));
+}
+
 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);
-    DECLARE_VM_BUILTIN(name({"vm_decl", "kind"}),       _vm_decl_kind);
-    DECLARE_VM_BUILTIN(name({"vm_decl", "to_name"}),    vm_decl_to_name);
-    DECLARE_VM_BUILTIN(name({"vm_decl", "idx"}),        vm_decl_idx);
-    DECLARE_VM_BUILTIN(name({"vm_decl", "arity"}),      vm_decl_arity);
-    DECLARE_VM_BUILTIN(name({"vm_decl", "pos"}),        vm_decl_pos);
-    DECLARE_VM_BUILTIN(name({"vm_decl", "olean"}),      vm_decl_olean);
-    DECLARE_VM_BUILTIN(name({"vm_decl", "args_info"}),  vm_decl_args_info);
-    DECLARE_VM_BUILTIN(name({"vm", "get_decl"}),        vm_get_decl);
-    DECLARE_VM_BUILTIN(name({"vm", "stack_size"}),      vm_stack_size);
-    DECLARE_VM_BUILTIN(name({"vm", "stack_obj"}),       vm_stack_obj);
-    DECLARE_VM_BUILTIN(name({"vm", "stack_obj_info"}),  vm_stack_obj_info);
-    DECLARE_VM_BUILTIN(name({"vm", "call_stack_size"}), vm_call_stack_size);
-    DECLARE_VM_BUILTIN(name({"vm", "call_stack_fn"}),   vm_call_stack_fn);
-    DECLARE_VM_BUILTIN(name({"vm", "bp"}),              vm_bp);
-    DECLARE_VM_BUILTIN(name({"vm", "pc"}),              vm_pc);
-    DECLARE_VM_BUILTIN(name({"vm", "curr_fn"}),         vm_curr_fn);
+    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);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "kind"}),            _vm_obj_kind);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "cidx"}),            vm_obj_cidx);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "fn_idx"}),          vm_obj_fn_idx);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "fields"}),          vm_obj_fields);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "to_nat"}),          vm_obj_to_nat);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "to_name"}),         vm_obj_to_name);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "to_level"}),        vm_obj_to_level);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "to_expr"}),         vm_obj_to_expr);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "to_declaration"}),  vm_obj_to_declaration);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "to_environment"}),  vm_obj_to_environment);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "to_tactic_state"}), vm_obj_to_tactic_state);
+    DECLARE_VM_BUILTIN(name({"vm_obj", "to_format"}),       vm_obj_to_format);
+    DECLARE_VM_BUILTIN(name({"vm_decl", "kind"}),           _vm_decl_kind);
+    DECLARE_VM_BUILTIN(name({"vm_decl", "to_name"}),        vm_decl_to_name);
+    DECLARE_VM_BUILTIN(name({"vm_decl", "idx"}),            vm_decl_idx);
+    DECLARE_VM_BUILTIN(name({"vm_decl", "arity"}),          vm_decl_arity);
+    DECLARE_VM_BUILTIN(name({"vm_decl", "pos"}),            vm_decl_pos);
+    DECLARE_VM_BUILTIN(name({"vm_decl", "olean"}),          vm_decl_olean);
+    DECLARE_VM_BUILTIN(name({"vm_decl", "args_info"}),      vm_decl_args_info);
+    DECLARE_VM_BUILTIN(name({"vm", "get_decl"}),            vm_get_decl);
+    DECLARE_VM_BUILTIN(name({"vm", "stack_size"}),          vm_stack_size);
+    DECLARE_VM_BUILTIN(name({"vm", "stack_obj"}),           vm_stack_obj);
+    DECLARE_VM_BUILTIN(name({"vm", "stack_obj_info"}),      vm_stack_obj_info);
+    DECLARE_VM_BUILTIN(name({"vm", "call_stack_size"}),     vm_call_stack_size);
+    DECLARE_VM_BUILTIN(name({"vm", "call_stack_fn"}),       vm_call_stack_fn);
+    DECLARE_VM_BUILTIN(name({"vm", "bp"}),                  vm_bp);
+    DECLARE_VM_BUILTIN(name({"vm", "pc"}),                  vm_pc);
+    DECLARE_VM_BUILTIN(name({"vm", "curr_fn"}),             vm_curr_fn);
+    DECLARE_VM_BUILTIN(name({"vm", "obj_to_string"}),       vm_obj_to_string);
 }
 
 void finalize_vm_monitor() {

src/library/vm/vm_declaration.cpp

@@ -44,6 +44,10 @@ struct vm_declaration : public vm_external {
     virtual void dealloc() override { this->~vm_declaration(); get_vm_allocator().deallocate(sizeof(vm_declaration), this); }
 };
 
+bool is_declaration(vm_obj const & o) {
+    return is_external(o) && dynamic_cast<vm_declaration*>(to_external(o));
+}
+
 declaration const & to_declaration(vm_obj const & o) {
     lean_assert(is_external(o));
     lean_assert(dynamic_cast<vm_declaration*>(to_external(o)));

src/library/vm/vm_declaration.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/declaration.h"
 
 namespace lean {
+bool is_declaration(vm_obj const & o);
 declaration const & to_declaration(vm_obj const & o);
 vm_obj to_obj(declaration const & n);
 void initialize_vm_declaration();

src/library/vm/vm_environment.cpp

@@ -30,6 +30,10 @@ struct vm_environment : public vm_external {
     virtual void dealloc() override { this->~vm_environment(); get_vm_allocator().deallocate(sizeof(vm_environment), this); }
 };
 
+bool is_env(vm_obj const & o) {
+    return is_external(o) && dynamic_cast<vm_environment*>(to_external(o));
+}
+
 environment const & to_env(vm_obj const & o) {
     lean_assert(is_external(o));
     lean_assert(dynamic_cast<vm_environment*>(to_external(o)));

src/library/vm/vm_environment.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 
 namespace lean {
+bool is_env(vm_obj const & o);
 environment const & to_env(vm_obj const & o);
 vm_obj to_obj(environment const & n);
 void initialize_vm_environment();

src/library/vm/vm_expr.cpp

@@ -51,6 +51,10 @@ struct vm_expr : public vm_external {
     virtual void dealloc() override { this->~vm_expr(); get_vm_allocator().deallocate(sizeof(vm_expr), this); }
 };
 
+bool is_expr(vm_obj const & o) {
+    return is_external(o) && dynamic_cast<vm_expr*>(to_external(o));
+}
+
 expr const & to_expr(vm_obj const & o) {
     lean_assert(is_external(o));
     lean_assert(dynamic_cast<vm_expr*>(to_external(o)));

src/library/vm/vm_expr.h

@@ -13,6 +13,7 @@ binder_info to_binder_info(vm_obj const & o);
 vm_obj to_obj(binder_info const & bi);
 macro_definition const & to_macro_definition(vm_obj const & o);
 vm_obj to_obj(macro_definition const & d);
+bool is_expr(vm_obj const & o);
 expr const & to_expr(vm_obj const & o);
 vm_obj to_obj(expr const & e);
 vm_obj to_obj(optional<expr> const & e);

src/library/vm/vm_format.cpp

@@ -20,6 +20,10 @@ struct vm_format : public vm_external {
     virtual void dealloc() override { this->~vm_format(); get_vm_allocator().deallocate(sizeof(vm_format), this); }
 };
 
+bool is_format(vm_obj const & o) {
+    return is_external(o) && dynamic_cast<vm_format*>(to_external(o));
+}
+
 format const & to_format(vm_obj const & o) {
     lean_assert(is_external(o));
     lean_assert(dynamic_cast<vm_format*>(to_external(o)));

src/library/vm/vm_format.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 
 namespace lean {
+bool is_format(vm_obj const & o);
 format const & to_format(vm_obj const & o);
 vm_obj to_obj(format const & fmt);
 

src/library/vm/vm_level.cpp

@@ -22,6 +22,10 @@ struct vm_level : public vm_external {
     virtual void dealloc() override { this->~vm_level(); get_vm_allocator().deallocate(sizeof(vm_level), this); }
 };
 
+bool is_level(vm_obj const & o) {
+    return is_external(o) && dynamic_cast<vm_level*>(to_external(o));
+}
+
 level const & to_level(vm_obj const & o) {
     lean_assert(is_external(o));
     lean_assert(dynamic_cast<vm_level*>(to_external(o)));

src/library/vm/vm_level.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/level.h"
 
 namespace lean {
+bool is_level(vm_obj const & o);
 level const & to_level(vm_obj const & o);
 vm_obj to_obj(level const & n);
 void initialize_vm_level();

src/library/vm/vm_name.cpp

@@ -20,6 +20,10 @@ struct vm_name : public vm_external {
     virtual void dealloc() override { this->~vm_name(); get_vm_allocator().deallocate(sizeof(vm_name), this); }
 };
 
+bool is_name(vm_obj const & o) {
+    return is_external(o) && dynamic_cast<vm_name*>(to_external(o));
+}
+
 name const & to_name(vm_obj const & o) {
     lean_assert(is_external(o));
     lean_assert(dynamic_cast<vm_name*>(to_external(o)));

src/library/vm/vm_name.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 
 namespace lean {
+bool is_name(vm_obj const & o);
 name const & to_name(vm_obj const & o);
 vm_obj to_obj(name const & n);
 void initialize_vm_name();

tests/lean/run/basic_monitor3.lean

@@ -0,0 +1,60 @@
+meta def get_file (fn : name) : vm format :=
+do {
+  d ← vm.get_decl fn,
+  some n ← return (vm_decl.olean d) | failure,
+  return (to_fmt n)
+}
+<|>
+return (to_fmt "<curr file>")
+
+meta def pos_info (fn : name) : vm format :=
+do {
+  d                ← vm.get_decl fn,
+  some (line, col) ← return (vm_decl.pos d) | failure,
+  file             ← get_file fn,
+  return (file ++ ":" ++ line ++ ":" ++ col)
+}
+<|>
+return (to_fmt "<position not available>")
+
+meta def obj_fmt (o : vm_obj) : vm format :=
+match o^.kind with
+| vm_obj_kind.tactic_state :=
+     return (to_fmt "state:" ++ format.nest 8 (format.line ++ o^.to_tactic_state^.to_format))
+| _ := do s ← vm.obj_to_string o, return $ to_fmt s
+end
+
+meta def display_args_aux : nat → vm unit
+| i := do
+   sz ← vm.stack_size,
+   if i = sz then return ()
+   else do
+     o ← vm.stack_obj i,
+     (n, t) ← vm.stack_obj_info i,
+     fmt ← obj_fmt o,
+     vm.trace (to_fmt "  " ++ to_fmt n ++ " := " ++ fmt),
+     display_args_aux (i+1)
+
+meta def display_args : vm unit :=
+do bp ← vm.bp,
+   display_args_aux bp
+
+meta def basic_monitor : vm_monitor nat :=
+{ init := 1000,
+  step := λ sz, do
+    csz ← vm.call_stack_size,
+    if sz = csz then return sz
+    else do
+      fn  ← vm.curr_fn,
+      pos ← pos_info fn,
+      vm.trace (to_fmt "[" ++ csz ++ "]: " ++ to_fmt fn ++ " @ " ++ pos),
+      display_args,
+      return csz }
+
+run_command vm_monitor.register `basic_monitor
+
+set_option debugger true
+open tactic
+
+example (a b : Prop) : a → b → a ∧ b :=
+by (intros >> constructor >> repeat assumption)