--- 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
--- 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 =
--- 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
--- 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,
--- 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) =
--- 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)
--- 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;
--- 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