made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"
authorblanchet
Mon Feb 28 17:53:10 2011 +0100 (2011-02-28)
changeset 41859c3a5912d0922
parent 41858 37ce158d6266
child 41860 49d0fc8c418c
made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 28 17:53:10 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 28 17:53:10 2011 +0100
     1.3 @@ -327,16 +327,30 @@
     1.4    else
     1.5      s
     1.6  
     1.7 -fun is_higher_order_type (Type (@{type_name fun}, _)) = true
     1.8 -  | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
     1.9 -  | is_higher_order_type _ = false
    1.10 +val evil_nix = 0
    1.11 +val evil_prod = 1
    1.12 +val evil_fun = 2
    1.13 +
    1.14 +(* Returns an approximation of how evil a type is (i.e., how much are we willing
    1.15 +   to try to specialize the argument even if it contains bound variables). *)
    1.16 +fun type_evil (Type (@{type_name fun}, _)) = evil_fun
    1.17 +  | type_evil (Type (s, Ts)) =
    1.18 +    (if s = @{type_name prod} then evil_prod else evil_nix)
    1.19 +    |> fold (Integer.max o type_evil) Ts
    1.20 +  | type_evil _ = evil_nix
    1.21 +
    1.22 +fun is_higher_order_type T = (type_evil T = evil_fun)
    1.23  
    1.24  fun is_special_eligible_arg strict Ts t =
    1.25 -  let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
    1.26 -    null bad_Ts orelse
    1.27 -    (is_higher_order_type (fastype_of1 (Ts, t)) andalso
    1.28 -     not strict orelse forall (not o is_higher_order_type) bad_Ts)
    1.29 -  end
    1.30 +  case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of
    1.31 +    [] => true
    1.32 +  | bad_Ts =>
    1.33 +    case type_evil (fastype_of1 (Ts, t)) of
    1.34 +      0 => false
    1.35 +    | T_evil =>
    1.36 +      let val bad_Ts_evil = fold (Integer.max o type_evil) bad_Ts evil_nix in
    1.37 +        (bad_Ts_evil, T_evil) |> (if strict then op < else op <=)
    1.38 +      end
    1.39  
    1.40  fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
    1.41