1.1 --- a/doc-src/Nitpick/nitpick.tex Sat Apr 24 16:44:45 2010 +0200
1.2 +++ b/doc-src/Nitpick/nitpick.tex Sat Apr 24 17:48:21 2010 +0200
1.3 @@ -2258,9 +2258,6 @@
1.4 arguments that are not accounted for are left alone, as if the specification had
1.5 been $1,\ldots,1,n_1,\ldots,n_k$.
1.6
1.7 -\nopagebreak
1.8 -{\small See also \textit{uncurry} (\S\ref{optimizations}).}
1.9 -
1.10 \opdefault{format}{int\_seq}{$\mathbf{1}$}
1.11 Specifies the default format to use. Irrespective of the default format, the
1.12 extra arguments to a Skolem constant corresponding to the outer bound variables
1.13 @@ -2474,15 +2471,6 @@
1.14 {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
1.15 (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
1.16
1.17 -\optrue{uncurry}{dont\_uncurry}
1.18 -Specifies whether Nitpick should uncurry functions. Uncurrying has on its own no
1.19 -tangible effect on efficiency, but it creates opportunities for the boxing
1.20 -optimization.
1.21 -
1.22 -\nopagebreak
1.23 -{\small See also \textit{box} (\S\ref{scope-of-search}), \textit{debug}
1.24 -(\S\ref{output-format}), and \textit{format} (\S\ref{output-format}).}
1.25 -
1.26 \optrue{fast\_descrs}{full\_descrs}
1.27 Specifies whether Nitpick should optimize the definite and indefinite
1.28 description operators (THE and SOME). The optimized versions usually help
2.1 --- a/src/HOL/Tools/Nitpick/HISTORY Sat Apr 24 16:44:45 2010 +0200
2.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Sat Apr 24 17:48:21 2010 +0200
2.3 @@ -17,6 +17,7 @@
2.4 * Added cache to speed up repeated Kodkod invocations on the same problems
2.5 * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
2.6 "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
2.7 + * Removed "sym_break", "flatten_prop", "sharing_depth", and "uncurry" options
2.8
2.9 Version 2009-1
2.10
3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 16:44:45 2010 +0200
3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 17:48:21 2010 +0200
3.3 @@ -34,7 +34,6 @@
3.4 specialize: bool,
3.5 skolemize: bool,
3.6 star_linear_preds: bool,
3.7 - uncurry: bool,
3.8 fast_descrs: bool,
3.9 peephole_optim: bool,
3.10 timeout: Time.time option,
3.11 @@ -107,7 +106,6 @@
3.12 specialize: bool,
3.13 skolemize: bool,
3.14 star_linear_preds: bool,
3.15 - uncurry: bool,
3.16 fast_descrs: bool,
3.17 peephole_optim: bool,
3.18 timeout: Time.time option,
3.19 @@ -194,10 +192,10 @@
3.20 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
3.21 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
3.22 verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
3.23 - destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
3.24 - fast_descrs, peephole_optim, tac_timeout, max_threads, show_skolems,
3.25 - show_datatypes, show_consts, evals, formats, max_potential,
3.26 - max_genuine, check_potential, check_genuine, batch_size, ...} =
3.27 + destroy_constrs, specialize, skolemize, star_linear_preds, fast_descrs,
3.28 + peephole_optim, tac_timeout, max_threads, show_skolems, show_datatypes,
3.29 + show_consts, evals, formats, max_potential, max_genuine,
3.30 + check_potential, check_genuine, batch_size, ...} =
3.31 params
3.32 val state_ref = Unsynchronized.ref state
3.33 val pprint =
3.34 @@ -265,14 +263,14 @@
3.35 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
3.36 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
3.37 specialize = specialize, skolemize = skolemize,
3.38 - star_linear_preds = star_linear_preds, uncurry = uncurry,
3.39 - fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
3.40 - case_names = case_names, def_table = def_table,
3.41 - nondef_table = nondef_table, user_nondefs = user_nondefs,
3.42 - simp_table = simp_table, psimp_table = psimp_table,
3.43 - choice_spec_table = choice_spec_table, intro_table = intro_table,
3.44 - ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
3.45 - skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
3.46 + star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
3.47 + tac_timeout = tac_timeout, evals = evals, case_names = case_names,
3.48 + def_table = def_table, nondef_table = nondef_table,
3.49 + user_nondefs = user_nondefs, simp_table = simp_table,
3.50 + psimp_table = psimp_table, choice_spec_table = choice_spec_table,
3.51 + intro_table = intro_table, ground_thm_table = ground_thm_table,
3.52 + ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
3.53 + special_funs = Unsynchronized.ref [],
3.54 unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
3.55 constr_cache = Unsynchronized.ref []}
3.56 val frees = Term.add_frees assms_t []
4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Apr 24 16:44:45 2010 +0200
4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Apr 24 17:48:21 2010 +0200
4.3 @@ -27,7 +27,6 @@
4.4 specialize: bool,
4.5 skolemize: bool,
4.6 star_linear_preds: bool,
4.7 - uncurry: bool,
4.8 fast_descrs: bool,
4.9 tac_timeout: Time.time option,
4.10 evals: term list,
4.11 @@ -238,7 +237,6 @@
4.12 specialize: bool,
4.13 skolemize: bool,
4.14 star_linear_preds: bool,
4.15 - uncurry: bool,
4.16 fast_descrs: bool,
4.17 tac_timeout: Time.time option,
4.18 evals: term list,
5.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 24 16:44:45 2010 +0200
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 24 17:48:21 2010 +0200
5.3 @@ -57,7 +57,6 @@
5.4 ("specialize", "true"),
5.5 ("skolemize", "true"),
5.6 ("star_linear_preds", "true"),
5.7 - ("uncurry", "true"),
5.8 ("fast_descrs", "true"),
5.9 ("peephole_optim", "true"),
5.10 ("timeout", "30 s"),
5.11 @@ -92,7 +91,6 @@
5.12 ("dont_specialize", "specialize"),
5.13 ("dont_skolemize", "skolemize"),
5.14 ("dont_star_linear_preds", "star_linear_preds"),
5.15 - ("dont_uncurry", "uncurry"),
5.16 ("full_descrs", "fast_descrs"),
5.17 ("no_peephole_optim", "peephole_optim"),
5.18 ("no_debug", "debug"),
5.19 @@ -254,7 +252,6 @@
5.20 val specialize = lookup_bool "specialize"
5.21 val skolemize = lookup_bool "skolemize"
5.22 val star_linear_preds = lookup_bool "star_linear_preds"
5.23 - val uncurry = lookup_bool "uncurry"
5.24 val fast_descrs = lookup_bool "fast_descrs"
5.25 val peephole_optim = lookup_bool "peephole_optim"
5.26 val timeout = if auto then NONE else lookup_time "timeout"
5.27 @@ -285,9 +282,8 @@
5.28 merge_type_vars = merge_type_vars, binary_ints = binary_ints,
5.29 destroy_constrs = destroy_constrs, specialize = specialize,
5.30 skolemize = skolemize, star_linear_preds = star_linear_preds,
5.31 - uncurry = uncurry, fast_descrs = fast_descrs,
5.32 - peephole_optim = peephole_optim, timeout = timeout,
5.33 - tac_timeout = tac_timeout, max_threads = max_threads,
5.34 + fast_descrs = fast_descrs, peephole_optim = peephole_optim,
5.35 + timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads,
5.36 show_skolems = show_skolems, show_datatypes = show_datatypes,
5.37 show_consts = show_consts, formats = formats, evals = evals,
5.38 max_potential = max_potential, max_genuine = max_genuine,
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 16:44:45 2010 +0200
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 17:48:21 2010 +0200
6.3 @@ -843,11 +843,11 @@
6.4 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
6.5 ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
6.6 debug, binary_ints, destroy_constrs, specialize,
6.7 - skolemize, star_linear_preds, uncurry, fast_descrs,
6.8 - tac_timeout, evals, case_names, def_table, nondef_table,
6.9 - user_nondefs, simp_table, psimp_table, choice_spec_table,
6.10 - intro_table, ground_thm_table, ersatz_table, skolems,
6.11 - special_funs, unrolled_preds, wf_cache, constr_cache},
6.12 + skolemize, star_linear_preds, fast_descrs, tac_timeout,
6.13 + evals, case_names, def_table, nondef_table, user_nondefs,
6.14 + simp_table, psimp_table, choice_spec_table, intro_table,
6.15 + ground_thm_table, ersatz_table, skolems, special_funs,
6.16 + unrolled_preds, wf_cache, constr_cache},
6.17 binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
6.18 formats all_frees free_names sel_names nonsel_names rel_table bounds =
6.19 let
6.20 @@ -859,19 +859,18 @@
6.21 stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
6.22 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
6.23 specialize = specialize, skolemize = skolemize,
6.24 - star_linear_preds = star_linear_preds, uncurry = uncurry,
6.25 - fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
6.26 - case_names = case_names, def_table = def_table,
6.27 - nondef_table = nondef_table, user_nondefs = user_nondefs,
6.28 - simp_table = simp_table, psimp_table = psimp_table,
6.29 - choice_spec_table = choice_spec_table, intro_table = intro_table,
6.30 - ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
6.31 - skolems = skolems, special_funs = special_funs,
6.32 - unrolled_preds = unrolled_preds, wf_cache = wf_cache,
6.33 - constr_cache = constr_cache}
6.34 - val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
6.35 - card_assigns = card_assigns, bits = bits,
6.36 - bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
6.37 + star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
6.38 + tac_timeout = tac_timeout, evals = evals, case_names = case_names,
6.39 + def_table = def_table, nondef_table = nondef_table,
6.40 + user_nondefs = user_nondefs, simp_table = simp_table,
6.41 + psimp_table = psimp_table, choice_spec_table = choice_spec_table,
6.42 + intro_table = intro_table, ground_thm_table = ground_thm_table,
6.43 + ersatz_table = ersatz_table, skolems = skolems,
6.44 + special_funs = special_funs, unrolled_preds = unrolled_preds,
6.45 + wf_cache = wf_cache, constr_cache = constr_cache}
6.46 + val scope =
6.47 + {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
6.48 + bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
6.49 fun term_for_rep unfold =
6.50 reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
6.51 fun nth_value_of_type card T n =
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 24 16:44:45 2010 +0200
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 24 17:48:21 2010 +0200
7.3 @@ -1227,8 +1227,7 @@
7.4 (** Preprocessor entry point **)
7.5
7.6 fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
7.7 - boxes, skolemize, uncurry, ...})
7.8 - finitizes monos t =
7.9 + boxes, skolemize, ...}) finitizes monos t =
7.10 let
7.11 val skolem_depth = if skolemize then 4 else ~1
7.12 val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
7.13 @@ -1246,13 +1245,12 @@
7.14 (binary_ints = SOME true orelse
7.15 exists should_use_binary_ints (nondef_ts @ def_ts))
7.16 val box = exists (not_equal (SOME false) o snd) boxes
7.17 - val uncurry = uncurry andalso box
7.18 val table =
7.19 Termtab.empty
7.20 - |> uncurry ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
7.21 + |> box ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
7.22 fun do_rest def =
7.23 binarize ? binarize_nat_and_int_in_term
7.24 - #> uncurry ? uncurry_term table
7.25 + #> box ? uncurry_term table
7.26 #> box ? box_fun_and_pair_in_term hol_ctxt def
7.27 #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
7.28 #> pull_out_existential_constrs hol_ctxt