1.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Tue Oct 27 17:53:19 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Oct 27 19:00:17 2009 +0100
     1.3 @@ -7,6 +7,8 @@
     1.4    * Replaced "special_depth" and "skolemize_depth" options by "specialize"
     1.5      and "skolemize"
     1.6    * Renamed "coalesce_type_vars" to "merge_type_vars"
     1.7 +  * Optimized Kodkod encoding of datatypes whose constructors don't appear in
     1.8 +    the formula to falsify
     1.9    * Fixed monotonicity check
    1.10  
    1.11  Version 1.2.2 (16 Oct 2009)

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 17:53:19 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 19:00:17 2009 +0100
     2.3 @@ -283,6 +283,21 @@
     2.4              handle TYPE (_, Ts, ts) =>
     2.5                     raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
     2.6  
     2.7 +    val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
     2.8 +    val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
     2.9 +                     def_ts
    2.10 +    val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
    2.11 +                        nondef_ts
    2.12 +    val (free_names, const_names) =
    2.13 +      fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
    2.14 +    val (sel_names, nonsel_names) =
    2.15 +      List.partition (is_sel o nickname_of) const_names
    2.16 +    val would_be_genuine = got_all_user_axioms andalso none_true wfs
    2.17 +(*
    2.18 +    val _ = List.app (priority o string_for_nut ctxt)
    2.19 +                     (core_u :: def_us @ nondef_us)
    2.20 +*)
    2.21 +
    2.22      val unique_scope = forall (equal 1 o length o snd) cards_assigns
    2.23      (* typ -> bool *)
    2.24      fun is_free_type_monotonic T =
    2.25 @@ -298,6 +313,8 @@
    2.26          not (is_pure_typedef thy T) orelse is_univ_typedef thy T
    2.27          orelse is_number_type thy T
    2.28          orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
    2.29 +    fun is_datatype_shallow T =
    2.30 +      not (exists (equal T o domain_type o type_of) sel_names)
    2.31      val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
    2.32               |> sort TermOrd.typ_ord
    2.33      val (all_dataTs, all_free_Ts) =
    2.34 @@ -326,7 +343,7 @@
    2.35          ()
    2.36      val mono_Ts = mono_dataTs @ mono_free_Ts
    2.37      val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
    2.38 -
    2.39 +    val shallow_dataTs = filter is_datatype_shallow mono_dataTs
    2.40  (*
    2.41      val _ = priority "Monotonic datatypes:"
    2.42      val _ = List.app (priority o string_for_type ctxt) mono_dataTs
    2.43 @@ -338,19 +355,6 @@
    2.44      val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts
    2.45  *)
    2.46  
    2.47 -    val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
    2.48 -    val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
    2.49 -                     def_ts
    2.50 -    val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
    2.51 -                        nondef_ts
    2.52 -    val (free_names, const_names) =
    2.53 -      fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
    2.54 -    val nonsel_names = filter_out (is_sel o nickname_of) const_names
    2.55 -    val would_be_genuine = got_all_user_axioms andalso none_true wfs
    2.56 -(*
    2.57 -    val _ = List.app (priority o string_for_nut ctxt)
    2.58 -                     (core_u :: def_us @ nondef_us)
    2.59 -*)
    2.60      val need_incremental = Int.max (max_potential, max_genuine) >= 2
    2.61      val effective_sat_solver =
    2.62        if sat_solver <> "smart" then
    2.63 @@ -812,6 +816,7 @@
    2.64  
    2.65      val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns
    2.66                                   iters_assigns bisim_depths mono_Ts nonmono_Ts
    2.67 +                                 shallow_dataTs
    2.68      val batches = batch_list batch_size (!scopes)
    2.69      val outcome_code =
    2.70        (run_batches 0 (length batches) batches (max_potential, max_genuine, 0)

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Oct 27 17:53:19 2009 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Oct 27 19:00:17 2009 +0100
     3.3 @@ -716,8 +716,8 @@
     3.4  (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
     3.5     -> dtype_spec -> nfa_entry option *)
     3.6  fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
     3.7 -  | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes
     3.8 -                           ({typ, constrs, ...} : dtype_spec) =
     3.9 +  | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE
    3.10 +  | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
    3.11      SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
    3.12                       o #const) constrs)
    3.13  
    3.14 @@ -884,12 +884,13 @@
    3.15  
    3.16  (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
    3.17     -> dtype_spec -> Kodkod.formula list *)
    3.18 -fun other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
    3.19 -  let val j0 = offset_of_type ofs typ in
    3.20 -    sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
    3.21 -    uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
    3.22 -    partition_axioms_for_datatype j0 kk rel_table dtype
    3.23 -  end
    3.24 +fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = []
    3.25 +  | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
    3.26 +    let val j0 = offset_of_type ofs typ in
    3.27 +      sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
    3.28 +      uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
    3.29 +      partition_axioms_for_datatype j0 kk rel_table dtype
    3.30 +    end
    3.31  
    3.32  (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
    3.33     -> dtype_spec list -> Kodkod.formula list *)

     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 27 17:53:19 2009 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 27 19:00:17 2009 +0100
     4.3 @@ -329,7 +329,8 @@
     4.4            HOLogic.mk_number nat_T j
     4.5          else case datatype_spec datatypes T of
     4.6            NONE => atom for_auto T j
     4.7 -        | SOME {constrs, co, ...} =>
     4.8 +        | SOME {shallow = true, ...} => atom for_auto T j
     4.9 +        | SOME {co, constrs, ...} =>
    4.10            let
    4.11              (* styp -> int list *)
    4.12              fun tuples_for_const (s, T) =
    4.13 @@ -600,11 +601,12 @@
    4.14      (* typ -> dtype_spec list *)
    4.15      fun integer_datatype T =
    4.16        [{typ = T, card = card_of_type card_assigns T, co = false,
    4.17 -        precise = false, constrs = []}]
    4.18 +        precise = false, shallow = false, constrs = []}]
    4.19        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    4.20      val (codatatypes, datatypes) =
    4.21 -      List.partition #co datatypes
    4.22 -      ||> append (integer_datatype nat_T @ integer_datatype int_T)
    4.23 +      datatypes |> filter_out #shallow
    4.24 +                |> List.partition #co
    4.25 +                ||> append (integer_datatype nat_T @ integer_datatype int_T)
    4.26      val block_of_datatypes =
    4.27        if show_datatypes andalso not (null datatypes) then
    4.28          [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")

     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Oct 27 17:53:19 2009 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Oct 27 19:00:17 2009 +0100
     5.3 @@ -749,8 +749,9 @@
     5.4             (~1 upto num_sels_for_constr_type T - 1)
     5.5  (* scope -> dtype_spec -> nut list * rep NameTable.table
     5.6     -> nut list * rep NameTable.table *)
     5.7 -fun choose_rep_for_sels_of_datatype scope ({constrs, ...} : dtype_spec) =
     5.8 -  fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
     5.9 +fun choose_rep_for_sels_of_datatype _ ({shallow = true, ...} : dtype_spec) = I
    5.10 +  | choose_rep_for_sels_of_datatype scope {constrs, ...} =
    5.11 +    fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
    5.12  (* scope -> rep NameTable.table -> nut list * rep NameTable.table *)
    5.13  fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
    5.14    fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []

     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Oct 27 17:53:19 2009 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Oct 27 19:00:17 2009 +0100
     6.3 @@ -22,6 +22,7 @@
     6.4      card: int,
     6.5      co: bool,
     6.6      precise: bool,
     6.7 +    shallow: bool,
     6.8      constrs: constr_spec list}
     6.9  
    6.10    type scope = {
    6.11 @@ -44,7 +45,7 @@
    6.12    val all_scopes :
    6.13      extended_context -> int -> (typ option * int list) list
    6.14      -> (styp option * int list) list -> (styp option * int list) list
    6.15 -    -> int list -> typ list -> typ list -> scope list
    6.16 +    -> int list -> typ list -> typ list -> typ list -> scope list
    6.17  end;
    6.18  
    6.19  structure Nitpick_Scope : NITPICK_SCOPE =
    6.20 @@ -66,6 +67,7 @@
    6.21    card: int,
    6.22    co: bool,
    6.23    precise: bool,
    6.24 +  shallow: bool,
    6.25    constrs: constr_spec list}
    6.26  
    6.27  type scope = {
    6.28 @@ -126,7 +128,7 @@
    6.29        card_assigns |> filter_out (equal @{typ bisim_iterator} o fst)
    6.30                     |> List.partition (is_fp_iterator_type o fst)
    6.31      val (unimportant_card_asgns, important_card_asgns) =
    6.32 -      card_asgns |> List.partition ((is_datatype thy orf is_integer_type) o fst)
    6.33 +      card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
    6.34      val cards =
    6.35        map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
    6.36                          string_of_int k)
    6.37 @@ -431,10 +433,11 @@
    6.38       explicit_max = max, total = total} :: constrs
    6.39    end
    6.40  
    6.41 -(* extended_context -> scope_desc -> typ * int -> dtype_spec *)
    6.42 -fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...})
    6.43 +(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
    6.44 +fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
    6.45                                          (desc as (card_asgns, _)) (T, card) =
    6.46    let
    6.47 +    val shallow = T mem shallow_dataTs
    6.48      val co = is_codatatype thy T
    6.49      val xs = boxed_datatype_constrs ext_ctxt T
    6.50      val self_recs = map (is_self_recursive_constr_type o snd) xs
    6.51 @@ -448,14 +451,18 @@
    6.52      val constrs =
    6.53        fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
    6.54                                  num_non_self_recs) (self_recs ~~ xs) []
    6.55 -  in {typ = T, card = card, co = co, precise = precise, constrs = constrs} end
    6.56 +  in
    6.57 +    {typ = T, card = card, co = co, precise = precise, shallow = shallow,
    6.58 +     constrs = constrs}
    6.59 +  end
    6.60  
    6.61 -(* extended_context -> int -> scope_desc -> scope *)
    6.62 -fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break
    6.63 +(* extended_context -> int -> typ list -> scope_desc -> scope *)
    6.64 +fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
    6.65                            (desc as (card_asgns, _)) =
    6.66    let
    6.67 -    val datatypes = map (datatype_spec_from_scope_descriptor ext_ctxt desc)
    6.68 -                        (filter (is_datatype thy o fst) card_asgns)
    6.69 +    val datatypes =
    6.70 +      map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
    6.71 +          (filter (is_datatype thy o fst) card_asgns)
    6.72      val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1
    6.73    in
    6.74      {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes,
    6.75 @@ -480,9 +487,9 @@
    6.76  
    6.77  (* extended_context -> int -> (typ option * int list) list
    6.78     -> (styp option * int list) list -> (styp option * int list) list -> int list
    6.79 -   -> typ list -> typ list -> scope list *)
    6.80 +   -> typ list -> typ list -> typ list -> scope list *)
    6.81  fun all_scopes (ext_ctxt as {thy, ctxt, ...}) sym_break cards_asgns maxes_asgns
    6.82 -               iters_asgns bisim_depths mono_Ts nonmono_Ts =
    6.83 +               iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
    6.84    let
    6.85      val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns
    6.86      val blocks = blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns
    6.87 @@ -492,7 +499,7 @@
    6.88                  |> map_filter (scope_descriptor_from_combination thy blocks)
    6.89    in
    6.90      descs |> length descs <= distinct_threshold ? distinct (op =)
    6.91 -          |> map (scope_from_descriptor ext_ctxt sym_break)
    6.92 +          |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs)
    6.93    end
    6.94  
    6.95  end;