# HG changeset patch # User boehmes # Date 1298927529 -3600 # Node ID 41b9acc0114dd31bc6d856fdf6948c4f1d25159c # Parent e5104b436ea145a19b6e8644eb4f81488eb29ad6# Parent a38536bf273629abc0ae79cc0474e0fb6ff02249 merged diff -r e5104b436ea1 -r 41b9acc0114d doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Mon Feb 28 22:10:57 2011 +0100 +++ b/doc-src/Nitpick/nitpick.tex Mon Feb 28 22:12:09 2011 +0100 @@ -2477,6 +2477,14 @@ Specifies the default preconstruction setting to use. This can be overridden on a per-term basis using the \textit{preconstr}~\qty{term} option described above. +\opsmart{total\_consts}{partial\_consts} +Specifies whether constants occurring in the problem other than constructors can +be assumed to be considered total for the representable values that approximate +a datatype. This option is highly incomplete; it should be used only for +problems that do not construct datatype values explicitly. Since this option is +(in rare cases) unsound, counterexamples generated under these conditions are +tagged as ``quasi genuine.'' + \opdefault{datatype\_sym\_break}{int}{\upshape 5} Specifies an upper bound on the number of datatypes for which Nitpick generates symmetry breaking predicates. Symmetry breaking can speed up the SAT solver diff -r e5104b436ea1 -r 41b9acc0114d src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 28 22:10:57 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 28 22:12:09 2011 +0100 @@ -34,6 +34,7 @@ destroy_constrs: bool, specialize: bool, star_linear_preds: bool, + total_consts: bool option, preconstrs: (term option * bool option) list, peephole_optim: bool, datatype_sym_break: int, @@ -108,6 +109,7 @@ destroy_constrs: bool, specialize: bool, star_linear_preds: bool, + total_consts: bool option, preconstrs: (term option * bool option) list, peephole_optim: bool, datatype_sym_break: int, @@ -211,10 +213,10 @@ boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord, user_axioms, assms, whacks, merge_type_vars, binary_ints, destroy_constrs, specialize, star_linear_preds, - preconstrs, peephole_optim, datatype_sym_break, kodkod_sym_break, - tac_timeout, max_threads, show_datatypes, show_consts, evals, formats, - atomss, max_potential, max_genuine, check_potential, check_genuine, - batch_size, ...} = params + total_consts, preconstrs, peephole_optim, datatype_sym_break, + kodkod_sym_break, tac_timeout, max_threads, show_datatypes, + show_consts, evals, formats, atomss, max_potential, max_genuine, + check_potential, check_genuine, batch_size, ...} = params val state_ref = Unsynchronized.ref state val pprint = if auto then @@ -487,7 +489,10 @@ string_of_int j0)) (Typtab.dest ofs) *) - val all_exact = forall (is_exact_type datatypes true) all_Ts + val effective_total_consts = + case total_consts of + SOME b => b + | NONE => forall (is_exact_type datatypes true) all_Ts val main_j0 = offset_of_type ofs bool_T val (nat_card, nat_j0) = spec_of_type scope nat_T val (int_card, int_j0) = spec_of_type scope int_T @@ -500,7 +505,8 @@ NameTable.empty 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 + choose_reps_for_consts scope effective_total_consts nonsel_names + rep_table val (guiltiest_party, min_highest_arity) = NameTable.fold (fn (name, R) => fn (s, n) => let val n' = arity_of_rep R in @@ -637,7 +643,8 @@ nonsel_names rel_table bounds val genuine_means_genuine = got_all_user_axioms andalso none_true wfs andalso - sound_finitizes andalso codatatypes_ok + sound_finitizes andalso total_consts <> SOME true andalso + codatatypes_ok fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts) in (pprint (Pretty.chunks @@ -693,6 +700,8 @@ ? cons ("wf", "\"smart\" or \"false\"") |> not sound_finitizes ? cons ("finitize", "\"smart\" or \"false\"") + |> total_consts = SOME true + ? cons ("total_consts", "\"smart\" or \"false\"") |> not codatatypes_ok ? cons ("bisim_depth", "a nonnegative value") val ss = diff -r e5104b436ea1 -r 41b9acc0114d src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 28 22:10:57 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 28 22:12:09 2011 +0100 @@ -66,12 +66,6 @@ val strip_first_name_sep : string -> string * string val original_name : string -> string val abs_var : indexname * typ -> term -> term - val is_higher_order_type : typ -> bool - val is_special_eligible_arg : bool -> typ list -> term -> bool - val s_let : - typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term - val s_betapply : typ list -> term * term -> term - val s_betapplys : typ list -> term * term list -> term val s_conj : term * term -> term val s_disj : term * term -> term val strip_any_connective : term -> term list * term @@ -105,6 +99,7 @@ val is_integer_like_type : typ -> bool val is_record_type : typ -> bool val is_number_type : Proof.context -> typ -> bool + val is_higher_order_type : typ -> bool val const_for_iterator_type : typ -> styp val strip_n_binders : int -> typ -> typ list * typ val nth_range_type : int -> typ -> typ @@ -165,6 +160,18 @@ val num_datatype_constrs : hol_context -> typ -> int val constr_name_for_sel_like : string -> string val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp + val card_of_type : (typ * int) list -> typ -> int + val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int + val bounded_exact_card_of_type : + hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int + val typical_card_of_type : typ -> int + val is_finite_type : hol_context -> typ -> bool + val is_small_finite_type : hol_context -> typ -> bool + val is_special_eligible_arg : bool -> typ list -> term -> bool + val s_let : + typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term + val s_betapply : typ list -> term * term -> term + val s_betapplys : typ list -> term * term list -> term val discriminate_value : hol_context -> styp -> term -> term val select_nth_constr_arg : Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ @@ -172,12 +179,6 @@ val construct_value : Proof.context -> (typ option * bool) list -> styp -> term list -> term val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term - val card_of_type : (typ * int) list -> typ -> int - val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int - val bounded_exact_card_of_type : - hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int - val is_finite_type : hol_context -> typ -> bool - val is_small_finite_type : hol_context -> typ -> bool val special_bounds : term list -> (indexname * typ) list val is_funky_typedef : Proof.context -> typ -> bool val all_axioms_of : @@ -327,68 +328,6 @@ else s -fun is_higher_order_type (Type (@{type_name fun}, _)) = true - | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts - | is_higher_order_type _ = false - -fun is_special_eligible_arg strict Ts t = - let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in - null bad_Ts orelse - (is_higher_order_type (fastype_of1 (Ts, t)) andalso - not strict orelse forall (not o is_higher_order_type) bad_Ts) - end - -fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) - -fun let_var s = (nitpick_prefix ^ s, 999) -val let_inline_threshold = 20 - -fun s_let Ts s n abs_T body_T f t = - if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse - is_special_eligible_arg false Ts t then - f t - else - let val z = (let_var s, abs_T) in - Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T) - $ t $ abs_var z (incr_boundvars 1 (f (Var z))) - end - -fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0 - | loose_bvar1_count (t1 $ t2, k) = - loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k) - | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1) - | loose_bvar1_count _ = 0 - -fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1' - | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2 - | s_betapply Ts (Const (@{const_name Let}, - Type (_, [bound_T, Type (_, [_, body_T])])) - $ t12 $ Abs (s, T, t13'), t2) = - let val body_T' = range_type body_T in - Const (@{const_name Let}, bound_T --> (bound_T --> body_T') --> body_T') - $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2)) - end - | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) = - (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1')) - (curry betapply t1) t2 - handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *) - | s_betapply _ (t1, t2) = t1 $ t2 -fun s_betapplys Ts = Library.foldl (s_betapply Ts) - -fun s_beta_norm Ts t = - let - fun aux _ (Var _) = raise Same.SAME - | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t') - | aux Ts ((t1 as Abs _) $ t2) = - Same.commit (aux Ts) (s_betapply Ts (t1, t2)) - | aux Ts (t1 $ t2) = - ((case aux Ts t1 of - t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2)) - | t1 => t1 $ Same.commit (aux Ts) t2) - handle Same.SAME => t1 $ aux Ts t2) - | aux _ _ = raise Same.SAME - in aux Ts t handle Same.SAME => t end - fun s_conj (t1, @{const True}) = t1 | s_conj (@{const True}, t2) = t2 | s_conj (t1, t2) = @@ -554,6 +493,9 @@ |> these |> null |> not | is_frac_type _ _ = false fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt +fun is_higher_order_type (Type (@{type_name fun}, _)) = true + | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts + | is_higher_order_type _ = false fun iterator_type_for_const gfp (s, T) = Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s, @@ -1000,6 +942,162 @@ |> the |> pair s end +fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) = + reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) + | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) = + card_of_type assigns T1 * card_of_type assigns T2 + | card_of_type _ (Type (@{type_name itself}, _)) = 1 + | card_of_type _ @{typ prop} = 2 + | card_of_type _ @{typ bool} = 2 + | card_of_type assigns T = + case AList.lookup (op =) assigns T of + SOME k => k + | NONE => if T = @{typ bisim_iterator} then 0 + else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) + +fun bounded_card_of_type max default_card assigns + (Type (@{type_name fun}, [T1, T2])) = + let + val k1 = bounded_card_of_type max default_card assigns T1 + val k2 = bounded_card_of_type max default_card assigns T2 + in + if k1 = max orelse k2 = max then max + else Int.min (max, reasonable_power k2 k1) + end + | bounded_card_of_type max default_card assigns + (Type (@{type_name prod}, [T1, T2])) = + let + val k1 = bounded_card_of_type max default_card assigns T1 + val k2 = bounded_card_of_type max default_card assigns T2 + in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end + | bounded_card_of_type max default_card assigns T = + Int.min (max, if default_card = ~1 then + card_of_type assigns T + else + card_of_type assigns T + handle TYPE ("Nitpick_HOL.card_of_type", _, _) => + default_card) + +fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card + assigns T = + let + fun aux avoid T = + (if member (op =) avoid T then + 0 + else if member (op =) finitizable_dataTs T then + raise SAME () + else case T of + Type (@{type_name fun}, [T1, T2]) => + let + val k1 = aux avoid T1 + val k2 = aux avoid T2 + in + if k1 = 0 orelse k2 = 0 then 0 + else if k1 >= max orelse k2 >= max then max + else Int.min (max, reasonable_power k2 k1) + end + | Type (@{type_name prod}, [T1, T2]) => + let + val k1 = aux avoid T1 + val k2 = aux avoid T2 + in + if k1 = 0 orelse k2 = 0 then 0 + else if k1 >= max orelse k2 >= max then max + else Int.min (max, k1 * k2) + end + | Type (@{type_name itself}, _) => 1 + | @{typ prop} => 2 + | @{typ bool} => 2 + | Type _ => + (case datatype_constrs hol_ctxt T of + [] => if is_integer_type T orelse is_bit_type T then 0 + else raise SAME () + | constrs => + let + val constr_cards = + map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd) + constrs + in + if exists (curry (op =) 0) constr_cards then 0 + else Integer.sum constr_cards + end) + | _ => raise SAME ()) + handle SAME () => + AList.lookup (op =) assigns T |> the_default default_card + in Int.min (max, aux [] T) end + +val typical_atomic_card = 4 +val typical_card_of_type = bounded_card_of_type 65536 typical_atomic_card [] + +val small_type_max_card = 5 + +fun is_finite_type hol_ctxt T = + bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0 +fun is_small_finite_type hol_ctxt T = + let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in + n > 0 andalso n <= small_type_max_card + end + +fun is_special_eligible_arg strict Ts t = + case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of + [] => true + | bad_Ts => + let + val bad_Ts_cost = fold (Integer.max o typical_card_of_type) bad_Ts 0 + val T_cost = typical_card_of_type (fastype_of1 (Ts, t)) + in (bad_Ts_cost, T_cost) |> (if strict then op < else op <=) end + +fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) + +fun let_var s = (nitpick_prefix ^ s, 999) +val let_inline_threshold = 20 + +fun s_let Ts s n abs_T body_T f t = + if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse + is_special_eligible_arg false Ts t then + f t + else + let val z = (let_var s, abs_T) in + Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T) + $ t $ abs_var z (incr_boundvars 1 (f (Var z))) + end + +fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0 + | loose_bvar1_count (t1 $ t2, k) = + loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k) + | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1) + | loose_bvar1_count _ = 0 + +fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1' + | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2 + | s_betapply Ts (Const (@{const_name Let}, + Type (_, [bound_T, Type (_, [_, body_T])])) + $ t12 $ Abs (s, T, t13'), t2) = + let val body_T' = range_type body_T in + Const (@{const_name Let}, bound_T --> (bound_T --> body_T') --> body_T') + $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2)) + end + | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) = + (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1')) + (curry betapply t1) t2 + handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *) + | s_betapply _ (t1, t2) = t1 $ t2 +fun s_betapplys Ts = Library.foldl (s_betapply Ts) + +fun s_beta_norm Ts t = + let + fun aux _ (Var _) = raise Same.SAME + | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t') + | aux Ts ((t1 as Abs _) $ t2) = + Same.commit (aux Ts) (s_betapply Ts (t1, t2)) + | aux Ts (t1 $ t2) = + ((case aux Ts t1 of + t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2)) + | t1 => t1 $ Same.commit (aux Ts) t2) + handle Same.SAME => t1 $ aux Ts t2) + | aux _ _ = raise Same.SAME + in aux Ts t handle Same.SAME => t end + fun discr_term_for_constr hol_ctxt (x as (s, T)) = let val dataT = body_type T in if s = @{const_name Suc} then @@ -1136,97 +1234,6 @@ raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) -fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) = - reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) - | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) = - card_of_type assigns T1 * card_of_type assigns T2 - | card_of_type _ (Type (@{type_name itself}, _)) = 1 - | card_of_type _ @{typ prop} = 2 - | card_of_type _ @{typ bool} = 2 - | card_of_type assigns T = - case AList.lookup (op =) assigns T of - SOME k => k - | NONE => if T = @{typ bisim_iterator} then 0 - else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) -fun bounded_card_of_type max default_card assigns - (Type (@{type_name fun}, [T1, T2])) = - let - val k1 = bounded_card_of_type max default_card assigns T1 - val k2 = bounded_card_of_type max default_card assigns T2 - in - if k1 = max orelse k2 = max then max - else Int.min (max, reasonable_power k2 k1) - end - | bounded_card_of_type max default_card assigns - (Type (@{type_name prod}, [T1, T2])) = - let - val k1 = bounded_card_of_type max default_card assigns T1 - val k2 = bounded_card_of_type max default_card assigns T2 - in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end - | bounded_card_of_type max default_card assigns T = - Int.min (max, if default_card = ~1 then - card_of_type assigns T - else - card_of_type assigns T - handle TYPE ("Nitpick_HOL.card_of_type", _, _) => - default_card) -fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card - assigns T = - let - fun aux avoid T = - (if member (op =) avoid T then - 0 - else if member (op =) finitizable_dataTs T then - raise SAME () - else case T of - Type (@{type_name fun}, [T1, T2]) => - let - val k1 = aux avoid T1 - val k2 = aux avoid T2 - in - if k1 = 0 orelse k2 = 0 then 0 - else if k1 >= max orelse k2 >= max then max - else Int.min (max, reasonable_power k2 k1) - end - | Type (@{type_name prod}, [T1, T2]) => - let - val k1 = aux avoid T1 - val k2 = aux avoid T2 - in - if k1 = 0 orelse k2 = 0 then 0 - else if k1 >= max orelse k2 >= max then max - else Int.min (max, k1 * k2) - end - | Type (@{type_name itself}, _) => 1 - | @{typ prop} => 2 - | @{typ bool} => 2 - | Type _ => - (case datatype_constrs hol_ctxt T of - [] => if is_integer_type T orelse is_bit_type T then 0 - else raise SAME () - | constrs => - let - val constr_cards = - map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd) - constrs - in - if exists (curry (op =) 0) constr_cards then 0 - else Integer.sum constr_cards - end) - | _ => raise SAME ()) - handle SAME () => - AList.lookup (op =) assigns T |> the_default default_card - in Int.min (max, aux [] T) end - -val small_type_max_card = 5 - -fun is_finite_type hol_ctxt T = - bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0 -fun is_small_finite_type hol_ctxt T = - let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in - n > 0 andalso n <= small_type_max_card - end - fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 | is_ground_term (Const _) = true | is_ground_term _ = false diff -r e5104b436ea1 -r 41b9acc0114d src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 28 22:10:57 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 28 22:12:09 2011 +0100 @@ -58,6 +58,7 @@ ("destroy_constrs", "true"), ("specialize", "true"), ("star_linear_preds", "true"), + ("total_consts", "smart"), ("preconstr", "smart"), ("peephole_optim", "true"), ("datatype_sym_break", "5"), @@ -91,6 +92,7 @@ ("dont_destroy_constrs", "destroy_constrs"), ("dont_specialize", "specialize"), ("dont_star_linear_preds", "star_linear_preds"), + ("partial_consts", "total_consts"), ("dont_preconstr", "preconstr"), ("no_peephole_optim", "peephole_optim"), ("no_debug", "debug"), @@ -253,6 +255,7 @@ val destroy_constrs = lookup_bool "destroy_constrs" val specialize = lookup_bool "specialize" val star_linear_preds = lookup_bool "star_linear_preds" + val total_consts = lookup_bool_option "total_consts" val preconstrs = lookup_bool_option_assigns read_term_polymorphic "preconstr" val peephole_optim = lookup_bool "peephole_optim" @@ -285,8 +288,9 @@ user_axioms = user_axioms, assms = assms, whacks = whacks, merge_type_vars = merge_type_vars, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, - star_linear_preds = star_linear_preds, preconstrs = preconstrs, - peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break, + star_linear_preds = star_linear_preds, total_consts = total_consts, + preconstrs = preconstrs, peephole_optim = peephole_optim, + datatype_sym_break = datatype_sym_break, kodkod_sym_break = kodkod_sym_break, timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads, show_datatypes = show_datatypes, show_consts = show_consts, diff -r e5104b436ea1 -r 41b9acc0114d src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 28 22:10:57 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 28 22:12:09 2011 +0100 @@ -649,7 +649,7 @@ best_non_opt_set_rep_for_type) scope (type_of v) val v = modify_name_rep v R in (v :: vs, NameTable.update (v, R) table) end -fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v +fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) total_consts v (vs, table) = let val x as (s, T) = (nickname_of v, type_of v) @@ -657,7 +657,7 @@ rep_for_abs_fun else if is_rep_fun ctxt x then Func oo best_non_opt_symmetric_reps_for_fun_type - else if all_exact orelse is_skolem_name v orelse + else if total_consts orelse is_skolem_name v orelse member (op =) [@{const_name bisim}, @{const_name bisim_iterator_max}] (original_name s) then @@ -674,8 +674,8 @@ fun choose_reps_for_free_vars scope pseudo_frees vs table = fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table) -fun choose_reps_for_consts scope all_exact vs table = - fold (choose_rep_for_const scope all_exact) vs ([], table) +fun choose_reps_for_consts scope total_consts vs table = + fold (choose_rep_for_const scope total_consts) vs ([], table) fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...}) (x as (_, T)) n (vs, table) = diff -r e5104b436ea1 -r 41b9acc0114d src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 28 22:10:57 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 28 22:12:09 2011 +0100 @@ -1165,12 +1165,10 @@ aux "" [] [] t1 $ aux "" [] [] t2 else let - val typical_card = 4 fun big_union proj ps = fold (fold (insert (op =)) o proj) ps [] val (ts, connective) = strip_any_connective t - val T_costs = - map (bounded_card_of_type 65536 typical_card []) Ts + val T_costs = map typical_card_of_type Ts val t_costs = map size_of_term ts val num_Ts = length Ts val flip = curry (op -) (num_Ts - 1) diff -r e5104b436ea1 -r 41b9acc0114d src/HOL/Tools/smallvalue_generators.ML --- a/src/HOL/Tools/smallvalue_generators.ML Mon Feb 28 22:10:57 2011 +0100 +++ b/src/HOL/Tools/smallvalue_generators.ML Mon Feb 28 22:12:09 2011 +0100 @@ -8,8 +8,12 @@ sig val compile_generator_expr: Proof.context -> term -> int -> term list option * Quickcheck.report option + val compile_generator_exprs: + Proof.context -> term list -> (int -> term list option) list val put_counterexample: (unit -> int -> term list option) -> Proof.context -> Proof.context + val put_counterexample_batch: (unit -> (int -> term list option) list) + -> Proof.context -> Proof.context val smart_quantifier : bool Config.T; val setup: theory -> theory end; @@ -218,6 +222,14 @@ ); val put_counterexample = Counterexample.put; +structure Counterexample_Batch = Proof_Data +( + type T = unit -> (int -> term list option) list + (* FIXME avoid user error with non-user text *) + fun init _ () = error "Counterexample" +); +val put_counterexample_batch = Counterexample_Batch.put; + val target = "Quickcheck"; fun mk_smart_generator_expr ctxt t = @@ -338,9 +350,25 @@ (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample") thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' []; in - fn size => rpair NONE (compile size |> Option.map (map post_process_term)) + fn size => rpair NONE (compile size |> Option.map (map post_process_term)) end; +fun compile_generator_exprs ctxt ts = + let + val thy = ProofContext.theory_of ctxt + val mk_generator_expr = + if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr + val ts' = map (mk_generator_expr ctxt) ts; + val compiles = Code_Runtime.dynamic_value_strict + (Counterexample_Batch.get, put_counterexample_batch, + "Smallvalue_Generators.put_counterexample_batch") + thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc)) + (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') []; + in + map (fn compile => fn size => compile size |> Option.map (map post_process_term)) compiles + end; + + (** setup **) val setup = @@ -348,6 +376,8 @@ (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype)) #> setup_smart_quantifier #> Context.theory_map - (Quickcheck.add_generator ("exhaustive", compile_generator_expr)); + (Quickcheck.add_generator ("exhaustive", compile_generator_expr)) + #> Context.theory_map + (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)); end; diff -r e5104b436ea1 -r 41b9acc0114d src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Mon Feb 28 22:10:57 2011 +0100 +++ b/src/Tools/quickcheck.ML Mon Feb 28 22:12:09 2011 +0100 @@ -30,6 +30,9 @@ val add_generator: string * (Proof.context -> term -> int -> term list option * report option) -> Context.generic -> Context.generic + val add_batch_generator: + string * (Proof.context -> term list -> (int -> term list option) list) + -> Context.generic -> Context.generic (* testing terms and proof states *) val test_term: Proof.context -> bool * bool -> term -> (string * term) list option * ((string * int) list * ((int * report) list) option) @@ -37,6 +40,8 @@ Proof.context -> bool * bool -> (string * typ) list -> term list -> (string * term) list option * ((string * int) list * ((int * report) list) option) list val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option + (* testing a batch of terms *) + val test_terms: Proof.context -> term list -> (string * term) list option list option end; structure Quickcheck : QUICKCHECK = @@ -104,12 +109,14 @@ structure Data = Generic_Data ( type T = - (string * (Proof.context -> term -> int -> term list option * report option)) list + ((string * (Proof.context -> term -> int -> term list option * report option)) list + * (string * (Proof.context -> term list -> (int -> term list option) list)) list) * test_params; - val empty = ([], Test_Params {default_type = [], expect = No_Expectation}); + val empty = (([], []), Test_Params {default_type = [], expect = No_Expectation}); val extend = I; - fun merge ((generators1, params1), (generators2, params2)) : T = - (AList.merge (op =) (K true) (generators1, generators2), + fun merge (((generators1, batch_generators1), params1), ((generators2, batch_generators2), params2)) : T = + ((AList.merge (op =) (K true) (generators1, generators2), + AList.merge (op =) (K true) (batch_generators1, batch_generators2)), merge_test_params (params1, params2)); ); @@ -121,28 +128,34 @@ val map_test_params = Data.map o apsnd o map_test_params' -val add_generator = Data.map o apfst o AList.update (op =); +val add_generator = Data.map o apfst o apfst o AList.update (op =); + +val add_batch_generator = Data.map o apfst o apsnd o AList.update (op =); (* generating tests *) -fun mk_tester ctxt t = +fun gen_mk_tester lookup ctxt v = let val name = Config.get ctxt tester - val tester = case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name + val tester = case lookup ctxt name of NONE => error ("No such quickcheck tester: " ^ name) | SOME tester => tester ctxt; in if Config.get ctxt quiet then - try tester t + try tester v else let - val tester = Exn.interruptible_capture tester t + val tester = Exn.interruptible_capture tester v in case Exn.get_result tester of NONE => SOME (Exn.release tester) | SOME tester => SOME tester end end +val mk_tester = gen_mk_tester (fn ctxt => + AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt)) +val mk_batch_tester = gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o fst o Data.get o Context.Proof) ctxt)) + (* testing propositions *) fun prep_test_term t = @@ -204,6 +217,21 @@ end) (fn () => error (excipit "ran out of time")) () end; +fun test_terms ctxt ts = + let + val (namess, ts') = split_list (map (fn t => apfst (map fst) (prep_test_term t)) ts) + val test_funs = mk_batch_tester ctxt ts' + fun with_size tester k = + if k > Config.get ctxt size then NONE + else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1) + val results = + Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) + (fn () => with_size test_fun 1) () + handle TimeLimit.TimeOut => NONE)) test_funs + in + Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results + end + (* FIXME: this function shows that many assumptions are made upon the generation *) (* In the end there is probably no generic quickcheck interface left... *) @@ -403,7 +431,7 @@ | read_expectation "counterexample" = Counterexample | read_expectation s = error ("Not an expectation value: " ^ s) -fun valid_tester_name genctxt = AList.defined (op =) (fst (Data.get genctxt)) +fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (Data.get genctxt))) fun parse_tester name genctxt = if valid_tester_name genctxt name then