max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc(library/init/meta/vm): document VM introspection API

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-16 13:05:08 -08:00
parent 91c8ff746f
commit aebe1f4946
2 changed files with 71 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

51
library/init/meta/vm.lean
View file

@ -16,16 +16,29 @@ inductive vm_obj_kind
namespace vm_obj
meta constant kind : vm_obj → vm_obj_kind
/- For simple and constructor vm_obj's, it returns the constructor tag/index.
Return 0 otherwise. -/
meta constant cidx : vm_obj → nat
/- For closure vm_obj's, it returns the internal function index. -/
meta constant fn_idx : vm_obj → nat
/- For constructor vm_obj's, it returns the data stored in the object.
For closure vm_obj's, it returns the local arguments captured by the closure. -/
meta constant fields : vm_obj → list vm_obj
/- For simple and mpz vm_obj's -/
meta constant to_nat : vm_obj → nat
/- For name vm_obj's, it returns the name wrapped by the vm_obj. -/
meta constant to_name : vm_obj → name
/- For level vm_obj's, it returns the universe level wrapped by the vm_obj. -/
meta constant to_level : vm_obj → level
/- For expr vm_obj's, it returns the expression wrapped by the vm_obj. -/
meta constant to_expr : vm_obj → expr
/- For declaration vm_obj's, it returns the declaration wrapped by the vm_obj. -/
meta constant to_declaration : vm_obj → declaration
/- For environment vm_obj's, it returns the environment wrapped by the vm_obj. -/
meta constant to_environment : vm_obj → environment
/- For tactic_state vm_obj's, it returns the tactic_state object wrapped by the vm_obj. -/
meta constant to_tactic_state : vm_obj → tactic_state
/- For format vm_obj's, it returns the format object wrapped by the vm_obj. -/
meta constant to_format : vm_obj → format
end vm_obj
@ -34,16 +47,23 @@ meta constant vm_decl : Type
inductive vm_decl_kind
| bytecode | builtin | cfun
structure vm_local_info :=
(id : name) (pos : option (nat × nat))
/- Information for local variables and arguments on the VM stack.
Remark: type is only available if it is a closed term at compilation time. -/
meta structure vm_local_info :=
(id : name) (type : option expr)
namespace vm_decl
meta constant kind : vm_decl → vm_decl_kind
meta constant to_name : vm_decl → name
/- Internal function index associated with the given VM declaration. -/
meta constant idx : vm_decl → nat
/- Number of arguments needed to execute the given VM declaration. -/
meta constant arity : vm_decl → nat
/- Return (line, column) if available -/
meta constant pos : vm_decl → option (nat × nat)
/- Return .olean file where the given VM declaration was imported from. -/
meta constant olean : vm_decl → option string
/- Return names .olean file where the given VM declaration was imported from. -/
meta constant args_info : vm_decl → list vm_local_info
end vm_decl
@ -62,20 +82,42 @@ meta constant get_env : vm environment
meta constant get_decl : name → vm vm_decl
meta constant get_options : vm options
meta constant stack_size : vm nat
/- Return the vm_obj stored at the given position on the execution stack.
It fails if position >= vm.stack_size -/
meta constant stack_obj : nat → vm vm_obj
/- Return (name, type) for the object at the given position on the execution stack.
It fails if position >= vm.stack_size.
The name is anonymous if vm_obj is a transient value created by the compiler.
Type information is only recorded if the type is a closed term at compilation time. -/
meta constant stack_obj_info : nat → vm (name × option expr)
/- Pretty print the vm_obj at the given position on the execution stack. -/
meta constant pp_stack_obj : nat → vm format
/- Pretty print the given expression. -/
meta constant pp_expr : expr → vm format
/- Number of frames on the call stack. -/
meta constant call_stack_size : vm nat
/- Return the function name at the given stack frame.
Action fails if position >= vm.call_stack_size. -/
meta constant call_stack_fn : nat → vm name
/- Return the range [start, end) for the given stack frame.
Action fails if position >= vm.call_stack_size.
The values start and end correspond to positions at the execution stack.
We have that 0 <= start < end <= vm.stack_size -/
meta constant call_stack_var_range : nat → vm (nat × nat)
/- Return the name of the function on top of the call stack. -/
meta constant curr_fn : vm name
/- Return the base stack pointer for the frame on top of the call stack. -/
meta constant bp : vm nat
/- Return the program counter. -/
meta constant pc : vm nat
/- Convert the given vm_obj into a string -/
meta constant obj_to_string : vm_obj → vm string
meta constant put_str : string → vm unit
meta constant get_line : vm string
/- Return tt if end of the input stream has been reached.
For example, this can happen if the user presses Ctrl-D -/
meta constant eof : vm bool
/- Return the list of declarations tagged with the given attribute. -/
meta constant get_attribute : name → vm (list name)
meta def trace {A : Type} [has_to_format A] (a : A) : vm unit :=
@ -88,5 +130,8 @@ meta structure vm_monitor (s : Type) :=
(init : s) (step : s → vm s)
/- Registers a new virtual machine monitor. The argument must be the name of a definition of type
`vm_monitor S`. The command will override the last monitor. -/
`vm_monitor S`. The command will override the last monitor.
If option 'debugger' is true, then the VM will initialize the vm_monitor state using the
'init' field, and will invoke the function 'step' before each instruction is invoked. -/
meta constant vm_monitor.register : name → command

33
tmp/cli_debugger.lean
View file

@ -61,16 +61,16 @@ do {
<|>
return "<position not available>"
meta def display_fn (header : string) (fn : name) (frame : nat) : vm unit :=
meta def show_fn (header : string) (fn : name) (frame : nat) : vm unit :=
do pos ← pos_info fn,
vm.put_str ("[" ++ frame^.to_string ++ "] " ++ header ++ " " ++ fn^.to_string ++ " at " ++ pos ++ "\n")
meta def display_curr_fn (header : string) : vm unit :=
meta def show_curr_fn (header : string) : vm unit :=
do fn ← vm.curr_fn,
sz ← vm.call_stack_size,
display_fn header fn (sz-1)
show_fn header fn (sz-1)
meta def display_help : vm unit :=
meta def show_help : vm unit :=
do
vm.put_str "exit - stop debugger\n",
vm.put_str "help - display this message\n",
@ -80,6 +80,7 @@ do
vm.put_str " up - move up in the stack trace\n",
vm.put_str " down - move down in the stack trace\n",
vm.put_str " vars - display variables in the current stack frame\n",
vm.put_str " stack - display all functions on the call stack\n",
vm.put_str "breakpoints\n",
vm.put_str " break fn - add breakpoint for fn\n",
vm.put_str " rbreak fn - remove breakpoint\n",
@ -128,7 +129,7 @@ meta def show_breakpoints : list name → vm unit
meta def show_frame (frame : nat) : vm unit :=
do sz ← vm.call_stack_size,
fn ← if frame >= sz then vm.curr_fn else vm.call_stack_fn frame,
display_fn "frame" fn frame
show_fn "frame" fn frame
meta def up (frame : nat) : vm nat :=
if frame = 0 then return 0
@ -175,6 +176,17 @@ meta def show_vars (frame : nat) : vm unit :=
do (s, e) ← vm.call_stack_var_range frame,
show_vars_core 0 s e
meta def show_stack_core : nat → vm unit
| 0 := return ()
| (i+1) := do
fn ← vm.call_stack_fn i,
show_fn "stack" fn i,
show_stack_core i
meta def show_stack : vm unit :=
do sz ← vm.call_stack_size,
show_stack_core sz
meta def cmd_loop_core : state → nat → list string → vm state
| s frame default_cmd := do
is_eof ← vm.eof,
@ -189,7 +201,7 @@ meta def cmd_loop_core : state → nat → list string → vm state
match tks with
| [] := cmd_loop_core s frame default_cmd
| (cmd::args) :=
if cmd = "help" then display_help >> cmd_loop_core s frame default_cmd
if cmd = "help" then show_help >> cmd_loop_core s frame default_cmd
else if cmd = "exit" then return {s with md := mode.done }
else if cmd = "run" ∨ cmd = "r" then return {s with md := mode.run }
else if cmd = "step" ∨ cmd = "s" then return {s with md := mode.step }
@ -201,7 +213,8 @@ meta def cmd_loop_core : state → nat → list string → vm state
cmd_loop_core s frame default_cmd
else if cmd = "up" ∨ cmd = "u" then do frame ← up frame, cmd_loop_core s frame ["u"]
else if cmd = "down" ∨ cmd = "d" then do frame ← down frame, cmd_loop_core s frame ["d"]
else if cmd = "vars" ∨ cmd = "v" then do show_vars frame, cmd_loop_core s frame ["vars"]
else if cmd = "vars" ∨ cmd = "v" then do show_vars frame, cmd_loop_core s frame []
else if cmd = "stack" then do show_stack, cmd_loop_core s frame []
else do vm.put_str "unknown command, type 'help' for help\n", cmd_loop_core s frame default_cmd
end
@ -231,7 +244,7 @@ do opts ← vm.get_options,
return {new_s with md := mode.run}
else do
vm.put_str "Lean debugger\n",
display_curr_fn "debugging",
show_curr_fn "debugging",
vm.put_str "type 'help' for help\n",
cmd_loop new_s []
@ -240,7 +253,7 @@ do
sz ← vm.call_stack_size,
if sz = s^.csz then return s
else do
display_curr_fn "step",
show_curr_fn "step",
cmd_loop s ["s"]
meta def bp_reached (s : state) : vm bool :=
@ -259,7 +272,7 @@ do b1 ← in_active_bps s,
b2 ← bp_reached s,
if b1 ∨ not b2 then return s
else do
display_curr_fn "breakpoint",
show_curr_fn "breakpoint",
fn ← vm.curr_fn,
sz ← vm.call_stack_size,
new_s ← return $ {s with active_bps := (sz, fn) :: s^.active_bps},