diff --git a/library/tools/debugger/cli.lean b/library/tools/debugger/cli.lean index f0a6cc3f38..fa4831f771 100644 --- a/library/tools/debugger/cli.lean +++ b/library/tools/debugger/cli.lean @@ -197,8 +197,10 @@ do cmd_loop s ["s"] meta def bp_reached (s : state) : vm bool := -do fn ← vm.curr_fn, - return $ s^.fn_bps^.any (λ p, p^.is_prefix_of fn) +(do fn ← vm.curr_fn, + return $ s^.fn_bps^.any (λ p, p^.is_prefix_of fn)) +<|> +return ff meta def in_active_bps (s : state) : vm bool := do sz ← vm.call_stack_size, diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp index f4f045c537..b0b7382ef3 100644 --- a/src/library/tactic/vm_monitor.cpp +++ b/src/library/tactic/vm_monitor.cpp @@ -375,7 +375,11 @@ vm_obj vm_get_options(vm_obj const & /*s*/) { } vm_obj vm_curr_fn(vm_obj const & /*s*/) { - return mk_vm_success(to_obj(get_vm_state_being_debugged().curr_fn())); + if (auto fn = get_vm_state_being_debugged().curr_fn()) { + return mk_vm_success(to_obj(*fn)); + } else { + return mk_vm_failure(); + } } vm_obj vm_obj_to_string(vm_obj const & o, vm_obj const & /*s*/) { diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 2abfccbdaa..e194ac6db4 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -3034,6 +3034,13 @@ optional vm_state::get_decl(name const & n) const { return optional(); } +optional vm_state::curr_fn() const { + if (m_fn_idx == g_null_fn_idx) + return optional(); + else + return optional(m_decl_map.find(m_fn_idx)->get_name()); +} + #if defined(LEAN_MULTI_THREAD) static name * g_profiler = nullptr; static name * g_profiler_freq = nullptr; diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 5982accc74..aa50824b22 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -687,7 +687,7 @@ public: optional get_decl(name const & n) const; - name curr_fn() const { return m_decl_map.find(m_fn_idx)->get_name(); } + optional curr_fn() const; void invoke_fn(name const & fn); void invoke_fn(unsigned fn_idx); diff --git a/tests/lean/run/basic_monitor3.lean b/tests/lean/run/basic_monitor3.lean index b7f8e512d5..1efcab3ae6 100644 --- a/tests/lean/run/basic_monitor3.lean +++ b/tests/lean/run/basic_monitor3.lean @@ -44,12 +44,18 @@ meta def basic_monitor : vm_monitor nat := step := λ sz, do csz ← vm.call_stack_size, if sz = csz then return sz - else do + else + do { fn ← vm.curr_fn, pos ← pos_info fn, vm.trace (to_fmt "[" ++ csz ++ "]: " ++ to_fmt fn ++ " @ " ++ pos), display_args, - return csz } + return csz + } + <|> + return csz -- curr_fn failed +} + run_command vm_monitor.register `basic_monitor