From 6ecbc9990a49a0dd51970c7fc8b13f39f02be773 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 18:34:39 +0100 Subject: Moving Ltac traces to Tacexpr and Tacinterp. --- dev/printers.mllib | 1 - intf/tacexpr.mli | 12 ++++++++++++ proofs/proof_type.ml | 52 --------------------------------------------------- proofs/proof_type.mli | 16 ---------------- proofs/proofs.mllib | 1 - tactics/tacinterp.ml | 2 ++ tactics/tacinterp.mli | 2 ++ tactics/tacsubst.ml | 2 ++ tactics/tacsubst.mli | 4 ++++ toplevel/cerrors.ml | 2 +- toplevel/himsg.ml | 22 +++++++++++----------- toplevel/himsg.mli | 2 +- 12 files changed, 35 insertions(+), 83 deletions(-) delete mode 100644 proofs/proof_type.ml diff --git a/dev/printers.mllib b/dev/printers.mllib index 39e4b1cdb1..34bde1ac27 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -174,7 +174,6 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Proof_type Goal Miscprint Logic diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index f2a567c00d..b1dc174d4b 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -394,3 +394,15 @@ type tactic_arg = type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen + +(** Traces *) + +type ltac_call_kind = + | LtacMLCall of glob_tactic_expr + | LtacNotationCall of KerName.t + | LtacNameCall of ltac_constant + | LtacAtomCall of glob_atomic_tactic_expr + | LtacVarCall of Id.t * glob_tactic_expr + | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map + +type ltac_trace = (Loc.t * ltac_call_kind) list diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml deleted file mode 100644 index dd2c7b253d..0000000000 --- a/proofs/proof_type.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* goal list sigma - -type prim_rule = - | Cut of bool * bool * Id.t * types - | FixRule of Id.t * int * (Id.t * int * constr) list * int - | Cofix of Id.t * (Id.t * constr) list * int - | Refine of constr - | Thin of Id.t list - | Move of Id.t * Id.t move_location - -(** Nowadays, the only rules we'll consider are the primitive rules *) - -type rule = prim_rule - -(** Ltac traces *) - -type ltac_call_kind = - | LtacMLCall of glob_tactic_expr - | LtacNotationCall of KerName.t - | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr - | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map - -type ltac_trace = (Loc.t * ltac_call_kind) list - -let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index aa05f58ab6..b4c9dae2a3 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -57,19 +57,3 @@ type rule = prim_rule type goal = Goal.goal type tactic = goal sigma -> goal list sigma - -(** Ltac traces *) - -(** TODO: Move those definitions somewhere sensible *) - -type ltac_call_kind = - | LtacMLCall of glob_tactic_expr - | LtacNotationCall of KerName.t - | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr - | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map - -type ltac_trace = (Loc.t * ltac_call_kind) list - -val ltac_trace_info : ltac_trace Exninfo.t diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 1bd701cb9b..47a637575f 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -2,7 +2,6 @@ Miscprint Goal Evar_refiner Proof_using -Proof_type Proof_errors Logic Proofview diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index bf5f9ddc86..82252610a8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -44,6 +44,8 @@ open Sigma.Notations open Proofview.Notations open Context.Named.Declaration +let ltac_trace_info = Tacsubst.ltac_trace_info + let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> let Val.Dyn (t, _) = v in match Val.eq t (val_tag wit) with diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index c5da3494cb..31327873e9 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -14,6 +14,8 @@ open Genarg open Redexpr open Misctypes +val ltac_trace_info : ltac_trace Exninfo.t + module Value : sig type t = Val.t diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 55941c1ca6..17cb8ad19b 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -18,6 +18,8 @@ open Genredexpr open Patternops open Pretyping +let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () + (** Substitution of tactics at module closing time *) (** For generic arguments, we declare and store substitutions diff --git a/tactics/tacsubst.mli b/tactics/tacsubst.mli index c1bf272579..8b686c5cec 100644 --- a/tactics/tacsubst.mli +++ b/tactics/tacsubst.mli @@ -11,6 +11,10 @@ open Mod_subst open Genarg open Misctypes +(** TODO: Move those definitions somewhere sensible *) + +val ltac_trace_info : ltac_trace Exninfo.t + (** Substitution of tactics at module closing time *) val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 600683d359..91ef45393c 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -120,7 +120,7 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, let err = Errors.make_anomaly msg in Util.iraise (err, info) in - let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in + let ltac_trace = Exninfo.get info Tacsubst.ltac_trace_info in let loc = Option.default Loc.ghost (Loc.get_loc info) in match ltac_trace with | None -> e diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index de7ec61c81..1af09dd845 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1247,9 +1247,9 @@ let explain_reduction_tactic_error = function let is_defined_ltac trace = let rec aux = function - | (_, Proof_type.LtacNameCall f) :: tail -> + | (_, Tacexpr.LtacNameCall f) :: tail -> not (Tacenv.is_ltac_for_ml_tactic f) - | (_, Proof_type.LtacAtomCall _) :: tail -> + | (_, Tacexpr.LtacAtomCall _) :: tail -> false | _ :: tail -> aux tail | [] -> false in @@ -1258,17 +1258,17 @@ let is_defined_ltac 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 - | Proof_type.LtacNotationCall kn -> quote (KerName.print kn) - | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst) - | Proof_type.LtacMLCall t -> + | 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) - | Proof_type.LtacVarCall (id,t) -> + | Tacexpr.LtacVarCall (id,t) -> quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" - | Proof_type.LtacAtomCall te -> + | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (Loc.ghost,te))) - | Proof_type.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) -> + | 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 " ++ @@ -1282,7 +1282,7 @@ let explain_ltac_call_trace last trace loc = | [] -> mt () | _ -> let kind_of_last_call = match List.last calls with - | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed." + | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed." | _ -> ", last call failed." in hov 0 (str "In nested Ltac calls to " ++ @@ -1290,9 +1290,9 @@ let explain_ltac_call_trace last trace loc = let skip_extensions trace = let rec aux = function - | (_,Proof_type.LtacNameCall f as tac) :: _ + | (_,Tacexpr.LtacNameCall f as tac) :: _ when Tacenv.is_ltac_for_ml_tactic f -> [tac] - | (_,(Proof_type.LtacNotationCall _ | Proof_type.LtacMLCall _) as tac) + | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac) :: _ -> [tac] | t :: tail -> t :: aux tail | [] -> [] in diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 3ef98380b5..50bbd15c6d 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -37,7 +37,7 @@ val explain_reduction_tactic_error : Tacred.reduction_tactic_error -> std_ppcmds val extract_ltac_trace : - Proof_type.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t + Tacexpr.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t val explain_module_error : Modops.module_typing_error -> std_ppcmds -- cgit v1.2.3 From 9e96794d6a4327761ce1ff992351199919431be1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 19:01:38 +0100 Subject: Moving Tactic_debug to tactics/ folder. --- dev/printers.mllib | 2 +- printing/pptactic.ml | 11 -- printing/pptacticsig.mli | 5 + proofs/proofs.mllib | 1 - proofs/tactic_debug.ml | 319 --------------------------------------------- proofs/tactic_debug.mli | 79 ----------- tactics/tacinterp.ml | 15 ++- tactics/tacsubst.ml | 2 - tactics/tacsubst.mli | 4 - tactics/tactic_debug.ml | 324 ++++++++++++++++++++++++++++++++++++++++++++++ tactics/tactic_debug.mli | 77 +++++++++++ tactics/tactics.mllib | 1 + toplevel/cerrors.ml | 2 +- toplevel/vernacentries.ml | 12 -- 14 files changed, 423 insertions(+), 431 deletions(-) delete mode 100644 proofs/tactic_debug.ml delete mode 100644 proofs/tactic_debug.mli create mode 100644 tactics/tactic_debug.ml create mode 100644 tactics/tactic_debug.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index 34bde1ac27..d8fb2b906c 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -187,13 +187,13 @@ Proofview Proof Proof_global Pfedit -Tactic_debug Decl_mode Ppconstr Entry Pcoq Printer Pptactic +Tactic_debug Ppdecl_proof Egramml Egramcoq diff --git a/printing/pptactic.ml b/printing/pptactic.ml index fdc1288aec..7d5e7772c3 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1415,17 +1415,6 @@ let () = let printer _ _ prtac = prtac (0, E) in declare_extra_genarg_pprule wit_tactic printer printer printer -let _ = Hook.set Tactic_debug.tactic_printer - (fun x -> pr_glob_tactic (Global.env()) x) - -let _ = Hook.set Tactic_debug.match_pattern_printer - (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp) - -let _ = Hook.set Tactic_debug.match_rule_printer - (fun rl -> - pr_match_rule false (pr_glob_tactic (Global.env())) - (fun (_,p) -> pr_constr_pattern p) rl) - module Richpp = struct include Make (Ppconstr.Richpp) (struct diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index c5ec6bb092..b98b6c67e7 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -67,4 +67,9 @@ module type Pp = sig ('constr -> std_ppcmds) -> ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds + val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds + + val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('b, 'a) match_rule -> std_ppcmds + end diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 47a637575f..08556d62ec 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -11,6 +11,5 @@ Redexpr Refiner Tacmach Pfedit -Tactic_debug Clenv Clenvtac diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml deleted file mode 100644 index d33278ff8d..0000000000 --- a/proofs/tactic_debug.ml +++ /dev/null @@ -1,319 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* mt()) - -let explain_logic_error_no_anomaly = ref (fun e -> mt()) - -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: = Continue" ++ fnl() ++ - str " h/? = Help" ++ fnl() ++ - str " r = Run times" ++ fnl() ++ - str " r = Run up to next idtac " ++ 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 () ++ Hook.get 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 ": " ++ Pervasives.(!) 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 () ++ Hook.get 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: " ++ - Hook.get 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 (Pervasives.(!) 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 () diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli deleted file mode 100644 index 215c5b29b5..0000000000 --- a/proofs/tactic_debug.mli +++ /dev/null @@ -1,79 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Pp.std_ppcmds) Hook.t -val match_pattern_printer : - (env -> evar_map -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t -val match_rule_printer : - ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t - -(** Debug information *) -type debug_info = - | DebugOn of int - | DebugOff - -(** Prints the state and waits *) -val debug_prompt : - int -> glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic - -(** Initializes debugger *) -val db_initialize : unit Proofview.NonLogical.t - -(** Prints a constr *) -val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t - -(** Prints the pattern rule *) -val db_pattern_rule : - debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t - -(** Prints a matched hypothesis *) -val db_matched_hyp : - debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t - -(** Prints the matched conclusion *) -val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t - -(** Prints a success message when the goal has been matched *) -val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t - -(** Prints a failure message for an hypothesis pattern *) -val db_hyp_pattern_failure : - debug_info -> env -> evar_map -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t - -(** Prints a matching failure message for a rule *) -val db_matching_failure : debug_info -> unit Proofview.NonLogical.t - -(** Prints an evaluation failure message for a rule *) -val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t - -(** An exception handler *) -val explain_logic_error: (exn -> Pp.std_ppcmds) ref - -(** For use in the Ltac debugger: some exception that are usually - consider anomalies are acceptable because they are caught later in - the process that is being debugged. One should not require - from users that they report these anomalies. *) -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 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 diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 82252610a8..36a23d5809 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -44,7 +44,7 @@ open Sigma.Notations open Proofview.Notations open Context.Named.Declaration -let ltac_trace_info = Tacsubst.ltac_trace_info +let ltac_trace_info = Tactic_debug.ltac_trace_info let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> let Val.Dyn (t, _) = v in @@ -2201,3 +2201,16 @@ let lift_constr_tac_to_ml_tac vars tac = tac args ist end } in tac + +let vernac_debug b = + set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) + +let _ = + let open Goptions in + declare_bool_option + { optsync = false; + optdepr = false; + optname = "Ltac debug"; + optkey = ["Ltac";"Debug"]; + optread = (fun () -> get_debug () != Tactic_debug.DebugOff); + optwrite = vernac_debug } diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 17cb8ad19b..55941c1ca6 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -18,8 +18,6 @@ open Genredexpr open Patternops open Pretyping -let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () - (** Substitution of tactics at module closing time *) (** For generic arguments, we declare and store substitutions diff --git a/tactics/tacsubst.mli b/tactics/tacsubst.mli index 8b686c5cec..c1bf272579 100644 --- a/tactics/tacsubst.mli +++ b/tactics/tacsubst.mli @@ -11,10 +11,6 @@ open Mod_subst open Genarg open Misctypes -(** TODO: Move those definitions somewhere sensible *) - -val ltac_trace_info : ltac_trace Exninfo.t - (** Substitution of tactics at module closing time *) val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml new file mode 100644 index 0000000000..b278c371b3 --- /dev/null +++ b/tactics/tactic_debug.ml @@ -0,0 +1,324 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 = ref (fun e -> mt()) + +let explain_logic_error_no_anomaly = ref (fun e -> mt()) + +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: = Continue" ++ fnl() ++ + str " h/? = Help" ++ fnl() ++ + str " r = Run times" ++ fnl() ++ + str " r = Run up to next idtac " ++ 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 ": " ++ Pervasives.(!) 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 (Pervasives.(!) 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 () diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli new file mode 100644 index 0000000000..fbb7ab66db --- /dev/null +++ b/tactics/tactic_debug.mli @@ -0,0 +1,77 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic + +(** Initializes debugger *) +val db_initialize : unit Proofview.NonLogical.t + +(** Prints a constr *) +val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t + +(** Prints the pattern rule *) +val db_pattern_rule : + debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t + +(** Prints a matched hypothesis *) +val db_matched_hyp : + debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t + +(** Prints the matched conclusion *) +val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t + +(** Prints a success message when the goal has been matched *) +val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t + +(** Prints a failure message for an hypothesis pattern *) +val db_hyp_pattern_failure : + debug_info -> env -> evar_map -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t + +(** Prints a matching failure message for a rule *) +val db_matching_failure : debug_info -> unit Proofview.NonLogical.t + +(** Prints an evaluation failure message for a rule *) +val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t + +(** An exception handler *) +val explain_logic_error: (exn -> Pp.std_ppcmds) ref + +(** For use in the Ltac debugger: some exception that are usually + consider anomalies are acceptable because they are caught later in + the process that is being debugged. One should not require + from users that they report these anomalies. *) +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 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 diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 2c5edc20ed..6246363173 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,3 +1,4 @@ +Tactic_debug Ftactic Geninterp Dnet diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 91ef45393c..b734f075ab 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -120,7 +120,7 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, let err = Errors.make_anomaly msg in Util.iraise (err, info) in - let ltac_trace = Exninfo.get info Tacsubst.ltac_trace_info in + let ltac_trace = Exninfo.get info Tactic_debug.ltac_trace_info in let loc = Option.default Loc.ghost (Loc.get_loc info) in match ltac_trace with | None -> e diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 38832b422f..d769c60332 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1433,18 +1433,6 @@ let _ = optread = Flags.get_dump_bytecode; optwrite = Flags.set_dump_bytecode } -let vernac_debug b = - set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) - -let _ = - declare_bool_option - { optsync = false; - optdepr = false; - optname = "Ltac debug"; - optkey = ["Ltac";"Debug"]; - optread = (fun () -> get_debug () != Tactic_debug.DebugOff); - optwrite = vernac_debug } - let _ = declare_bool_option { optsync = true; -- cgit v1.2.3 From 6f49db55e525a57378ca5600476c870a98a59dae Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 19:38:14 +0100 Subject: Removing dependency of Himsg in tactic files. --- tactics/tacenv.ml | 2 ++ tactics/tactic_debug.ml | 78 ++++++++++++++++++++++++++++++++++++++++++++++++ tactics/tactic_debug.mli | 5 ++++ toplevel/cerrors.ml | 2 +- toplevel/himsg.ml | 74 --------------------------------------------- toplevel/himsg.mli | 3 -- 6 files changed, 86 insertions(+), 78 deletions(-) diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index d2d3f3117f..cc87e197d1 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 b278c371b3..fa40b74160 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 fbb7ab66db..a3b519a712 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 b734f075ab..0b8edd91c1 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 1af09dd845..4ee1537c20 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 50bbd15c6d..ced54fd279 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 : -- cgit v1.2.3 From cdc91f02f98b4d857bfebe61d95b920787a8d0e5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 21:25:20 +0100 Subject: Putting Tactic_debug just below Tacinterp. --- dev/printers.mllib | 2 +- tactics/ftactic.ml | 2 -- tactics/ftactic.mli | 5 ----- tactics/tacenv.ml | 2 -- tactics/tacinterp.ml | 2 +- tactics/tactic_debug.ml | 6 ++---- tactics/tactic_debug.mli | 2 -- tactics/tactics.mllib | 2 +- 8 files changed, 5 insertions(+), 18 deletions(-) diff --git a/dev/printers.mllib b/dev/printers.mllib index d8fb2b906c..7710033dba 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -193,12 +193,12 @@ Entry Pcoq Printer Pptactic -Tactic_debug Ppdecl_proof Egramml Egramcoq Tacsubst Tacenv +Tactic_debug Trie Dn Btermdn diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml index 55463afd01..588709873e 100644 --- a/tactics/ftactic.ml +++ b/tactics/ftactic.ml @@ -99,8 +99,6 @@ end module Ftac = Monad.Make(Self) module List = Ftac.List -let debug_prompt = Tactic_debug.debug_prompt - module Notations = struct let (>>=) = bind diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli index fd05a44698..19041f1698 100644 --- a/tactics/ftactic.mli +++ b/tactics/ftactic.mli @@ -70,11 +70,6 @@ val (<*>) : unit t -> 'a t -> 'a t module List : Monad.ListS with type 'a t := 'a t -(** {5 Debug} *) - -val debug_prompt : - int -> Tacexpr.glob_tactic_expr -> (Tactic_debug.debug_info -> 'a t) -> 'a t - (** {5 Notations} *) module Notations : diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index cc87e197d1..d2d3f3117f 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -143,5 +143,3 @@ 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/tacinterp.ml b/tactics/tacinterp.ml index 36a23d5809..32f7c3c61c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1202,7 +1202,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti let ist = { ist with extra = TacStore.set ist.extra f_debug v } in value_interp ist >>= fun v -> return (name_vfun appl v) in - Ftactic.debug_prompt lev tac eval + Tactic_debug.debug_prompt lev tac eval | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml index fa40b74160..e991eb86dc 100644 --- a/tactics/tactic_debug.ml +++ b/tactics/tactic_debug.ml @@ -325,12 +325,10 @@ let db_breakpoint debug s = (** 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) + not (Tacenv.is_ltac_for_ml_tactic f) | (_, Tacexpr.LtacAtomCall _) :: tail -> false | _ :: tail -> aux tail @@ -373,7 +371,7 @@ let explain_ltac_call_trace last trace loc = let skip_extensions trace = let rec aux = function | (_,Tacexpr.LtacNameCall f as tac) :: _ - when Hook.get is_for_ml_f f -> [tac] + when Tacenv.is_ltac_for_ml_tactic f -> [tac] | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac) :: _ -> [tac] | t :: tail -> t :: aux tail diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli index a3b519a712..523398e75a 100644 --- a/tactics/tactic_debug.mli +++ b/tactics/tactic_debug.mli @@ -78,5 +78,3 @@ val db_breakpoint : debug_info -> 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/tactics/tactics.mllib b/tactics/tactics.mllib index 6246363173..eebac88fba 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,4 +1,3 @@ -Tactic_debug Ftactic Geninterp Dnet @@ -22,6 +21,7 @@ Hints Auto Tacintern Tactic_matching +Tactic_debug Tacinterp Evar_tactics Term_dnet -- cgit v1.2.3 From ffac73b8f3f3bf6877ce652eecac7849b7c2a182 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 23:00:58 +0100 Subject: Moving Autorewrite to Hightatctic. --- intf/vernacexpr.mli | 1 - parsing/g_vernac.ml4 | 1 - printing/ppvernac.ml | 2 -- tactics/g_rewrite.ml4 | 4 ++++ tactics/hightactics.mllib | 1 + tactics/tactics.mllib | 1 - toplevel/vernacentries.ml | 1 - 7 files changed, 5 insertions(+), 6 deletions(-) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 7273b92b9a..5501ca7c7f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -69,7 +69,6 @@ type printable = | PrintHint of reference or_by_notation | PrintHintGoal | PrintHintDbName of string - | PrintRewriteHintDbName of string | PrintHintDb | PrintScopes | PrintScope of string diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b5e9f9e067..49baeb5560 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -951,7 +951,6 @@ GEXTEND Gram | IDENT "Hint"; qid = smart_global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s - | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index ffec926a84..a101540aba 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -486,8 +486,6 @@ module Make keyword "Print Hint *" | PrintHintDbName s -> keyword "Print HintDb" ++ spc () ++ str s - | PrintRewriteHintDbName s -> - keyword "Print Rewrite HintDb" ++ spc() ++ str s | PrintUniverses (b, fopt) -> let cmd = if b then "Print Sorted Universes" diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 72cfb01a57..6b6dc7b21a 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -261,3 +261,7 @@ TACTIC EXTEND setoid_transitivity [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ] | [ "setoid_etransitivity" ] -> [ setoid_transitivity None ] END + +VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY + [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Pp.msg_notice (Autorewrite.print_rewrite_hintdb s) ] +END diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 0d73cc27aa..73f11d0be0 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,5 +1,6 @@ Extraargs Coretactics +Autorewrite Extratactics Eauto G_auto diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index eebac88fba..fd7fab0c58 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -25,5 +25,4 @@ Tactic_debug Tacinterp Evar_tactics Term_dnet -Autorewrite Tactic_option diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d769c60332..c63dac3026 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1629,7 +1629,6 @@ let vernac_print = function | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s) - | PrintRewriteHintDbName s -> msg_notice (Autorewrite.print_rewrite_hintdb s) | PrintHintDb -> msg_notice (Hints.pr_searchtable ()) | PrintScopes -> msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) -- cgit v1.2.3 From a9f6f401e66c0bbf0c50801d597cd18097bf91a6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 23:15:43 +0100 Subject: Expurging grammar.mllib from uselessly linked modules. --- grammar/grammar.mllib | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index fc7cb392bf..296d32dc04 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -29,35 +29,22 @@ CStack Util Ppstyle Errors -Bigint Predicate Segmenttree Unicodetable Unicode Genarg -Evar Names -Libnames - -Redops -Miscops -Locusops - Stdarg Constrarg -Constrexpr_ops Tok Compat Lexer Entry Pcoq -G_prim -G_tactic -G_ltac -G_constr Q_util Egramml -- cgit v1.2.3