diff options
-rw-r--r-- | tactics/tacenv.ml | 2 | ||||
-rw-r--r-- | tactics/tactic_debug.ml | 78 | ||||
-rw-r--r-- | tactics/tactic_debug.mli | 5 | ||||
-rw-r--r-- | toplevel/cerrors.ml | 2 | ||||
-rw-r--r-- | toplevel/himsg.ml | 74 | ||||
-rw-r--r-- | toplevel/himsg.mli | 3 |
6 files changed, 86 insertions, 78 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index d2d3f3117..cc87e197d 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -143,3 +143,5 @@ let register_ltac for_ml local id tac = let redefine_ltac local kn tac = Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac)) + +let () = Hook.set Tactic_debug.is_ltac_for_ml_tactic_hook is_ltac_for_ml_tactic diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml index b278c371b..fa40b7416 100644 --- a/tactics/tactic_debug.ml +++ b/tactics/tactic_debug.ml @@ -322,3 +322,81 @@ let db_breakpoint debug s = breakpoint:=None | _ -> return () + +(** Extrating traces *) + +let (is_for_ml_f, is_ltac_for_ml_tactic_hook) = Hook.make () + +let is_defined_ltac trace = + let rec aux = function + | (_, Tacexpr.LtacNameCall f) :: tail -> + not (Hook.get is_for_ml_f f) + | (_, Tacexpr.LtacAtomCall _) :: tail -> + 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 (KerName.print 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 () + | _ -> + 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 Hook.get is_for_ml_f f -> [tac] + | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac) + :: _ -> [tac] + | t :: tail -> t :: aux tail + | [] -> [] in + List.rev (aux (List.rev trace)) + +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, loc + else + (* We entered a primitive tactic, we don't display trace but + report on the finest location *) + let best_loc = + if not (Loc.is_ghost eloc) then eloc else + (* trace is with innermost call coming first *) + let rec aux = function + | (loc,_)::tail when not (Loc.is_ghost loc) -> loc + | _::tail -> aux tail + | [] -> Loc.ghost in + aux trace in + None, best_loc diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli index fbb7ab66d..a3b519a71 100644 --- a/tactics/tactic_debug.mli +++ b/tactics/tactic_debug.mli @@ -75,3 +75,8 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> Id.t Loc.located message_token list -> unit Proofview.NonLogical.t + +val extract_ltac_trace : + Tacexpr.ltac_trace -> Loc.t -> Pp.std_ppcmds option * Loc.t + +val is_ltac_for_ml_tactic_hook : (KerName.t -> bool) Hook.t diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index b734f075a..0b8edd91c 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -126,7 +126,7 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, | None -> e | Some trace -> let (e, info) = e in - match Himsg.extract_ltac_trace trace loc with + match Tactic_debug.extract_ltac_trace trace loc with | None, loc -> (e, Loc.add_loc info loc) | Some msg, loc -> (EvaluatedError (msg, Some e), Loc.add_loc info loc) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 1af09dd84..4ee1537c2 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1244,77 +1244,3 @@ let explain_reduction_tactic_error = function quote (pr_goal_concl_style_env env sigma c) ++ spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' Evd.empty e - -let is_defined_ltac trace = - let rec aux = function - | (_, Tacexpr.LtacNameCall f) :: tail -> - not (Tacenv.is_ltac_for_ml_tactic f) - | (_, Tacexpr.LtacAtomCall _) :: tail -> - 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 (KerName.print 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 (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 () - | _ -> - 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 _ | Tacexpr.LtacMLCall _) as tac) - :: _ -> [tac] - | t :: tail -> t :: aux tail - | [] -> [] in - List.rev (aux (List.rev trace)) - -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, loc - else - (* We entered a primitive tactic, we don't display trace but - report on the finest location *) - let best_loc = - if not (Loc.is_ghost eloc) then eloc else - (* trace is with innermost call coming first *) - let rec aux = function - | (loc,_)::tail when not (Loc.is_ghost loc) -> loc - | _::tail -> aux tail - | [] -> Loc.ghost in - aux trace in - None, best_loc diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 50bbd15c6..ced54fd27 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -36,9 +36,6 @@ val explain_pattern_matching_error : val explain_reduction_tactic_error : Tacred.reduction_tactic_error -> std_ppcmds -val extract_ltac_trace : - Tacexpr.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t - val explain_module_error : Modops.module_typing_error -> std_ppcmds val explain_module_internalization_error : |