made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 28 17:53:10 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 28 17:53:10 2011 +0100
@@ -327,16 +327,30 @@
else
s
-fun is_higher_order_type (Type (@{type_name fun}, _)) = true
- | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
- | is_higher_order_type _ = false
+val evil_nix = 0
+val evil_prod = 1
+val evil_fun = 2
+
+(* Returns an approximation of how evil a type is (i.e., how much are we willing
+ to try to specialize the argument even if it contains bound variables). *)
+fun type_evil (Type (@{type_name fun}, _)) = evil_fun
+ | type_evil (Type (s, Ts)) =
+ (if s = @{type_name prod} then evil_prod else evil_nix)
+ |> fold (Integer.max o type_evil) Ts
+ | type_evil _ = evil_nix
+
+fun is_higher_order_type T = (type_evil T = evil_fun)
fun is_special_eligible_arg strict Ts t =
- let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
- null bad_Ts orelse
- (is_higher_order_type (fastype_of1 (Ts, t)) andalso
- not strict orelse forall (not o is_higher_order_type) bad_Ts)
- end
+ case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of
+ [] => true
+ | bad_Ts =>
+ case type_evil (fastype_of1 (Ts, t)) of
+ 0 => false
+ | T_evil =>
+ let val bad_Ts_evil = fold (Integer.max o type_evil) bad_Ts evil_nix in
+ (bad_Ts_evil, T_evil) |> (if strict then op < else op <=)
+ end
fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))