# HG changeset patch
# User blanchet
# Date 1272124101 -7200
# Node ID 30f7ce76712da877b078f207a22a9c8e7981a4d2
# Parent  9ed32d1af63bdc970cb59193f6a2e915ba6e45d8
removed Nitpick's "uncurry" option

diff -r 9ed32d1af63b -r 30f7ce76712d doc-src/Nitpick/nitpick.tex
--- 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
diff -r 9ed32d1af63b -r 30f7ce76712d src/HOL/Tools/Nitpick/HISTORY
--- 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
 
diff -r 9ed32d1af63b -r 30f7ce76712d src/HOL/Tools/Nitpick/nitpick.ML
--- 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 []
diff -r 9ed32d1af63b -r 30f7ce76712d src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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,
diff -r 9ed32d1af63b -r 30f7ce76712d src/HOL/Tools/Nitpick/nitpick_isar.ML
--- 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,
diff -r 9ed32d1af63b -r 30f7ce76712d src/HOL/Tools/Nitpick/nitpick_model.ML
--- 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 =
diff -r 9ed32d1af63b -r 30f7ce76712d src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- 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