1.1 --- a/doc-src/Nitpick/nitpick.tex Thu Mar 03 10:55:41 2011 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Thu Mar 03 11:20:48 2011 +0100
1.3 @@ -2465,17 +2465,17 @@
1.4
1.5 {\small See also \textit{debug} (\S\ref{output-format}).}
1.6
1.7 -\opargboolorsmart{preconstr}{term}{dont\_preconstr}
1.8 -Specifies whether a datatype value should be preconstructed, meaning Nitpick
1.9 +\opargboolorsmart{need}{term}{dont\_need}
1.10 +Specifies whether a datatype value is required by the problem, meaning Nitpick
1.11 will reserve a Kodkod atom for it. If a value must necessarily belong to the
1.12 -subset of representable values that approximates a datatype, preconstructing
1.13 -it can speed up the search significantly, especially for high cardinalities. By
1.14 -default, Nitpick inspects the conjecture to infer terms that can be
1.15 -preconstructed.
1.16 -
1.17 -\opsmart{preconstr}{dont\_preconstr}
1.18 -Specifies the default preconstruction setting to use. This can be overridden on
1.19 -a per-term basis using the \textit{preconstr}~\qty{term} option described above.
1.20 +subset of representable values that approximates a datatype, specifying it can
1.21 +speed up the search significantly, especially for high cardinalities. By
1.22 +default, Nitpick inspects the conjecture to infer needed datatype values.
1.23 +
1.24 +\opsmart{need}{dont\_need}
1.25 +Specifies the default needed datatype value setting to use. This can be
1.26 +overridden on a per-term basis using the \textit{preconstr}~\qty{term} option
1.27 +described above.
1.28
1.29 \opsmart{total\_consts}{partial\_consts}
1.30 Specifies whether constants occurring in the problem other than constructors can
2.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 03 10:55:41 2011 +0100
2.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 03 11:20:48 2011 +0100
2.3 @@ -39,7 +39,7 @@
2.4 stds = stds, wfs = [], user_axioms = NONE, debug = false,
2.5 whacks = [], binary_ints = SOME false, destroy_constrs = true,
2.6 specialize = false, star_linear_preds = false, total_consts = NONE,
2.7 - preconstrs = [], tac_timeout = NONE, evals = [], case_names = case_names,
2.8 + needs = [], tac_timeout = NONE, evals = [], case_names = case_names,
2.9 def_tables = def_tables, nondef_table = nondef_table,
2.10 user_nondefs = user_nondefs, simp_table = simp_table,
2.11 psimp_table = psimp_table, choice_spec_table = choice_spec_table,
3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 03 10:55:41 2011 +0100
3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 03 11:20:48 2011 +0100
3.3 @@ -35,7 +35,7 @@
3.4 specialize: bool,
3.5 star_linear_preds: bool,
3.6 total_consts: bool option,
3.7 - preconstrs: (term option * bool option) list,
3.8 + needs: (term option * bool option) list,
3.9 peephole_optim: bool,
3.10 datatype_sym_break: int,
3.11 kodkod_sym_break: int,
3.12 @@ -110,7 +110,7 @@
3.13 specialize: bool,
3.14 star_linear_preds: bool,
3.15 total_consts: bool option,
3.16 - preconstrs: (term option * bool option) list,
3.17 + needs: (term option * bool option) list,
3.18 peephole_optim: bool,
3.19 datatype_sym_break: int,
3.20 kodkod_sym_break: int,
3.21 @@ -199,7 +199,7 @@
3.22
3.23 fun check_constr_nut (Construct (_, _, _, us)) = List.app check_constr_nut us
3.24 | check_constr_nut _ =
3.25 - error "The \"preconstr\" option requires a constructor term."
3.26 + error "The \"need\" option requires a constructor term."
3.27
3.28 fun pick_them_nits_in_term deadline state (params : params) auto i n step
3.29 subst assm_ts orig_t =
3.30 @@ -217,7 +217,7 @@
3.31 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
3.32 verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
3.33 binary_ints, destroy_constrs, specialize, star_linear_preds,
3.34 - total_consts, preconstrs, peephole_optim, datatype_sym_break,
3.35 + total_consts, needs, peephole_optim, datatype_sym_break,
3.36 kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
3.37 show_consts, evals, formats, atomss, max_potential, max_genuine,
3.38 check_potential, check_genuine, batch_size, ...} = params
3.39 @@ -258,7 +258,7 @@
3.40 o Date.fromTimeLocal o Time.now)
3.41 val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
3.42 else orig_t
3.43 - val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs
3.44 + val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
3.45 val tfree_table =
3.46 if merge_type_vars then merged_type_var_table_for_terms thy conj_ts
3.47 else []
3.48 @@ -266,8 +266,8 @@
3.49 val neg_t = neg_t |> merge_tfrees
3.50 val assm_ts = assm_ts |> map merge_tfrees
3.51 val evals = evals |> map merge_tfrees
3.52 - val preconstrs = preconstrs |> map (apfst (Option.map merge_tfrees))
3.53 - val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs
3.54 + val needs = needs |> map (apfst (Option.map merge_tfrees))
3.55 + val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
3.56 val original_max_potential = max_potential
3.57 val original_max_genuine = max_genuine
3.58 val max_bisim_depth = fold Integer.max bisim_depths ~1
3.59 @@ -289,7 +289,7 @@
3.60 whacks = whacks, binary_ints = binary_ints,
3.61 destroy_constrs = destroy_constrs, specialize = specialize,
3.62 star_linear_preds = star_linear_preds, total_consts = total_consts,
3.63 - preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals,
3.64 + needs = needs, tac_timeout = tac_timeout, evals = evals,
3.65 case_names = case_names, def_tables = def_tables,
3.66 nondef_table = nondef_table, user_nondefs = user_nondefs,
3.67 simp_table = simp_table, psimp_table = psimp_table,
3.68 @@ -302,7 +302,7 @@
3.69 val real_frees = fold Term.add_frees conj_ts []
3.70 val _ = null (fold Term.add_tvars conj_ts []) orelse
3.71 error "Nitpick cannot handle goals with schematic type variables."
3.72 - val (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
3.73 + val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms,
3.74 no_poly_user_axioms, binarize) =
3.75 preprocess_formulas hol_ctxt assm_ts neg_t
3.76 val got_all_user_axioms =
3.77 @@ -332,8 +332,8 @@
3.78
3.79 val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq)
3.80 val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq)
3.81 - val preconstr_us = preconstr_ts |> map (nut_from_term hol_ctxt Eq)
3.82 - val _ = List.app check_constr_nut preconstr_us
3.83 + val need_us = need_ts |> map (nut_from_term hol_ctxt Eq)
3.84 + val _ = List.app check_constr_nut need_us
3.85 val (free_names, const_names) =
3.86 fold add_free_and_const_names (nondef_us @ def_us) ([], [])
3.87 val (sel_names, nonsel_names) =
3.88 @@ -526,8 +526,8 @@
3.89 def_us |> map (choose_reps_in_nut scope unsound rep_table true)
3.90 val nondef_us =
3.91 nondef_us |> map (choose_reps_in_nut scope unsound rep_table false)
3.92 - val preconstr_us =
3.93 - preconstr_us |> map (choose_reps_in_nut scope unsound rep_table false)
3.94 + val need_us =
3.95 + need_us |> map (choose_reps_in_nut scope unsound rep_table false)
3.96 (*
3.97 val _ = List.app (print_g o string_for_nut ctxt)
3.98 (free_names @ sel_names @ nonsel_names @
3.99 @@ -541,8 +541,7 @@
3.100 rename_free_vars nonsel_names pool rel_table
3.101 val nondef_us = nondef_us |> map (rename_vars_in_nut pool rel_table)
3.102 val def_us = def_us |> map (rename_vars_in_nut pool rel_table)
3.103 - val preconstr_us =
3.104 - preconstr_us |> map (rename_vars_in_nut pool rel_table)
3.105 + val need_us = need_us |> map (rename_vars_in_nut pool rel_table)
3.106 val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
3.107 val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
3.108 val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
3.109 @@ -568,7 +567,7 @@
3.110 val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
3.111 val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
3.112 val dtype_axioms =
3.113 - declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
3.114 + declarative_axioms_for_datatypes hol_ctxt binarize need_us
3.115 datatype_sym_break bits ofs kk rel_table datatypes
3.116 val declarative_axioms = plain_axioms @ dtype_axioms
3.117 val univ_card = Int.max (univ_card nat_card int_card main_j0
4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 03 10:55:41 2011 +0100
4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 03 11:20:48 2011 +0100
4.3 @@ -28,7 +28,7 @@
4.4 specialize: bool,
4.5 star_linear_preds: bool,
4.6 total_consts: bool option,
4.7 - preconstrs: (term option * bool option) list,
4.8 + needs: (term option * bool option) list,
4.9 tac_timeout: Time.time option,
4.10 evals: term list,
4.11 case_names: (string * int) list,
4.12 @@ -261,7 +261,7 @@
4.13 specialize: bool,
4.14 star_linear_preds: bool,
4.15 total_consts: bool option,
4.16 - preconstrs: (term option * bool option) list,
4.17 + needs: (term option * bool option) list,
4.18 tac_timeout: Time.time option,
4.19 evals: term list,
4.20 case_names: (string * int) list,
5.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 03 10:55:41 2011 +0100
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 03 11:20:48 2011 +0100
5.3 @@ -59,7 +59,7 @@
5.4 ("specialize", "true"),
5.5 ("star_linear_preds", "true"),
5.6 ("total_consts", "smart"),
5.7 - ("preconstr", "smart"),
5.8 + ("need", "smart"),
5.9 ("peephole_optim", "true"),
5.10 ("datatype_sym_break", "5"),
5.11 ("kodkod_sym_break", "15"),
5.12 @@ -93,7 +93,7 @@
5.13 ("dont_specialize", "specialize"),
5.14 ("dont_star_linear_preds", "star_linear_preds"),
5.15 ("partial_consts", "total_consts"),
5.16 - ("dont_preconstr", "preconstr"),
5.17 + ("dont_need", "need"),
5.18 ("no_peephole_optim", "peephole_optim"),
5.19 ("no_debug", "debug"),
5.20 ("quiet", "verbose"),
5.21 @@ -109,8 +109,8 @@
5.22 member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse
5.23 exists (fn p => String.isPrefix (p ^ " ") s)
5.24 ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
5.25 - "mono", "non_mono", "std", "non_std", "wf", "non_wf", "preconstr",
5.26 - "dont_preconstr", "format", "atoms"]
5.27 + "mono", "non_mono", "std", "non_std", "wf", "non_wf", "need",
5.28 + "dont_need", "format", "atoms"]
5.29
5.30 fun check_raw_param (s, _) =
5.31 if is_known_raw_param s then ()
5.32 @@ -256,8 +256,7 @@
5.33 val specialize = lookup_bool "specialize"
5.34 val star_linear_preds = lookup_bool "star_linear_preds"
5.35 val total_consts = lookup_bool_option "total_consts"
5.36 - val preconstrs =
5.37 - lookup_bool_option_assigns read_term_polymorphic "preconstr"
5.38 + val needs = lookup_bool_option_assigns read_term_polymorphic "need"
5.39 val peephole_optim = lookup_bool "peephole_optim"
5.40 val datatype_sym_break = lookup_int "datatype_sym_break"
5.41 val kodkod_sym_break = lookup_int "kodkod_sym_break"
5.42 @@ -289,7 +288,7 @@
5.43 merge_type_vars = merge_type_vars, binary_ints = binary_ints,
5.44 destroy_constrs = destroy_constrs, specialize = specialize,
5.45 star_linear_preds = star_linear_preds, total_consts = total_consts,
5.46 - preconstrs = preconstrs, peephole_optim = peephole_optim,
5.47 + needs = needs, peephole_optim = peephole_optim,
5.48 datatype_sym_break = datatype_sym_break,
5.49 kodkod_sym_break = kodkod_sym_break, timeout = timeout,
5.50 tac_timeout = tac_timeout, max_threads = max_threads,
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 03 10:55:41 2011 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 03 11:20:48 2011 +0100
6.3 @@ -1478,8 +1478,8 @@
6.4 "malformed Kodkod formula")
6.5 end
6.6
6.7 -fun preconstructed_value_axioms_for_datatype [] _ _ _ = []
6.8 - | preconstructed_value_axioms_for_datatype preconstr_us ofs kk
6.9 +fun needed_value_axioms_for_datatype [] _ _ _ = []
6.10 + | needed_value_axioms_for_datatype need_us ofs kk
6.11 ({typ, card, constrs, ...} : datatype_spec) =
6.12 let
6.13 fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
6.14 @@ -1507,10 +1507,9 @@
6.15 else
6.16 accum)
6.17 | aux u =
6.18 - raise NUT ("Nitpick_Kodkod.preconstructed_value_axioms_for_datatype\
6.19 - \.aux", [u])
6.20 + raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u])
6.21 in
6.22 - case SOME (index_seq 0 card, []) |> fold aux preconstr_us of
6.23 + case SOME (index_seq 0 card, []) |> fold aux need_us of
6.24 SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk)
6.25 | NONE => [KK.False]
6.26 end
6.27 @@ -1654,14 +1653,14 @@
6.28 nfas dtypes)
6.29 end
6.30
6.31 -fun is_datatype_in_preconstructed_value T (Construct (_, T', _, us)) =
6.32 - T = T' orelse exists (is_datatype_in_preconstructed_value T) us
6.33 - | is_datatype_in_preconstructed_value _ _ = false
6.34 +fun is_datatype_in_needed_value T (Construct (_, T', _, us)) =
6.35 + T = T' orelse exists (is_datatype_in_needed_value T) us
6.36 + | is_datatype_in_needed_value _ _ = false
6.37
6.38 val min_sym_break_card = 7
6.39
6.40 -fun sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
6.41 - datatype_sym_break kk rel_table nfas dtypes =
6.42 +fun sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
6.43 + kk rel_table nfas dtypes =
6.44 if datatype_sym_break = 0 then
6.45 []
6.46 else
6.47 @@ -1673,8 +1672,7 @@
6.48 o binder_types o snd o #const) constrs)
6.49 |> filter_out
6.50 (fn {typ, ...} =>
6.51 - exists (is_datatype_in_preconstructed_value typ)
6.52 - preconstr_us)
6.53 + exists (is_datatype_in_needed_value typ) need_us)
6.54 |> (fn dtypes' =>
6.55 dtypes' |> length dtypes' > datatype_sym_break
6.56 ? (sort (datatype_ord o swap)
6.57 @@ -1779,7 +1777,7 @@
6.58 partition_axioms_for_datatype j0 kk rel_table dtype
6.59 end
6.60
6.61 -fun declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
6.62 +fun declarative_axioms_for_datatypes hol_ctxt binarize need_us
6.63 datatype_sym_break bits ofs kk rel_table dtypes =
6.64 let
6.65 val nfas =
6.66 @@ -1788,9 +1786,9 @@
6.67 |> strongly_connected_sub_nfas
6.68 in
6.69 acyclicity_axioms_for_datatypes kk nfas @
6.70 - maps (preconstructed_value_axioms_for_datatype preconstr_us ofs kk) dtypes @
6.71 - sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
6.72 - datatype_sym_break kk rel_table nfas dtypes @
6.73 + maps (needed_value_axioms_for_datatype need_us ofs kk) dtypes @
6.74 + sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
6.75 + kk rel_table nfas dtypes @
6.76 maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
6.77 dtypes
6.78 end
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 03 10:55:41 2011 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 03 11:20:48 2011 +0100
7.3 @@ -862,7 +862,7 @@
7.4 fun reconstruct_hol_model {show_datatypes, show_consts}
7.5 ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
7.6 debug, whacks, binary_ints, destroy_constrs, specialize,
7.7 - star_linear_preds, total_consts, preconstrs, tac_timeout,
7.8 + star_linear_preds, total_consts, needs, tac_timeout,
7.9 evals, case_names, def_tables, nondef_table, user_nondefs,
7.10 simp_table, psimp_table, choice_spec_table, intro_table,
7.11 ground_thm_table, ersatz_table, skolems, special_funs,
7.12 @@ -880,7 +880,7 @@
7.13 whacks = whacks, binary_ints = binary_ints,
7.14 destroy_constrs = destroy_constrs, specialize = specialize,
7.15 star_linear_preds = star_linear_preds, total_consts = total_consts,
7.16 - preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals,
7.17 + needs = needs, tac_timeout = tac_timeout, evals = evals,
7.18 case_names = case_names, def_tables = def_tables,
7.19 nondef_table = nondef_table, user_nondefs = user_nondefs,
7.20 simp_table = simp_table, psimp_table = psimp_table,
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 03 10:55:41 2011 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 03 11:20:48 2011 +0100
8.3 @@ -1244,7 +1244,7 @@
8.4
8.5 fun preprocess_formulas
8.6 (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
8.7 - preconstrs, ...}) assm_ts neg_t =
8.8 + needs, ...}) assm_ts neg_t =
8.9 let
8.10 val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
8.11 neg_t |> unfold_defs_in_term hol_ctxt
8.12 @@ -1281,18 +1281,17 @@
8.13 #> close_form
8.14 #> Term.map_abs_vars shortest_name
8.15 val nondef_ts = nondef_ts |> map (do_middle false)
8.16 - val preconstr_ts =
8.17 - (* FIXME: Implement preconstruction inference. *)
8.18 - preconstrs
8.19 - |> map_filter (fn (SOME t, SOME true) =>
8.20 - SOME (t |> unfold_defs_in_term hol_ctxt
8.21 - |> do_middle false)
8.22 - | _ => NONE)
8.23 + val need_ts =
8.24 + (* FIXME: Implement inference. *)
8.25 + needs |> map_filter (fn (SOME t, SOME true) =>
8.26 + SOME (t |> unfold_defs_in_term hol_ctxt
8.27 + |> do_middle false)
8.28 + | _ => NONE)
8.29 val nondef_ts = nondef_ts |> map (do_tail false)
8.30 val def_ts = def_ts |> map (do_middle true #> do_tail true)
8.31 in
8.32 - (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
8.33 - no_poly_user_axioms, binarize)
8.34 + (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, no_poly_user_axioms,
8.35 + binarize)
8.36 end
8.37
8.38 end;