# HG changeset patch # User blanchet # Date 1277111721 -7200 # Node ID 0681e46b4022dcbad2a5237f79629c1ae20934b9 # Parent 98c6f9dc58d01aaabc27e6a4dc8805f05cb99bbc 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) diff -r 98c6f9dc58d0 -r 0681e46b4022 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jun 21 09:38:20 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jun 21 11:15:21 2010 +0200 @@ -64,6 +64,10 @@ val iter_var_prefix : string val strip_first_name_sep : string -> string * string val original_name : string -> string + val abs_var : indexname * typ -> term -> term + val s_let : 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 @@ -162,7 +166,6 @@ 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 abs_var : indexname * typ -> term -> term val is_funky_typedef : theory -> typ -> bool val all_axioms_of : Proof.context -> (term * term) list -> term list * term list * term list @@ -302,10 +305,55 @@ else s -fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t - | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t - | s_betapply p = betapply p -val s_betapplys = Library.foldl s_betapply +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 s n abs_T body_T f t = + if (n - 1) * (size_of_term t - 1) <= let_inline_threshold 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 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 @@ -344,7 +392,7 @@ (@{const_name True}, 0), (@{const_name All}, 1), (@{const_name Ex}, 1), - (@{const_name "op ="}, 2), + (@{const_name "op ="}, 1), (@{const_name "op &"}, 2), (@{const_name "op |"}, 2), (@{const_name "op -->"}, 2), @@ -355,7 +403,6 @@ (@{const_name fst}, 1), (@{const_name snd}, 1), (@{const_name Id}, 0), - (@{const_name insert}, 2), (@{const_name converse}, 1), (@{const_name trancl}, 1), (@{const_name rel_comp}, 2), @@ -396,10 +443,7 @@ ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2), ((@{const_name of_nat}, nat_T --> int_T), 0)] val built_in_set_consts = - [(@{const_name semilattice_inf_class.inf}, 2), - (@{const_name semilattice_sup_class.sup}, 2), - (@{const_name minus_class.minus}, 2), - (@{const_name ord_class.less_eq}, 2)] + [(@{const_name ord_class.less_eq}, 2)] fun unarize_type @{typ "unsigned_bit word"} = nat_T | unarize_type @{typ "signed_bit word"} = int_T @@ -924,8 +968,8 @@ Const x' => if x = x' then @{const True} else if is_constr_like ctxt x' then @{const False} - else betapply (discr_term_for_constr hol_ctxt x, t) - | _ => betapply (discr_term_for_constr hol_ctxt x, t) + else s_betapply [] (discr_term_for_constr hol_ctxt x, t) + | _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t) fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n = let val (arg_Ts, dataT) = strip_type T in @@ -955,7 +999,8 @@ else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T) else raise SAME () | _ => raise SAME()) - handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t) + handle SAME () => + s_betapply [] (nth_arg_sel_term_for_constr thy stds x n, t) end fun construct_value _ _ x [] = Const x @@ -1150,8 +1195,6 @@ fun special_bounds ts = fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst) -fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) - fun is_funky_typedef_name thy s = member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, @{type_name int}] s orelse @@ -1309,7 +1352,8 @@ original_name s <> s then NONE else - x |> def_props_for_const thy [(NONE, false)] false table |> List.last + x |> def_props_for_const thy [(NONE, false)] false table + |> List.last |> normalized_rhs_of |> Option.map (prefix_abs_vars s) handle List.Empty => NONE @@ -1458,25 +1502,44 @@ (** Constant unfolding **) -fun constr_case_body ctxt stds (j, (x as (_, T))) = +fun constr_case_body ctxt stds (func_t, (x as (_, T))) = let val arg_Ts = binder_types T in - list_comb (Bound j, map2 (select_nth_constr_arg ctxt stds x (Bound 0)) - (index_seq 0 (length arg_Ts)) arg_Ts) + s_betapplys [] (func_t, map2 (select_nth_constr_arg ctxt stds x (Bound 0)) + (index_seq 0 (length arg_Ts)) arg_Ts) end -fun add_constr_case (hol_ctxt as {ctxt, stds, ...}) res_T (j, x) res_t = - Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T) - $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body ctxt stds (j, x) - $ res_t -fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T = +fun add_constr_case res_T (body_t, guard_t) res_t = + if res_T = bool_T then + s_conj (HOLogic.mk_imp (guard_t, body_t), res_t) + else + Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T) + $ guard_t $ body_t $ res_t +fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T func_ts = let val xs = datatype_constrs hol_ctxt dataT - val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs - val (xs', x) = split_last xs + val cases = + func_ts ~~ xs + |> map (fn (func_t, x) => + (constr_case_body ctxt stds (incr_boundvars 1 func_t, x), + discriminate_value hol_ctxt x (Bound 0))) + |> AList.group (op aconv) + |> map (apsnd (List.foldl s_disj @{const False})) + |> sort (int_ord o pairself (size_of_term o fst)) + |> rev in - constr_case_body ctxt stds (1, x) - |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs') - |> fold_rev (curry absdummy) (func_Ts @ [dataT]) + if res_T = bool_T then + if forall (member (op =) [@{const False}, @{const True}] o fst) cases then + case cases of + [(body_t, _)] => body_t + | [_, (@{const True}, head_t2)] => head_t2 + | [_, (@{const False}, head_t2)] => @{const Not} $ head_t2 + | _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases") + else + @{const True} |> fold_rev (add_constr_case res_T) cases + else + fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases) end + |> curry absdummy dataT + fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t = let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in case no_of_record_field thy s rec_T of @@ -1504,7 +1567,7 @@ map2 (fn j => fn T => let val t = select_nth_constr_arg ctxt stds constr_x rec_t j T in if j = special_j then - betapply (fun_t, t) + s_betapply [] (fun_t, t) else if j = n - 1 andalso special_j = ~1 then optimized_record_update hol_ctxt s (rec_T |> dest_Type |> snd |> List.last) fun_t t @@ -1542,12 +1605,13 @@ handle TERM _ => raise SAME () else raise SAME ()) - handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1)) + handle SAME () => + s_betapply [] (do_term depth Ts t0, do_term depth Ts t1)) | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 => do_const depth Ts t (@{const_name refl'}, range_type T) [t2] | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) => - betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts, - map (do_term depth Ts) [t1, t2]) + s_betapplys Ts (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts, + map (do_term depth Ts) [t1, t2]) | Const (x as (@{const_name distinct}, Type (@{type_name fun}, [Type (@{type_name list}, [T']), _]))) $ (t1 as _ $ _) => @@ -1560,11 +1624,11 @@ do_term depth Ts t2 else do_const depth Ts t x [t1, t2, t3] - | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3] - | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2] - | Const x $ t1 => do_const depth Ts t x [t1] | Const x => do_const depth Ts t x [] - | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2) + | t1 $ t2 => + (case strip_comb t of + (Const x, ts) => do_const depth Ts t x ts + | _ => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2)) | Free _ => t | Var _ => t | Bound _ => t @@ -1585,13 +1649,17 @@ (Const x, ts) else case AList.lookup (op =) case_names s of SOME n => - let - val (dataT, res_T) = nth_range_type n T - |> pairf domain_type range_type - in - (optimized_case_def hol_ctxt dataT res_T - |> do_term (depth + 1) Ts, ts) - end + if length ts < n then + (do_term depth Ts (eta_expand Ts t (n - length ts)), []) + else + let + val (dataT, res_T) = nth_range_type n T + |> pairf domain_type range_type + in + (optimized_case_def hol_ctxt dataT res_T + (map (do_term depth Ts) (take n ts)), + drop n ts) + end | _ => if is_constr ctxt stds x then (Const x, ts) @@ -1645,11 +1713,14 @@ string_of_int depth ^ ") while expanding " ^ quote s) else if s = @{const_name wfrec'} then - (do_term (depth + 1) Ts (betapplys (def, ts)), []) + (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), []) else (do_term (depth + 1) Ts def, ts) | NONE => (Const x, ts) - in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end + in + s_betapplys Ts (const, map (do_term depth Ts) ts) + |> s_beta_norm Ts + end in do_term 0 [] end (** Axiom extraction/generation **) @@ -1796,8 +1867,9 @@ in [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var) $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T) - $ (betapplys (optimized_case_def hol_ctxt T bool_T, - map case_func xs @ [x_var]))), + $ (s_betapply [] + (optimized_case_def hol_ctxt T bool_T (map case_func xs), + x_var))), HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var) $ (Const (@{const_name insert}, T --> set_T --> set_T) $ x_var $ Const (@{const_name bot_class.bot}, set_T))] @@ -2036,11 +2108,12 @@ val outer_bounds = map Bound (length outer - 1 downto 0) val cur = Var ((iter_var_prefix, j + 1), iter_T) val next = suc_const iter_T $ cur - val rhs = case fp_app of - Const _ $ t => - betapply (t, list_comb (Const x', next :: outer_bounds)) - | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\ - \const", [fp_app]) + val rhs = + case fp_app of + Const _ $ t => + s_betapply [] (t, list_comb (Const x', next :: outer_bounds)) + | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_const", + [fp_app]) val (inner, naked_rhs) = strip_abs rhs val all = outer @ inner val bounds = map Bound (length all - 1 downto 0) @@ -2056,10 +2129,10 @@ val def = the (def_of_const thy def_table x) val (outer, fp_app) = strip_abs def val outer_bounds = map Bound (length outer - 1 downto 0) - val rhs = case fp_app of - Const _ $ t => betapply (t, list_comb (Const x, outer_bounds)) - | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom", - [fp_app]) + val rhs = + case fp_app of + Const _ $ t => s_betapply [] (t, list_comb (Const x, outer_bounds)) + | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom", [fp_app]) val (inner, naked_rhs) = strip_abs rhs val all = outer @ inner val bounds = map Bound (length all - 1 downto 0) diff -r 98c6f9dc58d0 -r 0681e46b4022 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Jun 21 09:38:20 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Jun 21 11:15:21 2010 +0200 @@ -866,24 +866,8 @@ | _ => kk_rel_eq r (KK.Atom (j0 + 1)) val formula_from_atom = formula_from_opt_atom Pos - fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2) - val kk_or3 = - double_rel_rel_let kk - (fn r1 => fn r2 => - kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom - (kk_intersect r1 r2)) - val kk_and3 = - double_rel_rel_let kk - (fn r1 => fn r2 => - kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom - (kk_intersect r1 r2)) - fun kk_notimplies3 r1 r2 = kk_and3 r1 (kk_not3 r2) - val unpack_formulas = map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1 - fun kk_vect_set_op connective k r1 r2 = - fold1 kk_product (map2 (atom_from_formula kk bool_j0 oo connective) - (unpack_formulas k r1) (unpack_formulas k r2)) fun kk_vect_set_bool_op connective k r1 r2 = fold1 kk_and (map2 connective (unpack_formulas k r1) (unpack_formulas k r2)) @@ -1369,14 +1353,6 @@ kk_union (kk_rel_if f1 true_atom KK.None) (kk_rel_if f2 KK.None false_atom) end - | Op2 (Union, _, R, u1, u2) => - to_set_op kk_or kk_or3 kk_union kk_union kk_intersect false R u1 u2 - | Op2 (SetDifference, _, R, u1, u2) => - to_set_op kk_notimplies kk_notimplies3 kk_difference kk_intersect - kk_union true R u1 u2 - | Op2 (Intersect, _, R, u1, u2) => - to_set_op kk_and kk_and3 kk_intersect kk_intersect kk_union false R - u1 u2 | Op2 (Composition, _, R, u1, u2) => let val (a_T, b_T) = HOLogic.dest_prodT (domain_type (type_of u1)) @@ -1644,37 +1620,6 @@ (kk_join r2 true_atom) | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R]) end - and to_set_op connective connective3 set_oper true_set_oper false_set_oper - neg_second R u1 u2 = - let - val min_R = min_rep (rep_of u1) (rep_of u2) - val r1 = to_rep min_R u1 - val r2 = to_rep min_R u2 - val unopt_R = unopt_rep R - in - rel_expr_from_rel_expr kk unopt_R (unopt_rep min_R) - (case min_R of - Opt (Vect (k, Atom _)) => kk_vect_set_op connective k r1 r2 - | Vect (k, Atom _) => kk_vect_set_op connective k r1 r2 - | Func (_, Formula Neut) => set_oper r1 r2 - | Func (Unit, _) => connective3 r1 r2 - | Func _ => - double_rel_rel_let kk - (fn r1 => fn r2 => - kk_union - (kk_product - (true_set_oper (kk_join r1 true_atom) - (kk_join r2 (atom_for_bool bool_j0 - (not neg_second)))) - true_atom) - (kk_product - (false_set_oper (kk_join r1 false_atom) - (kk_join r2 (atom_for_bool bool_j0 - neg_second))) - false_atom)) - r1 r2 - | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R])) - end and to_bit_word_unary_op T R oper = let val Ts = strip_type T ||> single |> op @ diff -r 98c6f9dc58d0 -r 0681e46b4022 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Jun 21 09:38:20 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Jun 21 11:15:21 2010 +0200 @@ -54,8 +54,9 @@ exception MTYPE of string * mtyp list * typ list exception MTERM of string * mterm list -fun print_g (_ : string) = () -(* val print_g = tracing *) +val debug_mono = false + +fun print_g f = () |> debug_mono ? tracing o f val string_for_var = signed_string_of_int fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>" @@ -401,10 +402,10 @@ [M1, M2], []) fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) = - (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^ - " " ^ string_for_mtype M2); + (print_g (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^ + string_for_comp_op cmp ^ " " ^ string_for_mtype M2); case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of - NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ()) + NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ()) | SOME (lits, comps) => (lits, comps, sexps)) val add_mtypes_equal = add_mtype_comp Eq @@ -446,10 +447,11 @@ raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], []) fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) = - (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^ - (case sn of Minus => "concrete" | Plus => "complete") ^ "."); + (print_g (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^ + (case sn of Minus => "concrete" | Plus => "complete") ^ + "."); case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of - NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ()) + NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ()) | SOME (lits, sexps) => (lits, comps, sexps)) val add_mtype_is_concrete = add_notin_mtype_fv Minus @@ -491,15 +493,16 @@ subscript_string_for_vars " \ " xs ^ " " ^ string_for_sign_atom a2 fun print_problem lits comps sexps = - print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @ - map string_for_comp comps @ - map string_for_sign_expr sexps)) + print_g (fn () => "*** Problem:\n" ^ + cat_lines (map string_for_literal lits @ + map string_for_comp comps @ + map string_for_sign_expr sexps)) fun print_solution lits = let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in - print_g ("*** Solution:\n" ^ - "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^ - "-: " ^ commas (map (string_for_var o fst) neg)) + print_g (fn () => "*** Solution:\n" ^ + "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^ + "-: " ^ commas (map (string_for_var o fst) neg)) end fun solve max_var (lits, comps, sexps) = @@ -550,6 +553,12 @@ def_table, ...}, alpha_T, max_fresh, ...}) = let + fun is_enough_eta_expanded t = + case strip_comb t of + (Const x, ts) => + the_default 0 (arity_of_built_in_const thy stds fast_descrs x) + <= length ts + | _ => true val mtype_for = fresh_mtype_for_type mdata false fun plus_set_mtype_for_dom M = MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M) @@ -640,8 +649,10 @@ |>> mtype_of_mterm end | @{const_name "op ="} => do_equals T accum - | @{const_name The} => (print_g "*** The"; raise UNSOLVABLE ()) - | @{const_name Eps} => (print_g "*** Eps"; raise UNSOLVABLE ()) + | @{const_name The} => + (print_g (K "*** The"); raise UNSOLVABLE ()) + | @{const_name Eps} => + (print_g (K "*** Eps"); raise UNSOLVABLE ()) | @{const_name If} => do_robust_set_operation (range_type T) accum |>> curry3 MFun bool_M (S Minus) @@ -650,19 +661,6 @@ | @{const_name snd} => do_nth_pair_sel 1 T accum | @{const_name Id} => (MFun (mtype_for (domain_type T), S Minus, bool_M), accum) - | @{const_name insert} => - let - val set_T = domain_type (range_type T) - val M1 = mtype_for (domain_type set_T) - val M1' = plus_set_mtype_for_dom M1 - val M2 = mtype_for set_T - val M3 = mtype_for set_T - in - (MFun (M1, S Minus, MFun (M2, S Minus, M3)), - (gamma, cset |> add_mtype_is_concrete M1 - |> add_is_sub_mtype M1' M3 - |> add_is_sub_mtype M2 M3)) - end | @{const_name converse} => let val x = Unsynchronized.inc max_fresh @@ -720,25 +718,9 @@ val a_set_M = mtype_for (domain_type T) val a_M = dest_MFun a_set_M |> #1 in (MFun (a_set_M, S Minus, a_M), accum) end - else if s = @{const_name minus_class.minus} andalso - is_set_type (domain_type T) then - let - val set_T = domain_type T - val left_set_M = mtype_for set_T - val right_set_M = mtype_for set_T - in - (MFun (left_set_M, S Minus, - MFun (right_set_M, S Minus, left_set_M)), - (gamma, cset |> add_mtype_is_concrete right_set_M - |> add_is_sub_mtype right_set_M left_set_M)) - end else if s = @{const_name ord_class.less_eq} andalso is_set_type (domain_type T) then do_fragile_set_operation T accum - else if (s = @{const_name semilattice_inf_class.inf} orelse - s = @{const_name semilattice_sup_class.sup}) andalso - is_set_type (domain_type T) then - do_robust_set_operation T accum else if is_sel s then (mtype_for_sel mdata x, accum) else if is_constr ctxt stds x then @@ -758,7 +740,7 @@ (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frees = (x, M) :: frees, consts = consts}, cset)) end) |>> curry MRaw t - | Var _ => (print_g "*** Var"; raise UNSOLVABLE ()) + | Var _ => (print_g (K "*** Var"); raise UNSOLVABLE ()) | Bound j => (MRaw (t, nth bound_Ms j), accum) | Abs (s, T, t') => (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of @@ -771,10 +753,16 @@ | NONE => ((case t' of t1' $ Bound 0 => - if not (loose_bvar1 (t1', 0)) then + if not (loose_bvar1 (t1', 0)) andalso + is_enough_eta_expanded t1' then do_term (incr_boundvars ~1 t1') accum else raise SAME () + | (t11 as Const (@{const_name "op ="}, _)) $ Bound 0 $ t13 => + if not (loose_bvar1 (t13, 0)) then + do_term (incr_boundvars ~1 (t11 $ t13)) accum + else + raise SAME () | _ => raise SAME ()) handle SAME () => let @@ -803,8 +791,8 @@ val M2 = mtype_of_mterm m2 in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end end) - |> tap (fn (m, _) => print_g (" \ \ " ^ - string_for_mterm ctxt m)) + |> tap (fn (m, _) => print_g (fn () => " \ \ " ^ + string_for_mterm ctxt m)) in do_term end fun force_minus_funs 0 _ = I @@ -902,9 +890,9 @@ | _ => do_term t accum end |> tap (fn (m, _) => - print_g ("\ \ " ^ - string_for_mterm ctxt m ^ " : o\<^sup>" ^ - string_for_sign sn)) + print_g (fn () => "\ \ " ^ + string_for_mterm ctxt m ^ " : o\<^sup>" ^ + string_for_sign sn)) in do_formula end (* The harmless axiom optimization below is somewhat too aggressive in the face @@ -987,9 +975,10 @@ Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M) fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) = - map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @ - map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts - |> cat_lines |> print_g + print_g (fn () => + map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @ + map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts + |> cat_lines) fun amass f t (ms, accum) = let val (m, accum) = f t accum in (m :: ms, accum) end @@ -997,9 +986,9 @@ fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T (nondef_ts, def_ts) = let - val _ = print_g ("****** " ^ which ^ " analysis: " ^ - string_for_mtype MAlpha ^ " is " ^ - Syntax.string_of_typ ctxt alpha_T) + val _ = print_g (fn () => "****** " ^ which ^ " analysis: " ^ + string_for_mtype MAlpha ^ " is " ^ + Syntax.string_of_typ ctxt alpha_T) val mdata as {max_fresh, constr_mcache, ...} = initial_mdata hol_ctxt binarize no_harmless alpha_T val accum = (initial_gamma, ([], [], [])) @@ -1064,26 +1053,21 @@ in case t of Const (x as (s, _)) => - if s = @{const_name insert} then - case nth_range_type 2 T' of - set_T' as Type (@{type_name fin_fun}, [elem_T', _]) => - Abs (Name.uu, elem_T', Abs (Name.uu, set_T', - Const (@{const_name If}, - bool_T --> set_T' --> set_T' --> set_T') - $ (Const (@{const_name is_unknown}, - elem_T' --> bool_T) $ Bound 1) - $ (Const (@{const_name unknown}, set_T')) - $ (coerce_term hol_ctxt new_Ts T' T (Const x) - $ Bound 1 $ Bound 0))) - | _ => Const (s, T') - else if s = @{const_name finite} then + if s = @{const_name finite} then case domain_type T' of set_T' as Type (@{type_name fin_fun}, _) => Abs (Name.uu, set_T', @{const True}) | _ => Const (s, T') else if s = @{const_name "=="} orelse s = @{const_name "op ="} then - Const (s, T') + let + val T = + case T' of + Type (_, [T1, Type (_, [T2, T3])]) => + T1 --> T2 --> T3 + | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\ + \term_from_mterm", [T, T'], []) + in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end else if is_built_in_const thy stds fast_descrs x then coerce_term hol_ctxt new_Ts T' T t else if is_constr ctxt stds x then diff -r 98c6f9dc58d0 -r 0681e46b4022 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Jun 21 09:38:20 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Jun 21 11:15:21 2010 +0200 @@ -56,9 +56,6 @@ The | Eps | Triad | - Union | - SetDifference | - Intersect | Composition | Product | Image | @@ -176,9 +173,6 @@ The | Eps | Triad | - Union | - SetDifference | - Intersect | Composition | Product | Image | @@ -247,9 +241,6 @@ | string_for_op2 The = "The" | string_for_op2 Eps = "Eps" | string_for_op2 Triad = "Triad" - | string_for_op2 Union = "Union" - | string_for_op2 SetDifference = "SetDifference" - | string_for_op2 Intersect = "Intersect" | string_for_op2 Composition = "Composition" | string_for_op2 Product = "Product" | string_for_op2 Image = "Image" @@ -525,6 +516,8 @@ do_description_operator The @{const_name undefined_fast_The} x t1 | (Const (x as (@{const_name Eps}, _)), [t1]) => do_description_operator Eps @{const_name undefined_fast_Eps} x t1 + | (Const (@{const_name "op ="}, T), [t1]) => + Op1 (SingletonSet, range_type T, Any, sub t1) | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2 | (Const (@{const_name "op &"}, _), [t1, t2]) => Op2 (And, bool_T, Any, sub' t1, sub' t2) @@ -547,13 +540,6 @@ | (Const (@{const_name snd}, T), [t1]) => Op1 (Second, range_type T, Any, sub t1) | (Const (@{const_name Id}, T), []) => Cst (Iden, T, Any) - | (Const (@{const_name insert}, T), [t1, t2]) => - (case t2 of - Abs (_, _, @{const False}) => - Op1 (SingletonSet, nth_range_type 2 T, Any, sub t1) - | _ => - Op2 (Union, nth_range_type 2 T, Any, - Op1 (SingletonSet, nth_range_type 2 T, Any, sub t1), sub t2)) | (Const (@{const_name converse}, T), [t1]) => Op1 (Converse, range_type T, Any, sub t1) | (Const (@{const_name trancl}, T), [t1]) => @@ -585,11 +571,6 @@ | (Const (x as (s as @{const_name plus_class.plus}, T)), []) => if is_built_in_const thy stds false x then Cst (Add, T, Any) else ConstName (s, T, Any) - | (Const (@{const_name minus_class.minus}, - Type (@{type_name fun}, - [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])), - [t1, t2]) => - Op2 (SetDifference, T1, Any, sub t1, sub t2) | (Const (x as (s as @{const_name minus_class.minus}, T)), []) => if is_built_in_const thy stds false x then Cst (Subtract, T, Any) else ConstName (s, T, Any) @@ -643,16 +624,6 @@ | (Const (@{const_name of_nat}, T as @{typ "unsigned_bit word => signed_bit word"}), []) => Cst (NatToInt, T, Any) - | (Const (@{const_name semilattice_inf_class.inf}, - Type (@{type_name fun}, - [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])), - [t1, t2]) => - Op2 (Intersect, T1, Any, sub t1, sub t2) - | (Const (@{const_name semilattice_sup_class.sup}, - Type (@{type_name fun}, - [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])), - [t1, t2]) => - Op2 (Union, T1, Any, sub t1, sub t2) | (t0 as Const (x as (s, T)), ts) => if is_constr ctxt stds x then do_construct x ts @@ -685,15 +656,14 @@ | Op1 (SingletonSet, _, _, _) => true | Op1 (Converse, _, _, u1) => is_fully_representable_set u1 | Op2 (oper, _, _, u1, u2) => - if oper = Union orelse oper = SetDifference orelse oper = Intersect then - forall is_fully_representable_set [u1, u2] - else if oper = Apply then + if oper = Apply then case u1 of ConstName (s, _, _) => is_sel_like_and_no_discr s orelse s = @{const_name set} | _ => false else false + | Op2 (Lambda, _, _, _, Cst (False, _, _)) => true | _ => false fun rep_for_abs_fun scope T = diff -r 98c6f9dc58d0 -r 0681e46b4022 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Jun 21 09:38:20 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Jun 21 11:15:21 2010 +0200 @@ -91,7 +91,7 @@ fun uncurry_term table t = let fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args) - | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args) + | aux (Abs (s, T, t')) args = s_betapplys [] (Abs (s, T, aux t' []), args) | aux (t as Const (s, T)) args = (case Termtab.lookup table t of SOME n => @@ -111,17 +111,18 @@ val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts in if n - j < 2 then - betapplys (t, args) + s_betapplys [] (t, args) else - betapplys (Const (uncurry_prefix_for (n - j) j ^ s, - before_arg_Ts ---> tuple_T --> rest_T), - before_args @ [mk_flat_tuple tuple_T tuple_args] @ - after_args) + s_betapplys [] + (Const (uncurry_prefix_for (n - j) j ^ s, + before_arg_Ts ---> tuple_T --> rest_T), + before_args @ [mk_flat_tuple tuple_T tuple_args] @ + after_args) end else - betapplys (t, args) - | NONE => betapplys (t, args)) - | aux t args = betapplys (t, args) + s_betapplys [] (t, args) + | NONE => s_betapplys [] (t, args)) + | aux t args = s_betapplys [] (t, args) in aux t [] end (** Boxing **) @@ -248,13 +249,13 @@ val T2 = fastype_of1 (new_Ts, t2) val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2 in - betapply (if s1 = @{type_name fun} then - t1 - else - select_nth_constr_arg ctxt stds - (@{const_name FunBox}, - Type (@{type_name fun}, Ts1) --> T1) t1 0 - (Type (@{type_name fun}, Ts1)), t2) + s_betapply new_Ts (if s1 = @{type_name fun} then + t1 + else + select_nth_constr_arg ctxt stds + (@{const_name FunBox}, + Type (@{type_name fun}, Ts1) --> T1) t1 0 + (Type (@{type_name fun}, Ts1)), t2) end | t1 $ t2 => let @@ -265,13 +266,13 @@ val T2 = fastype_of1 (new_Ts, t2) val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2 in - betapply (if s1 = @{type_name fun} then - t1 - else - select_nth_constr_arg ctxt stds - (@{const_name FunBox}, - Type (@{type_name fun}, Ts1) --> T1) t1 0 - (Type (@{type_name fun}, Ts1)), t2) + s_betapply new_Ts (if s1 = @{type_name fun} then + t1 + else + select_nth_constr_arg ctxt stds + (@{const_name FunBox}, + Type (@{type_name fun}, Ts1) --> T1) t1 0 + (Type (@{type_name fun}, Ts1)), t2) end | Free (s, T) => Free (s, box_type hol_ctxt InExpr T) | Var (z as (x, T)) => @@ -388,18 +389,6 @@ (list_comb (t, args), seen) in aux [] 0 t [] [] |> fst end -val let_var_prefix = nitpick_prefix ^ "l" -val let_inline_threshold = 32 - -fun hol_let n abs_T body_T f t = - if n * size_of_term t <= let_inline_threshold then - f t - else - let val z = ((let_var_prefix, 0), 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 destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t = let val num_occs_of_var = @@ -439,10 +428,10 @@ x = (@{const_name Suc}, nat_T --> nat_T)) andalso (not careful orelse not (is_Var t1) orelse String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then - hol_let (n + 1) dataT bool_T - (fn t1 => discriminate_value hol_ctxt x t1 :: - map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args - |> foldr1 s_conj) t1 + s_let "l" (n + 1) dataT bool_T + (fn t1 => discriminate_value hol_ctxt x t1 :: + map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args + |> foldr1 s_conj) t1 else raise SAME () end @@ -572,7 +561,7 @@ map Bound (rev js)) val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t) in - if null js then betapply (abs_t, sko_t) + if null js then s_betapply Ts (abs_t, sko_t) else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t end else @@ -602,11 +591,9 @@ | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => do_quantifier s0 T0 s1 T1 t1 | @{const "op &"} $ t1 $ t2 => - @{const "op &"} $ aux ss Ts js depth polar t1 - $ aux ss Ts js depth polar t2 + s_conj (pairself (aux ss Ts js depth polar) (t1, t2)) | @{const "op |"} $ t1 $ t2 => - @{const "op |"} $ aux ss Ts js depth polar t1 - $ aux ss Ts js depth polar t2 + s_disj (pairself (aux ss Ts js depth polar) (t1, t2)) | @{const "op -->"} $ t1 $ t2 => @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1 $ aux ss Ts js depth polar t2 @@ -617,42 +604,30 @@ not (is_well_founded_inductive_pred hol_ctxt x) then let val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) - val (pref, connective, set_oper) = - if gfp then - (lbfp_prefix, @{const "op |"}, - @{const_name semilattice_sup_class.sup}) - else - (ubfp_prefix, @{const "op &"}, - @{const_name semilattice_inf_class.inf}) + val (pref, connective) = + if gfp then (lbfp_prefix, @{const "op |"}) + else (ubfp_prefix, @{const "op &"}) fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x |> aux ss Ts js depth polar fun neg () = Const (pref ^ s, T) in - (case polar |> gfp ? flip_polarity of - Pos => pos () - | Neg => neg () - | Neut => - if is_fun_type T then - let - val ((trunk_arg_Ts, rump_arg_T), body_T) = - T |> strip_type |>> split_last - val set_T = rump_arg_T --> body_T - fun app f = - list_comb (f (), - map Bound (length trunk_arg_Ts - 1 downto 0)) - in - List.foldr absdummy - (Const (set_oper, set_T --> set_T --> set_T) - $ app pos $ app neg) trunk_arg_Ts - end - else - connective $ pos () $ neg ()) + case polar |> gfp ? flip_polarity of + Pos => pos () + | Neg => neg () + | Neut => + let + val arg_Ts = binder_types T + fun app f = + list_comb (f (), map Bound (length arg_Ts - 1 downto 0)) + in + List.foldr absdummy (connective $ app pos $ app neg) arg_Ts + end end else Const x | t1 $ t2 => - betapply (aux ss Ts [] (skolem_depth + 1) polar t1, - aux ss Ts [] depth Neut t2) + s_betapply Ts (aux ss Ts [] (skolem_depth + 1) polar t1, + aux ss Ts [] depth Neut t2) | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1) | _ => t end @@ -1064,10 +1039,10 @@ | _ => raise SAME () else raise SAME ()) - handle SAME () => betapplys (t, args)) + handle SAME () => s_betapplys [] (t, args)) | do_term (Abs (s, T, t')) args = - betapplys (Abs (s, T, do_term t' []), args) - | do_term t args = betapplys (t, args) + s_betapplys [] (Abs (s, T, do_term t' []), args) + | do_term t args = s_betapplys [] (t, args) in do_term t [] end (** Quantifier massaging: Distributing quantifiers **) @@ -1223,15 +1198,20 @@ fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos (nondef_ts, def_ts) = - let - val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) - |> filter_out (fn Type (@{type_name fun_box}, _) => true - | @{typ signed_bit} => true - | @{typ unsigned_bit} => true - | T => is_small_finite_type hol_ctxt T orelse - triple_lookup (type_match thy) monos T - = SOME (SOME false)) - in fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) end + if forall (curry (op =) (SOME false) o snd) finitizes then + (nondef_ts, def_ts) + else + let + val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) + |> filter_out (fn Type (@{type_name fun_box}, _) => true + | @{typ signed_bit} => true + | @{typ unsigned_bit} => true + | T => is_small_finite_type hol_ctxt T orelse + triple_lookup (type_match thy) monos T + = SOME (SOME false)) + in + fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) + end (** Preprocessor entry point **)