# HG changeset patch
# User blanchet
# Date 1298911990 -3600
# Node ID 49d0fc8c418ce81206ce15b33b42824b257618ce
# Parent  c3a5912d092265dc132ea9177a90bc09993c900b
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)

diff -r c3a5912d0922 -r 49d0fc8c418c src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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
@@ -66,12 +66,6 @@
   val strip_first_name_sep : string -> string * string
   val original_name : string -> string
   val abs_var : indexname * typ -> term -> term
-  val is_higher_order_type : typ -> bool
-  val is_special_eligible_arg : bool -> typ list -> term -> bool
-  val s_let :
-    typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
-  val s_betapply : typ list -> term * term -> term
-  val s_betapplys : typ list -> term * term list -> term
   val s_conj : term * term -> term
   val s_disj : term * term -> term
   val strip_any_connective : term -> term list * term
@@ -105,6 +99,7 @@
   val is_integer_like_type : typ -> bool
   val is_record_type : typ -> bool
   val is_number_type : Proof.context -> typ -> bool
+  val is_higher_order_type : typ -> bool
   val const_for_iterator_type : typ -> styp
   val strip_n_binders : int -> typ -> typ list * typ
   val nth_range_type : int -> typ -> typ
@@ -165,6 +160,18 @@
   val num_datatype_constrs : hol_context -> typ -> int
   val constr_name_for_sel_like : string -> string
   val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
+  val card_of_type : (typ * int) list -> typ -> int
+  val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
+  val bounded_exact_card_of_type :
+    hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
+  val typical_card_of_type : typ -> int
+  val is_finite_type : hol_context -> typ -> bool
+  val is_small_finite_type : hol_context -> typ -> bool
+  val is_special_eligible_arg : bool -> typ list -> term -> bool
+  val s_let :
+    typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
+  val s_betapply : typ list -> term * term -> term
+  val s_betapplys : typ list -> term * term list -> term
   val discriminate_value : hol_context -> styp -> term -> term
   val select_nth_constr_arg :
     Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ
@@ -172,12 +179,6 @@
   val construct_value :
     Proof.context -> (typ option * bool) list -> styp -> term list -> term
   val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
-  val card_of_type : (typ * int) list -> typ -> int
-  val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
-  val bounded_exact_card_of_type :
-    hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
-  val is_finite_type : hol_context -> typ -> bool
-  val is_small_finite_type : hol_context -> typ -> bool
   val special_bounds : term list -> (indexname * typ) list
   val is_funky_typedef : Proof.context -> typ -> bool
   val all_axioms_of :
@@ -327,82 +328,6 @@
   else
     s
 
-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 =
-  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))
-
-fun let_var s = (nitpick_prefix ^ s, 999)
-val let_inline_threshold = 20
-
-fun s_let Ts s n abs_T body_T f t =
-  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
-     is_special_eligible_arg false Ts t then
-    f t
-  else
-    let val z = (let_var s, abs_T) in
-      Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
-      $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
-    end
-
-fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0
-  | loose_bvar1_count (t1 $ t2, k) =
-    loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k)
-  | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
-  | loose_bvar1_count _ = 0
-
-fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
-  | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2
-  | s_betapply Ts (Const (@{const_name Let},
-                          Type (_, [bound_T, Type (_, [_, body_T])]))
-                   $ t12 $ Abs (s, T, t13'), t2) =
-    let val body_T' = range_type body_T in
-      Const (@{const_name Let}, bound_T --> (bound_T --> body_T') --> body_T')
-      $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
-    end
-  | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
-    (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
-              (curry betapply t1) t2
-     handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
-  | s_betapply _ (t1, t2) = t1 $ t2
-fun s_betapplys Ts = Library.foldl (s_betapply Ts)
-
-fun s_beta_norm Ts t =
-  let
-    fun aux _ (Var _) = raise Same.SAME
-      | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t')
-      | aux Ts ((t1 as Abs _) $ t2) =
-        Same.commit (aux Ts) (s_betapply Ts (t1, t2))
-      | aux Ts (t1 $ t2) =
-        ((case aux Ts t1 of
-           t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2))
-         | t1 => t1 $ Same.commit (aux Ts) t2)
-        handle Same.SAME => t1 $ aux Ts t2)
-      | aux _ _ = raise Same.SAME
-  in aux Ts t handle Same.SAME => t end
-
 fun s_conj (t1, @{const True}) = t1
   | s_conj (@{const True}, t2) = t2
   | s_conj (t1, t2) =
@@ -568,6 +493,9 @@
       |> these |> null |> not
   | is_frac_type _ _ = false
 fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt
+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
 
 fun iterator_type_for_const gfp (s, T) =
   Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
@@ -1014,6 +942,162 @@
     |> the |> pair s
   end
 
+fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
+    reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
+  | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) =
+    card_of_type assigns T1 * card_of_type assigns T2
+  | card_of_type _ (Type (@{type_name itself}, _)) = 1
+  | card_of_type _ @{typ prop} = 2
+  | card_of_type _ @{typ bool} = 2
+  | card_of_type assigns T =
+    case AList.lookup (op =) assigns T of
+      SOME k => k
+    | NONE => if T = @{typ bisim_iterator} then 0
+              else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
+
+fun bounded_card_of_type max default_card assigns
+                         (Type (@{type_name fun}, [T1, T2])) =
+    let
+      val k1 = bounded_card_of_type max default_card assigns T1
+      val k2 = bounded_card_of_type max default_card assigns T2
+    in
+      if k1 = max orelse k2 = max then max
+      else Int.min (max, reasonable_power k2 k1)
+    end
+  | bounded_card_of_type max default_card assigns
+                         (Type (@{type_name prod}, [T1, T2])) =
+    let
+      val k1 = bounded_card_of_type max default_card assigns T1
+      val k2 = bounded_card_of_type max default_card assigns T2
+    in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
+  | bounded_card_of_type max default_card assigns T =
+    Int.min (max, if default_card = ~1 then
+                    card_of_type assigns T
+                  else
+                    card_of_type assigns T
+                    handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
+                           default_card)
+
+fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
+                               assigns T =
+  let
+    fun aux avoid T =
+      (if member (op =) avoid T then
+         0
+       else if member (op =) finitizable_dataTs T then
+         raise SAME ()
+       else case T of
+         Type (@{type_name fun}, [T1, T2]) =>
+         let
+           val k1 = aux avoid T1
+           val k2 = aux avoid T2
+         in
+           if k1 = 0 orelse k2 = 0 then 0
+           else if k1 >= max orelse k2 >= max then max
+           else Int.min (max, reasonable_power k2 k1)
+         end
+       | Type (@{type_name prod}, [T1, T2]) =>
+         let
+           val k1 = aux avoid T1
+           val k2 = aux avoid T2
+         in
+           if k1 = 0 orelse k2 = 0 then 0
+           else if k1 >= max orelse k2 >= max then max
+           else Int.min (max, k1 * k2)
+         end
+       | Type (@{type_name itself}, _) => 1
+       | @{typ prop} => 2
+       | @{typ bool} => 2
+       | Type _ =>
+         (case datatype_constrs hol_ctxt T of
+            [] => if is_integer_type T orelse is_bit_type T then 0
+                  else raise SAME ()
+          | constrs =>
+            let
+              val constr_cards =
+                map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
+                    constrs
+            in
+              if exists (curry (op =) 0) constr_cards then 0
+              else Integer.sum constr_cards
+            end)
+       | _ => raise SAME ())
+      handle SAME () =>
+             AList.lookup (op =) assigns T |> the_default default_card
+  in Int.min (max, aux [] T) end
+
+val typical_atomic_card = 4
+val typical_card_of_type = bounded_card_of_type 65536 typical_atomic_card []
+
+val small_type_max_card = 5
+
+fun is_finite_type hol_ctxt T =
+  bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
+fun is_small_finite_type hol_ctxt T =
+  let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
+    n > 0 andalso n <= small_type_max_card
+  end
+
+fun is_special_eligible_arg strict Ts t =
+  case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of
+    [] => true
+  | bad_Ts =>
+    let
+      val bad_Ts_cost = fold (Integer.max o typical_card_of_type) bad_Ts 0
+      val T_cost = typical_card_of_type (fastype_of1 (Ts, t))
+    in (bad_Ts_cost, T_cost) |> (if strict then op < else op <=) end
+
+fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
+
+fun let_var s = (nitpick_prefix ^ s, 999)
+val let_inline_threshold = 20
+
+fun s_let Ts s n abs_T body_T f t =
+  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
+     is_special_eligible_arg false Ts t then
+    f t
+  else
+    let val z = (let_var s, abs_T) in
+      Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
+      $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
+    end
+
+fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0
+  | loose_bvar1_count (t1 $ t2, k) =
+    loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k)
+  | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
+  | loose_bvar1_count _ = 0
+
+fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
+  | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2
+  | s_betapply Ts (Const (@{const_name Let},
+                          Type (_, [bound_T, Type (_, [_, body_T])]))
+                   $ t12 $ Abs (s, T, t13'), t2) =
+    let val body_T' = range_type body_T in
+      Const (@{const_name Let}, bound_T --> (bound_T --> body_T') --> body_T')
+      $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
+    end
+  | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
+    (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
+              (curry betapply t1) t2
+     handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
+  | s_betapply _ (t1, t2) = t1 $ t2
+fun s_betapplys Ts = Library.foldl (s_betapply Ts)
+
+fun s_beta_norm Ts t =
+  let
+    fun aux _ (Var _) = raise Same.SAME
+      | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t')
+      | aux Ts ((t1 as Abs _) $ t2) =
+        Same.commit (aux Ts) (s_betapply Ts (t1, t2))
+      | aux Ts (t1 $ t2) =
+        ((case aux Ts t1 of
+           t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2))
+         | t1 => t1 $ Same.commit (aux Ts) t2)
+        handle Same.SAME => t1 $ aux Ts t2)
+      | aux _ _ = raise Same.SAME
+  in aux Ts t handle Same.SAME => t end
+
 fun discr_term_for_constr hol_ctxt (x as (s, T)) =
   let val dataT = body_type T in
     if s = @{const_name Suc} then
@@ -1150,97 +1234,6 @@
         raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
     | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
 
-fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
-    reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
-  | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) =
-    card_of_type assigns T1 * card_of_type assigns T2
-  | card_of_type _ (Type (@{type_name itself}, _)) = 1
-  | card_of_type _ @{typ prop} = 2
-  | card_of_type _ @{typ bool} = 2
-  | card_of_type assigns T =
-    case AList.lookup (op =) assigns T of
-      SOME k => k
-    | NONE => if T = @{typ bisim_iterator} then 0
-              else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
-fun bounded_card_of_type max default_card assigns
-                         (Type (@{type_name fun}, [T1, T2])) =
-    let
-      val k1 = bounded_card_of_type max default_card assigns T1
-      val k2 = bounded_card_of_type max default_card assigns T2
-    in
-      if k1 = max orelse k2 = max then max
-      else Int.min (max, reasonable_power k2 k1)
-    end
-  | bounded_card_of_type max default_card assigns
-                         (Type (@{type_name prod}, [T1, T2])) =
-    let
-      val k1 = bounded_card_of_type max default_card assigns T1
-      val k2 = bounded_card_of_type max default_card assigns T2
-    in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
-  | bounded_card_of_type max default_card assigns T =
-    Int.min (max, if default_card = ~1 then
-                    card_of_type assigns T
-                  else
-                    card_of_type assigns T
-                    handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
-                           default_card)
-fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
-                               assigns T =
-  let
-    fun aux avoid T =
-      (if member (op =) avoid T then
-         0
-       else if member (op =) finitizable_dataTs T then
-         raise SAME ()
-       else case T of
-         Type (@{type_name fun}, [T1, T2]) =>
-         let
-           val k1 = aux avoid T1
-           val k2 = aux avoid T2
-         in
-           if k1 = 0 orelse k2 = 0 then 0
-           else if k1 >= max orelse k2 >= max then max
-           else Int.min (max, reasonable_power k2 k1)
-         end
-       | Type (@{type_name prod}, [T1, T2]) =>
-         let
-           val k1 = aux avoid T1
-           val k2 = aux avoid T2
-         in
-           if k1 = 0 orelse k2 = 0 then 0
-           else if k1 >= max orelse k2 >= max then max
-           else Int.min (max, k1 * k2)
-         end
-       | Type (@{type_name itself}, _) => 1
-       | @{typ prop} => 2
-       | @{typ bool} => 2
-       | Type _ =>
-         (case datatype_constrs hol_ctxt T of
-            [] => if is_integer_type T orelse is_bit_type T then 0
-                  else raise SAME ()
-          | constrs =>
-            let
-              val constr_cards =
-                map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
-                    constrs
-            in
-              if exists (curry (op =) 0) constr_cards then 0
-              else Integer.sum constr_cards
-            end)
-       | _ => raise SAME ())
-      handle SAME () =>
-             AList.lookup (op =) assigns T |> the_default default_card
-  in Int.min (max, aux [] T) end
-
-val small_type_max_card = 5
-
-fun is_finite_type hol_ctxt T =
-  bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
-fun is_small_finite_type hol_ctxt T =
-  let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
-    n > 0 andalso n <= small_type_max_card
-  end
-
 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
   | is_ground_term (Const _) = true
   | is_ground_term _ = false
diff -r c3a5912d0922 -r 49d0fc8c418c src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 28 17:53:10 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 28 17:53:10 2011 +0100
@@ -1165,12 +1165,10 @@
                  aux "" [] [] t1 $ aux "" [] [] t2
                else
                  let
-                   val typical_card = 4
                    fun big_union proj ps =
                      fold (fold (insert (op =)) o proj) ps []
                    val (ts, connective) = strip_any_connective t
-                   val T_costs =
-                     map (bounded_card_of_type 65536 typical_card []) Ts
+                   val T_costs = map typical_card_of_type Ts
                    val t_costs = map size_of_term ts
                    val num_Ts = length Ts
                    val flip = curry (op -) (num_Ts - 1)