[mq]: nitpick_tuning
authorblanchet
Wed May 04 18:48:25 2011 +0200 (2011-05-04)
changeset 42679223f01b32f17
parent 42678 593e375b939f
child 42680 b6c27cf04fe9
[mq]: nitpick_tuning
src/HOL/Tools/Nitpick/nitpick_hol.ML
     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 () =>