--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 03 14:54:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Aug 03 15:15:17 2010 +0200
@@ -466,12 +466,15 @@
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
val (nonsel_names, rep_table) =
choose_reps_for_consts scope all_exact nonsel_names rep_table
- val min_highest_arity =
- NameTable.fold (Integer.max o arity_of_rep o snd) rep_table 1
+ val (guiltiest_party, min_highest_arity) =
+ NameTable.fold (fn (name, R) => fn (s, n) =>
+ let val n' = arity_of_rep R in
+ if n' > n then (nickname_of name, n') else (s, n)
+ end) rep_table ("", 1)
val min_univ_card =
NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table
(univ_card nat_card int_card main_j0 [] KK.True)
- val _ = check_arity min_univ_card min_highest_arity
+ val _ = check_arity guiltiest_party min_univ_card min_highest_arity
val def_us = map (choose_reps_in_nut scope unsound rep_table true)
def_us
@@ -533,7 +536,7 @@
val formula = fold_rev s_and axioms formula
val _ = if bits = 0 then () else check_bits bits formula
val _ = if formula = KK.False then ()
- else check_arity univ_card highest_arity
+ else check_arity "" univ_card highest_arity
in
SOME ({comment = comment, settings = settings, univ_card = univ_card,
tuple_assigns = [], bounds = bounds,
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Aug 03 14:54:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Aug 03 15:15:17 2010 +0200
@@ -17,7 +17,7 @@
val univ_card :
int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int
val check_bits : int -> Kodkod.formula -> unit
- val check_arity : int -> int -> unit
+ val check_arity : string -> int -> int -> unit
val kk_tuple : bool -> int -> int list -> Kodkod.tuple
val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
val sequential_int_bounds : int -> Kodkod.int_bound list
@@ -93,11 +93,17 @@
int_expr_func = int_expr_func}
in KK.fold_formula expr_F formula () end
-fun check_arity univ_card n =
+fun check_arity guilty_party univ_card n =
if n > KK.max_arity univ_card then
raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
- "arity " ^ string_of_int n ^ " too large for universe of \
- \cardinality " ^ string_of_int univ_card)
+ "arity " ^ string_of_int n ^
+ (if guilty_party = "" then
+ ""
+ else
+ " of Kodkod relation associated with " ^
+ quote guilty_party) ^
+ " too large for universe of cardinality " ^
+ string_of_int univ_card)
else
()
@@ -200,7 +206,7 @@
fun tabulate_built_in_rel debug ofs univ_card nat_card int_card j0
(x as (n, _)) =
- (check_arity univ_card n;
+ (check_arity "" univ_card n;
if x = not3_rel then
("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1))
else if x = suc_rel then