# HG changeset patch # User berghofe # Date 1299148570 -3600 # Node ID 01f3e2df796cfc38557d9a3b75e89117511d30fb # Parent 3f9adc372e0a3e2aac57e6ae0d9c40088f2f8b6a# Parent 7f9c48c17d2aa4f02f77160709099438ddb97eb0 merged diff -r 7f9c48c17d2a -r 01f3e2df796c NEWS --- a/NEWS Thu Mar 03 11:15:50 2011 +0100 +++ b/NEWS Thu Mar 03 11:36:10 2011 +0100 @@ -20,6 +20,7 @@ *** HOL *** * Nitpick: + - Added "need" and "total_consts" options. - Renamed attribute: nitpick_def ~> nitpick_unfold. INCOMPATIBILITY. diff -r 7f9c48c17d2a -r 01f3e2df796c doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Thu Mar 03 11:15:50 2011 +0100 +++ b/doc-src/Nitpick/nitpick.tex Thu Mar 03 11:36:10 2011 +0100 @@ -2465,17 +2465,13 @@ {\small See also \textit{debug} (\S\ref{output-format}).} -\opargboolorsmart{preconstr}{term}{dont\_preconstr} -Specifies whether a datatype value should be preconstructed, meaning Nitpick -will reserve a Kodkod atom for it. If a value must necessarily belong to the -subset of representable values that approximates a datatype, preconstructing -it can speed up the search significantly, especially for high cardinalities. By -default, Nitpick inspects the conjecture to infer terms that can be -preconstructed. - -\opsmart{preconstr}{dont\_preconstr} -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. +\opnodefault{need}{term\_list} +Specifies a list of datatype values (ground constructor terms) that should be +part of the subterm-closed subsets used to approximate datatypes. If you know +that a value must necessarily belong to the subset of representable values that +approximates a datatype, specifying it can speed up the search, especially for +high cardinalities. By default, Nitpick inspects the conjecture to infer needed +datatype values. \opsmart{total\_consts}{partial\_consts} Specifies whether constants occurring in the problem other than constructors can diff -r 7f9c48c17d2a -r 01f3e2df796c src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 03 11:15:50 2011 +0100 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 03 11:36:10 2011 +0100 @@ -39,7 +39,7 @@ stds = stds, wfs = [], user_axioms = NONE, debug = false, whacks = [], binary_ints = SOME false, destroy_constrs = true, specialize = false, star_linear_preds = false, total_consts = NONE, - preconstrs = [], tac_timeout = NONE, evals = [], case_names = case_names, + needs = NONE, tac_timeout = NONE, evals = [], case_names = case_names, def_tables = def_tables, nondef_table = nondef_table, user_nondefs = user_nondefs, simp_table = simp_table, psimp_table = psimp_table, choice_spec_table = choice_spec_table, diff -r 7f9c48c17d2a -r 01f3e2df796c src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 03 11:15:50 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 03 11:36:10 2011 +0100 @@ -35,7 +35,7 @@ specialize: bool, star_linear_preds: bool, total_consts: bool option, - preconstrs: (term option * bool option) list, + needs: term list option, peephole_optim: bool, datatype_sym_break: int, kodkod_sym_break: int, @@ -110,7 +110,7 @@ specialize: bool, star_linear_preds: bool, total_consts: bool option, - preconstrs: (term option * bool option) list, + needs: term list option, peephole_optim: bool, datatype_sym_break: int, kodkod_sym_break: int, @@ -199,7 +199,7 @@ fun check_constr_nut (Construct (_, _, _, us)) = List.app check_constr_nut us | check_constr_nut _ = - error "The \"preconstr\" option requires a constructor term." + error "The \"need\" option requires a constructor term." fun pick_them_nits_in_term deadline state (params : params) auto i n step subst assm_ts orig_t = @@ -217,7 +217,7 @@ 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, - total_consts, preconstrs, peephole_optim, datatype_sym_break, + total_consts, needs, 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 @@ -258,7 +258,7 @@ o Date.fromTimeLocal o Time.now) val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) else orig_t - val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs + val conj_ts = neg_t :: assm_ts @ evals @ these needs val tfree_table = if merge_type_vars then merged_type_var_table_for_terms thy conj_ts else [] @@ -266,8 +266,8 @@ val neg_t = neg_t |> merge_tfrees val assm_ts = assm_ts |> map merge_tfrees val evals = evals |> map merge_tfrees - val preconstrs = preconstrs |> map (apfst (Option.map merge_tfrees)) - val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs + val needs = needs |> Option.map (map merge_tfrees) + val conj_ts = neg_t :: assm_ts @ evals @ these needs val original_max_potential = max_potential val original_max_genuine = max_genuine val max_bisim_depth = fold Integer.max bisim_depths ~1 @@ -289,7 +289,7 @@ whacks = whacks, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, star_linear_preds = star_linear_preds, total_consts = total_consts, - preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals, + needs = needs, tac_timeout = tac_timeout, evals = evals, case_names = case_names, def_tables = def_tables, nondef_table = nondef_table, user_nondefs = user_nondefs, simp_table = simp_table, psimp_table = psimp_table, @@ -302,7 +302,7 @@ val real_frees = fold Term.add_frees conj_ts [] val _ = null (fold Term.add_tvars conj_ts []) orelse error "Nitpick cannot handle goals with schematic type variables." - val (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms, + val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize) = preprocess_formulas hol_ctxt assm_ts neg_t val got_all_user_axioms = @@ -332,8 +332,8 @@ val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq) val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq) - val preconstr_us = preconstr_ts |> map (nut_from_term hol_ctxt Eq) - val _ = List.app check_constr_nut preconstr_us + val need_us = need_ts |> map (nut_from_term hol_ctxt Eq) + val _ = List.app check_constr_nut need_us val (free_names, const_names) = fold add_free_and_const_names (nondef_us @ def_us) ([], []) val (sel_names, nonsel_names) = @@ -526,8 +526,8 @@ def_us |> map (choose_reps_in_nut scope unsound rep_table true) val nondef_us = nondef_us |> map (choose_reps_in_nut scope unsound rep_table false) - val preconstr_us = - preconstr_us |> map (choose_reps_in_nut scope unsound rep_table false) + val need_us = + need_us |> map (choose_reps_in_nut scope unsound rep_table false) (* val _ = List.app (print_g o string_for_nut ctxt) (free_names @ sel_names @ nonsel_names @ @@ -541,8 +541,7 @@ rename_free_vars nonsel_names pool rel_table val nondef_us = nondef_us |> map (rename_vars_in_nut pool rel_table) val def_us = def_us |> map (rename_vars_in_nut pool rel_table) - val preconstr_us = - preconstr_us |> map (rename_vars_in_nut pool rel_table) + val need_us = need_us |> map (rename_vars_in_nut pool rel_table) val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us val def_fs = map (kodkod_formula_from_nut ofs kk) def_us val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True @@ -568,7 +567,7 @@ val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels val dtype_axioms = - declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us + declarative_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break bits ofs kk rel_table datatypes val declarative_axioms = plain_axioms @ dtype_axioms val univ_card = Int.max (univ_card nat_card int_card main_j0 diff -r 7f9c48c17d2a -r 01f3e2df796c src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 03 11:15:50 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 03 11:36:10 2011 +0100 @@ -28,7 +28,7 @@ specialize: bool, star_linear_preds: bool, total_consts: bool option, - preconstrs: (term option * bool option) list, + needs: term list option, tac_timeout: Time.time option, evals: term list, case_names: (string * int) list, @@ -261,7 +261,7 @@ specialize: bool, star_linear_preds: bool, total_consts: bool option, - preconstrs: (term option * bool option) list, + needs: term list option, tac_timeout: Time.time option, evals: term list, case_names: (string * int) list, diff -r 7f9c48c17d2a -r 01f3e2df796c src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 03 11:15:50 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 03 11:36:10 2011 +0100 @@ -59,7 +59,6 @@ ("specialize", "true"), ("star_linear_preds", "true"), ("total_consts", "smart"), - ("preconstr", "smart"), ("peephole_optim", "true"), ("datatype_sym_break", "5"), ("kodkod_sym_break", "15"), @@ -93,7 +92,6 @@ ("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"), ("quiet", "verbose"), @@ -106,11 +104,12 @@ fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) negated_params s orelse - member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse + member (op =) ["max", "show_all", "whack", "eval", "need", "atoms", + "expect"] s orelse exists (fn p => String.isPrefix (p ^ " ") s) ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize", - "mono", "non_mono", "std", "non_std", "wf", "non_wf", "preconstr", - "dont_preconstr", "format", "atoms"] + "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format", + "atoms"] fun check_raw_param (s, _) = if is_known_raw_param s then () @@ -226,8 +225,8 @@ #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type val read_term_polymorphic = Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt) - val lookup_term_list_polymorphic = - AList.lookup (op =) raw_params #> these #> map read_term_polymorphic + val lookup_term_list_option_polymorphic = + AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic) val read_const_polymorphic = read_term_polymorphic #> dest_Const val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1 |> auto ? map (apsnd (take max_auto_scopes)) @@ -249,15 +248,14 @@ val overlord = lookup_bool "overlord" val user_axioms = lookup_bool_option "user_axioms" val assms = lookup_bool "assms" - val whacks = lookup_term_list_polymorphic "whack" + val whacks = lookup_term_list_option_polymorphic "whack" |> these val merge_type_vars = lookup_bool "merge_type_vars" val binary_ints = lookup_bool_option "binary_ints" 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 needs = lookup_term_list_option_polymorphic "need" val peephole_optim = lookup_bool "peephole_optim" val datatype_sym_break = lookup_int "datatype_sym_break" val kodkod_sym_break = lookup_int "kodkod_sym_break" @@ -266,7 +264,7 @@ val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads") val show_datatypes = debug orelse lookup_bool "show_datatypes" val show_consts = debug orelse lookup_bool "show_consts" - val evals = lookup_term_list_polymorphic "eval" + val evals = lookup_term_list_option_polymorphic "eval" |> these val formats = lookup_ints_assigns read_term_polymorphic "format" 0 val atomss = lookup_strings_assigns read_type_polymorphic "atoms" val max_potential = @@ -289,7 +287,7 @@ merge_type_vars = merge_type_vars, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, star_linear_preds = star_linear_preds, total_consts = total_consts, - preconstrs = preconstrs, peephole_optim = peephole_optim, + needs = needs, 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, diff -r 7f9c48c17d2a -r 01f3e2df796c src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 03 11:15:50 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 03 11:36:10 2011 +0100 @@ -1478,8 +1478,8 @@ "malformed Kodkod formula") end -fun preconstructed_value_axioms_for_datatype [] _ _ _ = [] - | preconstructed_value_axioms_for_datatype preconstr_us ofs kk +fun needed_value_axioms_for_datatype [] _ _ _ = [] + | needed_value_axioms_for_datatype need_us ofs kk ({typ, card, constrs, ...} : datatype_spec) = let fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) = @@ -1507,10 +1507,9 @@ else accum) | aux u = - raise NUT ("Nitpick_Kodkod.preconstructed_value_axioms_for_datatype\ - \.aux", [u]) + raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u]) in - case SOME (index_seq 0 card, []) |> fold aux preconstr_us of + case SOME (index_seq 0 card, []) |> fold aux need_us of SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk) | NONE => [KK.False] end @@ -1654,14 +1653,14 @@ nfas dtypes) end -fun is_datatype_in_preconstructed_value T (Construct (_, T', _, us)) = - T = T' orelse exists (is_datatype_in_preconstructed_value T) us - | is_datatype_in_preconstructed_value _ _ = false +fun is_datatype_in_needed_value T (Construct (_, T', _, us)) = + T = T' orelse exists (is_datatype_in_needed_value T) us + | is_datatype_in_needed_value _ _ = false val min_sym_break_card = 7 -fun sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us - datatype_sym_break kk rel_table nfas dtypes = +fun sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break + kk rel_table nfas dtypes = if datatype_sym_break = 0 then [] else @@ -1673,8 +1672,7 @@ o binder_types o snd o #const) constrs) |> filter_out (fn {typ, ...} => - exists (is_datatype_in_preconstructed_value typ) - preconstr_us) + exists (is_datatype_in_needed_value typ) need_us) |> (fn dtypes' => dtypes' |> length dtypes' > datatype_sym_break ? (sort (datatype_ord o swap) @@ -1779,7 +1777,7 @@ partition_axioms_for_datatype j0 kk rel_table dtype end -fun declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us +fun declarative_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break bits ofs kk rel_table dtypes = let val nfas = @@ -1788,9 +1786,9 @@ |> strongly_connected_sub_nfas in acyclicity_axioms_for_datatypes kk nfas @ - maps (preconstructed_value_axioms_for_datatype preconstr_us ofs kk) dtypes @ - sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us - datatype_sym_break kk rel_table nfas dtypes @ + maps (needed_value_axioms_for_datatype need_us ofs kk) dtypes @ + sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break + kk rel_table nfas dtypes @ maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table) dtypes end diff -r 7f9c48c17d2a -r 01f3e2df796c src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 03 11:15:50 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 03 11:36:10 2011 +0100 @@ -862,7 +862,7 @@ fun reconstruct_hol_model {show_datatypes, show_consts} ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms, debug, whacks, binary_ints, destroy_constrs, specialize, - star_linear_preds, total_consts, preconstrs, tac_timeout, + star_linear_preds, total_consts, needs, tac_timeout, evals, case_names, def_tables, nondef_table, user_nondefs, simp_table, psimp_table, choice_spec_table, intro_table, ground_thm_table, ersatz_table, skolems, special_funs, @@ -880,7 +880,7 @@ whacks = whacks, binary_ints = binary_ints, destroy_constrs = destroy_constrs, specialize = specialize, star_linear_preds = star_linear_preds, total_consts = total_consts, - preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals, + needs = needs, tac_timeout = tac_timeout, evals = evals, case_names = case_names, def_tables = def_tables, nondef_table = nondef_table, user_nondefs = user_nondefs, simp_table = simp_table, psimp_table = psimp_table, diff -r 7f9c48c17d2a -r 01f3e2df796c src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 03 11:15:50 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 03 11:36:10 2011 +0100 @@ -1244,7 +1244,7 @@ fun preprocess_formulas (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes, - preconstrs, ...}) assm_ts neg_t = + needs, ...}) assm_ts neg_t = let val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) = neg_t |> unfold_defs_in_term hol_ctxt @@ -1281,18 +1281,16 @@ #> close_form #> Term.map_abs_vars shortest_name val nondef_ts = nondef_ts |> map (do_middle false) - val preconstr_ts = - (* FIXME: Implement preconstruction inference. *) - preconstrs - |> map_filter (fn (SOME t, SOME true) => - SOME (t |> unfold_defs_in_term hol_ctxt - |> do_middle false) - | _ => NONE) + val need_ts = + case needs of + SOME needs => + needs |> map (unfold_defs_in_term hol_ctxt #> do_middle false) + | NONE => [] (* FIXME: Implement inference. *) val nondef_ts = nondef_ts |> map (do_tail false) val def_ts = def_ts |> map (do_middle true #> do_tail true) in - (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms, - no_poly_user_axioms, binarize) + (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, no_poly_user_axioms, + binarize) end end;