--- a/doc-src/Nitpick/nitpick.tex Mon Feb 21 10:44:19 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex Mon Feb 21 11:50:31 2011 +0100
@@ -2108,26 +2108,18 @@
per-type basis using the \textit{box}~\qty{type} option described above.
\opargboolorsmart{finitize}{type}{dont\_finitize}
-Specifies whether Nitpick should attempt to finitize an infinite ``shallow
-datatype'' (an infinite datatype whose constructors don't appear in the
-problem). The option can then take the following values:
-
-\begin{enum}
-\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
-\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}:} Finitize the
-type wherever possible.
-\end{enum}
-
-The semantics of the option is somewhat different for infinite shallow
-datatypes:
+Specifies whether Nitpick should attempt to finitize an infinite datatype. The
+option can then take the following values:
\begin{enum}
\item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
unsound, counterexamples generated under these conditions are tagged as ``quasi
genuine.''
\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
-\item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to
-detect whether the datatype can be soundly finitized before finitizing it.
+\item[$\bullet$] \textbf{\textit{smart}:}
+If the datatype's constructors don't appear in the problem, perform a
+monotonicity analysis to detect whether the datatype can be soundly finitized;
+otherwise, don't finitize it.
\end{enum}
\nopagebreak
--- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Feb 21 10:44:19 2011 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Mon Feb 21 11:50:31 2011 +0100
@@ -169,7 +169,7 @@
val is_problem_trivially_false : problem -> bool
val problems_equivalent : problem * problem -> bool
val solve_any_problem :
- bool -> Time.time option -> int -> int -> problem list -> outcome
+ bool -> bool -> Time.time option -> int -> int -> problem list -> outcome
end;
structure Kodkod : KODKOD =
@@ -1090,13 +1090,14 @@
Synchronized.var "Kodkod.cached_outcome"
(NONE : ((int * problem list) * outcome) option)
-fun solve_any_problem overlord deadline max_threads max_solutions problems =
+fun solve_any_problem debug overlord deadline max_threads max_solutions
+ problems =
let
fun do_solve () =
uncached_solve_any_problem overlord deadline max_threads max_solutions
problems
in
- if overlord then
+ if debug orelse overlord then
do_solve ()
else
case AList.lookup (fn ((max1, ps1), (max2, ps2)) =>
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 21 10:44:19 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 21 11:50:31 2011 +0100
@@ -363,6 +363,8 @@
SOME (SOME b) => b
| _ => is_type_fundamentally_monotonic T orelse
is_type_actually_monotonic T
+ fun is_deep_datatype_finitizable T =
+ triple_lookup (type_match thy) finitizes T = SOME (SOME true)
fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
is_type_kind_of_monotonic T
| is_shallow_datatype_finitizable T =
@@ -407,8 +409,10 @@
all_Ts |> filter (is_datatype ctxt stds)
|> List.partition is_datatype_deep
val finitizable_dataTs =
- shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
- |> filter is_shallow_datatype_finitizable
+ (deep_dataTs |> filter_out (is_finite_type hol_ctxt)
+ |> filter is_deep_datatype_finitizable) @
+ (shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
+ |> filter is_shallow_datatype_finitizable)
val _ =
if verbose andalso not (null finitizable_dataTs) then
pprint_v (K (monotonicity_message finitizable_dataTs
@@ -735,8 +739,8 @@
if max_solutions <= 0 then
(found_really_genuine, 0, 0, donno)
else
- case KK.solve_any_problem overlord deadline max_threads max_solutions
- (map fst problems) of
+ case KK.solve_any_problem debug overlord deadline max_threads
+ max_solutions (map fst problems) of
KK.JavaNotInstalled =>
(print_m install_java_message;
(found_really_genuine, max_potential, max_genuine, donno + 1))
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 21 10:44:19 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 21 11:50:31 2011 +0100
@@ -66,7 +66,9 @@
val original_name : string -> string
val abs_var : indexname * typ -> term -> term
val is_higher_order_type : typ -> bool
- val s_let : string -> int -> typ -> typ -> (term -> term) -> term -> term
+ 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
@@ -327,14 +329,23 @@
| 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 s n abs_T body_T f t =
+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_higher_order_type abs_T then
+ is_special_eligible_arg true Ts t then
+ (* TODO: the "true" argument to "is_special_eligible_arg" should perhaps be
+ "false" instead to account for potential future specializations. *)
f t
else
let val z = (let_var s, abs_T) in
@@ -358,7 +369,7 @@
$ 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 s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
+ (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
@@ -1617,7 +1628,7 @@
(* Inline definitions or define as an equational constant? Booleans tend to
benefit more from inlining, due to the polarity analysis. *)
-val def_inline_threshold_for_booleans = 50
+val def_inline_threshold_for_booleans = 60
val def_inline_threshold_for_non_booleans = 20
fun unfold_defs_in_term
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 21 10:44:19 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 21 11:50:31 2011 +0100
@@ -392,18 +392,18 @@
val num_occs_of_var =
fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
| _ => I) t (K 0)
- fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
- aux_eq careful true t0 t1 t2
- | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
- t0 $ aux false t1 $ aux careful t2
- | aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
- aux_eq careful true t0 t1 t2
- | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
- t0 $ aux false t1 $ aux careful t2
- | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
- | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
- | aux _ t = t
- and aux_eq careful pass1 t0 t1 t2 =
+ fun aux Ts careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
+ aux_eq Ts careful true t0 t1 t2
+ | aux Ts careful ((t0 as @{const "==>"}) $ t1 $ t2) =
+ t0 $ aux Ts false t1 $ aux Ts careful t2
+ | aux Ts careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
+ aux_eq Ts careful true t0 t1 t2
+ | aux Ts careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
+ t0 $ aux Ts false t1 $ aux Ts careful t2
+ | aux Ts careful (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) careful t')
+ | aux Ts careful (t1 $ t2) = aux Ts careful t1 $ aux Ts careful t2
+ | aux _ _ t = t
+ and aux_eq Ts careful pass1 t0 t1 t2 =
((if careful then
raise SAME ()
else if axiom andalso is_Var t2 andalso
@@ -426,22 +426,23 @@
x = (@{const_name Suc}, nat_T --> nat_T)) andalso
(not careful orelse not (is_Var t1) orelse
String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
- s_let "l" (n + 1) dataT bool_T
- (fn t1 => discriminate_value hol_ctxt x t1 ::
- map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
- |> foldr1 s_conj) t1
+ s_let Ts "l" (n + 1) dataT bool_T
+ (fn t1 =>
+ discriminate_value hol_ctxt x t1 ::
+ map3 (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args
+ |> foldr1 s_conj) t1
else
raise SAME ()
end
| _ => raise SAME ())
|> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
- handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
- else t0 $ aux false t2 $ aux false t1
- and sel_eq x t n nth_T nth_t =
+ handle SAME () => if pass1 then aux_eq Ts careful false t0 t2 t1
+ else t0 $ aux Ts false t2 $ aux Ts false t1
+ and sel_eq Ts x t n nth_T nth_t =
HOLogic.eq_const nth_T $ nth_t
$ select_nth_constr_arg ctxt stds x t n nth_T
- |> aux false
- in aux axiom t end
+ |> aux Ts false
+ in aux [] axiom t end
(** Destruction of universal and existential equalities **)
@@ -709,13 +710,6 @@
else if j1 > j2 then overlapping_indices ps1 ps2'
else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
-fun is_eligible_arg 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
- forall (not o is_higher_order_type) bad_Ts)
- end
-
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
(* If a constant's definition is picked up deeper than this threshold, we
@@ -747,8 +741,9 @@
not (is_constr ctxt stds x) andalso
not (is_choice_spec_fun hol_ctxt x))) then
let
- val eligible_args = filter (is_eligible_arg Ts o snd)
- (index_seq 0 (length args) ~~ args)
+ val eligible_args =
+ filter (is_special_eligible_arg true Ts o snd)
+ (index_seq 0 (length args) ~~ args)
val _ = not (null eligible_args) orelse raise SAME ()
val old_axs = equational_fun_axioms hol_ctxt x
|> map (destroy_existential_equalities hol_ctxt)
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 21 10:44:19 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 21 11:50:31 2011 +0100
@@ -211,11 +211,11 @@
fun run_all_tests () =
let
- val {overlord, ...} = Nitpick_Isar.default_params @{theory} []
+ val {debug, overlord, ...} = Nitpick_Isar.default_params @{theory} []
val max_threads = 1
val max_solutions = 1
in
- case Kodkod.solve_any_problem overlord NONE max_threads max_solutions
+ case Kodkod.solve_any_problem debug overlord NONE max_threads max_solutions
(map (problem_for_nut @{context}) tests) of
Kodkod.Normal ([], _, _) => ()
| _ => error "Tests failed."