src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41045 2a41709f34c1
parent 40132 7ee65dbffa31
child 41046 f2e94005d283
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 09:58:56 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
     1.3 @@ -65,6 +65,7 @@
     1.4    val strip_first_name_sep : string -> string * string
     1.5    val original_name : string -> string
     1.6    val abs_var : indexname * typ -> term -> term
     1.7 +  val is_higher_order_type : typ -> bool
     1.8    val s_let : string -> int -> typ -> typ -> (term -> term) -> term -> term
     1.9    val s_betapply : typ list -> term * term -> term
    1.10    val s_betapplys : typ list -> term * term list -> term
    1.11 @@ -87,7 +88,6 @@
    1.12    val term_match : theory -> term * term -> bool
    1.13    val frac_from_term_pair : typ -> term -> term -> term
    1.14    val is_TFree : typ -> bool
    1.15 -  val is_higher_order_type : typ -> bool
    1.16    val is_fun_type : typ -> bool
    1.17    val is_set_type : typ -> bool
    1.18    val is_pair_type : typ -> bool
    1.19 @@ -319,13 +319,18 @@
    1.20    else
    1.21      s
    1.22  
    1.23 +fun is_higher_order_type (Type (@{type_name fun}, _)) = true
    1.24 +  | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    1.25 +  | is_higher_order_type _ = false
    1.26 +
    1.27  fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
    1.28  
    1.29  fun let_var s = (nitpick_prefix ^ s, 999)
    1.30  val let_inline_threshold = 20
    1.31  
    1.32  fun s_let s n abs_T body_T f t =
    1.33 -  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold then
    1.34 +  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
    1.35 +     is_higher_order_type abs_T then
    1.36      f t
    1.37    else
    1.38      let val z = (let_var s, abs_T) in
    1.39 @@ -512,9 +517,6 @@
    1.40  
    1.41  fun is_TFree (TFree _) = true
    1.42    | is_TFree _ = false
    1.43 -fun is_higher_order_type (Type (@{type_name fun}, _)) = true
    1.44 -  | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    1.45 -  | is_higher_order_type _ = false
    1.46  fun is_fun_type (Type (@{type_name fun}, _)) = true
    1.47    | is_fun_type _ = false
    1.48  fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
    1.49 @@ -1658,6 +1660,8 @@
    1.50            do_term depth Ts t2
    1.51          else
    1.52            do_const depth Ts t x [t1, t2, t3]
    1.53 +      | Const (@{const_name Let}, _) $ t1 $ t2 =>
    1.54 +        s_betapply Ts (pairself (do_term depth Ts) (t2, t1))
    1.55        | Const x => do_const depth Ts t x []
    1.56        | t1 $ t2 =>
    1.57          (case strip_comb t of