simplify "need" option's syntax
authorblanchet
Thu Mar 03 11:20:48 2011 +0100 (2011-03-03 ago)
changeset 4187603f699556955
parent 41875 e3cd0dce9b1a
child 41877 3f9adc372e0a
simplify "need" option's syntax
doc-src/Nitpick/nitpick.tex
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Mar 03 11:20:48 2011 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Mar 03 11:20:48 2011 +0100
     1.3 @@ -2465,17 +2465,13 @@
     1.4  
     1.5  {\small See also \textit{debug} (\S\ref{output-format}).}
     1.6  
     1.7 -\opargboolorsmart{need}{term}{dont\_need}
     1.8 -Specifies whether a datatype value is required by the problem, meaning Nitpick
     1.9 -will reserve a Kodkod atom for it. If a value must necessarily belong to the
    1.10 -subset of representable values that approximates a datatype, specifying it can
    1.11 -speed up the search significantly, especially for high cardinalities. By
    1.12 -default, Nitpick inspects the conjecture to infer needed datatype values.
    1.13 -
    1.14 -\opsmart{need}{dont\_need}
    1.15 -Specifies the default needed datatype value setting to use. This can be
    1.16 -overridden on a per-term basis using the \textit{preconstr}~\qty{term} option
    1.17 -described above.
    1.18 +\opnodefault{need}{term\_list}
    1.19 +Specifies a list of datatype values (ground constructor terms) that should be
    1.20 +part of the subterm-closed subsets used to approximate datatypes. If you know
    1.21 +that a value must necessarily belong to the subset of representable values that
    1.22 +approximates a datatype, specifying it can speed up the search, especially for
    1.23 +high cardinalities. By default, Nitpick inspects the conjecture to infer needed
    1.24 +datatype values.
    1.25  
    1.26  \opsmart{total\_consts}{partial\_consts}
    1.27  Specifies whether constants occurring in the problem other than constructors can
     2.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Mar 03 11:20:48 2011 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Mar 03 11:20:48 2011 +0100
     2.3 @@ -39,7 +39,7 @@
     2.4     stds = stds, wfs = [], user_axioms = NONE, debug = false,
     2.5     whacks = [], binary_ints = SOME false, destroy_constrs = true,
     2.6     specialize = false, star_linear_preds = false, total_consts = NONE,
     2.7 -   needs = [], tac_timeout = NONE, evals = [], case_names = case_names,
     2.8 +   needs = NONE, tac_timeout = NONE, evals = [], case_names = case_names,
     2.9     def_tables = def_tables, nondef_table = nondef_table,
    2.10     user_nondefs = user_nondefs, simp_table = simp_table,
    2.11     psimp_table = psimp_table, choice_spec_table = choice_spec_table,
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 03 11:20:48 2011 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 03 11:20:48 2011 +0100
     3.3 @@ -35,7 +35,7 @@
     3.4       specialize: bool,
     3.5       star_linear_preds: bool,
     3.6       total_consts: bool option,
     3.7 -     needs: (term option * bool option) list,
     3.8 +     needs: term list option,
     3.9       peephole_optim: bool,
    3.10       datatype_sym_break: int,
    3.11       kodkod_sym_break: int,
    3.12 @@ -110,7 +110,7 @@
    3.13     specialize: bool,
    3.14     star_linear_preds: bool,
    3.15     total_consts: bool option,
    3.16 -   needs: (term option * bool option) list,
    3.17 +   needs: term list option,
    3.18     peephole_optim: bool,
    3.19     datatype_sym_break: int,
    3.20     kodkod_sym_break: int,
    3.21 @@ -258,7 +258,7 @@
    3.22                       o Date.fromTimeLocal o Time.now)
    3.23      val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
    3.24                  else orig_t
    3.25 -    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
    3.26 +    val conj_ts = neg_t :: assm_ts @ evals @ these needs
    3.27      val tfree_table =
    3.28        if merge_type_vars then merged_type_var_table_for_terms thy conj_ts
    3.29        else []
    3.30 @@ -266,8 +266,8 @@
    3.31      val neg_t = neg_t |> merge_tfrees
    3.32      val assm_ts = assm_ts |> map merge_tfrees
    3.33      val evals = evals |> map merge_tfrees
    3.34 -    val needs = needs |> map (apfst (Option.map merge_tfrees))
    3.35 -    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
    3.36 +    val needs = needs |> Option.map (map merge_tfrees)
    3.37 +    val conj_ts = neg_t :: assm_ts @ evals @ these needs
    3.38      val original_max_potential = max_potential
    3.39      val original_max_genuine = max_genuine
    3.40      val max_bisim_depth = fold Integer.max bisim_depths ~1
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 03 11:20:48 2011 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 03 11:20:48 2011 +0100
     4.3 @@ -28,7 +28,7 @@
     4.4       specialize: bool,
     4.5       star_linear_preds: bool,
     4.6       total_consts: bool option,
     4.7 -     needs: (term option * bool option) list,
     4.8 +     needs: term list option,
     4.9       tac_timeout: Time.time option,
    4.10       evals: term list,
    4.11       case_names: (string * int) list,
    4.12 @@ -261,7 +261,7 @@
    4.13     specialize: bool,
    4.14     star_linear_preds: bool,
    4.15     total_consts: bool option,
    4.16 -   needs: (term option * bool option) list,
    4.17 +   needs: term list option,
    4.18     tac_timeout: Time.time option,
    4.19     evals: term list,
    4.20     case_names: (string * int) list,
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Mar 03 11:20:48 2011 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Mar 03 11:20:48 2011 +0100
     5.3 @@ -59,7 +59,6 @@
     5.4     ("specialize", "true"),
     5.5     ("star_linear_preds", "true"),
     5.6     ("total_consts", "smart"),
     5.7 -   ("need", "smart"),
     5.8     ("peephole_optim", "true"),
     5.9     ("datatype_sym_break", "5"),
    5.10     ("kodkod_sym_break", "15"),
    5.11 @@ -93,7 +92,6 @@
    5.12     ("dont_specialize", "specialize"),
    5.13     ("dont_star_linear_preds", "star_linear_preds"),
    5.14     ("partial_consts", "total_consts"),
    5.15 -   ("dont_need", "need"),
    5.16     ("no_peephole_optim", "peephole_optim"),
    5.17     ("no_debug", "debug"),
    5.18     ("quiet", "verbose"),
    5.19 @@ -106,11 +104,12 @@
    5.20  fun is_known_raw_param s =
    5.21    AList.defined (op =) default_default_params s orelse
    5.22    AList.defined (op =) negated_params s orelse
    5.23 -  member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse
    5.24 +  member (op =) ["max", "show_all", "whack", "eval", "need", "atoms",
    5.25 +                 "expect"] s orelse
    5.26    exists (fn p => String.isPrefix (p ^ " ") s)
    5.27           ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
    5.28 -          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "need",
    5.29 -          "dont_need", "format", "atoms"]
    5.30 +          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
    5.31 +          "atoms"]
    5.32  
    5.33  fun check_raw_param (s, _) =
    5.34    if is_known_raw_param s then ()
    5.35 @@ -226,8 +225,8 @@
    5.36        #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
    5.37      val read_term_polymorphic =
    5.38        Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
    5.39 -    val lookup_term_list_polymorphic =
    5.40 -      AList.lookup (op =) raw_params #> these #> map read_term_polymorphic
    5.41 +    val lookup_term_list_option_polymorphic =
    5.42 +      AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic)
    5.43      val read_const_polymorphic = read_term_polymorphic #> dest_Const
    5.44      val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
    5.45                          |> auto ? map (apsnd (take max_auto_scopes))
    5.46 @@ -249,14 +248,14 @@
    5.47      val overlord = lookup_bool "overlord"
    5.48      val user_axioms = lookup_bool_option "user_axioms"
    5.49      val assms = lookup_bool "assms"
    5.50 -    val whacks = lookup_term_list_polymorphic "whack"
    5.51 +    val whacks = lookup_term_list_option_polymorphic "whack" |> these
    5.52      val merge_type_vars = lookup_bool "merge_type_vars"
    5.53      val binary_ints = lookup_bool_option "binary_ints"
    5.54      val destroy_constrs = lookup_bool "destroy_constrs"
    5.55      val specialize = lookup_bool "specialize"
    5.56      val star_linear_preds = lookup_bool "star_linear_preds"
    5.57      val total_consts = lookup_bool_option "total_consts"
    5.58 -    val needs = lookup_bool_option_assigns read_term_polymorphic "need"
    5.59 +    val needs = lookup_term_list_option_polymorphic "need"
    5.60      val peephole_optim = lookup_bool "peephole_optim"
    5.61      val datatype_sym_break = lookup_int "datatype_sym_break"
    5.62      val kodkod_sym_break = lookup_int "kodkod_sym_break"
    5.63 @@ -265,7 +264,7 @@
    5.64      val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")
    5.65      val show_datatypes = debug orelse lookup_bool "show_datatypes"
    5.66      val show_consts = debug orelse lookup_bool "show_consts"
    5.67 -    val evals = lookup_term_list_polymorphic "eval"
    5.68 +    val evals = lookup_term_list_option_polymorphic "eval" |> these
    5.69      val formats = lookup_ints_assigns read_term_polymorphic "format" 0
    5.70      val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
    5.71      val max_potential =
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Mar 03 11:20:48 2011 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Mar 03 11:20:48 2011 +0100
     6.3 @@ -1282,11 +1282,10 @@
     6.4        #> Term.map_abs_vars shortest_name
     6.5      val nondef_ts = nondef_ts |> map (do_middle false)
     6.6      val need_ts =
     6.7 -      (* FIXME: Implement inference. *)
     6.8 -      needs |> map_filter (fn (SOME t, SOME true) =>
     6.9 -                              SOME (t |> unfold_defs_in_term hol_ctxt
    6.10 -                                      |> do_middle false)
    6.11 -                            | _ => NONE)
    6.12 +      case needs of
    6.13 +        SOME needs =>
    6.14 +        needs |> map (unfold_defs_in_term hol_ctxt #> do_middle false)
    6.15 +      | NONE => [] (* FIXME: Implement inference. *)
    6.16      val nondef_ts = nondef_ts |> map (do_tail false)
    6.17      val def_ts = def_ts |> map (do_middle true #> do_tail true)
    6.18    in