support non-ground "need" values
authorblanchet
Tue Mar 15 15:49:42 2011 +0100 (2011-03-15 ago)
changeset 4198509b75d55008f
parent 41984 e5dba3d75e9e
child 41986 95a67e3f29ad
support non-ground "need" values
doc-src/Nitpick/nitpick.tex
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Mar 15 13:03:54 2011 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Mar 15 15:49:42 2011 +0100
     1.3 @@ -2466,12 +2466,12 @@
     1.4  {\small See also \textit{debug} (\S\ref{output-format}).}
     1.5  
     1.6  \opnodefault{need}{term\_list}
     1.7 -Specifies a list of datatype values (ground constructor terms) that should be
     1.8 -part of the subterm-closed subsets used to approximate datatypes. If you know
     1.9 -that a value must necessarily belong to the subset of representable values that
    1.10 -approximates a datatype, specifying it can speed up the search, especially for
    1.11 -high cardinalities. By default, Nitpick inspects the conjecture to infer needed
    1.12 -datatype values.
    1.13 +Specifies a list of datatype values (normally ground constructor terms) that
    1.14 +should be part of the subterm-closed subsets used to approximate datatypes. If
    1.15 +you know that a value must necessarily belong to the subset of representable
    1.16 +values that approximates a datatype, specifying it can speed up the search,
    1.17 +especially for high cardinalities.
    1.18 +%By default, Nitpick inspects the conjecture to infer needed datatype values.
    1.19  
    1.20  \opsmart{total\_consts}{partial\_consts}
    1.21  Specifies whether constants occurring in the problem other than constructors can
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 15 13:03:54 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 15 15:49:42 2011 +0100
     2.3 @@ -197,10 +197,6 @@
     2.4  
     2.5  fun plazy f = Pretty.blk (0, pstrs (f ()))
     2.6  
     2.7 -fun check_constr_nut (Construct (_, _, _, us)) = List.app check_constr_nut us
     2.8 -  | check_constr_nut _ =
     2.9 -    error "The \"need\" option requires a constructor term."
    2.10 -
    2.11  fun pick_them_nits_in_term deadline state (params : params) auto i n step
    2.12                             subst assm_ts orig_t =
    2.13    let
    2.14 @@ -333,7 +329,6 @@
    2.15      val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq)
    2.16      val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq)
    2.17      val need_us = need_ts |> map (nut_from_term hol_ctxt Eq)
    2.18 -    val _ = List.app check_constr_nut need_us
    2.19      val (free_names, const_names) =
    2.20        fold add_free_and_const_names (nondef_us @ def_us @ need_us) ([], [])
    2.21      val (sel_names, nonsel_names) =
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Mar 15 13:03:54 2011 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Mar 15 15:49:42 2011 +0100
     3.3 @@ -1506,8 +1506,7 @@
     3.4                       end
     3.5                   else
     3.6                     accum)
     3.7 -        | aux u =
     3.8 -          raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u])
     3.9 +        | aux _ = I
    3.10      in
    3.11        case SOME (index_seq 0 card, []) |> fold aux need_us of
    3.12          SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk)