renamed "preconstr" option "need"
authorblanchet
Thu Mar 03 11:20:48 2011 +0100 (2011-03-03)
changeset 41875e3cd0dce9b1a
parent 41874 a3035d56171d
child 41876 03f699556955
renamed "preconstr" option "need"
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_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Mar 03 10:55:41 2011 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Mar 03 11:20:48 2011 +0100
     1.3 @@ -2465,17 +2465,17 @@
     1.4  
     1.5  {\small See also \textit{debug} (\S\ref{output-format}).}
     1.6  
     1.7 -\opargboolorsmart{preconstr}{term}{dont\_preconstr}
     1.8 -Specifies whether a datatype value should be preconstructed, meaning Nitpick
     1.9 +\opargboolorsmart{need}{term}{dont\_need}
    1.10 +Specifies whether a datatype value is required by the problem, meaning Nitpick
    1.11  will reserve a Kodkod atom for it. If a value must necessarily belong to the
    1.12 -subset of representable values that approximates a datatype, preconstructing
    1.13 -it can speed up the search significantly, especially for high cardinalities. By
    1.14 -default, Nitpick inspects the conjecture to infer terms that can be
    1.15 -preconstructed.
    1.16 -
    1.17 -\opsmart{preconstr}{dont\_preconstr}
    1.18 -Specifies the default preconstruction setting to use. This can be overridden on
    1.19 -a per-term basis using the \textit{preconstr}~\qty{term} option described above.
    1.20 +subset of representable values that approximates a datatype, specifying it can
    1.21 +speed up the search significantly, especially for high cardinalities. By
    1.22 +default, Nitpick inspects the conjecture to infer needed datatype values.
    1.23 +
    1.24 +\opsmart{need}{dont\_need}
    1.25 +Specifies the default needed datatype value setting to use. This can be
    1.26 +overridden on a per-term basis using the \textit{preconstr}~\qty{term} option
    1.27 +described above.
    1.28  
    1.29  \opsmart{total\_consts}{partial\_consts}
    1.30  Specifies whether constants occurring in the problem other than constructors can
     2.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Mar 03 10:55:41 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 -   preconstrs = [], tac_timeout = NONE, evals = [], case_names = case_names,
     2.8 +   needs = [], 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 10:55:41 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 -     preconstrs: (term option * bool option) list,
     3.8 +     needs: (term option * bool option) list,
     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 -   preconstrs: (term option * bool option) list,
    3.17 +   needs: (term option * bool option) list,
    3.18     peephole_optim: bool,
    3.19     datatype_sym_break: int,
    3.20     kodkod_sym_break: int,
    3.21 @@ -199,7 +199,7 @@
    3.22  
    3.23  fun check_constr_nut (Construct (_, _, _, us)) = List.app check_constr_nut us
    3.24    | check_constr_nut _ =
    3.25 -    error "The \"preconstr\" option requires a constructor term."
    3.26 +    error "The \"need\" option requires a constructor term."
    3.27  
    3.28  fun pick_them_nits_in_term deadline state (params : params) auto i n step
    3.29                             subst assm_ts orig_t =
    3.30 @@ -217,7 +217,7 @@
    3.31           boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
    3.32           verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
    3.33           binary_ints, destroy_constrs, specialize, star_linear_preds,
    3.34 -         total_consts, preconstrs, peephole_optim, datatype_sym_break,
    3.35 +         total_consts, needs, peephole_optim, datatype_sym_break,
    3.36           kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
    3.37           show_consts, evals, formats, atomss, max_potential, max_genuine,
    3.38           check_potential, check_genuine, batch_size, ...} = params
    3.39 @@ -258,7 +258,7 @@
    3.40                       o Date.fromTimeLocal o Time.now)
    3.41      val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
    3.42                  else orig_t
    3.43 -    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs
    3.44 +    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
    3.45      val tfree_table =
    3.46        if merge_type_vars then merged_type_var_table_for_terms thy conj_ts
    3.47        else []
    3.48 @@ -266,8 +266,8 @@
    3.49      val neg_t = neg_t |> merge_tfrees
    3.50      val assm_ts = assm_ts |> map merge_tfrees
    3.51      val evals = evals |> map merge_tfrees
    3.52 -    val preconstrs = preconstrs |> map (apfst (Option.map merge_tfrees))
    3.53 -    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs
    3.54 +    val needs = needs |> map (apfst (Option.map merge_tfrees))
    3.55 +    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst needs
    3.56      val original_max_potential = max_potential
    3.57      val original_max_genuine = max_genuine
    3.58      val max_bisim_depth = fold Integer.max bisim_depths ~1
    3.59 @@ -289,7 +289,7 @@
    3.60         whacks = whacks, binary_ints = binary_ints,
    3.61         destroy_constrs = destroy_constrs, specialize = specialize,
    3.62         star_linear_preds = star_linear_preds, total_consts = total_consts,
    3.63 -       preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals,
    3.64 +       needs = needs, tac_timeout = tac_timeout, evals = evals,
    3.65         case_names = case_names, def_tables = def_tables,
    3.66         nondef_table = nondef_table, user_nondefs = user_nondefs,
    3.67         simp_table = simp_table, psimp_table = psimp_table,
    3.68 @@ -302,7 +302,7 @@
    3.69      val real_frees = fold Term.add_frees conj_ts []
    3.70      val _ = null (fold Term.add_tvars conj_ts []) orelse
    3.71              error "Nitpick cannot handle goals with schematic type variables."
    3.72 -    val (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
    3.73 +    val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms,
    3.74           no_poly_user_axioms, binarize) =
    3.75        preprocess_formulas hol_ctxt assm_ts neg_t
    3.76      val got_all_user_axioms =
    3.77 @@ -332,8 +332,8 @@
    3.78  
    3.79      val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq)
    3.80      val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq)
    3.81 -    val preconstr_us = preconstr_ts |> map (nut_from_term hol_ctxt Eq)
    3.82 -    val _ = List.app check_constr_nut preconstr_us
    3.83 +    val need_us = need_ts |> map (nut_from_term hol_ctxt Eq)
    3.84 +    val _ = List.app check_constr_nut need_us
    3.85      val (free_names, const_names) =
    3.86        fold add_free_and_const_names (nondef_us @ def_us) ([], [])
    3.87      val (sel_names, nonsel_names) =
    3.88 @@ -526,8 +526,8 @@
    3.89            def_us |> map (choose_reps_in_nut scope unsound rep_table true)
    3.90          val nondef_us =
    3.91            nondef_us |> map (choose_reps_in_nut scope unsound rep_table false)
    3.92 -        val preconstr_us =
    3.93 -          preconstr_us |> map (choose_reps_in_nut scope unsound rep_table false)
    3.94 +        val need_us =
    3.95 +          need_us |> map (choose_reps_in_nut scope unsound rep_table false)
    3.96  (*
    3.97          val _ = List.app (print_g o string_for_nut ctxt)
    3.98                           (free_names @ sel_names @ nonsel_names @
    3.99 @@ -541,8 +541,7 @@
   3.100            rename_free_vars nonsel_names pool rel_table
   3.101          val nondef_us = nondef_us |> map (rename_vars_in_nut pool rel_table)
   3.102          val def_us = def_us |> map (rename_vars_in_nut pool rel_table)
   3.103 -        val preconstr_us =
   3.104 -          preconstr_us |> map (rename_vars_in_nut pool rel_table)
   3.105 +        val need_us = need_us |> map (rename_vars_in_nut pool rel_table)
   3.106          val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
   3.107          val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
   3.108          val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
   3.109 @@ -568,7 +567,7 @@
   3.110          val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
   3.111          val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
   3.112          val dtype_axioms =
   3.113 -          declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
   3.114 +          declarative_axioms_for_datatypes hol_ctxt binarize need_us
   3.115                datatype_sym_break bits ofs kk rel_table datatypes
   3.116          val declarative_axioms = plain_axioms @ dtype_axioms
   3.117          val univ_card = Int.max (univ_card nat_card int_card main_j0
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 03 10:55:41 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 -     preconstrs: (term option * bool option) list,
     4.8 +     needs: (term option * bool option) list,
     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 -   preconstrs: (term option * bool option) list,
    4.17 +   needs: (term option * bool option) list,
    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 10:55:41 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,7 @@
     5.4     ("specialize", "true"),
     5.5     ("star_linear_preds", "true"),
     5.6     ("total_consts", "smart"),
     5.7 -   ("preconstr", "smart"),
     5.8 +   ("need", "smart"),
     5.9     ("peephole_optim", "true"),
    5.10     ("datatype_sym_break", "5"),
    5.11     ("kodkod_sym_break", "15"),
    5.12 @@ -93,7 +93,7 @@
    5.13     ("dont_specialize", "specialize"),
    5.14     ("dont_star_linear_preds", "star_linear_preds"),
    5.15     ("partial_consts", "total_consts"),
    5.16 -   ("dont_preconstr", "preconstr"),
    5.17 +   ("dont_need", "need"),
    5.18     ("no_peephole_optim", "peephole_optim"),
    5.19     ("no_debug", "debug"),
    5.20     ("quiet", "verbose"),
    5.21 @@ -109,8 +109,8 @@
    5.22    member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse
    5.23    exists (fn p => String.isPrefix (p ^ " ") s)
    5.24           ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
    5.25 -          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "preconstr",
    5.26 -          "dont_preconstr", "format", "atoms"]
    5.27 +          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "need",
    5.28 +          "dont_need", "format", "atoms"]
    5.29  
    5.30  fun check_raw_param (s, _) =
    5.31    if is_known_raw_param s then ()
    5.32 @@ -256,8 +256,7 @@
    5.33      val specialize = lookup_bool "specialize"
    5.34      val star_linear_preds = lookup_bool "star_linear_preds"
    5.35      val total_consts = lookup_bool_option "total_consts"
    5.36 -    val preconstrs =
    5.37 -      lookup_bool_option_assigns read_term_polymorphic "preconstr"
    5.38 +    val needs = lookup_bool_option_assigns read_term_polymorphic "need"
    5.39      val peephole_optim = lookup_bool "peephole_optim"
    5.40      val datatype_sym_break = lookup_int "datatype_sym_break"
    5.41      val kodkod_sym_break = lookup_int "kodkod_sym_break"
    5.42 @@ -289,7 +288,7 @@
    5.43       merge_type_vars = merge_type_vars, binary_ints = binary_ints,
    5.44       destroy_constrs = destroy_constrs, specialize = specialize,
    5.45       star_linear_preds = star_linear_preds, total_consts = total_consts,
    5.46 -     preconstrs = preconstrs, peephole_optim = peephole_optim,
    5.47 +     needs = needs, peephole_optim = peephole_optim,
    5.48       datatype_sym_break = datatype_sym_break,
    5.49       kodkod_sym_break = kodkod_sym_break, timeout = timeout,
    5.50       tac_timeout = tac_timeout, max_threads = max_threads,
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Mar 03 10:55:41 2011 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Mar 03 11:20:48 2011 +0100
     6.3 @@ -1478,8 +1478,8 @@
     6.4                        "malformed Kodkod formula")
     6.5    end
     6.6  
     6.7 -fun preconstructed_value_axioms_for_datatype [] _ _ _ = []
     6.8 -  | preconstructed_value_axioms_for_datatype preconstr_us ofs kk
     6.9 +fun needed_value_axioms_for_datatype [] _ _ _ = []
    6.10 +  | needed_value_axioms_for_datatype need_us ofs kk
    6.11          ({typ, card, constrs, ...} : datatype_spec) =
    6.12      let
    6.13        fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
    6.14 @@ -1507,10 +1507,9 @@
    6.15                   else
    6.16                     accum)
    6.17          | aux u =
    6.18 -          raise NUT ("Nitpick_Kodkod.preconstructed_value_axioms_for_datatype\
    6.19 -                     \.aux", [u])
    6.20 +          raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u])
    6.21      in
    6.22 -      case SOME (index_seq 0 card, []) |> fold aux preconstr_us of
    6.23 +      case SOME (index_seq 0 card, []) |> fold aux need_us of
    6.24          SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk)
    6.25        | NONE => [KK.False]
    6.26      end
    6.27 @@ -1654,14 +1653,14 @@
    6.28                                                nfas dtypes)
    6.29    end
    6.30  
    6.31 -fun is_datatype_in_preconstructed_value T (Construct (_, T', _, us)) =
    6.32 -    T = T' orelse exists (is_datatype_in_preconstructed_value T) us
    6.33 -  | is_datatype_in_preconstructed_value _ _ = false
    6.34 +fun is_datatype_in_needed_value T (Construct (_, T', _, us)) =
    6.35 +    T = T' orelse exists (is_datatype_in_needed_value T) us
    6.36 +  | is_datatype_in_needed_value _ _ = false
    6.37  
    6.38  val min_sym_break_card = 7
    6.39  
    6.40 -fun sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
    6.41 -                                   datatype_sym_break kk rel_table nfas dtypes =
    6.42 +fun sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
    6.43 +                                   kk rel_table nfas dtypes =
    6.44    if datatype_sym_break = 0 then
    6.45      []
    6.46    else
    6.47 @@ -1673,8 +1672,7 @@
    6.48                                   o binder_types o snd o #const) constrs)
    6.49             |> filter_out
    6.50                    (fn {typ, ...} =>
    6.51 -                      exists (is_datatype_in_preconstructed_value typ)
    6.52 -                             preconstr_us)
    6.53 +                      exists (is_datatype_in_needed_value typ) need_us)
    6.54             |> (fn dtypes' =>
    6.55                    dtypes' |> length dtypes' > datatype_sym_break
    6.56                               ? (sort (datatype_ord o swap)
    6.57 @@ -1779,7 +1777,7 @@
    6.58        partition_axioms_for_datatype j0 kk rel_table dtype
    6.59      end
    6.60  
    6.61 -fun declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
    6.62 +fun declarative_axioms_for_datatypes hol_ctxt binarize need_us
    6.63          datatype_sym_break bits ofs kk rel_table dtypes =
    6.64    let
    6.65      val nfas =
    6.66 @@ -1788,9 +1786,9 @@
    6.67               |> strongly_connected_sub_nfas
    6.68    in
    6.69      acyclicity_axioms_for_datatypes kk nfas @
    6.70 -    maps (preconstructed_value_axioms_for_datatype preconstr_us ofs kk) dtypes @
    6.71 -    sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
    6.72 -        datatype_sym_break kk rel_table nfas dtypes @
    6.73 +    maps (needed_value_axioms_for_datatype need_us ofs kk) dtypes @
    6.74 +    sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
    6.75 +                                   kk rel_table nfas dtypes @
    6.76      maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
    6.77           dtypes
    6.78    end
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 03 10:55:41 2011 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 03 11:20:48 2011 +0100
     7.3 @@ -862,7 +862,7 @@
     7.4  fun reconstruct_hol_model {show_datatypes, show_consts}
     7.5          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
     7.6                        debug, whacks, binary_ints, destroy_constrs, specialize,
     7.7 -                      star_linear_preds, total_consts, preconstrs, tac_timeout,
     7.8 +                      star_linear_preds, total_consts, needs, tac_timeout,
     7.9                        evals, case_names, def_tables, nondef_table, user_nondefs,
    7.10                        simp_table, psimp_table, choice_spec_table, intro_table,
    7.11                        ground_thm_table, ersatz_table, skolems, special_funs,
    7.12 @@ -880,7 +880,7 @@
    7.13         whacks = whacks, binary_ints = binary_ints,
    7.14         destroy_constrs = destroy_constrs, specialize = specialize,
    7.15         star_linear_preds = star_linear_preds, total_consts = total_consts,
    7.16 -       preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals,
    7.17 +       needs = needs, tac_timeout = tac_timeout, evals = evals,
    7.18         case_names = case_names, def_tables = def_tables,
    7.19         nondef_table = nondef_table, user_nondefs = user_nondefs,
    7.20         simp_table = simp_table, psimp_table = psimp_table,
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Mar 03 10:55:41 2011 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Mar 03 11:20:48 2011 +0100
     8.3 @@ -1244,7 +1244,7 @@
     8.4  
     8.5  fun preprocess_formulas
     8.6          (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
     8.7 -                      preconstrs, ...}) assm_ts neg_t =
     8.8 +                      needs, ...}) assm_ts neg_t =
     8.9    let
    8.10      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
    8.11        neg_t |> unfold_defs_in_term hol_ctxt
    8.12 @@ -1281,18 +1281,17 @@
    8.13        #> close_form
    8.14        #> Term.map_abs_vars shortest_name
    8.15      val nondef_ts = nondef_ts |> map (do_middle false)
    8.16 -    val preconstr_ts =
    8.17 -      (* FIXME: Implement preconstruction inference. *)
    8.18 -      preconstrs
    8.19 -      |> map_filter (fn (SOME t, SOME true) =>
    8.20 -                        SOME (t |> unfold_defs_in_term hol_ctxt
    8.21 -                                |> do_middle false)
    8.22 -                      | _ => NONE)
    8.23 +    val need_ts =
    8.24 +      (* FIXME: Implement inference. *)
    8.25 +      needs |> map_filter (fn (SOME t, SOME true) =>
    8.26 +                              SOME (t |> unfold_defs_in_term hol_ctxt
    8.27 +                                      |> do_middle false)
    8.28 +                            | _ => NONE)
    8.29      val nondef_ts = nondef_ts |> map (do_tail false)
    8.30      val def_ts = def_ts |> map (do_middle true #> do_tail true)
    8.31    in
    8.32 -    (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
    8.33 -     no_poly_user_axioms, binarize)
    8.34 +    (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, no_poly_user_axioms,
    8.35 +     binarize)
    8.36    end
    8.37  
    8.38  end;