--- a/doc-src/Nitpick/nitpick.tex Sat Apr 24 16:44:45 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Sat Apr 24 17:48:21 2010 +0200
@@ -2258,9 +2258,6 @@
arguments that are not accounted for are left alone, as if the specification had
been $1,\ldots,1,n_1,\ldots,n_k$.
-\nopagebreak
-{\small See also \textit{uncurry} (\S\ref{optimizations}).}
-
\opdefault{format}{int\_seq}{$\mathbf{1}$}
Specifies the default format to use. Irrespective of the default format, the
extra arguments to a Skolem constant corresponding to the outer bound variables
@@ -2474,15 +2471,6 @@
{\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
(\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
-\optrue{uncurry}{dont\_uncurry}
-Specifies whether Nitpick should uncurry functions. Uncurrying has on its own no
-tangible effect on efficiency, but it creates opportunities for the boxing
-optimization.
-
-\nopagebreak
-{\small See also \textit{box} (\S\ref{scope-of-search}), \textit{debug}
-(\S\ref{output-format}), and \textit{format} (\S\ref{output-format}).}
-
\optrue{fast\_descrs}{full\_descrs}
Specifies whether Nitpick should optimize the definite and indefinite
description operators (THE and SOME). The optimized versions usually help
--- a/src/HOL/Tools/Nitpick/HISTORY Sat Apr 24 16:44:45 2010 +0200
+++ b/src/HOL/Tools/Nitpick/HISTORY Sat Apr 24 17:48:21 2010 +0200
@@ -17,6 +17,7 @@
* Added cache to speed up repeated Kodkod invocations on the same problems
* Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
"MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
+ * Removed "sym_break", "flatten_prop", "sharing_depth", and "uncurry" options
Version 2009-1
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 16:44:45 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 17:48:21 2010 +0200
@@ -34,7 +34,6 @@
specialize: bool,
skolemize: bool,
star_linear_preds: bool,
- uncurry: bool,
fast_descrs: bool,
peephole_optim: bool,
timeout: Time.time option,
@@ -107,7 +106,6 @@
specialize: bool,
skolemize: bool,
star_linear_preds: bool,
- uncurry: bool,
fast_descrs: bool,
peephole_optim: bool,
timeout: Time.time option,
@@ -194,10 +192,10 @@
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
- destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
- fast_descrs, peephole_optim, tac_timeout, max_threads, show_skolems,
- show_datatypes, show_consts, evals, formats, max_potential,
- max_genuine, check_potential, check_genuine, batch_size, ...} =
+ destroy_constrs, specialize, skolemize, star_linear_preds, fast_descrs,
+ peephole_optim, tac_timeout, max_threads, show_skolems, show_datatypes,
+ show_consts, evals, formats, max_potential, max_genuine,
+ check_potential, check_genuine, batch_size, ...} =
params
val state_ref = Unsynchronized.ref state
val pprint =
@@ -265,14 +263,14 @@
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
binary_ints = binary_ints, destroy_constrs = destroy_constrs,
specialize = specialize, skolemize = skolemize,
- star_linear_preds = star_linear_preds, uncurry = uncurry,
- fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
- case_names = case_names, def_table = def_table,
- nondef_table = nondef_table, user_nondefs = user_nondefs,
- simp_table = simp_table, psimp_table = psimp_table,
- choice_spec_table = choice_spec_table, intro_table = intro_table,
- ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
- skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
+ star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
+ tac_timeout = tac_timeout, evals = evals, case_names = case_names,
+ def_table = def_table, nondef_table = nondef_table,
+ user_nondefs = user_nondefs, simp_table = simp_table,
+ psimp_table = psimp_table, choice_spec_table = choice_spec_table,
+ intro_table = intro_table, ground_thm_table = ground_thm_table,
+ ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
+ special_funs = Unsynchronized.ref [],
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []}
val frees = Term.add_frees assms_t []
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Apr 24 16:44:45 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Apr 24 17:48:21 2010 +0200
@@ -27,7 +27,6 @@
specialize: bool,
skolemize: bool,
star_linear_preds: bool,
- uncurry: bool,
fast_descrs: bool,
tac_timeout: Time.time option,
evals: term list,
@@ -238,7 +237,6 @@
specialize: bool,
skolemize: bool,
star_linear_preds: bool,
- uncurry: bool,
fast_descrs: bool,
tac_timeout: Time.time option,
evals: term list,
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 24 16:44:45 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 24 17:48:21 2010 +0200
@@ -57,7 +57,6 @@
("specialize", "true"),
("skolemize", "true"),
("star_linear_preds", "true"),
- ("uncurry", "true"),
("fast_descrs", "true"),
("peephole_optim", "true"),
("timeout", "30 s"),
@@ -92,7 +91,6 @@
("dont_specialize", "specialize"),
("dont_skolemize", "skolemize"),
("dont_star_linear_preds", "star_linear_preds"),
- ("dont_uncurry", "uncurry"),
("full_descrs", "fast_descrs"),
("no_peephole_optim", "peephole_optim"),
("no_debug", "debug"),
@@ -254,7 +252,6 @@
val specialize = lookup_bool "specialize"
val skolemize = lookup_bool "skolemize"
val star_linear_preds = lookup_bool "star_linear_preds"
- val uncurry = lookup_bool "uncurry"
val fast_descrs = lookup_bool "fast_descrs"
val peephole_optim = lookup_bool "peephole_optim"
val timeout = if auto then NONE else lookup_time "timeout"
@@ -285,9 +282,8 @@
merge_type_vars = merge_type_vars, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
skolemize = skolemize, star_linear_preds = star_linear_preds,
- uncurry = uncurry, fast_descrs = fast_descrs,
- peephole_optim = peephole_optim, timeout = timeout,
- tac_timeout = tac_timeout, max_threads = max_threads,
+ fast_descrs = fast_descrs, peephole_optim = peephole_optim,
+ timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads,
show_skolems = show_skolems, show_datatypes = show_datatypes,
show_consts = show_consts, formats = formats, evals = evals,
max_potential = max_potential, max_genuine = max_genuine,
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 16:44:45 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 17:48:21 2010 +0200
@@ -843,11 +843,11 @@
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
debug, binary_ints, destroy_constrs, specialize,
- skolemize, star_linear_preds, uncurry, fast_descrs,
- tac_timeout, evals, case_names, def_table, nondef_table,
- user_nondefs, simp_table, psimp_table, choice_spec_table,
- intro_table, ground_thm_table, ersatz_table, skolems,
- special_funs, unrolled_preds, wf_cache, constr_cache},
+ skolemize, star_linear_preds, fast_descrs, tac_timeout,
+ evals, case_names, def_table, nondef_table, user_nondefs,
+ simp_table, psimp_table, choice_spec_table, intro_table,
+ ground_thm_table, ersatz_table, skolems, special_funs,
+ unrolled_preds, wf_cache, constr_cache},
binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
formats all_frees free_names sel_names nonsel_names rel_table bounds =
let
@@ -859,19 +859,18 @@
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
binary_ints = binary_ints, destroy_constrs = destroy_constrs,
specialize = specialize, skolemize = skolemize,
- star_linear_preds = star_linear_preds, uncurry = uncurry,
- fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
- case_names = case_names, def_table = def_table,
- nondef_table = nondef_table, user_nondefs = user_nondefs,
- simp_table = simp_table, psimp_table = psimp_table,
- choice_spec_table = choice_spec_table, intro_table = intro_table,
- ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
- skolems = skolems, special_funs = special_funs,
- unrolled_preds = unrolled_preds, wf_cache = wf_cache,
- constr_cache = constr_cache}
- val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
- card_assigns = card_assigns, bits = bits,
- bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
+ star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
+ tac_timeout = tac_timeout, evals = evals, case_names = case_names,
+ def_table = def_table, nondef_table = nondef_table,
+ user_nondefs = user_nondefs, simp_table = simp_table,
+ psimp_table = psimp_table, choice_spec_table = choice_spec_table,
+ intro_table = intro_table, ground_thm_table = ground_thm_table,
+ ersatz_table = ersatz_table, skolems = skolems,
+ special_funs = special_funs, unrolled_preds = unrolled_preds,
+ wf_cache = wf_cache, constr_cache = constr_cache}
+ val scope =
+ {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
+ bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
fun term_for_rep unfold =
reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
fun nth_value_of_type card T n =
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 24 16:44:45 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 24 17:48:21 2010 +0200
@@ -1227,8 +1227,7 @@
(** Preprocessor entry point **)
fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
- boxes, skolemize, uncurry, ...})
- finitizes monos t =
+ boxes, skolemize, ...}) finitizes monos t =
let
val skolem_depth = if skolemize then 4 else ~1
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
@@ -1246,13 +1245,12 @@
(binary_ints = SOME true orelse
exists should_use_binary_ints (nondef_ts @ def_ts))
val box = exists (not_equal (SOME false) o snd) boxes
- val uncurry = uncurry andalso box
val table =
Termtab.empty
- |> uncurry ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
+ |> box ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
fun do_rest def =
binarize ? binarize_nat_and_int_in_term
- #> uncurry ? uncurry_term table
+ #> box ? uncurry_term table
#> box ? box_fun_and_pair_in_term hol_ctxt def
#> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
#> pull_out_existential_constrs hol_ctxt