--- 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
--- 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 => ""
--- 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
--- 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