src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41793 c7a2669ae75d
parent 41792 ff3cb0c418b7
child 41795 79a79460b70c
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 10:44:19 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 11:50:31 2011 +0100
     1.3 @@ -66,7 +66,9 @@
     1.4    val original_name : string -> string
     1.5    val abs_var : indexname * typ -> term -> term
     1.6    val is_higher_order_type : typ -> bool
     1.7 -  val s_let : string -> int -> typ -> typ -> (term -> term) -> term -> term
     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    val s_betapply : typ list -> term * term -> term
    1.12    val s_betapplys : typ list -> term * term list -> term
    1.13    val s_conj : term * term -> term
    1.14 @@ -327,14 +329,23 @@
    1.15    | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    1.16    | is_higher_order_type _ = false
    1.17  
    1.18 +fun is_special_eligible_arg strict Ts t =
    1.19 +  let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
    1.20 +    null bad_Ts orelse
    1.21 +    (is_higher_order_type (fastype_of1 (Ts, t)) andalso
    1.22 +     not strict orelse forall (not o is_higher_order_type) bad_Ts)
    1.23 +  end
    1.24 +
    1.25  fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
    1.26  
    1.27  fun let_var s = (nitpick_prefix ^ s, 999)
    1.28  val let_inline_threshold = 20
    1.29  
    1.30 -fun s_let s n abs_T body_T f t =
    1.31 +fun s_let Ts s n abs_T body_T f t =
    1.32    if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
    1.33 -     is_higher_order_type abs_T then
    1.34 +     is_special_eligible_arg true Ts t then
    1.35 +     (* TODO: the "true" argument to "is_special_eligible_arg" should perhaps be
    1.36 +        "false" instead to account for potential future specializations. *)
    1.37      f t
    1.38    else
    1.39      let val z = (let_var s, abs_T) in
    1.40 @@ -358,7 +369,7 @@
    1.41        $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
    1.42      end
    1.43    | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
    1.44 -    (s_let s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
    1.45 +    (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
    1.46                (curry betapply t1) t2
    1.47       handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
    1.48    | s_betapply _ (t1, t2) = t1 $ t2
    1.49 @@ -1617,7 +1628,7 @@
    1.50  
    1.51  (* Inline definitions or define as an equational constant? Booleans tend to
    1.52     benefit more from inlining, due to the polarity analysis. *)
    1.53 -val def_inline_threshold_for_booleans = 50
    1.54 +val def_inline_threshold_for_booleans = 60
    1.55  val def_inline_threshold_for_non_booleans = 20
    1.56  
    1.57  fun unfold_defs_in_term