diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 97 | ||||
| -rw-r--r-- | proofs/tactic_debug.mli | 7 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 5 |
4 files changed, 81 insertions, 33 deletions
@@ -13,6 +13,11 @@ Vernacular commands - New command "Set Parsing Explicit" for deactivating parsing (and printing) of implicit arguments (useful for teaching). +Tactics + +- New command "r string" that interprets "idtac string" as a breakpoint + and jumps to its next use in Ltac debugger. + Changes from V8.3 to V8.4beta ============================= diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 1c2fb2787..7d7688873 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -49,11 +49,12 @@ let db_pr_goal g = (* Prints the commands *) let help () = - msgnl (str "Commands: <Enter>=Continue" ++ fnl() ++ - str " h/?=Help" ++ fnl() ++ - str " r<num>=Run <num> times" ++ fnl() ++ - str " s=Skip" ++ fnl() ++ - str " x=Exit") + msgnl (str "Commands: <Enter> = Continue" ++ fnl() ++ + str " h/? = Help" ++ fnl() ++ + str " r <num> = Run <num> times" ++ fnl() ++ + str " r <string> = Run up to next idtac <string>" ++ fnl() ++ + str " s = Skip" ++ fnl() ++ + str " x = Exit") (* Prints the goal and the command to be executed *) let goal_com g tac = @@ -62,37 +63,56 @@ let goal_com g tac = msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ()) end -(* Gives the number of a run command *) +let skipped = ref 0 +let skip = ref 0 +let breakpoint = ref None + +let rec drop_spaces inst i = + if String.length inst > i && inst.[i] = ' ' then drop_spaces inst (i+1) + else i + +(* (Re-)initialize debugger *) +let db_initialize () = + skip:=0;skipped:=0;breakpoint:=None + +(* Gives the number of steps or next breakpoint of a run command *) let run_com inst = if (String.get inst 0)='r' then - let num = int_of_string (String.sub inst 1 ((String.length inst)-1)) in - if num>0 then num - else raise (Invalid_argument "run_com") + let i = drop_spaces inst 1 in + if String.length inst > i then + let s = String.sub inst i (String.length inst - i) in + if inst.[0] >= '0' && inst.[0] <= '9' then + let num = int_of_string s in + if num<0 then raise (Invalid_argument "run_com"); + skip:=num;skipped:=0 + else + breakpoint:=Some s + else + raise (Invalid_argument "run_com") else raise (Invalid_argument "run_com") -let allskip = ref 0 -let skip = ref 0 - (* Prints the run counter *) let run ini = if not ini then + begin for i=1 to 2 do print_char (Char.chr 8);print_char (Char.chr 13) done; - msg (str "Executed expressions: " ++ int (!allskip - !skip) ++ - fnl() ++ fnl()) + msg (str "Executed expressions: " ++ int !skipped ++ fnl() ++ fnl()) + end; + incr skipped (* Prints the prompt *) let rec prompt level = begin msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > "); flush stdout; - let exit () = skip:=0;allskip:=0;raise Sys.Break in + let exit () = skip:=0;skipped:=0;raise Sys.Break in let inst = try read_line () with End_of_file -> exit () in match inst with - | "" -> true - | "s" -> false + | "" -> DebugOn (level+1) + | "s" -> DebugOff | "x" -> print_char (Char.chr 8); exit () | "h"| "?" -> begin @@ -100,32 +120,34 @@ let rec prompt level = prompt level end | _ -> - (try let ctr=run_com inst in skip:=ctr;allskip:=ctr;run true;true + (try run_com inst;run true;DebugOn (level+1) with Failure _ | Invalid_argument _ -> prompt level) end (* Prints the state and waits for an instruction *) let debug_prompt lev g tac f = (* What to print and to do next *) - let continue = - if !skip = 0 then (goal_com g tac; prompt lev) - else (decr skip; run false; if !skip=0 then allskip:=0; true) in + let newlevel = + if !skip = 0 then + if !breakpoint = None then (goal_com g tac; prompt lev) + else (run false; DebugOn (lev+1)) + else (decr skip; run false; if !skip=0 then skipped:=0; DebugOn (lev+1)) in (* What to execute *) - try f (if continue then DebugOn (lev+1) else DebugOff) + try f newlevel with e -> - skip:=0; allskip:=0; + skip:=0; skipped:=0; if Logic.catchable_exception e then ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e); raise e (* Prints a constr *) let db_constr debug env c = - if debug <> DebugOff & !skip = 0 then + if debug <> DebugOff & !skip = 0 & !breakpoint = None then msgnl (str "Evaluated term: " ++ print_constr_env env c) (* Prints the pattern rule *) let db_pattern_rule debug num r = - if debug <> DebugOff & !skip = 0 then + if debug <> DebugOff & !skip = 0 & !breakpoint = None then begin msgnl (str "Pattern rule " ++ int num ++ str ":"); msgnl (str "|" ++ spc () ++ !prmatchrl r) @@ -138,38 +160,38 @@ let hyp_bound = function (* Prints a matched hypothesis *) let db_matched_hyp debug env (id,_,c) ido = - if debug <> DebugOff & !skip = 0 then + if debug <> DebugOff & !skip = 0 & !breakpoint = None then msgnl (str "Hypothesis " ++ str ((Names.string_of_id id)^(hyp_bound ido)^ " has been matched: ") ++ print_constr_env env c) (* Prints the matched conclusion *) let db_matched_concl debug env c = - if debug <> DebugOff & !skip = 0 then + if debug <> DebugOff & !skip = 0 & !breakpoint = None then msgnl (str "Conclusion has been matched: " ++ print_constr_env env c) (* Prints a success message when the goal has been matched *) let db_mc_pattern_success debug = - if debug <> DebugOff & !skip = 0 then + if debug <> DebugOff & !skip = 0 & !breakpoint = None then msgnl (str "The goal has been successfully matched!" ++ fnl() ++ str "Let us execute the right-hand side part..." ++ fnl()) (* Prints a failure message for an hypothesis pattern *) let db_hyp_pattern_failure debug env (na,hyp) = - if debug <> DebugOff & !skip = 0 then + if debug <> DebugOff & !skip = 0 & !breakpoint = None then msgnl (str ("The pattern hypothesis"^(hyp_bound na)^ " cannot match: ") ++ !prmatchpatt env hyp) (* Prints a matching failure message for a rule *) let db_matching_failure debug = - if debug <> DebugOff & !skip = 0 then + if debug <> DebugOff & !skip = 0 & !breakpoint = None then msgnl (str "This rule has failed due to matching errors!" ++ fnl() ++ str "Let us try the next one...") (* Prints an evaluation failure message for a rule *) let db_eval_failure debug s = - if debug <> DebugOff & !skip = 0 then + if debug <> DebugOff & !skip = 0 & !breakpoint = None then let s = str "message \"" ++ s ++ str "\"" in msgnl (str "This rule has failed due to \"Fail\" tactic (" ++ @@ -177,9 +199,20 @@ let db_eval_failure debug s = (* Prints a logic failure message for a rule *) let db_logic_failure debug err = - if debug <> DebugOff & !skip = 0 then + if debug <> DebugOff & !skip = 0 & !breakpoint = None then begin msgnl (!explain_logic_error err); msgnl (str "This rule has failed due to a logic error!" ++ fnl() ++ str "Let us try the next one...") end + +let is_breakpoint brkname s = match brkname, s with + | Some s, MsgString s'::_ -> s = s' + | _ -> false + +let db_breakpoint debug s = + match debug with + | DebugOn lev when s <> [] & is_breakpoint !breakpoint s -> + breakpoint:=None + | _ -> + () diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index d96f4c746..62c2359b6 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -34,6 +34,9 @@ type debug_info = val debug_prompt : int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a +(** Initializes debugger *) +val db_initialize : unit -> unit + (** Prints a constr *) val db_constr : debug_info -> env -> constr -> unit @@ -72,3 +75,7 @@ val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref (** Prints a logic failure message for a rule *) val db_logic_failure : debug_info -> exn -> unit + +(** Prints a logic failure message for a rule *) +val db_breakpoint : debug_info -> + identifier Util.located message_token list -> unit diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a41cd6e72..fecc2bac1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1769,7 +1769,9 @@ and eval_tactic ist = function catch_error (push_trace(loc,call)ist.trace) tac gl | TacFun _ | TacLetIn _ -> assert false | TacMatchGoal _ | TacMatch _ -> assert false - | TacId s -> fun gl -> tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl + | TacId s -> fun gl -> + let res = tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl in + db_breakpoint ist.debug s; res | TacFail (n,s) -> fun gl -> tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) | TacAbstract (tac,ido) -> @@ -2488,6 +2490,7 @@ let interp_tac_gen lfun avoid_ids debug t gl = gsigma = project gl; genv = pf_env gl } t) gl let eval_tactic t gls = + db_initialize (); interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } t gls |