improved formula for specialization, to prevent needless specializations -- and removed dead code
authorblanchet
Wed Mar 09 10:28:01 2011 +0100 (2011-03-09)
changeset 4189855d981e1232a
parent 41897 c24e7fd17464
child 41899 83dd157ec9ab
improved formula for specialization, to prevent needless specializations -- and removed dead code
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 09 10:25:29 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 09 10:28:01 2011 +0100
     1.3 @@ -167,7 +167,6 @@
     1.4      hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
     1.5    val typical_card_of_type : typ -> int
     1.6    val is_finite_type : hol_context -> typ -> bool
     1.7 -  val is_small_finite_type : hol_context -> typ -> bool
     1.8    val is_special_eligible_arg : bool -> typ list -> term -> bool
     1.9    val s_let :
    1.10      typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
    1.11 @@ -1029,23 +1028,19 @@
    1.12    in Int.min (max, aux [] T) end
    1.13  
    1.14  val typical_atomic_card = 4
    1.15 -val typical_card_of_type = bounded_card_of_type 65536 typical_atomic_card []
    1.16 -
    1.17 -val small_type_max_card = 5
    1.18 +val typical_card_of_type = bounded_card_of_type 16777217 typical_atomic_card []
    1.19  
    1.20  fun is_finite_type hol_ctxt T =
    1.21    bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
    1.22 -fun is_small_finite_type hol_ctxt T =
    1.23 -  let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
    1.24 -    n > 0 andalso n <= small_type_max_card
    1.25 -  end
    1.26  
    1.27  fun is_special_eligible_arg strict Ts t =
    1.28    case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of
    1.29      [] => true
    1.30    | bad_Ts =>
    1.31      let
    1.32 -      val bad_Ts_cost = fold (Integer.max o typical_card_of_type) bad_Ts 0
    1.33 +      val bad_Ts_cost =
    1.34 +        if strict then fold (curry (op *) o typical_card_of_type) bad_Ts 1
    1.35 +        else fold (Integer.max o typical_card_of_type) bad_Ts 0
    1.36        val T_cost = typical_card_of_type (fastype_of1 (Ts, t))
    1.37      in (bad_Ts_cost, T_cost) |> (if strict then op < else op <=) end
    1.38