summaryrefslogtreecommitdiff
path: root/ltac/tactic_debug.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ltac/tactic_debug.ml')
-rw-r--r--ltac/tactic_debug.ml422
1 files changed, 422 insertions, 0 deletions
diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
new file mode 100644
index 00000000..5cbddc7f
--- /dev/null
+++ b/ltac/tactic_debug.ml
@@ -0,0 +1,422 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Util
+open Names
+open Pp
+open Tacexpr
+open Termops
+open Nameops
+open Proofview.Notations
+
+
+let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
+
+let prtac x =
+ Pptactic.pr_glob_tactic (Global.env()) x
+let prmatchpatt env sigma hyp =
+ Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
+let prmatchrl rl =
+ Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
+ (fun (_,p) -> Printer.pr_constr_pattern p) rl
+
+(* This module intends to be a beginning of debugger for tactic expressions.
+ Currently, it is quite simple and we can hope to have, in the future, a more
+ complete panel of commands dedicated to a proof assistant framework *)
+
+(* Debug information *)
+type debug_info =
+ | DebugOn of int
+ | DebugOff
+
+(* An exception handler *)
+let explain_logic_error e =
+ CErrors.print (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)))
+
+let explain_logic_error_no_anomaly e =
+ CErrors.print_no_report
+ (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)))
+
+let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
+let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
+
+(* Prints the goal *)
+
+let db_pr_goal gl =
+ let env = Proofview.Goal.env gl in
+ let concl = Proofview.Goal.concl gl in
+ let penv = print_named_context env in
+ let pc = print_constr_env env concl in
+ str" " ++ hv 0 (penv ++ fnl () ++
+ str "============================" ++ fnl () ++
+ str" " ++ pc) ++ fnl ()
+
+let db_pr_goal =
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let pg = db_pr_goal gl in
+ Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
+ end }
+
+
+(* Prints the commands *)
+let help () =
+ msg_tac_debug (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 tac =
+ Proofview.tclTHEN
+ db_pr_goal
+ (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ prtac tac)))
+
+(* [run (new_ref _)] gives us a ref shared among [NonLogical.t]
+ expressions. It avoids parametrizing everything over a
+ reference. *)
+let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
+let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
+let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None)
+
+let rec drop_spaces inst i =
+ if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
+ else i
+
+let possibly_unquote s =
+ if String.length s >= 2 && s.[0] == '"' && s.[String.length s - 1] == '"' then
+ String.sub s 1 (String.length s - 2)
+ else
+ s
+
+(* (Re-)initialize debugger *)
+let db_initialize =
+ let open Proofview.NonLogical in
+ (skip:=0) >> (skipped:=0) >> (breakpoint:=None)
+
+let int_of_string s =
+ try Proofview.NonLogical.return (int_of_string s)
+ with e -> Proofview.NonLogical.raise e
+
+let string_get s i =
+ try Proofview.NonLogical.return (String.get s i)
+ with e -> Proofview.NonLogical.raise e
+
+(* Gives the number of steps or next breakpoint of a run command *)
+let run_com inst =
+ let open Proofview.NonLogical in
+ string_get inst 0 >>= fun first_char ->
+ if first_char ='r' then
+ 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
+ int_of_string s >>= fun num ->
+ (if num<0 then invalid_arg "run_com" else return ()) >>
+ (skip:=num) >> (skipped:=0)
+ else
+ breakpoint:=Some (possibly_unquote s)
+ else
+ invalid_arg "run_com"
+ else
+ invalid_arg "run_com"
+
+(* Prints the run counter *)
+let run ini =
+ let open Proofview.NonLogical in
+ if not ini then
+ begin
+ Proofview.NonLogical.print_notice (str"\b\r\b\r") >>
+ !skipped >>= fun skipped ->
+ msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl())
+ end >>
+ !skipped >>= fun x ->
+ skipped := x+1
+ else
+ return ()
+
+(* Prints the prompt *)
+let rec prompt level =
+ (* spiwack: avoid overriding by the open below *)
+ let runtrue = run true in
+ begin
+ let open Proofview.NonLogical in
+ Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+ let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
+ Proofview.NonLogical.catch Proofview.NonLogical.read_line
+ begin function (e, info) -> match e with
+ | End_of_file -> exit
+ | e -> raise ~info e
+ end
+ >>= fun inst ->
+ match inst with
+ | "" -> return (DebugOn (level+1))
+ | "s" -> return (DebugOff)
+ | "x" -> Proofview.NonLogical.print_char '\b' >> exit
+ | "h"| "?" ->
+ begin
+ help () >>
+ prompt level
+ end
+ | _ ->
+ Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1)))
+ begin function (e, info) -> match e with
+ | Failure _ | Invalid_argument _ -> prompt level
+ | e -> raise ~info e
+ end
+ end
+
+(* Prints the state and waits for an instruction *)
+(* spiwack: the only reason why we need to take the continuation [f]
+ as an argument rather than returning the new level directly seems to
+ be that [f] is wrapped in with "explain_logic_error". I don't think
+ it serves any purpose in the current design, so we could just drop
+ that. *)
+let debug_prompt lev tac f =
+ (* spiwack: avoid overriding by the open below *)
+ let runfalse = run false in
+ let open Proofview.NonLogical in
+ let (>=) = Proofview.tclBIND in
+ (* What to print and to do next *)
+ let newlevel =
+ Proofview.tclLIFT !skip >= fun initial_skip ->
+ if Int.equal initial_skip 0 then
+ Proofview.tclLIFT !breakpoint >= fun breakpoint ->
+ if Option.is_empty breakpoint then Proofview.tclTHEN (goal_com tac) (Proofview.tclLIFT (prompt lev))
+ else Proofview.tclLIFT(runfalse >> return (DebugOn (lev+1)))
+ else Proofview.tclLIFT begin
+ (!skip >>= fun s -> skip:=s-1) >>
+ runfalse >>
+ !skip >>= fun new_skip ->
+ (if Int.equal new_skip 0 then skipped:=0 else return ()) >>
+ return (DebugOn (lev+1))
+ end in
+ newlevel >= fun newlevel ->
+ (* What to execute *)
+ Proofview.tclOR
+ (f newlevel)
+ begin fun (reraise, info) ->
+ Proofview.tclTHEN
+ (Proofview.tclLIFT begin
+ (skip:=0) >> (skipped:=0) >>
+ if Logic.catchable_exception reraise then
+ msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise)
+ else return ()
+ end)
+ (Proofview.tclZERO ~info reraise)
+ end
+
+let is_debug db =
+ let open Proofview.NonLogical in
+ !breakpoint >>= fun breakpoint ->
+ match db, breakpoint with
+ | DebugOff, _ -> return false
+ | _, Some _ -> return false
+ | _ ->
+ !skip >>= fun skip ->
+ return (Int.equal skip 0)
+
+(* Prints a constr *)
+let db_constr debug env c =
+ let open Proofview.NonLogical in
+ is_debug debug >>= fun db ->
+ if db then
+ msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c)
+ else return ()
+
+(* Prints the pattern rule *)
+let db_pattern_rule debug num r =
+ let open Proofview.NonLogical in
+ is_debug debug >>= fun db ->
+ if db then
+ begin
+ msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
+ str "|" ++ spc () ++ prmatchrl r)
+ end
+ else return ()
+
+(* Prints the hypothesis pattern identifier if it exists *)
+let hyp_bound = function
+ | Anonymous -> str " (unbound)"
+ | Name id -> str " (bound to " ++ pr_id id ++ str ")"
+
+(* Prints a matched hypothesis *)
+let db_matched_hyp debug env (id,_,c) ido =
+ let open Proofview.NonLogical in
+ is_debug debug >>= fun db ->
+ if db then
+ msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++
+ str " has been matched: " ++ print_constr_env env c)
+ else return ()
+
+(* Prints the matched conclusion *)
+let db_matched_concl debug env c =
+ let open Proofview.NonLogical in
+ is_debug debug >>= fun db ->
+ if db then
+ msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c)
+ else return ()
+
+(* Prints a success message when the goal has been matched *)
+let db_mc_pattern_success debug =
+ let open Proofview.NonLogical in
+ is_debug debug >>= fun db ->
+ if db then
+ msg_tac_debug (str "The goal has been successfully matched!" ++ fnl() ++
+ str "Let us execute the right-hand side part..." ++ fnl())
+ else return ()
+
+(* Prints a failure message for an hypothesis pattern *)
+let db_hyp_pattern_failure debug env sigma (na,hyp) =
+ let open Proofview.NonLogical in
+ is_debug debug >>= fun db ->
+ if db then
+ msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++
+ str " cannot match: " ++
+ prmatchpatt env sigma hyp)
+ else return ()
+
+(* Prints a matching failure message for a rule *)
+let db_matching_failure debug =
+ let open Proofview.NonLogical in
+ is_debug debug >>= fun db ->
+ if db then
+ msg_tac_debug (str "This rule has failed due to matching errors!" ++ fnl() ++
+ str "Let us try the next one...")
+ else return ()
+
+(* Prints an evaluation failure message for a rule *)
+let db_eval_failure debug s =
+ let open Proofview.NonLogical in
+ is_debug debug >>= fun db ->
+ if db then
+ let s = str "message \"" ++ s ++ str "\"" in
+ msg_tac_debug
+ (str "This rule has failed due to \"Fail\" tactic (" ++
+ s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
+ else return ()
+
+(* Prints a logic failure message for a rule *)
+let db_logic_failure debug err =
+ let open Proofview.NonLogical in
+ is_debug debug >>= fun db ->
+ if db then
+ begin
+ msg_tac_debug (explain_logic_error err) >>
+ msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++
+ str "Let us try the next one...")
+ end
+ else return ()
+
+let is_breakpoint brkname s = match brkname, s with
+ | Some s, MsgString s'::_ -> String.equal s s'
+ | _ -> false
+
+let db_breakpoint debug s =
+ let open Proofview.NonLogical in
+ !breakpoint >>= fun opt_breakpoint ->
+ match debug with
+ | DebugOn lev when not (CList.is_empty s) && is_breakpoint opt_breakpoint s ->
+ breakpoint:=None
+ | _ ->
+ return ()
+
+(** Extrating traces *)
+
+let is_defined_ltac trace =
+ let rec aux = function
+ | (_, Tacexpr.LtacNameCall f) :: _ -> not (Tacenv.is_ltac_for_ml_tactic f)
+ | (_, Tacexpr.LtacNotationCall f) :: _ -> true
+ | (_, Tacexpr.LtacAtomCall _) :: _ -> false
+ | _ :: tail -> aux tail
+ | [] -> false in
+ aux (List.rev trace)
+
+let explain_ltac_call_trace last trace loc =
+ let calls = last :: List.rev_map snd trace in
+ let pr_call ck = match ck with
+ | Tacexpr.LtacNotationCall kn -> quote (Pptactic.pr_alias_key kn)
+ | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
+ | Tacexpr.LtacMLCall t ->
+ quote (Pptactic.pr_glob_tactic (Global.env()) t)
+ | Tacexpr.LtacVarCall (id,t) ->
+ quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
+ Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+ | Tacexpr.LtacAtomCall te ->
+ quote (Pptactic.pr_glob_tactic (Global.env())
+ (Tacexpr.TacAtom (Loc.ghost,te)))
+ | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
+ quote (Printer.pr_glob_constr_env (Global.env()) c) ++
+ (if not (Id.Map.is_empty vars) then
+ strbrk " (with " ++
+ prlist_with_sep pr_comma
+ (fun (id,c) ->
+ pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
+ (List.rev (Id.Map.bindings vars)) ++ str ")"
+ else mt())
+ in
+ match calls with
+ | [] -> mt ()
+ | [a] -> hov 0 (str "Ltac call to " ++ pr_call a ++ str " failed.")
+ | _ ->
+ let kind_of_last_call = match List.last calls with
+ | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed."
+ | _ -> ", last call failed."
+ in
+ hov 0 (str "In nested Ltac calls to " ++
+ pr_enum pr_call calls ++ strbrk kind_of_last_call)
+
+let skip_extensions trace =
+ let rec aux = function
+ | (_,Tacexpr.LtacNameCall f as tac) :: _
+ when Tacenv.is_ltac_for_ml_tactic f -> [tac]
+ | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ ->
+ (* Case of an ML defined tactic with entry of the form <<"foo" args>> *)
+ (* see tacextend.mlp *)
+ [tac]
+ | (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac]
+ | t :: tail -> t :: aux tail
+ | [] -> [] in
+ List.rev (aux (List.rev trace))
+
+let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2
+
+let extract_ltac_trace trace eloc =
+ let trace = skip_extensions trace in
+ let (loc,c),tail = List.sep_last trace in
+ if is_defined_ltac trace then
+ (* We entered a user-defined tactic,
+ we display the trace with location of the call *)
+ let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
+ Some msg, if finer_loc eloc loc then eloc else loc
+ else
+ (* We entered a primitive tactic, we don't display trace but
+ report on the finest location *)
+ let best_loc =
+ (* trace is with innermost call coming first *)
+ let rec aux best_loc = function
+ | (loc,_)::tail ->
+ if Loc.is_ghost best_loc ||
+ not (Loc.is_ghost loc) && finer_loc loc best_loc
+ then
+ aux loc tail
+ else
+ aux best_loc tail
+ | [] -> best_loc in
+ aux eloc trace in
+ None, best_loc
+
+let get_ltac_trace (_, info) =
+ let ltac_trace = Exninfo.get info ltac_trace_info in
+ let loc = Option.default Loc.ghost (Loc.get_loc info) in
+ match ltac_trace with
+ | None -> None
+ | Some trace -> Some (extract_ltac_trace trace loc)
+
+let () = ExplainErr.register_additional_error_info get_ltac_trace
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 21:48:48 +0000