# HG changeset patch # User blanchet # Date 1271157966 -7200 # Node ID a3d8d5329438e45c2bbe7602ea776f9d3aebcf4d # Parent e91292c520be855bb54463bc7a1633936e6aedd3 make Nitpick output everything to tracing in debug mode; so that when an exception occurs, I can switch to the tracing window to see what was in the response window before the exception blew everything away diff -r e91292c520be -r a3d8d5329438 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 13 13:24:03 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 13 13:26:06 2010 +0200 @@ -225,13 +225,15 @@ o Pretty.chunks o cons (Pretty.str "") o single o Pretty.mark Markup.hilite else - priority o Pretty.string_of + (fn s => (priority s; if debug then tracing s else ())) + o Pretty.string_of (* (unit -> Pretty.T) -> unit *) fun pprint_m f = () |> not auto ? pprint o f fun pprint_v f = () |> verbose ? pprint o f fun pprint_d f = () |> debug ? pprint o f (* string -> unit *) val print = pprint o curry Pretty.blk 0 o pstrs + val print_g = pprint o Pretty.str (* (unit -> string) -> unit *) val print_m = pprint_m o K o plazy val print_v = pprint_v o K o plazy @@ -265,8 +267,8 @@ val original_max_potential = max_potential val original_max_genuine = max_genuine (* - val _ = priority ("*** " ^ Syntax.string_of_term ctxt orig_t) - val _ = List.app (fn t => priority ("*** " ^ Syntax.string_of_term ctxt t)) + val _ = print_g ("*** " ^ Syntax.string_of_term ctxt orig_t) + val _ = List.app (fn t => print_g ("*** " ^ Syntax.string_of_term ctxt t)) orig_assm_ts *) val max_bisim_depth = fold Integer.max bisim_depths ~1 @@ -338,7 +340,7 @@ | _ => false) finitizes) val standard = forall snd stds (* - val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us) + val _ = List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us) *) val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns @@ -431,10 +433,10 @@ else () (* - val _ = priority "Monotonic types:" - val _ = List.app (priority o string_for_type ctxt) mono_Ts - val _ = priority "Nonmonotonic types:" - val _ = List.app (priority o string_for_type ctxt) nonmono_Ts + val _ = print_g "Monotonic types:" + val _ = List.app (print_g o string_for_type ctxt) mono_Ts + val _ = print_g "Nonmonotonic types:" + val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts *) val need_incremental = Int.max (max_potential, max_genuine) >= 2 @@ -472,10 +474,10 @@ raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\ \problem_for_scope", "too large scope") (* - val _ = priority "Offsets:" + val _ = print_g "Offsets:" val _ = List.app (fn (T, j0) => - priority (string_for_type ctxt T ^ " = " ^ - string_of_int j0)) + print_g (string_for_type ctxt T ^ " = " ^ + string_of_int j0)) (Typtab.dest ofs) *) val all_exact = forall (is_exact_type datatypes true) all_Ts @@ -504,7 +506,7 @@ val nondef_us = map (choose_reps_in_nut scope unsound rep_table false) nondef_us (* - val _ = List.app (priority o string_for_nut ctxt) + val _ = List.app (print_g o string_for_nut ctxt) (free_names @ sel_names @ nonsel_names @ nondef_us @ def_us) *) diff -r e91292c520be -r a3d8d5329438 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Apr 13 13:24:03 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Apr 13 13:26:06 2010 +0200 @@ -1130,8 +1130,8 @@ if is_boolean_type T then bool_rep polar opt else - smart_range_rep ofs T1 (fn () => card_of_type card_assigns T) - (unopt_rep R1) + lazy_range_rep ofs T1 (fn () => card_of_type card_assigns T) + (unopt_rep R1) |> opt ? opt_rep ofs T in s_op2 Apply T ran_R u1 u2 end | Op2 (Lambda, T, _, u1, u2) => diff -r e91292c520be -r a3d8d5329438 src/HOL/Tools/Nitpick/nitpick_rep.ML --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Apr 13 13:24:03 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Apr 13 13:26:06 2010 +0200 @@ -34,7 +34,7 @@ val is_one_rep : rep -> bool val is_lone_rep : rep -> bool val dest_Func : rep -> rep * rep - val smart_range_rep : int Typtab.table -> typ -> (unit -> int) -> rep -> rep + val lazy_range_rep : int Typtab.table -> typ -> (unit -> int) -> rep -> rep val binder_reps : rep -> rep list val body_rep : rep -> rep val one_rep : int Typtab.table -> typ -> rep -> rep @@ -153,16 +153,16 @@ fun dest_Func (Func z) = z | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R]) (* int Typtab.table -> typ -> (unit -> int) -> rep -> rep *) -fun smart_range_rep _ _ _ Unit = Unit - | smart_range_rep _ _ _ (Vect (_, R)) = R - | smart_range_rep _ _ _ (Func (_, R2)) = R2 - | smart_range_rep ofs T ran_card (Opt R) = - Opt (smart_range_rep ofs T ran_card R) - | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) = +fun lazy_range_rep _ _ _ Unit = Unit + | lazy_range_rep _ _ _ (Vect (_, R)) = R + | lazy_range_rep _ _ _ (Func (_, R2)) = R2 + | lazy_range_rep ofs T ran_card (Opt R) = + Opt (lazy_range_rep ofs T ran_card R) + | lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) = Atom (1, offset_of_type ofs T2) - | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) = + | lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) = Atom (ran_card (), offset_of_type ofs T2) - | smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R]) + | lazy_range_rep _ _ _ R = raise REP ("Nitpick_Rep.lazy_range_rep", [R]) (* rep -> rep list *) fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2