# HG changeset patch
# User blanchet
# Date 1299147648 -3600
# Node ID 03f6995569558530377cc3690709819a57f8bcb6
# Parent  e3cd0dce9b1a251fc3322f746b5a7837ea5e7b09
simplify "need" option's syntax

diff -r e3cd0dce9b1a -r 03f699556955 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Thu Mar 03 11:20:48 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Thu Mar 03 11:20:48 2011 +0100
@@ -2465,17 +2465,13 @@
 
 {\small See also \textit{debug} (\S\ref{output-format}).}
 
-\opargboolorsmart{need}{term}{dont\_need}
-Specifies whether a datatype value is required by the problem, 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, specifying it can
-speed up the search significantly, especially for high cardinalities. By
-default, Nitpick inspects the conjecture to infer needed datatype values.
-
-\opsmart{need}{dont\_need}
-Specifies the default needed datatype value 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 e3cd0dce9b1a -r 03f699556955 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Mar 03 11:20:48 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,
-   needs = [], 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 e3cd0dce9b1a -r 03f699556955 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 03 11:20:48 2011 +0100
@@ -35,7 +35,7 @@
      specialize: bool,
      star_linear_preds: bool,
      total_consts: bool option,
-     needs: (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,
-   needs: (term option * bool option) list,
+   needs: term list option,
    peephole_optim: bool,
    datatype_sym_break: int,
    kodkod_sym_break: int,
@@ -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 needs
+    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 needs = needs |> map (apfst (Option.map merge_tfrees))
-    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
+    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
diff -r e3cd0dce9b1a -r 03f699556955 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 03 11:20:48 2011 +0100
@@ -28,7 +28,7 @@
      specialize: bool,
      star_linear_preds: bool,
      total_consts: bool option,
-     needs: (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,
-   needs: (term option * bool option) list,
+   needs: term list option,
    tac_timeout: Time.time option,
    evals: term list,
    case_names: (string * int) list,
diff -r e3cd0dce9b1a -r 03f699556955 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Mar 03 11:20:48 2011 +0100
@@ -59,7 +59,6 @@
    ("specialize", "true"),
    ("star_linear_preds", "true"),
    ("total_consts", "smart"),
-   ("need", "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_need", "need"),
    ("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", "need",
-          "dont_need", "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,14 +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 needs = lookup_bool_option_assigns read_term_polymorphic "need"
+    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"
@@ -265,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 =
diff -r e3cd0dce9b1a -r 03f699556955 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Mar 03 11:20:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Mar 03 11:20:48 2011 +0100
@@ -1282,11 +1282,10 @@
       #> Term.map_abs_vars shortest_name
     val nondef_ts = nondef_ts |> map (do_middle false)
     val need_ts =
-      (* FIXME: Implement inference. *)
-      needs |> map_filter (fn (SOME t, SOME true) =>
-                              SOME (t |> unfold_defs_in_term hol_ctxt
-                                      |> do_middle false)
-                            | _ => NONE)
+      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