author blanchet Wed May 04 18:48:25 2011 +0200 (2011-05-04) changeset 42679 223f01b32f17 parent 42678 593e375b939f child 42680 b6c27cf04fe9
[mq]: nitpick_tuning
```     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed May 04 18:43:42 2011 +0200
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed May 04 18:48:25 2011 +0200
1.3 @@ -980,6 +980,7 @@
1.4                      handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
1.5                             default_card)
1.6
1.7 +(* Similar to similarly named function in "Sledgehammer_ATP_Translate". *)
1.8  fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
1.9                                 assigns T =
1.10    let
1.11 @@ -990,24 +991,20 @@
1.12           raise SAME ()
1.13         else case T of
1.14           Type (@{type_name fun}, [T1, T2]) =>
1.15 -         let
1.16 -           val k1 = aux avoid T1
1.17 -           val k2 = aux avoid T2
1.18 -         in
1.19 -           if k2 = 1 then 1
1.20 -           else if k1 = 0 orelse k2 = 0 then 0
1.21 -           else if k1 >= max orelse k2 >= max then max
1.22 -           else Int.min (max, reasonable_power k2 k1)
1.23 -         end
1.24 +         (case (aux avoid T1, aux avoid T2) of
1.25 +            (_, 1) => 1
1.26 +          | (0, _) => 0
1.27 +          | (_, 0) => 0
1.28 +          | (k1, k2) =>
1.29 +            if k1 >= max orelse k2 >= max then max
1.30 +            else Int.min (max, reasonable_power k2 k1))
1.31         | Type (@{type_name prod}, [T1, T2]) =>
1.32 -         let
1.33 -           val k1 = aux avoid T1
1.34 -           val k2 = aux avoid T2
1.35 -         in
1.36 -           if k1 = 0 orelse k2 = 0 then 0
1.37 -           else if k1 >= max orelse k2 >= max then max
1.38 -           else Int.min (max, k1 * k2)
1.39 -         end
1.40 +         (case (aux avoid T1, aux avoid T2) of
1.41 +            (0, _) => 0
1.42 +          | (_, 0) => 0
1.43 +          | (k1, k2) =>
1.44 +            if k1 >= max orelse k2 >= max then max
1.45 +            else Int.min (max, k1 * k2))
1.46         | Type (@{type_name itself}, _) => 1
1.47         | @{typ prop} => 2
1.48         | @{typ bool} => 2
1.49 @@ -1022,7 +1019,7 @@
1.50                      constrs
1.51              in
1.52                if exists (curry (op =) 0) constr_cards then 0
1.53 -              else Integer.sum constr_cards
1.54 +              else Int.min (max, Integer.sum constr_cards)
1.55              end)
1.56         | _ => raise SAME ())
1.57        handle SAME () =>
```