# HG changeset patch # User blanchet # Date 1280863231 -7200 # Node ID 7f12a03c513c9f77e133bdbc0348a5d741df1656 # Parent fd28328daf7314d3f5500405e15dabd710a20b61 better "Pretty" handling diff -r fd28328daf73 -r 7f12a03c513c src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 03 18:27:21 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 03 21:20:31 2010 +0200 @@ -321,14 +321,16 @@ val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns fun monotonicity_message Ts extra = - let val ss = map (quote o string_for_type ctxt) Ts in - "The type" ^ plural_s_for_list ss ^ " " ^ - space_implode " " (serial_commas "and" ss) ^ " " ^ - (if none_true monos then - "passed the monotonicity test" - else - (if length ss = 1 then "is" else "are") ^ " considered monotonic") ^ - ". " ^ extra + let val pretties = map (pretty_maybe_quote o pretty_for_type ctxt) Ts in + Pretty.blk (0, + pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @ + pretty_serial_commas "and" pretties @ + pstrs (" " ^ + (if none_true monos then + "passed the monotonicity test" + else + (if length pretties = 1 then "is" else "are") ^ " considered monotonic") ^ + ". " ^ extra)) end fun is_type_fundamentally_monotonic T = (is_datatype ctxt stds T andalso not (is_quot_type thy T) andalso @@ -373,8 +375,8 @@ case filter_out is_type_fundamentally_monotonic mono_Ts of [] => () | interesting_mono_Ts => - print_v (K (monotonicity_message interesting_mono_Ts - "Nitpick might be able to skip some scopes.")) + pprint_v (K (monotonicity_message interesting_mono_Ts + "Nitpick might be able to skip some scopes.")) else () val (deep_dataTs, shallow_dataTs) = @@ -385,8 +387,8 @@ |> filter is_shallow_datatype_finitizable val _ = if verbose andalso not (null finitizable_dataTs) then - print_v (K (monotonicity_message finitizable_dataTs - "Nitpick can use a more precise finite encoding.")) + pprint_v (K (monotonicity_message finitizable_dataTs + "Nitpick can use a more precise finite encoding.")) else () (* This detection code is an ugly hack. Fortunately, it is used only to @@ -660,7 +662,7 @@ options in print ("Try again with " ^ - space_implode " " (serial_commas "and" ss) ^ + implode (serial_commas "and" ss) ^ " to confirm that the " ^ das_wort_model ^ " is genuine.") end diff -r fd28328daf73 -r 7f12a03c513c src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 03 18:27:21 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Aug 03 21:20:31 2010 +0200 @@ -76,6 +76,7 @@ val unarize_unbox_etc_type : typ -> typ val uniterize_unarize_unbox_etc_type : typ -> typ val string_for_type : Proof.context -> typ -> string + val pretty_for_type : Proof.context -> typ -> Pretty.T val prefix_name : string -> string -> string val shortest_name : string -> string val short_name : string -> string @@ -467,6 +468,7 @@ val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type +fun pretty_for_type ctxt = Syntax.pretty_typ ctxt o unarize_unbox_etc_type val prefix_name = Long_Name.qualify o Long_Name.base_name fun shortest_name s = List.last (space_explode "." s) handle List.Empty => "" diff -r fd28328daf73 -r 7f12a03c513c src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Aug 03 18:27:21 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Aug 03 21:20:31 2010 +0200 @@ -141,7 +141,7 @@ (card_of_type card_assigns T handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T) -fun quintuple_for_scope quote +fun quintuple_for_scope code_type code_term code_string ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth, datatypes, ...} : scope) = let @@ -154,26 +154,26 @@ card_assigns |> List.partition ((is_integer_type orf is_datatype ctxt stds) o fst) val cards = - map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^ - string_of_int k) + map (fn (T, k) => + [code_type ctxt T, code_string (" = " ^ string_of_int k)]) fun maxes () = maps (map_filter (fn {const, explicit_max, ...} => if explicit_max < 0 then NONE else - SOME (Syntax.string_of_term ctxt (Const const) ^ " = " ^ - string_of_int explicit_max)) + SOME [code_term ctxt (Const const), + code_string (" = " ^ string_of_int explicit_max)]) o #constrs) datatypes fun iters () = map (fn (T, k) => - quote (Syntax.string_of_term ctxt - (Const (const_for_iterator_type T))) ^ " = " ^ - string_of_int (k - 1)) iter_assigns + [code_term ctxt (Const (const_for_iterator_type T)), + code_string (" = " ^ string_of_int (k - 1))]) iter_assigns fun miscs () = - (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @ + (if bits = 0 then [] + else [code_string ("bits = " ^ string_of_int bits)]) @ (if bisim_depth < 0 andalso forall (not o #co) datatypes then [] - else ["bisim_depth = " ^ signed_string_of_int bisim_depth]) + else [code_string ("bisim_depth = " ^ signed_string_of_int bisim_depth)]) in setmp_show_all_types (fn () => (cards primary_card_assigns, cards secondary_card_assigns, @@ -182,31 +182,33 @@ fun pretties_for_scope scope verbose = let - val (primary_cards, secondary_cards, maxes, iters, bisim_depths) = - quintuple_for_scope maybe_quote scope - val ss = map (prefix "card ") primary_cards @ - (if verbose then - map (prefix "card ") secondary_cards @ - map (prefix "max ") maxes @ - map (prefix "iter ") iters @ - bisim_depths - else - []) + fun standard_blocks s = map (Pretty.block o cons (Pretty.str (s ^ " "))) + val (primary_cards, secondary_cards, maxes, iters, miscs) = + quintuple_for_scope (pretty_maybe_quote oo pretty_for_type) + (pretty_maybe_quote oo Syntax.pretty_term) + Pretty.str scope in - if null ss then [] - else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks + standard_blocks "card" primary_cards @ + (if verbose then + standard_blocks "card" secondary_cards @ + standard_blocks "max" maxes @ + standard_blocks "iter" iters @ + miscs + else + []) + |> pretty_serial_commas "and" end fun multiline_string_for_scope scope = let - val (primary_cards, secondary_cards, maxes, iters, bisim_depths) = - quintuple_for_scope I scope + val (primary_cards, secondary_cards, maxes, iters, miscs) = + quintuple_for_scope Syntax.string_of_typ Syntax.string_of_term I scope val cards = primary_cards @ secondary_cards in - case (if null cards then [] else ["card: " ^ commas cards]) @ - (if null maxes then [] else ["max: " ^ commas maxes]) @ - (if null iters then [] else ["iter: " ^ commas iters]) @ - bisim_depths of + case (if null cards then [] else ["card: " ^ commas (map implode cards)]) @ + (if null maxes then [] else ["max: " ^ commas (map implode maxes)]) @ + (if null iters then [] else ["iter: " ^ commas (map implode iters)]) @ + miscs of [] => "empty" | lines => space_implode "\n" lines end diff -r fd28328daf73 -r 7f12a03c513c src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Aug 03 18:27:21 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Aug 03 21:20:31 2010 +0200 @@ -49,6 +49,7 @@ val plural_s : int -> string val plural_s_for_list : 'a list -> string val serial_commas : string -> string list -> string list + val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option val flip_polarity : polarity -> polarity @@ -72,7 +73,7 @@ val indent_size : int val pstrs : string -> Pretty.T list val unyxml : string -> string - val maybe_quote : string -> string + val pretty_maybe_quote : Pretty.T -> Pretty.T val hashw : word * word -> word val hashw_string : string * word -> word end; @@ -222,6 +223,16 @@ val serial_commas = Sledgehammer_Util.serial_commas +fun pretty_serial_commas _ [] = [] + | pretty_serial_commas _ [p] = [p] + | pretty_serial_commas conj [p1, p2] = + [p1, Pretty.brk 1, Pretty.str conj, Pretty.brk 1, p2] + | pretty_serial_commas conj [p1, p2, p3] = + [p1, Pretty.str ",", Pretty.brk 1, p2, Pretty.str ",", Pretty.brk 1, + Pretty.str conj, Pretty.brk 1, p3] + | pretty_serial_commas conj (p :: ps) = + p :: Pretty.str "," :: Pretty.brk 1 :: pretty_serial_commas conj ps + val parse_bool_option = Sledgehammer_Util.parse_bool_option val parse_time_option = Sledgehammer_Util.parse_time_option @@ -262,14 +273,19 @@ fun setmp_show_all_types f = setmp_CRITICAL show_all_types - (! show_types orelse ! show_sorts orelse ! show_all_types) f + (!show_types orelse !show_sorts orelse !show_all_types) f val indent_size = 2 val pstrs = Pretty.breaks o map Pretty.str o space_explode " " val unyxml = Sledgehammer_Util.unyxml + val maybe_quote = Sledgehammer_Util.maybe_quote +fun pretty_maybe_quote pretty = + let val s = Pretty.str_of pretty in + if maybe_quote s = s then pretty else Pretty.enum "" "\"" "\"" [pretty] + end (* This hash function is recommended in Compilers: Principles, Techniques, and Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they