src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 46112 31bc296a1257
parent 46104 eb85282db54e
child 47909 5f1afeebafbc
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jan 04 11:01:08 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jan 04 12:09:53 2012 +0100
     1.3 @@ -473,18 +473,25 @@
     1.4              #> format_fun (uniterize_unarize_unbox_etc_type T')
     1.5                            (uniterize_unarize_unbox_etc_type T1)
     1.6                            (uniterize_unarize_unbox_etc_type T2))
     1.7 -    fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
     1.8 +
     1.9 +
    1.10 +    fun term_for_fun_or_set seen T T' j =
    1.11          let
    1.12 -          val k1 = card_of_type card_assigns T1
    1.13 -          val k2 = card_of_type card_assigns T2
    1.14 +          val k1 = card_of_type card_assigns (pseudo_domain_type T)
    1.15 +          val k2 = card_of_type card_assigns (pseudo_range_type T)
    1.16          in
    1.17            term_for_rep true seen T T' (Vect (k1, Atom (k2, 0)))
    1.18                         [nth_combination (replicate k1 (k2, 0)) j]
    1.19            handle General.Subscript =>
    1.20 -                 raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
    1.21 +                 raise ARG ("Nitpick_Model.reconstruct_term.\
    1.22 +                            \term_for_fun_or_set",
    1.23                              signed_string_of_int j ^ " for " ^
    1.24                              string_for_rep (Vect (k1, Atom (k2, 0))))
    1.25          end
    1.26 +    and term_for_atom seen (T as Type (@{type_name fun}, _)) T' j _ =
    1.27 +        term_for_fun_or_set seen T T' j
    1.28 +      | term_for_atom seen (T as Type (@{type_name set}, _)) T' j _ =
    1.29 +        term_for_fun_or_set seen T T' j
    1.30        | term_for_atom seen (Type (@{type_name prod}, [T1, T2])) _ j k =
    1.31          let
    1.32            val k1 = card_of_type card_assigns T1
    1.33 @@ -492,7 +499,8 @@
    1.34          in
    1.35            list_comb (HOLogic.pair_const T1 T2,
    1.36                       map3 (fn T => term_for_atom seen T T) [T1, T2]
    1.37 -                          [j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *)
    1.38 +                          (* ### k2 or k1? FIXME *)
    1.39 +                          [j div k2, j mod k2] [k1, k2])
    1.40          end
    1.41        | term_for_atom seen @{typ prop} _ j k =
    1.42          HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)