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

feat(library): add debugger

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-16 14:53:13 -08:00
parent a94368375c
commit 47cd475052
6 changed files with 162 additions and 149 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/data/list.lean
View file

@ -5,7 +5,6 @@ Author: Jeremy Avigad
This is a minimal port of functions from the lean2 list library.
-/
import init.list
import algebra.order
import data.nat

167
tmp/cli_debugger.lean → library/debugger/cli.lean
View file

@ -1,3 +1,12 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Simple command line interface for debugging Lean programs and tactics.
-/
import debugger.util
namespace debugger
inductive mode
@ -16,66 +25,12 @@ def init_state : state :=
{ md := mode.init, csz := 0,
fn_bps := [], active_bps := [] }
def is_space (c : char) : bool :=
if c = ' ' ∨ c = char.of_nat 11 ∨ c = '\n' then tt else ff
def split_core : string → string → list string
| (c::cs) [] :=
if is_space c then split_core cs [] else split_core cs [c]
| (c::cs) r :=
if is_space c then r^.reverse :: split_core cs [] else split_core cs (c::r)
| [] [] := []
| [] r := [r^.reverse]
def split (s : string) : list string :=
(split_core s [])^.reverse
def to_qualified_name_core : string → string → name
| [] r := if r = [] then name.anonymous else mk_simple_name r^.reverse
| (c::cs) r :=
if is_space c then to_qualified_name_core cs r
else if c = '.' then
if r = [] then to_qualified_name_core cs []
else name.mk_string r^.reverse (to_qualified_name_core cs [])
else to_qualified_name_core cs (c::r)
def to_qualified_name (s : string) : name :=
to_qualified_name_core s []
meta def get_file (fn : name) : vm string :=
do {
d ← vm.get_decl fn,
some n ← return (vm_decl.olean d) | failure,
return n
}
<|>
return "[current file]"
meta def pos_info (fn : name) : vm string :=
do {
d ← vm.get_decl fn,
some (line, col) ← return (vm_decl.pos d) | failure,
file ← get_file fn,
return (file ++ ":" ++ line^.to_string ++ ":" ++ col^.to_string)
}
<|>
return "<position not available>"
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 show_curr_fn (header : string) : vm unit :=
do fn ← vm.curr_fn,
sz ← vm.call_stack_size,
show_fn header fn (sz-1)
meta def show_help : vm unit :=
do
vm.put_str "exit - stop debugger\n",
vm.put_str "help - display this message\n",
vm.put_str "run - continue execution\n",
vm.put_str "step - execute until another function in on the top of the stack\n",
vm.put_str "exit - stop debugger\n",
vm.put_str "help - display this message\n",
vm.put_str "run - continue execution\n",
vm.put_str "step - execute until another function in on the top of the stack\n",
vm.put_str "stack trace\n",
vm.put_str " up - move up in the stack trace\n",
vm.put_str " down - move down in the stack trace\n",
@ -88,13 +43,6 @@ do
vm.put_str " rbreak fn - remove breakpoint\n",
vm.put_str " bs - show breakpoints\n"
meta def is_valid_fn_prefix (p : name) : vm bool :=
do env ← vm.get_env,
return $ env^.fold ff (λ d r,
r ||
let n := d^.to_name in
p^.is_prefix_of n)
meta def add_breakpoint (s : state) (args : list string) : vm state :=
match args with
| [arg] := do
@ -128,67 +76,15 @@ meta def show_breakpoints : list name → vm unit
vm.put_str "\n",
show_breakpoints fns
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,
show_fn "frame" fn frame
meta def up (frame : nat) : vm nat :=
meta def up_cmd (frame : nat) : vm nat :=
if frame = 0 then return 0
else show_frame (frame - 1) >> return (frame - 1)
meta def down (frame : nat) : vm nat :=
meta def down_cmd (frame : nat) : vm nat :=
do sz ← vm.call_stack_size,
if frame >= sz - 1 then return frame
else show_frame (frame + 1) >> return (frame + 1)
meta def type_to_string : option expr → nat → vm string
| none i := do
o ← vm.stack_obj i,
match o^.kind with
| vm_obj_kind.simple := return "[tagged value]"
| vm_obj_kind.constructor := return "[constructor]"
| vm_obj_kind.closure := return "[closure]"
| vm_obj_kind.mpz := return "[big num]"
| vm_obj_kind.name := return "name"
| vm_obj_kind.level := return "level"
| vm_obj_kind.expr := return "expr"
| vm_obj_kind.declaration := return "declaration"
| vm_obj_kind.environment := return "environment"
| vm_obj_kind.tactic_state := return "tactic_state"
| vm_obj_kind.format := return "format"
| vm_obj_kind.options := return "options"
| vm_obj_kind.other := return "[other]"
end
| (some type) i := do
fmt ← vm.pp_expr type,
opts ← vm.get_options,
return (fmt^.to_string opts)
meta def show_vars_core : nat → nat → nat → vm unit
| c i e :=
if i = e then return ()
else do
(n, type) ← vm.stack_obj_info i,
type_str ← type_to_string type i,
vm.put_str $ "#" ++ c^.to_string ++ " " ++ n^.to_string ++ " : " ++ type_str ++ "\n",
show_vars_core (c+1) (i+1) e
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 pidx_cmd : nat → list string → vm unit
| frame [arg] := do
idx ← return $ arg^.to_nat,
@ -243,18 +139,18 @@ 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 show_help >> cmd_loop_core s frame default_cmd
if cmd = "help" ∨ cmd = "h" then show_help >> cmd_loop_core s frame []
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 }
else if cmd = "break" ∨ cmd = "b" then do new_s ← add_breakpoint s args, cmd_loop_core new_s frame default_cmd
else if cmd = "rbreak" then do new_s ← remove_breakpoint s args, cmd_loop_core new_s frame default_cmd
else if cmd = "break" ∨ cmd = "b" then do new_s ← add_breakpoint s args, cmd_loop_core new_s frame []
else if cmd = "rbreak" then do new_s ← remove_breakpoint s args, cmd_loop_core new_s frame []
else if cmd = "bs" then do
vm.put_str "breakpoints\n",
show_breakpoints s^.fn_bps,
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 = "up" ∨ cmd = "u" then do frame ← up_cmd frame, cmd_loop_core s frame ["u"]
else if cmd = "down" ∨ cmd = "d" then do frame ← down_cmd frame, cmd_loop_core s frame ["d"]
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 if cmd = "pidx" then do pidx_cmd frame args, cmd_loop_core s frame []
@ -332,29 +228,6 @@ do s ← prune_active_bps s,
meta def monitor : vm_monitor state :=
{ init := init_state, step := step_fn }
def attr : user_attribute :=
{ name := `breakpoint,
descr := "breakpoint for debugger" }
end debugger
run_command vm_monitor.register `debugger.monitor
run_command attribute.register `debugger.attr
set_option debugger true
set_option debugger.autorun true
def g (c : nat) := c + 1
def h (a : nat) (b : nat) := g (b+2) + a
def s (a : nat) := h 2 a + h 3 a
local attribute [breakpoint] h
def f : nat → nat
| 0 := s 0
| (a+1) := f a
vm_eval f 3

6
library/debugger/default.lean Normal file
View file

@ -0,0 +1,6 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import debugger.util debugger.cli

124
library/debugger/util.lean Normal file
View file

@ -0,0 +1,124 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
namespace debugger
def is_space (c : char) : bool :=
if c = ' ' ∨ c = char.of_nat 11 ∨ c = '\n' then tt else ff
def split_core : string → string → list string
| (c::cs) [] :=
if is_space c then split_core cs [] else split_core cs [c]
| (c::cs) r :=
if is_space c then r^.reverse :: split_core cs [] else split_core cs (c::r)
| [] [] := []
| [] r := [r^.reverse]
def split (s : string) : list string :=
(split_core s [])^.reverse
def to_qualified_name_core : string → string → name
| [] r := if r = [] then name.anonymous else mk_simple_name r^.reverse
| (c::cs) r :=
if is_space c then to_qualified_name_core cs r
else if c = '.' then
if r = [] then to_qualified_name_core cs []
else name.mk_string r^.reverse (to_qualified_name_core cs [])
else to_qualified_name_core cs (c::r)
def to_qualified_name (s : string) : name :=
to_qualified_name_core s []
def olean_to_lean (s : string) :=
list.dropn 5 s ++ "lean"
meta def get_file (fn : name) : vm string :=
do {
d ← vm.get_decl fn,
some n ← return (vm_decl.olean d) | failure,
return (olean_to_lean n)
}
<|>
return "[current file]"
meta def pos_info (fn : name) : vm string :=
do {
d ← vm.get_decl fn,
some (line, col) ← return (vm_decl.pos d) | failure,
file ← get_file fn,
return (file ++ ":" ++ line^.to_string ++ ":" ++ col^.to_string)
}
<|>
return "<position not available>"
meta def show_fn (header : string) (fn : name) (frame : nat) : vm unit :=
do pos ← pos_info fn,
vm.put_str ("[" ++ frame^.to_string ++ "] " ++ header),
if header = "" then return () else vm.put_str " ",
vm.put_str (fn^.to_string ++ " at " ++ pos ++ "\n")
meta def show_curr_fn (header : string) : vm unit :=
do fn ← vm.curr_fn,
sz ← vm.call_stack_size,
show_fn header fn (sz-1)
meta def is_valid_fn_prefix (p : name) : vm bool :=
do env ← vm.get_env,
return $ env^.fold ff (λ d r,
r ||
let n := d^.to_name in
p^.is_prefix_of n)
meta def show_frame (frame_idx : nat) : vm unit :=
do sz ← vm.call_stack_size,
fn ← if frame_idx >= sz then vm.curr_fn else vm.call_stack_fn frame_idx,
show_fn "" fn frame_idx
meta def type_to_string : option expr → nat → vm string
| none i := do
o ← vm.stack_obj i,
match o^.kind with
| vm_obj_kind.simple := return "[tagged value]"
| vm_obj_kind.constructor := return "[constructor]"
| vm_obj_kind.closure := return "[closure]"
| vm_obj_kind.mpz := return "[big num]"
| vm_obj_kind.name := return "name"
| vm_obj_kind.level := return "level"
| vm_obj_kind.expr := return "expr"
| vm_obj_kind.declaration := return "declaration"
| vm_obj_kind.environment := return "environment"
| vm_obj_kind.tactic_state := return "tactic_state"
| vm_obj_kind.format := return "format"
| vm_obj_kind.options := return "options"
| vm_obj_kind.other := return "[other]"
end
| (some type) i := do
fmt ← vm.pp_expr type,
opts ← vm.get_options,
return (fmt^.to_string opts)
meta def show_vars_core : nat → nat → nat → vm unit
| c i e :=
if i = e then return ()
else do
(n, type) ← vm.stack_obj_info i,
type_str ← type_to_string type i,
vm.put_str $ "#" ++ c^.to_string ++ " " ++ n^.to_string ++ " : " ++ type_str ++ "\n",
show_vars_core (c+1) (i+1) e
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 "" fn i,
show_stack_core i
meta def show_stack : vm unit :=
do sz ← vm.call_stack_size,
show_stack_core sz
end debugger

2
library/init/default.lean
View file

@ -11,5 +11,5 @@ import init.funext init.function init.subtype init.classical init.congr
import init.monad init.option init.state init.fin init.list init.char init.string init.to_string
import init.monad_combinators init.set
import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe
import init.wf init.nat_div init.meta init.instances
import init.wf init.nat_div init.meta init.instances init.breakpoint
import init.sigma_lex init.id_locked init.order init.algebra

11
tmp/debugger_example.lean Normal file
View file

@ -0,0 +1,11 @@
import debugger
set_option debugger true
set_option debugger.autorun true
open tactic
local attribute [breakpoint] tactic.constructor
example (p q : Prop) : p → q → p ∧ q :=
by do intros, constructor, repeat assumption