optimized code generated for datatype cases + more;
authorblanchet
Mon Jun 21 11:15:21 2010 +0200 (2010-06-21)
changeset 374760681e46b4022
parent 37475 98c6f9dc58d0
child 37477 e482320bcbfe
optimized code generated for datatype cases + more;
more = lazy creation of debugging messages in mono code
+ use of "let" when performing some beta-applications (to avoid exponential blowup)
+ removal of some set constructs, to simplify the code and increase precision in some cases (and decrease it in others, but this can be regained)
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Jun 21 09:38:20 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Jun 21 11:15:21 2010 +0200
     1.3 @@ -64,6 +64,10 @@
     1.4    val iter_var_prefix : string
     1.5    val strip_first_name_sep : string -> string * string
     1.6    val original_name : string -> string
     1.7 +  val abs_var : indexname * typ -> term -> term
     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    val s_conj : term * term -> term
    1.12    val s_disj : term * term -> term
    1.13    val strip_any_connective : term -> term list * term
    1.14 @@ -162,7 +166,6 @@
    1.15    val is_finite_type : hol_context -> typ -> bool
    1.16    val is_small_finite_type : hol_context -> typ -> bool
    1.17    val special_bounds : term list -> (indexname * typ) list
    1.18 -  val abs_var : indexname * typ -> term -> term
    1.19    val is_funky_typedef : theory -> typ -> bool
    1.20    val all_axioms_of :
    1.21      Proof.context -> (term * term) list -> term list * term list * term list
    1.22 @@ -302,10 +305,55 @@
    1.23    else
    1.24      s
    1.25  
    1.26 -fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
    1.27 -  | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
    1.28 -  | s_betapply p = betapply p
    1.29 -val s_betapplys = Library.foldl s_betapply
    1.30 +fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
    1.31 +
    1.32 +fun let_var s = (nitpick_prefix ^ s, 999)
    1.33 +val let_inline_threshold = 20
    1.34 +
    1.35 +fun s_let s n abs_T body_T f t =
    1.36 +  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold then
    1.37 +    f t
    1.38 +  else
    1.39 +    let val z = (let_var s, abs_T) in
    1.40 +      Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
    1.41 +      $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
    1.42 +    end
    1.43 +
    1.44 +fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0
    1.45 +  | loose_bvar1_count (t1 $ t2, k) =
    1.46 +    loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k)
    1.47 +  | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
    1.48 +  | loose_bvar1_count _ = 0
    1.49 +
    1.50 +fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
    1.51 +  | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2
    1.52 +  | s_betapply Ts (Const (@{const_name Let},
    1.53 +                          Type (_, [bound_T, Type (_, [_, body_T])]))
    1.54 +                   $ t12 $ Abs (s, T, t13'), t2) =
    1.55 +    let val body_T' = range_type body_T in
    1.56 +      Const (@{const_name Let}, bound_T --> (bound_T --> body_T') --> body_T')
    1.57 +      $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
    1.58 +    end
    1.59 +  | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
    1.60 +    (s_let s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
    1.61 +              (curry betapply t1) t2
    1.62 +     handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
    1.63 +  | s_betapply _ (t1, t2) = t1 $ t2
    1.64 +fun s_betapplys Ts = Library.foldl (s_betapply Ts)
    1.65 +
    1.66 +fun s_beta_norm Ts t =
    1.67 +  let
    1.68 +    fun aux _ (Var _) = raise Same.SAME
    1.69 +      | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t')
    1.70 +      | aux Ts ((t1 as Abs _) $ t2) =
    1.71 +        Same.commit (aux Ts) (s_betapply Ts (t1, t2))
    1.72 +      | aux Ts (t1 $ t2) =
    1.73 +        ((case aux Ts t1 of
    1.74 +           t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2))
    1.75 +         | t1 => t1 $ Same.commit (aux Ts) t2)
    1.76 +        handle Same.SAME => t1 $ aux Ts t2)
    1.77 +      | aux _ _ = raise Same.SAME
    1.78 +  in aux Ts t handle Same.SAME => t end
    1.79  
    1.80  fun s_conj (t1, @{const True}) = t1
    1.81    | s_conj (@{const True}, t2) = t2
    1.82 @@ -344,7 +392,7 @@
    1.83     (@{const_name True}, 0),
    1.84     (@{const_name All}, 1),
    1.85     (@{const_name Ex}, 1),
    1.86 -   (@{const_name "op ="}, 2),
    1.87 +   (@{const_name "op ="}, 1),
    1.88     (@{const_name "op &"}, 2),
    1.89     (@{const_name "op |"}, 2),
    1.90     (@{const_name "op -->"}, 2),
    1.91 @@ -355,7 +403,6 @@
    1.92     (@{const_name fst}, 1),
    1.93     (@{const_name snd}, 1),
    1.94     (@{const_name Id}, 0),
    1.95 -   (@{const_name insert}, 2),
    1.96     (@{const_name converse}, 1),
    1.97     (@{const_name trancl}, 1),
    1.98     (@{const_name rel_comp}, 2),
    1.99 @@ -396,10 +443,7 @@
   1.100     ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
   1.101     ((@{const_name of_nat}, nat_T --> int_T), 0)]
   1.102  val built_in_set_consts =
   1.103 -  [(@{const_name semilattice_inf_class.inf}, 2),
   1.104 -   (@{const_name semilattice_sup_class.sup}, 2),
   1.105 -   (@{const_name minus_class.minus}, 2),
   1.106 -   (@{const_name ord_class.less_eq}, 2)]
   1.107 +  [(@{const_name ord_class.less_eq}, 2)]
   1.108  
   1.109  fun unarize_type @{typ "unsigned_bit word"} = nat_T
   1.110    | unarize_type @{typ "signed_bit word"} = int_T
   1.111 @@ -924,8 +968,8 @@
   1.112      Const x' =>
   1.113      if x = x' then @{const True}
   1.114      else if is_constr_like ctxt x' then @{const False}
   1.115 -    else betapply (discr_term_for_constr hol_ctxt x, t)
   1.116 -  | _ => betapply (discr_term_for_constr hol_ctxt x, t)
   1.117 +    else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
   1.118 +  | _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
   1.119  
   1.120  fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
   1.121    let val (arg_Ts, dataT) = strip_type T in
   1.122 @@ -955,7 +999,8 @@
   1.123         else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T)
   1.124         else raise SAME ()
   1.125       | _ => raise SAME())
   1.126 -    handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
   1.127 +    handle SAME () =>
   1.128 +           s_betapply [] (nth_arg_sel_term_for_constr thy stds x n, t)
   1.129    end
   1.130  
   1.131  fun construct_value _ _ x [] = Const x
   1.132 @@ -1150,8 +1195,6 @@
   1.133  fun special_bounds ts =
   1.134    fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
   1.135  
   1.136 -fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
   1.137 -
   1.138  fun is_funky_typedef_name thy s =
   1.139    member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
   1.140                   @{type_name int}] s orelse
   1.141 @@ -1309,7 +1352,8 @@
   1.142       original_name s <> s then
   1.143      NONE
   1.144    else
   1.145 -    x |> def_props_for_const thy [(NONE, false)] false table |> List.last
   1.146 +    x |> def_props_for_const thy [(NONE, false)] false table
   1.147 +      |> List.last
   1.148        |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
   1.149      handle List.Empty => NONE
   1.150  
   1.151 @@ -1458,25 +1502,44 @@
   1.152  
   1.153  (** Constant unfolding **)
   1.154  
   1.155 -fun constr_case_body ctxt stds (j, (x as (_, T))) =
   1.156 +fun constr_case_body ctxt stds (func_t, (x as (_, T))) =
   1.157    let val arg_Ts = binder_types T in
   1.158 -    list_comb (Bound j, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
   1.159 -                             (index_seq 0 (length arg_Ts)) arg_Ts)
   1.160 +    s_betapplys [] (func_t, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
   1.161 +                                 (index_seq 0 (length arg_Ts)) arg_Ts)
   1.162    end
   1.163 -fun add_constr_case (hol_ctxt as {ctxt, stds, ...}) res_T (j, x) res_t =
   1.164 -  Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
   1.165 -  $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body ctxt stds (j, x)
   1.166 -  $ res_t
   1.167 -fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T =
   1.168 +fun add_constr_case res_T (body_t, guard_t) res_t =
   1.169 +  if res_T = bool_T then
   1.170 +    s_conj (HOLogic.mk_imp (guard_t, body_t), res_t)
   1.171 +  else
   1.172 +    Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
   1.173 +    $ guard_t $ body_t $ res_t
   1.174 +fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T func_ts =
   1.175    let
   1.176      val xs = datatype_constrs hol_ctxt dataT
   1.177 -    val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
   1.178 -    val (xs', x) = split_last xs
   1.179 +    val cases =
   1.180 +      func_ts ~~ xs
   1.181 +      |> map (fn (func_t, x) =>
   1.182 +                 (constr_case_body ctxt stds (incr_boundvars 1 func_t, x),
   1.183 +                  discriminate_value hol_ctxt x (Bound 0)))
   1.184 +      |> AList.group (op aconv)
   1.185 +      |> map (apsnd (List.foldl s_disj @{const False}))
   1.186 +      |> sort (int_ord o pairself (size_of_term o fst))
   1.187 +      |> rev
   1.188    in
   1.189 -    constr_case_body ctxt stds (1, x)
   1.190 -    |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
   1.191 -    |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   1.192 +    if res_T = bool_T then
   1.193 +      if forall (member (op =) [@{const False}, @{const True}] o fst) cases then
   1.194 +        case cases of
   1.195 +          [(body_t, _)] => body_t
   1.196 +        | [_, (@{const True}, head_t2)] => head_t2
   1.197 +        | [_, (@{const False}, head_t2)] => @{const Not} $ head_t2
   1.198 +        | _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases")
   1.199 +      else 
   1.200 +        @{const True} |> fold_rev (add_constr_case res_T) cases
   1.201 +    else
   1.202 +      fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
   1.203    end
   1.204 +  |> curry absdummy dataT
   1.205 +
   1.206  fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
   1.207    let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
   1.208      case no_of_record_field thy s rec_T of
   1.209 @@ -1504,7 +1567,7 @@
   1.210        map2 (fn j => fn T =>
   1.211                 let val t = select_nth_constr_arg ctxt stds constr_x rec_t j T in
   1.212                   if j = special_j then
   1.213 -                   betapply (fun_t, t)
   1.214 +                   s_betapply [] (fun_t, t)
   1.215                   else if j = n - 1 andalso special_j = ~1 then
   1.216                     optimized_record_update hol_ctxt s
   1.217                         (rec_T |> dest_Type |> snd |> List.last) fun_t t
   1.218 @@ -1542,12 +1605,13 @@
   1.219              handle TERM _ => raise SAME ()
   1.220            else
   1.221              raise SAME ())
   1.222 -         handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
   1.223 +         handle SAME () =>
   1.224 +                s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
   1.225        | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
   1.226          do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
   1.227        | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
   1.228 -        betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
   1.229 -                   map (do_term depth Ts) [t1, t2])
   1.230 +        s_betapplys Ts (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
   1.231 +                        map (do_term depth Ts) [t1, t2])
   1.232        | Const (x as (@{const_name distinct},
   1.233                 Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
   1.234          $ (t1 as _ $ _) =>
   1.235 @@ -1560,11 +1624,11 @@
   1.236            do_term depth Ts t2
   1.237          else
   1.238            do_const depth Ts t x [t1, t2, t3]
   1.239 -      | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3]
   1.240 -      | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2]
   1.241 -      | Const x $ t1 => do_const depth Ts t x [t1]
   1.242        | Const x => do_const depth Ts t x []
   1.243 -      | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2)
   1.244 +      | t1 $ t2 =>
   1.245 +        (case strip_comb t of
   1.246 +           (Const x, ts) => do_const depth Ts t x ts
   1.247 +         | _ => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2))
   1.248        | Free _ => t
   1.249        | Var _ => t
   1.250        | Bound _ => t
   1.251 @@ -1585,13 +1649,17 @@
   1.252                (Const x, ts)
   1.253              else case AList.lookup (op =) case_names s of
   1.254                SOME n =>
   1.255 -              let
   1.256 -                val (dataT, res_T) = nth_range_type n T
   1.257 -                                     |> pairf domain_type range_type
   1.258 -              in
   1.259 -                (optimized_case_def hol_ctxt dataT res_T
   1.260 -                 |> do_term (depth + 1) Ts, ts)
   1.261 -              end
   1.262 +              if length ts < n then
   1.263 +                (do_term depth Ts (eta_expand Ts t (n - length ts)), [])
   1.264 +              else
   1.265 +                let
   1.266 +                  val (dataT, res_T) = nth_range_type n T
   1.267 +                                       |> pairf domain_type range_type
   1.268 +                in
   1.269 +                  (optimized_case_def hol_ctxt dataT res_T
   1.270 +                                      (map (do_term depth Ts) (take n ts)),
   1.271 +                   drop n ts)
   1.272 +                end
   1.273              | _ =>
   1.274                if is_constr ctxt stds x then
   1.275                  (Const x, ts)
   1.276 @@ -1645,11 +1713,14 @@
   1.277                                     string_of_int depth ^ ") while expanding " ^
   1.278                                     quote s)
   1.279                  else if s = @{const_name wfrec'} then
   1.280 -                  (do_term (depth + 1) Ts (betapplys (def, ts)), [])
   1.281 +                  (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
   1.282                  else
   1.283                    (do_term (depth + 1) Ts def, ts)
   1.284                | NONE => (Const x, ts)
   1.285 -        in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
   1.286 +        in
   1.287 +          s_betapplys Ts (const, map (do_term depth Ts) ts)
   1.288 +          |> s_beta_norm Ts
   1.289 +        end
   1.290    in do_term 0 [] end
   1.291  
   1.292  (** Axiom extraction/generation **)
   1.293 @@ -1796,8 +1867,9 @@
   1.294    in
   1.295      [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
   1.296       $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
   1.297 -        $ (betapplys (optimized_case_def hol_ctxt T bool_T,
   1.298 -                      map case_func xs @ [x_var]))),
   1.299 +        $ (s_betapply []
   1.300 +                      (optimized_case_def hol_ctxt T bool_T (map case_func xs),
   1.301 +                       x_var))),
   1.302       HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
   1.303       $ (Const (@{const_name insert}, T --> set_T --> set_T)
   1.304          $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
   1.305 @@ -2036,11 +2108,12 @@
   1.306          val outer_bounds = map Bound (length outer - 1 downto 0)
   1.307          val cur = Var ((iter_var_prefix, j + 1), iter_T)
   1.308          val next = suc_const iter_T $ cur
   1.309 -        val rhs = case fp_app of
   1.310 -                    Const _ $ t =>
   1.311 -                    betapply (t, list_comb (Const x', next :: outer_bounds))
   1.312 -                  | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
   1.313 -                                     \const", [fp_app])
   1.314 +        val rhs =
   1.315 +          case fp_app of
   1.316 +            Const _ $ t =>
   1.317 +            s_betapply [] (t, list_comb (Const x', next :: outer_bounds))
   1.318 +          | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_const",
   1.319 +                             [fp_app])
   1.320          val (inner, naked_rhs) = strip_abs rhs
   1.321          val all = outer @ inner
   1.322          val bounds = map Bound (length all - 1 downto 0)
   1.323 @@ -2056,10 +2129,10 @@
   1.324      val def = the (def_of_const thy def_table x)
   1.325      val (outer, fp_app) = strip_abs def
   1.326      val outer_bounds = map Bound (length outer - 1 downto 0)
   1.327 -    val rhs = case fp_app of
   1.328 -                Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
   1.329 -              | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
   1.330 -                                 [fp_app])
   1.331 +    val rhs =
   1.332 +      case fp_app of
   1.333 +        Const _ $ t => s_betapply [] (t, list_comb (Const x, outer_bounds))
   1.334 +      | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom", [fp_app])
   1.335      val (inner, naked_rhs) = strip_abs rhs
   1.336      val all = outer @ inner
   1.337      val bounds = map Bound (length all - 1 downto 0)
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Jun 21 09:38:20 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Jun 21 11:15:21 2010 +0200
     2.3 @@ -866,24 +866,8 @@
     2.4        | _ => kk_rel_eq r (KK.Atom (j0 + 1))
     2.5      val formula_from_atom = formula_from_opt_atom Pos
     2.6  
     2.7 -    fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2)
     2.8 -    val kk_or3 =
     2.9 -      double_rel_rel_let kk
    2.10 -          (fn r1 => fn r2 =>
    2.11 -              kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom
    2.12 -                        (kk_intersect r1 r2))
    2.13 -    val kk_and3 =
    2.14 -      double_rel_rel_let kk
    2.15 -          (fn r1 => fn r2 =>
    2.16 -              kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom
    2.17 -                        (kk_intersect r1 r2))
    2.18 -    fun kk_notimplies3 r1 r2 = kk_and3 r1 (kk_not3 r2)
    2.19 -
    2.20      val unpack_formulas =
    2.21        map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1
    2.22 -    fun kk_vect_set_op connective k r1 r2 =
    2.23 -      fold1 kk_product (map2 (atom_from_formula kk bool_j0 oo connective)
    2.24 -                             (unpack_formulas k r1) (unpack_formulas k r2))
    2.25      fun kk_vect_set_bool_op connective k r1 r2 =
    2.26        fold1 kk_and (map2 connective (unpack_formulas k r1)
    2.27                           (unpack_formulas k r2))
    2.28 @@ -1369,14 +1353,6 @@
    2.29              kk_union (kk_rel_if f1 true_atom KK.None)
    2.30                       (kk_rel_if f2 KK.None false_atom)
    2.31          end
    2.32 -      | Op2 (Union, _, R, u1, u2) =>
    2.33 -        to_set_op kk_or kk_or3 kk_union kk_union kk_intersect false R u1 u2
    2.34 -      | Op2 (SetDifference, _, R, u1, u2) =>
    2.35 -        to_set_op kk_notimplies kk_notimplies3 kk_difference kk_intersect
    2.36 -                  kk_union true R u1 u2
    2.37 -      | Op2 (Intersect, _, R, u1, u2) =>
    2.38 -        to_set_op kk_and kk_and3 kk_intersect kk_intersect kk_union false R
    2.39 -                  u1 u2
    2.40        | Op2 (Composition, _, R, u1, u2) =>
    2.41          let
    2.42            val (a_T, b_T) = HOLogic.dest_prodT (domain_type (type_of u1))
    2.43 @@ -1644,37 +1620,6 @@
    2.44                                         (kk_join r2 true_atom)
    2.45          | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
    2.46        end
    2.47 -    and to_set_op connective connective3 set_oper true_set_oper false_set_oper
    2.48 -                  neg_second R u1 u2 =
    2.49 -      let
    2.50 -        val min_R = min_rep (rep_of u1) (rep_of u2)
    2.51 -        val r1 = to_rep min_R u1
    2.52 -        val r2 = to_rep min_R u2
    2.53 -        val unopt_R = unopt_rep R
    2.54 -      in
    2.55 -        rel_expr_from_rel_expr kk unopt_R (unopt_rep min_R)
    2.56 -            (case min_R of
    2.57 -               Opt (Vect (k, Atom _)) => kk_vect_set_op connective k r1 r2
    2.58 -             | Vect (k, Atom _) => kk_vect_set_op connective k r1 r2
    2.59 -             | Func (_, Formula Neut) => set_oper r1 r2
    2.60 -             | Func (Unit, _) => connective3 r1 r2
    2.61 -             | Func _ =>
    2.62 -               double_rel_rel_let kk
    2.63 -                   (fn r1 => fn r2 =>
    2.64 -                       kk_union
    2.65 -                           (kk_product
    2.66 -                                (true_set_oper (kk_join r1 true_atom)
    2.67 -                                     (kk_join r2 (atom_for_bool bool_j0
    2.68 -                                                             (not neg_second))))
    2.69 -                                true_atom)
    2.70 -                           (kk_product
    2.71 -                                (false_set_oper (kk_join r1 false_atom)
    2.72 -                                     (kk_join r2 (atom_for_bool bool_j0
    2.73 -                                                                neg_second)))
    2.74 -                                false_atom))
    2.75 -                   r1 r2
    2.76 -             | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
    2.77 -      end
    2.78      and to_bit_word_unary_op T R oper =
    2.79        let
    2.80          val Ts = strip_type T ||> single |> op @
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Jun 21 09:38:20 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Jun 21 11:15:21 2010 +0200
     3.3 @@ -54,8 +54,9 @@
     3.4  exception MTYPE of string * mtyp list * typ list
     3.5  exception MTERM of string * mterm list
     3.6  
     3.7 -fun print_g (_ : string) = ()
     3.8 -(* val print_g = tracing *)
     3.9 +val debug_mono = false
    3.10 +
    3.11 +fun print_g f = () |> debug_mono ? tracing o f
    3.12  
    3.13  val string_for_var = signed_string_of_int
    3.14  fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
    3.15 @@ -401,10 +402,10 @@
    3.16                   [M1, M2], [])
    3.17  
    3.18  fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) =
    3.19 -    (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
    3.20 -              " " ^ string_for_mtype M2);
    3.21 +    (print_g (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
    3.22 +                       string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
    3.23       case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
    3.24 -       NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ())
    3.25 +       NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ())
    3.26       | SOME (lits, comps) => (lits, comps, sexps))
    3.27  
    3.28  val add_mtypes_equal = add_mtype_comp Eq
    3.29 @@ -446,10 +447,11 @@
    3.30      raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
    3.31  
    3.32  fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
    3.33 -    (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
    3.34 -              (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
    3.35 +    (print_g (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
    3.36 +                       (case sn of Minus => "concrete" | Plus => "complete") ^
    3.37 +                       ".");
    3.38       case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
    3.39 -       NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ())
    3.40 +       NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ())
    3.41       | SOME (lits, sexps) => (lits, comps, sexps))
    3.42  
    3.43  val add_mtype_is_concrete = add_notin_mtype_fv Minus
    3.44 @@ -491,15 +493,16 @@
    3.45    subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2
    3.46  
    3.47  fun print_problem lits comps sexps =
    3.48 -  print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @
    3.49 -                                         map string_for_comp comps @
    3.50 -                                         map string_for_sign_expr sexps))
    3.51 +  print_g (fn () => "*** Problem:\n" ^
    3.52 +                    cat_lines (map string_for_literal lits @
    3.53 +                               map string_for_comp comps @
    3.54 +                               map string_for_sign_expr sexps))
    3.55  
    3.56  fun print_solution lits =
    3.57    let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
    3.58 -    print_g ("*** Solution:\n" ^
    3.59 -             "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
    3.60 -             "-: " ^ commas (map (string_for_var o fst) neg))
    3.61 +    print_g (fn () => "*** Solution:\n" ^
    3.62 +                      "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
    3.63 +                      "-: " ^ commas (map (string_for_var o fst) neg))
    3.64    end
    3.65  
    3.66  fun solve max_var (lits, comps, sexps) =
    3.67 @@ -550,6 +553,12 @@
    3.68                                            def_table, ...},
    3.69                               alpha_T, max_fresh, ...}) =
    3.70    let
    3.71 +    fun is_enough_eta_expanded t =
    3.72 +      case strip_comb t of
    3.73 +        (Const x, ts) =>
    3.74 +        the_default 0 (arity_of_built_in_const thy stds fast_descrs x)
    3.75 +        <= length ts
    3.76 +      | _ => true
    3.77      val mtype_for = fresh_mtype_for_type mdata false
    3.78      fun plus_set_mtype_for_dom M =
    3.79        MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
    3.80 @@ -640,8 +649,10 @@
    3.81                    |>> mtype_of_mterm
    3.82                  end
    3.83                | @{const_name "op ="} => do_equals T accum
    3.84 -              | @{const_name The} => (print_g "*** The"; raise UNSOLVABLE ())
    3.85 -              | @{const_name Eps} => (print_g "*** Eps"; raise UNSOLVABLE ())
    3.86 +              | @{const_name The} =>
    3.87 +                (print_g (K "*** The"); raise UNSOLVABLE ())
    3.88 +              | @{const_name Eps} =>
    3.89 +                (print_g (K "*** Eps"); raise UNSOLVABLE ())
    3.90                | @{const_name If} =>
    3.91                  do_robust_set_operation (range_type T) accum
    3.92                  |>> curry3 MFun bool_M (S Minus)
    3.93 @@ -650,19 +661,6 @@
    3.94                | @{const_name snd} => do_nth_pair_sel 1 T accum 
    3.95                | @{const_name Id} =>
    3.96                  (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
    3.97 -              | @{const_name insert} =>
    3.98 -                let
    3.99 -                  val set_T = domain_type (range_type T)
   3.100 -                  val M1 = mtype_for (domain_type set_T)
   3.101 -                  val M1' = plus_set_mtype_for_dom M1
   3.102 -                  val M2 = mtype_for set_T
   3.103 -                  val M3 = mtype_for set_T
   3.104 -                in
   3.105 -                  (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
   3.106 -                   (gamma, cset |> add_mtype_is_concrete M1
   3.107 -                                |> add_is_sub_mtype M1' M3
   3.108 -                                |> add_is_sub_mtype M2 M3))
   3.109 -                end
   3.110                | @{const_name converse} =>
   3.111                  let
   3.112                    val x = Unsynchronized.inc max_fresh
   3.113 @@ -720,25 +718,9 @@
   3.114                      val a_set_M = mtype_for (domain_type T)
   3.115                      val a_M = dest_MFun a_set_M |> #1
   3.116                    in (MFun (a_set_M, S Minus, a_M), accum) end
   3.117 -                else if s = @{const_name minus_class.minus} andalso
   3.118 -                        is_set_type (domain_type T) then
   3.119 -                  let
   3.120 -                    val set_T = domain_type T
   3.121 -                    val left_set_M = mtype_for set_T
   3.122 -                    val right_set_M = mtype_for set_T
   3.123 -                  in
   3.124 -                    (MFun (left_set_M, S Minus,
   3.125 -                           MFun (right_set_M, S Minus, left_set_M)),
   3.126 -                     (gamma, cset |> add_mtype_is_concrete right_set_M
   3.127 -                                  |> add_is_sub_mtype right_set_M left_set_M))
   3.128 -                  end
   3.129                  else if s = @{const_name ord_class.less_eq} andalso
   3.130                          is_set_type (domain_type T) then
   3.131                    do_fragile_set_operation T accum
   3.132 -                else if (s = @{const_name semilattice_inf_class.inf} orelse
   3.133 -                         s = @{const_name semilattice_sup_class.sup}) andalso
   3.134 -                        is_set_type (domain_type T) then
   3.135 -                  do_robust_set_operation T accum
   3.136                  else if is_sel s then
   3.137                    (mtype_for_sel mdata x, accum)
   3.138                  else if is_constr ctxt stds x then
   3.139 @@ -758,7 +740,7 @@
   3.140                  (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
   3.141                        frees = (x, M) :: frees, consts = consts}, cset))
   3.142                end) |>> curry MRaw t
   3.143 -         | Var _ => (print_g "*** Var"; raise UNSOLVABLE ())
   3.144 +         | Var _ => (print_g (K "*** Var"); raise UNSOLVABLE ())
   3.145           | Bound j => (MRaw (t, nth bound_Ms j), accum)
   3.146           | Abs (s, T, t') =>
   3.147             (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
   3.148 @@ -771,10 +753,16 @@
   3.149              | NONE =>
   3.150                ((case t' of
   3.151                    t1' $ Bound 0 =>
   3.152 -                  if not (loose_bvar1 (t1', 0)) then
   3.153 +                  if not (loose_bvar1 (t1', 0)) andalso
   3.154 +                     is_enough_eta_expanded t1' then
   3.155                      do_term (incr_boundvars ~1 t1') accum
   3.156                    else
   3.157                      raise SAME ()
   3.158 +                | (t11 as Const (@{const_name "op ="}, _)) $ Bound 0 $ t13 =>
   3.159 +                  if not (loose_bvar1 (t13, 0)) then
   3.160 +                    do_term (incr_boundvars ~1 (t11 $ t13)) accum
   3.161 +                  else
   3.162 +                    raise SAME ()
   3.163                  | _ => raise SAME ())
   3.164                 handle SAME () =>
   3.165                        let
   3.166 @@ -803,8 +791,8 @@
   3.167                 val M2 = mtype_of_mterm m2
   3.168               in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
   3.169             end)
   3.170 -        |> tap (fn (m, _) => print_g ("  \<Gamma> \<turnstile> " ^
   3.171 -                                      string_for_mterm ctxt m))
   3.172 +        |> tap (fn (m, _) => print_g (fn () => "  \<Gamma> \<turnstile> " ^
   3.173 +                                               string_for_mterm ctxt m))
   3.174    in do_term end
   3.175  
   3.176  fun force_minus_funs 0 _ = I
   3.177 @@ -902,9 +890,9 @@
   3.178            | _ => do_term t accum
   3.179          end
   3.180          |> tap (fn (m, _) =>
   3.181 -                   print_g ("\<Gamma> \<turnstile> " ^
   3.182 -                            string_for_mterm ctxt m ^ " : o\<^sup>" ^
   3.183 -                            string_for_sign sn))
   3.184 +                   print_g (fn () => "\<Gamma> \<turnstile> " ^
   3.185 +                                     string_for_mterm ctxt m ^ " : o\<^sup>" ^
   3.186 +                                     string_for_sign sn))
   3.187    in do_formula end
   3.188  
   3.189  (* The harmless axiom optimization below is somewhat too aggressive in the face
   3.190 @@ -987,9 +975,10 @@
   3.191    Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
   3.192  
   3.193  fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
   3.194 -  map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
   3.195 -  map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
   3.196 -  |> cat_lines |> print_g
   3.197 +  print_g (fn () =>
   3.198 +      map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
   3.199 +      map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
   3.200 +      |> cat_lines)
   3.201  
   3.202  fun amass f t (ms, accum) =
   3.203    let val (m, accum) = f t accum in (m :: ms, accum) end
   3.204 @@ -997,9 +986,9 @@
   3.205  fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
   3.206            (nondef_ts, def_ts) =
   3.207    let
   3.208 -    val _ = print_g ("****** " ^ which ^ " analysis: " ^
   3.209 -                     string_for_mtype MAlpha ^ " is " ^
   3.210 -                     Syntax.string_of_typ ctxt alpha_T)
   3.211 +    val _ = print_g (fn () => "****** " ^ which ^ " analysis: " ^
   3.212 +                              string_for_mtype MAlpha ^ " is " ^
   3.213 +                              Syntax.string_of_typ ctxt alpha_T)
   3.214      val mdata as {max_fresh, constr_mcache, ...} =
   3.215        initial_mdata hol_ctxt binarize no_harmless alpha_T
   3.216      val accum = (initial_gamma, ([], [], []))
   3.217 @@ -1064,26 +1053,21 @@
   3.218              in
   3.219                case t of
   3.220                  Const (x as (s, _)) =>
   3.221 -                if s = @{const_name insert} then
   3.222 -                  case nth_range_type 2 T' of
   3.223 -                    set_T' as Type (@{type_name fin_fun}, [elem_T', _]) =>
   3.224 -                      Abs (Name.uu, elem_T', Abs (Name.uu, set_T',
   3.225 -                          Const (@{const_name If},
   3.226 -                                 bool_T --> set_T' --> set_T' --> set_T')
   3.227 -                          $ (Const (@{const_name is_unknown},
   3.228 -                                    elem_T' --> bool_T) $ Bound 1)
   3.229 -                          $ (Const (@{const_name unknown}, set_T'))
   3.230 -                          $ (coerce_term hol_ctxt new_Ts T' T (Const x)
   3.231 -                             $ Bound 1 $ Bound 0)))
   3.232 -                  | _ => Const (s, T')
   3.233 -                else if s = @{const_name finite} then
   3.234 +                if s = @{const_name finite} then
   3.235                    case domain_type T' of
   3.236                      set_T' as Type (@{type_name fin_fun}, _) =>
   3.237                      Abs (Name.uu, set_T', @{const True})
   3.238                    | _ => Const (s, T')
   3.239                  else if s = @{const_name "=="} orelse
   3.240                          s = @{const_name "op ="} then
   3.241 -                  Const (s, T')
   3.242 +                  let
   3.243 +                    val T =
   3.244 +                      case T' of
   3.245 +                        Type (_, [T1, Type (_, [T2, T3])]) =>
   3.246 +                        T1 --> T2 --> T3
   3.247 +                      | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
   3.248 +                                         \term_from_mterm", [T, T'], [])
   3.249 +                  in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
   3.250                  else if is_built_in_const thy stds fast_descrs x then
   3.251                    coerce_term hol_ctxt new_Ts T' T t
   3.252                  else if is_constr ctxt stds x then
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Jun 21 09:38:20 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Jun 21 11:15:21 2010 +0200
     4.3 @@ -56,9 +56,6 @@
     4.4      The |
     4.5      Eps |
     4.6      Triad |
     4.7 -    Union |
     4.8 -    SetDifference |
     4.9 -    Intersect |
    4.10      Composition |
    4.11      Product |
    4.12      Image |
    4.13 @@ -176,9 +173,6 @@
    4.14    The |
    4.15    Eps |
    4.16    Triad |
    4.17 -  Union |
    4.18 -  SetDifference |
    4.19 -  Intersect |
    4.20    Composition |
    4.21    Product |
    4.22    Image |
    4.23 @@ -247,9 +241,6 @@
    4.24    | string_for_op2 The = "The"
    4.25    | string_for_op2 Eps = "Eps"
    4.26    | string_for_op2 Triad = "Triad"
    4.27 -  | string_for_op2 Union = "Union"
    4.28 -  | string_for_op2 SetDifference = "SetDifference"
    4.29 -  | string_for_op2 Intersect = "Intersect"
    4.30    | string_for_op2 Composition = "Composition"
    4.31    | string_for_op2 Product = "Product"
    4.32    | string_for_op2 Image = "Image"
    4.33 @@ -525,6 +516,8 @@
    4.34            do_description_operator The @{const_name undefined_fast_The} x t1
    4.35          | (Const (x as (@{const_name Eps}, _)), [t1]) =>
    4.36            do_description_operator Eps @{const_name undefined_fast_Eps} x t1
    4.37 +        | (Const (@{const_name "op ="}, T), [t1]) =>
    4.38 +          Op1 (SingletonSet, range_type T, Any, sub t1)
    4.39          | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
    4.40          | (Const (@{const_name "op &"}, _), [t1, t2]) =>
    4.41            Op2 (And, bool_T, Any, sub' t1, sub' t2)
    4.42 @@ -547,13 +540,6 @@
    4.43          | (Const (@{const_name snd}, T), [t1]) =>
    4.44            Op1 (Second, range_type T, Any, sub t1)
    4.45          | (Const (@{const_name Id}, T), []) => Cst (Iden, T, Any)
    4.46 -        | (Const (@{const_name insert}, T), [t1, t2]) =>
    4.47 -          (case t2 of
    4.48 -             Abs (_, _, @{const False}) =>
    4.49 -             Op1 (SingletonSet, nth_range_type 2 T, Any, sub t1)
    4.50 -           | _ =>
    4.51 -             Op2 (Union, nth_range_type 2 T, Any,
    4.52 -                  Op1 (SingletonSet, nth_range_type 2 T, Any, sub t1), sub t2))
    4.53          | (Const (@{const_name converse}, T), [t1]) =>
    4.54            Op1 (Converse, range_type T, Any, sub t1)
    4.55          | (Const (@{const_name trancl}, T), [t1]) =>
    4.56 @@ -585,11 +571,6 @@
    4.57          | (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
    4.58            if is_built_in_const thy stds false x then Cst (Add, T, Any)
    4.59            else ConstName (s, T, Any)
    4.60 -        | (Const (@{const_name minus_class.minus},
    4.61 -                  Type (@{type_name fun},
    4.62 -                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
    4.63 -           [t1, t2]) =>
    4.64 -          Op2 (SetDifference, T1, Any, sub t1, sub t2)
    4.65          | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
    4.66            if is_built_in_const thy stds false x then Cst (Subtract, T, Any)
    4.67            else ConstName (s, T, Any)
    4.68 @@ -643,16 +624,6 @@
    4.69          | (Const (@{const_name of_nat},
    4.70                    T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
    4.71            Cst (NatToInt, T, Any)
    4.72 -        | (Const (@{const_name semilattice_inf_class.inf},
    4.73 -                  Type (@{type_name fun},
    4.74 -                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
    4.75 -           [t1, t2]) =>
    4.76 -          Op2 (Intersect, T1, Any, sub t1, sub t2)
    4.77 -        | (Const (@{const_name semilattice_sup_class.sup},
    4.78 -                  Type (@{type_name fun},
    4.79 -                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
    4.80 -           [t1, t2]) =>
    4.81 -          Op2 (Union, T1, Any, sub t1, sub t2)
    4.82          | (t0 as Const (x as (s, T)), ts) =>
    4.83            if is_constr ctxt stds x then
    4.84              do_construct x ts
    4.85 @@ -685,15 +656,14 @@
    4.86    | Op1 (SingletonSet, _, _, _) => true
    4.87    | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
    4.88    | Op2 (oper, _, _, u1, u2) =>
    4.89 -    if oper = Union orelse oper = SetDifference orelse oper = Intersect then
    4.90 -      forall is_fully_representable_set [u1, u2]
    4.91 -    else if oper = Apply then
    4.92 +    if oper = Apply then
    4.93        case u1 of
    4.94          ConstName (s, _, _) =>
    4.95          is_sel_like_and_no_discr s orelse s = @{const_name set}
    4.96        | _ => false
    4.97      else
    4.98        false
    4.99 +  | Op2 (Lambda, _, _, _, Cst (False, _, _)) => true
   4.100    | _ => false
   4.101  
   4.102  fun rep_for_abs_fun scope T =
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Jun 21 09:38:20 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Jun 21 11:15:21 2010 +0200
     5.3 @@ -91,7 +91,7 @@
     5.4  fun uncurry_term table t =
     5.5    let
     5.6      fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
     5.7 -      | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
     5.8 +      | aux (Abs (s, T, t')) args = s_betapplys [] (Abs (s, T, aux t' []), args)
     5.9        | aux (t as Const (s, T)) args =
    5.10          (case Termtab.lookup table t of
    5.11             SOME n =>
    5.12 @@ -111,17 +111,18 @@
    5.13                 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
    5.14               in
    5.15                 if n - j < 2 then
    5.16 -                 betapplys (t, args)
    5.17 +                 s_betapplys [] (t, args)
    5.18                 else
    5.19 -                 betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
    5.20 -                                   before_arg_Ts ---> tuple_T --> rest_T),
    5.21 -                            before_args @ [mk_flat_tuple tuple_T tuple_args] @
    5.22 -                            after_args)
    5.23 +                 s_betapplys []
    5.24 +                     (Const (uncurry_prefix_for (n - j) j ^ s,
    5.25 +                             before_arg_Ts ---> tuple_T --> rest_T),
    5.26 +                      before_args @ [mk_flat_tuple tuple_T tuple_args] @
    5.27 +                      after_args)
    5.28               end
    5.29             else
    5.30 -             betapplys (t, args)
    5.31 -         | NONE => betapplys (t, args))
    5.32 -      | aux t args = betapplys (t, args)
    5.33 +             s_betapplys [] (t, args)
    5.34 +         | NONE => s_betapplys [] (t, args))
    5.35 +      | aux t args = s_betapplys [] (t, args)
    5.36    in aux t [] end
    5.37  
    5.38  (** Boxing **)
    5.39 @@ -248,13 +249,13 @@
    5.40            val T2 = fastype_of1 (new_Ts, t2)
    5.41            val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
    5.42          in
    5.43 -          betapply (if s1 = @{type_name fun} then
    5.44 -                      t1
    5.45 -                    else
    5.46 -                      select_nth_constr_arg ctxt stds
    5.47 -                          (@{const_name FunBox},
    5.48 -                           Type (@{type_name fun}, Ts1) --> T1) t1 0
    5.49 -                          (Type (@{type_name fun}, Ts1)), t2)
    5.50 +          s_betapply new_Ts (if s1 = @{type_name fun} then
    5.51 +                               t1
    5.52 +                             else
    5.53 +                               select_nth_constr_arg ctxt stds
    5.54 +                                   (@{const_name FunBox},
    5.55 +                                    Type (@{type_name fun}, Ts1) --> T1) t1 0
    5.56 +                                   (Type (@{type_name fun}, Ts1)), t2)
    5.57          end
    5.58        | t1 $ t2 =>
    5.59          let
    5.60 @@ -265,13 +266,13 @@
    5.61            val T2 = fastype_of1 (new_Ts, t2)
    5.62            val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
    5.63          in
    5.64 -          betapply (if s1 = @{type_name fun} then
    5.65 -                      t1
    5.66 -                    else
    5.67 -                      select_nth_constr_arg ctxt stds
    5.68 -                          (@{const_name FunBox},
    5.69 -                           Type (@{type_name fun}, Ts1) --> T1) t1 0
    5.70 -                          (Type (@{type_name fun}, Ts1)), t2)
    5.71 +          s_betapply new_Ts (if s1 = @{type_name fun} then
    5.72 +                               t1
    5.73 +                             else
    5.74 +                               select_nth_constr_arg ctxt stds
    5.75 +                                   (@{const_name FunBox},
    5.76 +                                    Type (@{type_name fun}, Ts1) --> T1) t1 0
    5.77 +                                   (Type (@{type_name fun}, Ts1)), t2)
    5.78          end
    5.79        | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
    5.80        | Var (z as (x, T)) =>
    5.81 @@ -388,18 +389,6 @@
    5.82            (list_comb (t, args), seen)
    5.83    in aux [] 0 t [] [] |> fst end
    5.84  
    5.85 -val let_var_prefix = nitpick_prefix ^ "l"
    5.86 -val let_inline_threshold = 32
    5.87 -
    5.88 -fun hol_let n abs_T body_T f t =
    5.89 -  if n * size_of_term t <= let_inline_threshold then
    5.90 -    f t
    5.91 -  else
    5.92 -    let val z = ((let_var_prefix, 0), abs_T) in
    5.93 -      Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
    5.94 -      $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
    5.95 -    end
    5.96 -
    5.97  fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t =
    5.98    let
    5.99      val num_occs_of_var =
   5.100 @@ -439,10 +428,10 @@
   5.101                  x = (@{const_name Suc}, nat_T --> nat_T)) andalso
   5.102                 (not careful orelse not (is_Var t1) orelse
   5.103                  String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
   5.104 -                hol_let (n + 1) dataT bool_T
   5.105 -                    (fn t1 => discriminate_value hol_ctxt x t1 ::
   5.106 -                              map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
   5.107 -                              |> foldr1 s_conj) t1
   5.108 +                s_let "l" (n + 1) dataT bool_T
   5.109 +                      (fn t1 => discriminate_value hol_ctxt x t1 ::
   5.110 +                                map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
   5.111 +                                |> foldr1 s_conj) t1
   5.112              else
   5.113                raise SAME ()
   5.114            end
   5.115 @@ -572,7 +561,7 @@
   5.116                                       map Bound (rev js))
   5.117                val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
   5.118              in
   5.119 -              if null js then betapply (abs_t, sko_t)
   5.120 +              if null js then s_betapply Ts (abs_t, sko_t)
   5.121                else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
   5.122              end
   5.123            else
   5.124 @@ -602,11 +591,9 @@
   5.125          | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
   5.126            do_quantifier s0 T0 s1 T1 t1
   5.127          | @{const "op &"} $ t1 $ t2 =>
   5.128 -          @{const "op &"} $ aux ss Ts js depth polar t1
   5.129 -          $ aux ss Ts js depth polar t2
   5.130 +          s_conj (pairself (aux ss Ts js depth polar) (t1, t2))
   5.131          | @{const "op |"} $ t1 $ t2 =>
   5.132 -          @{const "op |"} $ aux ss Ts js depth polar t1
   5.133 -          $ aux ss Ts js depth polar t2
   5.134 +          s_disj (pairself (aux ss Ts js depth polar) (t1, t2))
   5.135          | @{const "op -->"} $ t1 $ t2 =>
   5.136            @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
   5.137            $ aux ss Ts js depth polar t2
   5.138 @@ -617,42 +604,30 @@
   5.139               not (is_well_founded_inductive_pred hol_ctxt x) then
   5.140              let
   5.141                val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
   5.142 -              val (pref, connective, set_oper) =
   5.143 -                if gfp then
   5.144 -                  (lbfp_prefix, @{const "op |"},
   5.145 -                   @{const_name semilattice_sup_class.sup})
   5.146 -                else
   5.147 -                  (ubfp_prefix, @{const "op &"},
   5.148 -                   @{const_name semilattice_inf_class.inf})
   5.149 +              val (pref, connective) =
   5.150 +                if gfp then (lbfp_prefix, @{const "op |"})
   5.151 +                else (ubfp_prefix, @{const "op &"})
   5.152                fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
   5.153                             |> aux ss Ts js depth polar
   5.154                fun neg () = Const (pref ^ s, T)
   5.155              in
   5.156 -              (case polar |> gfp ? flip_polarity of
   5.157 -                 Pos => pos ()
   5.158 -               | Neg => neg ()
   5.159 -               | Neut =>
   5.160 -                 if is_fun_type T then
   5.161 -                   let
   5.162 -                     val ((trunk_arg_Ts, rump_arg_T), body_T) =
   5.163 -                       T |> strip_type |>> split_last
   5.164 -                     val set_T = rump_arg_T --> body_T
   5.165 -                     fun app f =
   5.166 -                       list_comb (f (),
   5.167 -                                  map Bound (length trunk_arg_Ts - 1 downto 0))
   5.168 -                   in
   5.169 -                     List.foldr absdummy
   5.170 -                                (Const (set_oper, set_T --> set_T --> set_T)
   5.171 -                                        $ app pos $ app neg) trunk_arg_Ts
   5.172 -                   end
   5.173 -                 else
   5.174 -                   connective $ pos () $ neg ())
   5.175 +              case polar |> gfp ? flip_polarity of
   5.176 +                Pos => pos ()
   5.177 +              | Neg => neg ()
   5.178 +              | Neut =>
   5.179 +                let
   5.180 +                  val arg_Ts = binder_types T
   5.181 +                  fun app f =
   5.182 +                    list_comb (f (), map Bound (length arg_Ts - 1 downto 0))
   5.183 +                in
   5.184 +                  List.foldr absdummy (connective $ app pos $ app neg) arg_Ts
   5.185 +                end
   5.186              end
   5.187            else
   5.188              Const x
   5.189          | t1 $ t2 =>
   5.190 -          betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
   5.191 -                    aux ss Ts [] depth Neut t2)
   5.192 +          s_betapply Ts (aux ss Ts [] (skolem_depth + 1) polar t1,
   5.193 +                         aux ss Ts [] depth Neut t2)
   5.194          | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
   5.195          | _ => t
   5.196        end
   5.197 @@ -1064,10 +1039,10 @@
   5.198              | _ => raise SAME ()
   5.199            else
   5.200              raise SAME ())
   5.201 -         handle SAME () => betapplys (t, args))
   5.202 +         handle SAME () => s_betapplys [] (t, args))
   5.203        | do_term (Abs (s, T, t')) args =
   5.204 -        betapplys (Abs (s, T, do_term t' []), args)
   5.205 -      | do_term t args = betapplys (t, args)
   5.206 +        s_betapplys [] (Abs (s, T, do_term t' []), args)
   5.207 +      | do_term t args = s_betapplys [] (t, args)
   5.208    in do_term t [] end
   5.209  
   5.210  (** Quantifier massaging: Distributing quantifiers **)
   5.211 @@ -1223,15 +1198,20 @@
   5.212  
   5.213  fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
   5.214                                 (nondef_ts, def_ts) =
   5.215 -  let
   5.216 -    val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
   5.217 -             |> filter_out (fn Type (@{type_name fun_box}, _) => true
   5.218 -                             | @{typ signed_bit} => true
   5.219 -                             | @{typ unsigned_bit} => true
   5.220 -                             | T => is_small_finite_type hol_ctxt T orelse
   5.221 -                                    triple_lookup (type_match thy) monos T
   5.222 -                                    = SOME (SOME false))
   5.223 -  in fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) end
   5.224 +  if forall (curry (op =) (SOME false) o snd) finitizes then
   5.225 +    (nondef_ts, def_ts)
   5.226 +  else
   5.227 +    let
   5.228 +      val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
   5.229 +               |> filter_out (fn Type (@{type_name fun_box}, _) => true
   5.230 +                               | @{typ signed_bit} => true
   5.231 +                               | @{typ unsigned_bit} => true
   5.232 +                               | T => is_small_finite_type hol_ctxt T orelse
   5.233 +                                      triple_lookup (type_match thy) monos T
   5.234 +                                      = SOME (SOME false))
   5.235 +    in
   5.236 +      fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts)
   5.237 +    end
   5.238  
   5.239  (** Preprocessor entry point **)
   5.240