1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Mar 18 10:17:37 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Mar 18 11:43:28 2011 +0100
     1.3 @@ -564,9 +564,13 @@
     1.4          val plain_rels = free_rels @ other_rels
     1.5          val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
     1.6          val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
     1.7 -        val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
     1.8 +        val need_vals =
     1.9 +          map (fn dtype as {typ, ...} =>
    1.10 +                  (typ, needed_values_for_datatype need_us ofs dtype)) datatypes
    1.11 +        val sel_bounds =
    1.12 +          map (bound_for_sel_rel ctxt debug need_vals datatypes) sel_rels
    1.13          val dtype_axioms =
    1.14 -          declarative_axioms_for_datatypes hol_ctxt binarize need_us
    1.15 +          declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
    1.16                datatype_sym_break bits ofs kk rel_table datatypes
    1.17          val declarative_axioms = plain_axioms @ dtype_axioms
    1.18          val univ_card = Int.max (univ_card nat_card int_card main_j0

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Mar 18 10:17:37 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Mar 18 11:43:28 2011 +0100
     2.3 @@ -27,15 +27,18 @@
     2.4      -> Kodkod.bound list * Kodkod.formula list
     2.5    val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
     2.6    val bound_for_sel_rel :
     2.7 -    Proof.context -> bool -> datatype_spec list -> nut -> Kodkod.bound
     2.8 +    Proof.context -> bool -> (typ * (nut * int) list option) list
     2.9 +    -> datatype_spec list -> nut -> Kodkod.bound
    2.10    val merge_bounds : Kodkod.bound list -> Kodkod.bound list
    2.11    val kodkod_formula_from_nut :
    2.12      int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
    2.13 +  val needed_values_for_datatype :
    2.14 +    nut list -> int Typtab.table -> datatype_spec -> (nut * int) list option
    2.15    val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
    2.16    val declarative_axioms_for_datatypes :
    2.17 -    hol_context -> bool -> nut list -> int -> int -> int Typtab.table
    2.18 -    -> kodkod_constrs -> nut NameTable.table -> datatype_spec list
    2.19 -    -> Kodkod.formula list
    2.20 +    hol_context -> bool -> nut list -> (typ * (nut * int) list option) list
    2.21 +    -> int -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
    2.22 +    -> datatype_spec list -> Kodkod.formula list
    2.23  end;
    2.24  
    2.25  structure Nitpick_Kodkod : NITPICK_KODKOD =
    2.26 @@ -297,24 +300,39 @@
    2.27    | bound_for_plain_rel _ _ u =
    2.28      raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
    2.29  
    2.30 -fun bound_for_sel_rel ctxt debug dtypes
    2.31 +fun bound_for_sel_rel ctxt debug need_vals dtypes
    2.32          (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
    2.33                    R as Func (Atom (_, j0), R2), nick)) =
    2.34      let
    2.35 +      val constr_s = original_name nick
    2.36        val {delta, epsilon, exclusive, explicit_max, ...} =
    2.37 -        constr_spec dtypes (original_name nick, T1)
    2.38 +        constr_spec dtypes (constr_s, T1)
    2.39 +      val dtype as {card, ...} = datatype_spec dtypes T1 |> the
    2.40 +      val need_vals =
    2.41 +        AList.lookup (op =) need_vals T1 |> the_default NONE |> these
    2.42      in
    2.43        ([(x, bound_comment ctxt debug nick T R)],
    2.44 -       if explicit_max = 0 then
    2.45 -         [KK.TupleSet []]
    2.46 -       else
    2.47 -         let val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) in
    2.48 +       let
    2.49 +         val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0)
    2.50 +         val complete_need_vals = (length need_vals = card)
    2.51 +         val (my_need_vals, other_need_vals) =
    2.52 +           need_vals
    2.53 +           |> List.partition
    2.54 +                  (fn (Construct (sel_us, _, _, _), _) =>
    2.55 +                      exists (fn FreeRel (x', _, _, _) => x = x'
    2.56 +                               | _ => false) sel_us
    2.57 +                    | _ => false)
    2.58 +       in
    2.59 +         if explicit_max = 0 orelse
    2.60 +            (complete_need_vals andalso null my_need_vals) then
    2.61 +           [KK.TupleSet []]
    2.62 +         else
    2.63             if R2 = Formula Neut then
    2.64               [ts] |> not exclusive ? cons (KK.TupleSet [])
    2.65             else
    2.66               [KK.TupleSet [],
    2.67                if T1 = T2 andalso epsilon > delta andalso
    2.68 -                 is_datatype_acyclic (the (datatype_spec dtypes T1)) then
    2.69 +                 is_datatype_acyclic dtype then
    2.70                  index_seq delta (epsilon - delta)
    2.71                  |> map (fn j =>
    2.72                             KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
    2.73 @@ -324,7 +342,7 @@
    2.74                  KK.TupleProduct (ts, upper_bound_for_rep R2)]
    2.75           end)
    2.76      end
    2.77 -  | bound_for_sel_rel _ _ _ u =
    2.78 +  | bound_for_sel_rel _ _ _ _ u =
    2.79      raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])
    2.80  
    2.81  fun merge_bounds bs =
    2.82 @@ -1478,8 +1496,8 @@
    2.83                        "malformed Kodkod formula")
    2.84    end
    2.85  
    2.86 -fun needed_value_axioms_for_datatype [] _ _ _ = []
    2.87 -  | needed_value_axioms_for_datatype need_us ofs kk
    2.88 +fun needed_values_for_datatype [] _ _ = SOME []
    2.89 +  | needed_values_for_datatype need_us ofs
    2.90          ({typ, card, constrs, ...} : datatype_spec) =
    2.91      let
    2.92        fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
    2.93 @@ -1507,11 +1525,11 @@
    2.94                   else
    2.95                     accum)
    2.96          | aux _ = I
    2.97 -    in
    2.98 -      case SOME (index_seq 0 card, []) |> fold aux need_us of
    2.99 -        SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk)
   2.100 -      | NONE => [KK.False]
   2.101 -    end
   2.102 +    in SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map snd end
   2.103 +
   2.104 +fun needed_value_axioms_for_datatype _ _ NONE = [KK.False]
   2.105 +  | needed_value_axioms_for_datatype ofs kk (SOME fixed) =
   2.106 +    fixed |> map (atom_equation_for_nut ofs kk)
   2.107  
   2.108  fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
   2.109    kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
   2.110 @@ -1679,7 +1697,6 @@
   2.111             |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table
   2.112                                                    nfas dtypes)
   2.113  
   2.114 -
   2.115  fun sel_axiom_for_sel hol_ctxt binarize j0
   2.116          (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
   2.117          rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
   2.118 @@ -1776,7 +1793,7 @@
   2.119        partition_axioms_for_datatype j0 kk rel_table dtype
   2.120      end
   2.121  
   2.122 -fun declarative_axioms_for_datatypes hol_ctxt binarize need_us
   2.123 +fun declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
   2.124          datatype_sym_break bits ofs kk rel_table dtypes =
   2.125    let
   2.126      val nfas =
   2.127 @@ -1785,7 +1802,7 @@
   2.128               |> strongly_connected_sub_nfas
   2.129    in
   2.130      acyclicity_axioms_for_datatypes kk nfas @
   2.131 -    maps (needed_value_axioms_for_datatype need_us ofs kk) dtypes @
   2.132 +    maps (needed_value_axioms_for_datatype ofs kk o snd) need_vals @
   2.133      sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
   2.134                                     kk rel_table nfas dtypes @
   2.135      maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)