optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem

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

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 17:53:19 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Oct 27 19:00:17 2009 +0100
@@ -283,6 +283,21 @@
             handle TYPE (_, Ts, ts) =>
                    raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
 
+    val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
+    val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
+                     def_ts
+    val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
+                        nondef_ts
+    val (free_names, const_names) =
+      fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
+    val (sel_names, nonsel_names) =
+      List.partition (is_sel o nickname_of) const_names
+    val would_be_genuine = got_all_user_axioms andalso none_true wfs
+(*
+    val _ = List.app (priority o string_for_nut ctxt)
+                     (core_u :: def_us @ nondef_us)
+*)
+
     val unique_scope = forall (equal 1 o length o snd) cards_assigns
     (* typ -> bool *)
     fun is_free_type_monotonic T =
@@ -298,6 +313,8 @@
         not (is_pure_typedef thy T) orelse is_univ_typedef thy T
         orelse is_number_type thy T
         orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
+    fun is_datatype_shallow T =
+      not (exists (equal T o domain_type o type_of) sel_names)
     val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
              |> sort TermOrd.typ_ord
     val (all_dataTs, all_free_Ts) =
@@ -326,7 +343,7 @@
         ()
     val mono_Ts = mono_dataTs @ mono_free_Ts
     val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
-
+    val shallow_dataTs = filter is_datatype_shallow mono_dataTs
 (*
     val _ = priority "Monotonic datatypes:"
     val _ = List.app (priority o string_for_type ctxt) mono_dataTs
@@ -338,19 +355,6 @@
     val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts
 *)
 
-    val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
-    val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
-                     def_ts
-    val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
-                        nondef_ts
-    val (free_names, const_names) =
-      fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
-    val nonsel_names = filter_out (is_sel o nickname_of) const_names
-    val would_be_genuine = got_all_user_axioms andalso none_true wfs
-(*
-    val _ = List.app (priority o string_for_nut ctxt)
-                     (core_u :: def_us @ nondef_us)
-*)
     val need_incremental = Int.max (max_potential, max_genuine) >= 2
     val effective_sat_solver =
       if sat_solver <> "smart" then
@@ -812,6 +816,7 @@
 
     val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns
                                  iters_assigns bisim_depths mono_Ts nonmono_Ts
+                                 shallow_dataTs
     val batches = batch_list batch_size (!scopes)
     val outcome_code =
       (run_batches 0 (length batches) batches (max_potential, max_genuine, 0)

--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Oct 27 17:53:19 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Oct 27 19:00:17 2009 +0100
@@ -716,8 +716,8 @@
 (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    -> dtype_spec -> nfa_entry option *)
 fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
-  | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes
-                           ({typ, constrs, ...} : dtype_spec) =
+  | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE
+  | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
     SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
                      o #const) constrs)
 
@@ -884,12 +884,13 @@
 
 (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
    -> dtype_spec -> Kodkod.formula list *)
-fun other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
-  let val j0 = offset_of_type ofs typ in
-    sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
-    uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
-    partition_axioms_for_datatype j0 kk rel_table dtype
-  end
+fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = []
+  | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
+    let val j0 = offset_of_type ofs typ in
+      sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
+      uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
+      partition_axioms_for_datatype j0 kk rel_table dtype
+    end
 
 (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
    -> dtype_spec list -> Kodkod.formula list *)

--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 27 17:53:19 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 27 19:00:17 2009 +0100
@@ -329,7 +329,8 @@
           HOLogic.mk_number nat_T j
         else case datatype_spec datatypes T of
           NONE => atom for_auto T j
-        | SOME {constrs, co, ...} =>
+        | SOME {shallow = true, ...} => atom for_auto T j
+        | SOME {co, constrs, ...} =>
           let
             (* styp -> int list *)
             fun tuples_for_const (s, T) =
@@ -600,11 +601,12 @@
     (* typ -> dtype_spec list *)
     fun integer_datatype T =
       [{typ = T, card = card_of_type card_assigns T, co = false,
-        precise = false, constrs = []}]
+        precise = false, shallow = false, constrs = []}]
       handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
     val (codatatypes, datatypes) =
-      List.partition #co datatypes
-      ||> append (integer_datatype nat_T @ integer_datatype int_T)
+      datatypes |> filter_out #shallow
+                |> List.partition #co
+                ||> append (integer_datatype nat_T @ integer_datatype int_T)
     val block_of_datatypes =
       if show_datatypes andalso not (null datatypes) then
         [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")

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

--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Oct 27 17:53:19 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Oct 27 19:00:17 2009 +0100
@@ -22,6 +22,7 @@
     card: int,
     co: bool,
     precise: bool,
+    shallow: bool,
     constrs: constr_spec list}
 
   type scope = {
@@ -44,7 +45,7 @@
   val all_scopes :
     extended_context -> int -> (typ option * int list) list
     -> (styp option * int list) list -> (styp option * int list) list
-    -> int list -> typ list -> typ list -> scope list
+    -> int list -> typ list -> typ list -> typ list -> scope list
 end;
 
 structure Nitpick_Scope : NITPICK_SCOPE =
@@ -66,6 +67,7 @@
   card: int,
   co: bool,
   precise: bool,
+  shallow: bool,
   constrs: constr_spec list}
 
 type scope = {
@@ -126,7 +128,7 @@
       card_assigns |> filter_out (equal @{typ bisim_iterator} o fst)
                    |> List.partition (is_fp_iterator_type o fst)
     val (unimportant_card_asgns, important_card_asgns) =
-      card_asgns |> List.partition ((is_datatype thy orf is_integer_type) o fst)
+      card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
     val cards =
       map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
                         string_of_int k)
@@ -431,10 +433,11 @@
      explicit_max = max, total = total} :: constrs
   end
 
-(* extended_context -> scope_desc -> typ * int -> dtype_spec *)
-fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...})
+(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
+fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
                                         (desc as (card_asgns, _)) (T, card) =
   let
+    val shallow = T mem shallow_dataTs
     val co = is_codatatype thy T
     val xs = boxed_datatype_constrs ext_ctxt T
     val self_recs = map (is_self_recursive_constr_type o snd) xs
@@ -448,14 +451,18 @@
     val constrs =
       fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
                                 num_non_self_recs) (self_recs ~~ xs) []
-  in {typ = T, card = card, co = co, precise = precise, constrs = constrs} end
+  in
+    {typ = T, card = card, co = co, precise = precise, shallow = shallow,
+     constrs = constrs}
+  end
 
-(* extended_context -> int -> scope_desc -> scope *)
-fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break
+(* extended_context -> int -> typ list -> scope_desc -> scope *)
+fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
                           (desc as (card_asgns, _)) =
   let
-    val datatypes = map (datatype_spec_from_scope_descriptor ext_ctxt desc)
-                        (filter (is_datatype thy o fst) card_asgns)
+    val datatypes =
+      map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
+          (filter (is_datatype thy o fst) card_asgns)
     val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1
   in
     {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes,
@@ -480,9 +487,9 @@
 
 (* extended_context -> int -> (typ option * int list) list
    -> (styp option * int list) list -> (styp option * int list) list -> int list
-   -> typ list -> typ list -> scope list *)
+   -> typ list -> typ list -> typ list -> scope list *)
 fun all_scopes (ext_ctxt as {thy, ctxt, ...}) sym_break cards_asgns maxes_asgns
-               iters_asgns bisim_depths mono_Ts nonmono_Ts =
+               iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
   let
     val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns
     val blocks = blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns
@@ -492,7 +499,7 @@
                 |> map_filter (scope_descriptor_from_combination thy blocks)
   in
     descs |> length descs <= distinct_threshold ? distinct (op =)
-          |> map (scope_from_descriptor ext_ctxt sym_break)
+          |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs)
   end
 
 end;